Nuprl - Proof: hanoi sol2 via permshift 2 1 3

(28steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi sol2 via permshift 2 1 3

1. n :

2. 0<n
3.

p,q:Peg.
3. p

q
3.

3. (

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

{1...n-1}

Peg).
3. (s is a Hanoi(n-1 disk) seq on 1..z & s(1) = (

i.p) & s(z) = (

i.q))
4. p : Peg
5. q : Peg
6. p

q
7. p

otherPeg(p; q)
8. otherPeg(p; q)

q
9. m : {1...}
10. s1 : {1...m}

{1...n-1}

Peg
11. s1 is a Hanoi(n-1 disk) seq on 1..m
12. s1(1) = (

i.p)
13. s1(m) = (

i.otherPeg(p; q))

z:{1...}, m:{1...z-1}, s1:({1...m}

{1...n}

Peg),

s2:({m+1...z}

{1...n}

Peg).

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

& s1(1) = (

i.p)

{1...n}

Peg

& s2(z) = (

i.q)

By:

(q

p

Peg By SimilarTo:

p = q

Peg ; Id)
THEN
FwdThru:
Thm*

n:

, a,z:

, s:({a...z}

{1...n}

Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Thm*

Thm* (

f:(Peg

Peg).
Thm* (Inj(Peg; Peg; f)

(

x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)
on [ Hyp:11 ]
Using:[permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)]

Generated subgoals:

1   Inj(Peg; Peg; permute(p to otherPeg(p; q) ; otherPeg(p; q) to q))
1 step

2 14. (x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x,i)))
14. is a Hanoi(n-1 disk) seq on 1..m
  z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2) is a Hanoi(n disk) seq on 1..z
  & s1(1) = (i.p)  {1...n}Peg
  & s2(z) = (i.q)
13 steps

About:

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

(28steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc