Nuprl - Proof: hanoi seq join part1 1 1

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

1. n :

2. m :

3. a :

4. z :

5. s1 : {a...m}

{1...n}

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

{1...n}

Peg
7. x : {a...m}

if x

s1(x) else s2(x) fi = s1(x)

By:	SplitOnConclITE

Generated subgoals:

None

About:

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