(40steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-support-feasible 1 1 1
1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. (iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg))  L)
5. (iL.(ltgma-outlinks(M(i);i).
5. interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
6. l : IdLnk
7. tg : Id
8. (source(l)  L)
9. (destination(l)  L)
  M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)
By: Unfold `ma-dout` 0 THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE

Generated subgoals:

1   1of(2of(M(source(l))))  a:Knd fp-> Top
1 step
2 10. rcv(l; tg)  dom(1of(2of(M(source(l)))))
  1of(2of(M(source(l))))(rcv(l; tg)) r M(destination(l)).din(l,tg)
15 steps
3 10. rcv(l; tg)  dom(1of(2of(M(source(l)))))
  Void r M(destination(l)).din(l,tg)
1 step

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

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