Nuprl - Proof: hanoi seq join seq 1

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

1. n :

2. a :

3. z :

4. m : {a...z-1}
5. s1 : {a...m}

{1...n}

Peg
6. s2 : {m+1...z}

{1...n}

Peg
7.

k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1)
8. s1 is a Hanoi(n disk) seq on a..m
9. s2 is a Hanoi(n disk) seq on m+1..z

(s1 @(m) s2) is a Hanoi(n disk) seq on a..z

By:

Analyze

Generated subgoal:

1 10. x : {a...z}
11. x' : {a...z}
12. x+1 = x'
k:{1...n}. Moving disk k of n takes (s1 @(m) s2)(x) to (s1 @(m) s2)(x')
7 steps

About:

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