Nuprl - Proof: select concat 2 1 1 2

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

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||

||concat(firstn(0;[u / v]))||

& n-||concat(firstn(0;[u / v]))||<||[u / v][0]||

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

By:	RWO Thm* L:Top List. firstn(0;L) ~ nil 0 THEN Reduce 0 THEN Subst' (n-0 = n) 0 THEN BackThru Thm* as,bs:T List, i:\|\|as\|\|. (as @ bs)[i] = as[i]

Generated subgoals:

None

About:

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