Nuprl - Proof: hanoi seq join wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi seq join wf 1

1. n :

2. m :

3. a :

4. z :

5. s1 : {a...m}

{1...n}

Peg
6. s2 : {m+1...z}

{1...n}

Peg

(

x.if x

s1(x) else s2(x) fi)

{a...z}

{1...n}

Peg

By:

Analyze

Generated subgoal:

1 7. x : {a...z}
if xm s1(x) else s2(x) fi {1...n}Peg
1 step

About:

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