Nuprl - Proof: select concat 2 1 2 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select concat 2 1 2 1 1 2 1

1. T : Type
2. (T List) List
3. u : T List
4. v : (T List) List
5.

||concat(v)||.
5.

||v||.
5. ||concat(firstn(m;v))||

n
5. & n-||concat(firstn(m;v))||<||v[m]||
5. & concat(v)[n] = v[m][(n-||concat(firstn(m;v))||)]
6. n :

||u @ concat(v)||
7.

n<||u||
8. m :

||v||
9. ||concat(firstn(m;v))||

n-||u||
10. n-||u||-||concat(firstn(m;v))||<||v[m]||
11. concat(v)[(n-||u||)] = v[m][(n-||u||-||concat(firstn(m;v))||)]

||u @ concat(firstn(m;v))||

& n-||u @ concat(firstn(m;v))||<||[u / v][(m+1)]||

& (u @ concat(v))[n] = [u / v][(m+1)][(n-||u @ concat(firstn(m;v))||)]

By:

Auto

Generated subgoals:

1 n-||u @ concat(firstn(m;v))||<||[u / v][(m+1)]||
3 steps

2 (u @ concat(v))[n] = [u / v][(m+1)][(n-||u @ concat(firstn(m;v))||)]
3 steps

About:

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

1	n-\|\|u @ concat(firstn(m;v))\|\|<\|\|[u / v][(m+1)]\|\|	3 steps
2	(u @ concat(v))[n] = [u / v][(m+1)][(n-\|\|u @ concat(firstn(m;v))\|\|)]	3 steps