IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
core
Nuprl Section: core - Some basic concepts defined type-theoretically.

 def unit Unit == 0 def true True == 0 def false False == Void def and P & Q == PQ def or P  Q == P+Q def implies P  Q == PQ def rev_implies P  Q == Q  P def squash T == {:True| T } def not A == A  False def nequal a  b  T == a = b  T def iff P  Q == (P  Q) & (P  Q) def exists x:A. B(x) == x:AB(x) def sq_exists x:A. B(x) == {x:A| B(x) } def all x:A. B(x) == x:AB(x) def le AB == Bj == j = p  a:AB(a) def spread3 let x,y,z = a in t(x;y;z) == a/x,zz. zz/y,z. t(x;y;z) def spread4 let w,x,y,z = a in t(w;x;y;z) == a/w,zz1. zz1/x,zz2. zz2/y,z. t(w;x;y;z) def spread5 let a,b,c,d,e = u in v(a;b;c;d;e) == u/a,zz1. zz1/b,zz2. zz2/c,zz3. zz3/d,e. v(a;b;c;d;e) def spread6 let a,b,c,d,e,f = u in v(a;b;c;d;e;f) == u/a,zz1. zz1/b,zz2. zz2/c,zz3. zz3/d,zz4. zz4/e,f. v(a;b;c;d;e;f) def spread7 let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g) == u/a,zz1. == zz1/b,zz2. zz2/c,zz3. zz3/d,zz4. zz4/e,zz5. zz5/f,g. v(a;b;c;d;e;f;g) COM UNIT_DEFS_acom Inhabitant of Unit type def it == * THM unit_triviality a:Unit. a = COM CONSTR_PROPERTIES_com Predicates for constructive properties of propositions, andlemmas characterizing how these predicates are inherited.Worthwhile sometime redoing thms for soft abstractionsin terms of the underlying hard abstractions / primitives. def decidable Dec(P) == P  P THM decidable__or Dec(P)  Dec(Q)  Dec(P  Q) THM decidable__and Dec(P)  Dec(Q)  Dec(P & Q) THM decidable__implies Dec(P)  Dec(Q)  Dec(P  Q) THM decidable__false Dec(False) THM decidable__iff Dec(P)  Dec(Q)  Dec(P  Q) THM decidable__int_equal i,j:. Dec(i = j) THM decidable__atom_equal a,b:Atom. Dec(a = b) THM iff_preserves_decidability Dec(A)  (A  B)  Dec(B) def stable Stable{P} == P  P THM stable__not Stable{P} THM stable__function_equal f,g:(AB). (x:A. Stable{f(x) = g(x)})  Stable{f = g} THM stable__from_decidable Dec(P)  Stable{P} def sq_stable SqStable(P) == P  P THM sq_stable__and SqStable(P)  SqStable(Q)  SqStable(P & Q) THM sq_stable__implies SqStable(Q)  SqStable(P  Q) THM sq_stable__iff SqStable(P)  SqStable(Q)  SqStable(P  Q) THM sq_stable__all P:(AProp). (x:A. SqStable(P(x)))  SqStable(x:A. P(x)) THM sq_stable__equal x,y:A. SqStable(x = y) THM sq_stable__squash SqStable(P) THM sq_stable__from_stable Stable{P}  SqStable(P) THM sq_stable__not SqStable(P) THM sq_stable_from_decidable Dec(P)  SqStable(P) def xmiddle XM == P:Prop. Dec(P) THM squash_elim SqStable(P)  (P  P) COM LOGIC_THMS_tcom Theorems of inituitionistic propositional and predicate logic. THM dneg_elim Dec(A)  A  A THM dneg_elim_a Dec(A)  (A  A) THM iff_symmetry (A  B)  (B  A) THM and_assoc A & (B & C)  (A & B) & C THM and_comm A & B  B & A THM or_assoc A  (B  C)  (A  B)  C THM or_comm A  B  B  A THM not_over_or (A  B)  A & B THM not_over_or_a (A  B)  A & B THM not_over_and_b A  B  (A & B) THM not_over_and Dec(A)  ((A & B)  A  B) THM and_false_l False & A  False THM and_false_r A & False  False THM and_true_l True & A  A THM and_true_r A & True  A THM or_false_l False  A  A THM or_false_r A  False  A THM or_true_l True  A  True THM or_true_r A  True  True THM exists_over_and_r B:(TProp). (x:T. A & B(x))  A & (x:T. B(x)) THM not_over_exists Q:(TProp). (x:T. Q(x))  (x:T. Q(x)) COM EQUALITY_THMS_tcom Equality Theorems COM REWRITE_SUPPORT_tcom Lemma support for rewriting. THM iff_transitivity (P  Q)  (Q  R)  (P  R) THM implies_transitivity (P  Q)  (Q  R)  P  R THM and_functionality_wrt_iff (P1  P2)  (Q1  Q2)  (P1 & Q1  P2 & Q2) THM and_functionality_wrt_implies (P1  P2)  (Q1  Q2)  P1 & Q1  P2 & Q2 THM implies_functionality_wrt_iff (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2)) THM implies_functionality_wrt_implies (P1  P2)  (Q1  Q2)  (P1  Q1)  P2  Q2 THM decidable_functionality (P  Q)  (Dec(P)  Dec(Q)) THM iff_functionality_wrt_iff (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2)) THM all_functionality_wrt_iff P,Q:(SProp). S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y))) THM all_functionality_wrt_implies P,Q:(SProp). S = T  (z:S. P(z)  Q(z))  (x:S. P(x))  (y:T. Q(y)) THM exists_functionality_wrt_iff P,Q:(SProp). S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y))) THM exists_functionality_wrt_implies P,Q:(SProp). S = T  (x:S. P(x)  Q(x))  (x:S. P(x))  (y:T. Q(y)) THM not_functionality_wrt_iff (P  Q)  (P  Q) THM not_functionality_wrt_implies (P  Q)  P  Q THM or_functionality_wrt_iff (P1  P2)  (Q1  Q2)  (P1  Q1  P2  Q2) THM or_functionality_wrt_implies (P1  P2)  (Q1  Q2)  P1  Q1  P2  Q2 THM squash_functionality_wrt_implies (P  Q)  P  Q THM squash_functionality_wrt_iff (P  Q)  (P  Q) THM implies_antisymmetry (P  Q)  (Q  P)  (P  Q) COM MISC_DEFS_com Miscellaneous General Definitions def let let x = a in b(x) == (x.b(x))(a) COM type_inj_acom type_inj is intended chiefly for injecting into quotienttypes. For convenience, typing lemmas should be provenfor each application. e.g. ... x:T. [x]{a,b:T//Eab}A general typing lemma for type_inj(x;T) cannotbe proven, because it's antecedent would involve the subtypepredicate which isn't typeable. def type_inj [x]{T} == x THM fun_thru_spread B:(AType), p:(x:AB(x)), C,D:Type, f:(CD), b:(x:AB(x)C). f(p/x,y. b(x,y)) = (p/x,y. f(b(x,y))) THM spread_to_pi12 B:(AType), p:(x:AB(x)), C:Type, b:(x:AB(x)C). (p/x,y. b(x,y)) = b(1of(p),2of(p)) def singleton {a:T} == {x:T| x = a  T } THM singleton_properties a:T, x:{a:T}. x = a  T def unique_set {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) } def uni_sat a = !x:T. Q(x) == Q(a) & (a':T. Q(a')  a' = a) THM uni_sat_imp_in_uni_set a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)} def ycomb Y(f) == (x.f(x(x)))(x.f(x(x)))
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html