Nuprl - Proof: sub-join-list-din

(12steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Search Doc

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sub-join-list-din

T:Type, l:IdLnk, tg:Id, L:MsgA List.

(

L.T

r M.din(l,tg))

(L).din(l,tg))

By:	InductionOnList THEN Unfold `ma-join-list` 0 THEN Reduce 0 THEN Try (Fold `ma-join-list` 0)

Generated subgoals:

1 1. T : Type
2. l : IdLnk
3. tg : Id
4. MsgA List
  (Mnil.T r M.din(l,tg))  (T r .din(l,tg))
1 step

2 1. T : Type
2. l : IdLnk
3. tg : Id
4. MsgA List
5. u : MsgA
6. v : MsgA List
7. (Mv.T r M.din(l,tg))  (T r (v).din(l,tg))
  (M[u / v].T r M.din(l,tg))  (T r u  (v).din(l,tg))
10 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(12steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Search Doc

1	1. T : Type 2. l : IdLnk 3. tg : Id 4. MsgA List (Mnil.T r M.din(l,tg)) (T r .din(l,tg))	1 step
2	1. T : Type 2. l : IdLnk 3. tg : Id 4. MsgA List 5. u : MsgA 6. v : MsgA List 7. (Mv.T r M.din(l,tg)) (T r (v).din(l,tg)) (M[u / v].T r M.din(l,tg)) (T r u (v).din(l,tg))	10 steps