(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 2 2 1 1 2
1. D : Dsys
2. L : Id List
3. i:Id. (i  L)  ma-is-empty(M(i))
4. i:Id. Feasible(M(i))
5. i:Id. 
5. (i  L)
5. 
5. (ltg:(IdLnkIdType). 
5. ((ltg  ma-outlinks(M(i);i))
5. (
5. ((destination(1of(ltg))  L)
5. (
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)
10. ds : x:Id fp-> Type
11. da : a:Knd fp-> Type
12. init : x:Id fp-> ds(x)?Void
13. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
14. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
15. send : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
15. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
16. frame : x:Id fp-> Knd List
17. sframe : ltg:IdLnkId fp-> Knd List
18. M8 : Top
19. M(source(l)) = <ds,da,init,pre,ef,send,frame,sframe,M8>
20. rcv(l; tg)  dom(da)
  (rcv(l; tg)  fpf-dom-list(da))
By: AssertBY (fpf-dom-list(da)  {k:Knd| k  dom(da) } List) Auto THEN DupHyp -2
THEN
Unfold `fpf-dom` -1
THEN
Fold `fpf-dom-list` -1
THEN
RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1

Generated subgoals:

1 21. fpf-dom-list(da)  {k:Knd| k  dom(da) } List
22. deq-member(KindDeq;rcv(l; tg);fpf-dom-list(da))
  fpf-dom-list(da)  Knd List
1 step
2 21. fpf-dom-list(da)  {k:Knd| k  dom(da) } List
22. (rcv(l; tg)  fpf-dom-list(da))
  (rcv(l; tg)  fpf-dom-list(da))
3 steps

About:
pairproductproductlistassertvoidset
functionuniverseequalmembertoppropimpliesor
all
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