is mentioned by
[sfa_doc_nat_sqrt] | |
[sfa_doc_simple_existential_2] | |
[sfa_doc_simple_existential_1] | |
[sfa_doc_bool_vs_decidable_fun] | |
[sfa_doc_bool_vs_decidable] | |
Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm* Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x) | [sfa_doc_alternate_zero_beyond] |
[sfa_doc_or_dec] | |
Thm* P:((A List)Prop). Thm* (P(nil) Q) & (a:A, x:A List. P(a.x) R(a,x,P(x))) | [sfa_doc_listind_via_so] |
[sfa_doc_some_via_so] | |
[sfa_doc_sexpr_case_thm] | |
[kleene_minimize_is_lb] | |
[kleene_minimize_is_fp] | |
[kleene_minimize_wf] | |
[kleene_tail] | |
[sfa_doc_sample_intmod] |
In prior sections: core fun 1 int 2
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html