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

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

1. n :

2. f : {1...n}

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

Peg
4. f(n) = g(n)
5. a :

6. z : {a...}
7. s : {a...z}

{1...n-1}

Peg
8. s is a Hanoi(n-1 disk) seq on a..z
9. s(a) = f
10. s(z) = g
11. x : {1...n}
12. x<n

(s(?) {to n-1}

i.f(n) {to n})(a,x) = f(x)

By:	Rewrite by Thm: hanoi seq deepen loweq

Generated subgoal:

1 s(a,x) = f(x)
1 step

About:

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