Nuprl - Proof: hanoi seq join part1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hanoi seq join part1 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}

(s1 @(m) s2)(x) = s1(x)

By:	Compute (s1 @(m) s2)(x) * if xm s1(x) else s2(x) fi

Generated subgoal:

1 if xm s1(x) else s2(x) fi = s1(x)
1 step

About:

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