(17steps 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: ma-outlinks-join-list 2
1. MsgA List
2. u : MsgA
3. v : MsgA List
4. P:(IdLnkIdTypeProp), i:Id.
4. (Mv.(ltgma-outlinks(M;i).P(ltg)))  (ltgma-outlinks((v);i).P(ltg))
  P:(IdLnkIdTypeProp), i:Id.
  (M[u / v].(ltgma-outlinks(M;i).P(ltg)))
  
  (ltgma-outlinks(u  (v);i).P(ltg))
By: RepeatFor 3 ParallelLast

Generated subgoals:

1 4. P : IdLnkIdTypeProp
5. i : Id
6. (M[u / v].(ltgma-outlinks(M;i).P(ltg)))
  (Mv.(ltgma-outlinks(M;i).P(ltg)))
1 step
2 4. P : IdLnkIdTypeProp
5. i : Id
6. (M[u / v].(ltgma-outlinks(M;i).P(ltg)))
7. (ltgma-outlinks((v);i).P(ltg))
  (ltgma-outlinks(u  (v);i).P(ltg))
13 steps

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

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