f:(
).
Thm* (
n:. f(n) = 0)
Thm*
Thm* (
n:. if f(n)=
0
False else C:Prop{1}. C fi) 
Prop{1}
(C:Prop. C)list xs == Case of xs; nil False ; x.ys x = a A 
a list ys
Def (recursive)
is mentioned by
| f:().
Thm* ( n:. f(n) = 0)
Thm*
Thm* ( n:. if f(n)=0 False else C:Prop{1}. C fi) Prop{1} | [sfa_doc_predicativity_sample8] |
| (C:Prop. C) | [sfa_doc_false_via_so] |
| list xs == Case of xs; nil False ; x.ys x = a A a list ys
Def (recursive) | [sfa_doc_inlist] |
In prior sections: core bool 1
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html