Nuprl - Proof: hanoi general exists 2 2 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi general exists 2 2 2 1 1

1. n :

2. 0<n
3.

f,g:({1...n-1}

Peg), a:

.
3.

z:{a...}, s:({a...z}

{1...n-1}

Peg).
3. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g
4. f : {1...n}

Peg
5. g : {1...n}

Peg
6. a :

f(n) = g(n)
8. z : {a...}
9. m : {a...z-1}
10. s1 : {a...m}

{1...n}

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

{1...n}

Peg
12. (s1 @(m) s2) is a Hanoi(n disk) seq on a..z
13. s1(a) = f
14. s2(z) = g

(s1 @(m) s2)(a) = f

By:	Rewrite by Thm* n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg), Thm* x:{a...m}. (s1 @(m) s2)(x) = s1(x)

Generated subgoals:

None

About:

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