Nuprl - HanoiTowers LEMMAs for hanoi_seq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
2	Thm* n':, n:{n'...}, a:, z:{a...}, s:({a...z}{1...n}Peg). Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (x:{a...z}, i:{n'+1...n}. s(a,i) = s(x,i)) Thm* Thm* s is a Hanoi(n' disk) seq on a..z	[hanoi_seq_shallower]
cites the following:
1	Thm* n':, n:{n'...}, a,z:, s:({a...z}{1...n}Peg). Thm* s is a Hanoi(n disk) seq on a..z Thm* Thm* (a',z':{a...z}. Thm* ((x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i)) Thm* ( Thm* (s is a Hanoi(n' disk) seq on a'..z')	[hanoi_seq_core]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html