Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
hanoi_seqDef  s is a Hanoi(n disk) seq on a..z
Def  == x,x':{a...z}.
Def  == x+1 = x'  (k:{1...n}. Moving disk k of n takes s(x) to s(x'))
Thm*  n:a,z:s:({a...z}{1...n}Peg).
Thm*  s is a Hanoi(n disk) seq on a..z  Prop
hanoi_PEGDef  Peg == {1...3}
Thm*  Peg  Type
hanoi_seq_deepenDef  (s(?) {to n h {to n'})(x) == s(x) {to n h {to n'}
Thm*  a,z:n:s:({a...z}{1...n}Peg), n':.
Thm*  nn'
Thm*  
Thm*  (h:({n+1...n'}Peg). (s(?) {to n h {to n'})  {a...z}{1...n'}Peg)
hanoi_extendDef  (f {to n f' {to n'})(i) == if in f(i) else f'(i) fi
Thm*  n:f:({1...n}Peg), n':.
Thm*  nn'  (f':({n+1...n'}Peg). (f {to n f' {to n'})  {1...n'}Peg)
int_isegDef  {i...j} == {k:ik & kj }
Thm*  i,j:. {i...j Type
natDef   == {i:| 0i }
Thm*    Type
leDef  AB == B<A
Thm*  i,j:. (ij Prop
le_intDef  ij == j<i
Thm*  i,j:. (ij 

About:
boolifthenelseintnatural_numberaddless_thansetapplyfunction
universeequalmemberpropimpliesandallexists!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions HanoiTowers Sections NuprlLIB Doc