Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This proof that

Thm*  n:p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:
Thm*  (HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
Thm*  (s is a Hanoi(n disk) seq on a..z
Thm*  (s(a) = (i.p {1...n}Peg
Thm*  (s(z) = (i.q {1...n}Peg)

is based on that of

Thm*  n:p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:
Thm*  (z:{a...}, s:({a...z}{1...n}Peg).
Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))

Gloss

from which the program HanoiSTD(n disks; from: p; to: q; indexing from: a) was derived as a realizer.

About:
spreadintnatural_numberlambdaapply
functionequalimpliesandall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions HanoiTowers Sections NuprlLIB Doc