Nuprl - HanoiTowers LEMMAs for hanoi_step_at

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

Theorem	Name
Thm* n:, f,g:({1...n}Peg), k:{1...n}. Thm* Moving disk k of n takes f to g Thm* Thm* f = (i.otherPeg(f(k); g(k))) {1...k-1}Peg	[hanoi_step_at_otherpeg]
cites the following:
Thm* n:, f,g:({1...n}Peg), k:{1...n}. Thm* Moving disk k of n takes f to g f(k) g(k)	[hanoi_step_at_change2]
Thm* x,y,z:Peg. x y x z y z x = otherPeg(y; z)	[hanoi_otherpeg_only]
Thm* n:, f,g:({1...n}Peg), k,i:{1...n}. Thm* Moving disk k of n takes f to g i k f(i) = g(i)	[hanoi_step_at_same]

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