Nuprl - Proof: hanoi sol2 analemma 1

(24steps total) PfGloss PfGloss 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 analemma 1

1. n :

2. p : Peg
3. q : Peg
4. p

q
5. a :

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

f:({a...z}

Peg).
7. f(a) = p & f(z) = q
7.

7. (

x:{a...z-1}, y:{x+1...z}.
7. ((

u:{a...x}. f(u) = p) & f(x+1)

p & f(y-1)

q & (

u:{y...z}. f(u) = q))
8. s : {a...z}

{1...n}

Peg
9. s is a Hanoi(n disk) seq on a..z
10. s(a) = (

i.p)
11. s(z) = (

i.q)

x:{a...z-1}, y:{x+1...z}, p',q':Peg.

(

u:{a...x}. s(u,n) = p) & (

u:{y...z}. s(u,n) = q)

& s(x) = (

i.p')

{1...n-1}

Peg & s(y) = (

i.q')

{1...n-1}

Peg

& p

p'

& q

q'

By:	Inst: Hyp:7 Using:[f(u):= s(u,n)]

Generated subgoals:

1   s(a,n) = p
1 step

2   s(z,n) = q
1 step

3 12. x:{a...z-1}, y:{x+1...z}.
12. (u:{a...x}. s(u,n) = p)
12. & s(x+1,n)  p
12. & s(y-1,n)  q
12. & (u:{y...z}. s(u,n) = q)
  x:{a...z-1}, y:{x+1...z}, p',q':Peg.
  (u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
  & s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg
  & p  p'
  & q  q'
20 steps

About:

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

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