Nuprl - Proof: hanoi seq permutepegs 1

(7steps total) PfGloss PrintForm Definitions HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi seq permutepegs 1

1. n :

2. a :

3. z :

4. s : {a...z}

{1...n}

Peg
5. s is a Hanoi(n disk) seq on a..z
6. f : Peg

Peg
7. Inj(Peg; Peg; f)

(

x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z

By:	(x,i. f(s(x,i))) {a...z}{1...n}Peg Asserted THEN SimilarTo Hyp:5 THEN Reduce Concl

Generated subgoal:

1 8. (x,i. f(s(x,i))) {a...z}{1...n}Peg
9. x : {a...z}
10. x' : {a...z}
11. x+1 = x'
12. k : {1...n}
13. Moving disk k of n takes s(x) to s(x')
Moving disk k of n takes i.f(s(x,i)) to i.f(s(x',i))
5 steps

About:

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

(7steps total) PfGloss PrintForm Definitions HanoiTowers Sections NuprlLIB Doc