Nuprl - Proof: hanoi seq permutepegs 1 1 3

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

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)
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. i : {1...k-1}
14. f(s(x,i)) = f(s(x,k))

s(x,i) = s(x,k)

By:	BackThru: Inj(Peg; Peg; f)

Generated subgoals:

None

About:

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