(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi pegseq analemma 1 1 1 1 1
1. p : Peg
2. k : 
3. k1:. 
3. k1<k
3. 
3. (a:, z:{a...}.
3. (z-ak1
3. (
3. ((f:({a...z}Peg). 
3. ((f(a) = p & f(z)  p
3. ((
3. (((x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)))
4. a : 
5. z : {a...}
6. z-ak
7. f : {a...z}Peg
8. f(a) = p
9. a = z
  f(z) = p
By: ApFun: f to: Hyp:-1

Generated subgoals:

None

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

(28steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc