Nuprl - Proof: hanoi general exists 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi general exists 1

1. f : {1...0}

Peg
2. g : {1...0}

Peg
3. a :

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

{1...0}

Peg).

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

By:	Witness: a \| x.f THEN Reduce Concl

Generated subgoals:

1 (x.f) is a Hanoi(0 disk) seq on a..a
1 step

2 f = g
1 step

About:

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