Nuprl - Proof: hanoi seq join part1

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

, m,a,z:

, s1:({a...m}

{1...n}

Peg), s2:({m+1...z}

{1...n}

Peg),

x:{a...m}. (s1 @(m) s2)(x) = s1(x)

By:

Auto

Generated subgoal:

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)
2 steps

About:

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