Nuprl - Proof: hanoi sol2 via permshift 1

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

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

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

{1...0}

Peg).

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

i.p) & s(z) = (

i.q)

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

Generated subgoals:

1   (x,i. whatever) is a Hanoi(0 disk) seq on 1..1
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 1..1	1 step
2	(i.whatever) = (i.p) {1...0}Peg	1 step
3	(i.whatever) = (i.q) {1...0}Peg	1 step