Nuprl - Proof: hanoi general exists lemma1 1 1 2 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. 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}

(s(?) {to n-1}

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

By:	Decide: x<n

Generated subgoals:

1 12. x<n
(s(?) {to n-1} i.f(n) {to n})(a,x) = f(x)
2 steps

2 12. x<n
(s(?) {to n-1} i.f(n) {to n})(a,x) = f(x)
2 steps

About:

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

1	12. x<n (s(?) {to n-1} i.f(n) {to n})(a,x) = f(x)	2 steps
2	12. x<n (s(?) {to n-1} i.f(n) {to n})(a,x) = f(x)	2 steps