Nuprl - Proof: hanoi sol2 ala generalPROGworks 2

(19steps total) Remark PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi sol2 ala generalPROGworks 2

1. n :

2. 0<n
3.

p,q:Peg.
3. p

q
3.

3. (

a:

.
3. (HanoiSTD(n-1 disks; from: p; to: q; indexing from: a)/z,s.
3. (s is a Hanoi(n-1 disk) seq on a..z & s(a) = (

i.p) & s(z) = (

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

q
7. a :

HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.

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

& s(a) = (

i.p)

{1...n}

Peg

& s(z) = (

i.q)

{1...n}

Peg

By:	p = otherPeg(p; q) \| otherPeg(p; q) = q Asserted

Generated subgoals:

1   p = otherPeg(p; q)
1 step

2 8. p = otherPeg(p; q)
  otherPeg(p; q) = q
1 step

3 8. p = otherPeg(p; q)
9. otherPeg(p; q) = q
  HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
  s is a Hanoi(n disk) seq on a..z
  & s(a) = (i.p)  {1...n}Peg
  & s(z) = (i.q)  {1...n}Peg
11 steps

About:

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

(19steps total) Remark PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc