(14steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no finite model lemma 1 2 1 1 1
1. A : Type
2. R : AAProp
3. A
4. Trans x,y:A. R(x;y)
5. x:A. y:A. R(x;y)
6. k : 
7. 1<k
8. f : (k-1)A
9. i,j:(k-1). i<j  R(f(i);f(j))
10. y : A
11. R(f(k-2);y)
  (z.if z<k-1 f(z) else y fi)  kA
By: Analyze THEN SplitITE Concl

Generated subgoals:

None

About:
ifthenelseintnatural_numbersubtractless_thanlambdaapply
functionuniversememberpropimpliesallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(14steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc