Nuprl - Proof: hanoi general exists lemma1 1

(16steps 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 general exists lemma1 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).
7. s is a Hanoi(n-1 disk) seq on a..z & s(a) = f & s(z) = g

s:({a...z}

{1...n}

Peg).

s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g

By:	ExistHD Hyp:-1

Generated subgoal:

1 7. s : {a...z}{1...n-1}Peg
8. s is a Hanoi(n-1 disk) seq on a..z
9. s(a) = f  {1...n-1}Peg
10. s(z) = g  {1...n-1}Peg
  s:({a...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on a..z
  & s(a) = f  {1...n}Peg
  & s(z) = g  {1...n}Peg
14 steps

About:

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

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