Nuprl - Proof: hanoi sol2 ala general 1

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

1. p : Peg
2. q : Peg
3. p

q
4. a :

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

{1...0}

Peg).

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

i.p) & s(z) = (

i.q)

By:	Witness: a \| x,i. whatever THEN Reduce Concl

Generated subgoals:

1   (x,i. whatever) is a Hanoi(0 disk) seq on a..a
1 step

2   (i.whatever) = (i.p)  {1...0}Peg
1 step

3   (i.whatever) = (i.q)  {1...0}Peg
1 step

About:

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

1	(x,i. whatever) is a Hanoi(0 disk) seq on a..a	1 step
2	(i.whatever) = (i.p) {1...0}Peg	1 step
3	(i.whatever) = (i.q) {1...0}Peg	1 step