Nuprl - Proof: select concat 2

(22steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select concat 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))||)]

||concat([u / v])||.

||[u / v]||.

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

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

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

By:	Unfold `concat` 0 THEN Reduce 0 THEN Try (Fold `concat` 0)

Generated subgoal:

1   n:||u @ concat(v)||.
  m:(||v||+1).
  ||concat(firstn(m;[u / v]))||n
  & n-||concat(firstn(m;[u / v]))||<||[u / v][m]||
  & (u @ concat(v))[n] = [u / v][m][(n-||concat(firstn(m;[u / v]))||)]
19 steps

About:

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

(22steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc