(87steps 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: ma-join-feasible
  A,B:MsgA.
  A || B
  
  ma-frame-compatible(A; B)
  
  ma-sframe-compatible(A; B)  Feasible(A)  Feasible(B)  Feasible(A  B)
By: Auto THEN Unfold_MsgA -7 THEN Unfold_MsgA -6 THEN All (Unfold `ma-feasible`)
THEN
All (Unfold `fpf-all`)
THEN
All Reduce
THEN
SplitAndHyps
THEN
SplitAndConcl

Generated subgoals:

1 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22. x:Id. x  dom(ds)  ds(x)
23. k:Knd. k  dom(da)  Dec(da(k))
24. a:Id. a  dom(pre)  (s:State(ds). Dec(v:da(locl(a))?Top. pre(a)(s,v)))
25. kx:(KndId). 
25. kx  dom(ef)
25. 
25. <ds,da,init,pre,ef,send,frame,sframe,A8>.frame(1of(kx) affects 2of(kx))
26. kl:(KndIdLnk). 
26. kl  dom(send)
26. 
26. (tg:Id. 
26. ((tg  map(p.1of(p);send(kl)))
26. (
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <2of(
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <kl),tg>))
27. x:Id. x  dom(d1)  d1(x)
28. k:Knd. k  dom(d2)  Dec(d2(k))
29. a:Id. a  dom(p1)  (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30. kx:(KndId). 
30. kx  dom(e1)  <d1,d2,i1,p1,e1,s1,f1,s2,B8>.frame(1of(kx) affects 2of(kx))
31. kl:(KndIdLnk). 
31. kl  dom(s1)
31. 
31. (tg:Id. 
31. ((tg  map(p.1of(p);s1(kl)))
31. (
31. (<d1,d2,i1,p1,e1,s1,f1,s2,B8>.sframe(1of(kl) sends <2of(kl),tg>))
  x:Id. x  dom(ds  d1)  ds  d1(x)
1 step
2 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22. x:Id. x  dom(ds)  ds(x)
23. k:Knd. k  dom(da)  Dec(da(k))
24. a:Id. a  dom(pre)  (s:State(ds). Dec(v:da(locl(a))?Top. pre(a)(s,v)))
25. kx:(KndId). 
25. kx  dom(ef)
25. 
25. <ds,da,init,pre,ef,send,frame,sframe,A8>.frame(1of(kx) affects 2of(kx))
26. kl:(KndIdLnk). 
26. kl  dom(send)
26. 
26. (tg:Id. 
26. ((tg  map(p.1of(p);send(kl)))
26. (
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <2of(
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <kl),tg>))
27. x:Id. x  dom(d1)  d1(x)
28. k:Knd. k  dom(d2)  Dec(d2(k))
29. a:Id. a  dom(p1)  (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30. kx:(KndId). 
30. kx  dom(e1)  <d1,d2,i1,p1,e1,s1,f1,s2,B8>.frame(1of(kx) affects 2of(kx))
31. kl:(KndIdLnk). 
31. kl  dom(s1)
31. 
31. (tg:Id. 
31. ((tg  map(p.1of(p);s1(kl)))
31. (
31. (<d1,d2,i1,p1,e1,s1,f1,s2,B8>.sframe(1of(kl) sends <2of(kl),tg>))
  k:Knd. k  dom(da  d2)  Dec(da  d2(k))
1 step
3 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22. x:Id. x  dom(ds)  ds(x)
23. k:Knd. k  dom(da)  Dec(da(k))
24. a:Id. a  dom(pre)  (s:State(ds). Dec(v:da(locl(a))?Top. pre(a)(s,v)))
25. kx:(KndId). 
25. kx  dom(ef)
25. 
25. <ds,da,init,pre,ef,send,frame,sframe,A8>.frame(1of(kx) affects 2of(kx))
26. kl:(KndIdLnk). 
26. kl  dom(send)
26. 
26. (tg:Id. 
26. ((tg  map(p.1of(p);send(kl)))
26. (
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <2of(
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <kl),tg>))
27. x:Id. x  dom(d1)  d1(x)
28. k:Knd. k  dom(d2)  Dec(d2(k))
29. a:Id. a  dom(p1)  (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30. kx:(KndId). 
30. kx  dom(e1)  <d1,d2,i1,p1,e1,s1,f1,s2,B8>.frame(1of(kx) affects 2of(kx))
31. kl:(KndIdLnk). 
31. kl  dom(s1)
31. 
31. (tg:Id. 
31. ((tg  map(p.1of(p);s1(kl)))
31. (
31. (<d1,d2,i1,p1,e1,s1,f1,s2,B8>.sframe(1of(kl) sends <2of(kl),tg>))
  a:Id. 
  a  dom(pre  p1)
  
  (s:State(ds  d1). Dec(v:da  d2(locl(a))?Top. pre  p1(a)(s,v)))
45 steps
4 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22. x:Id. x  dom(ds)  ds(x)
23. k:Knd. k  dom(da)  Dec(da(k))
24. a:Id. a  dom(pre)  (s:State(ds). Dec(v:da(locl(a))?Top. pre(a)(s,v)))
25. kx:(KndId). 
25. kx  dom(ef)
25. 
25. <ds,da,init,pre,ef,send,frame,sframe,A8>.frame(1of(kx) affects 2of(kx))
26. kl:(KndIdLnk). 
26. kl  dom(send)
26. 
26. (tg:Id. 
26. ((tg  map(p.1of(p);send(kl)))
26. (
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <2of(
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <kl),tg>))
27. x:Id. x  dom(d1)  d1(x)
28. k:Knd. k  dom(d2)  Dec(d2(k))
29. a:Id. a  dom(p1)  (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30. kx:(KndId). 
30. kx  dom(e1)  <d1,d2,i1,p1,e1,s1,f1,s2,B8>.frame(1of(kx) affects 2of(kx))
31. kl:(KndIdLnk). 
31. kl  dom(s1)
31. 
31. (tg:Id. 
31. ((tg  map(p.1of(p);s1(kl)))
31. (
31. (<d1,d2,i1,p1,e1,s1,f1,s2,B8>.sframe(1of(kl) sends <2of(kl),tg>))
  kx:(KndId). 
  kx  dom(ef  e1)
  
  <ds  d1
  ,da  d2
  ,init  i1
  ,pre  p1
  ,ef  e1
  ,send  s1
  ,frame  f1
  ,sframe  s2
  ,>.frame(1of(kx) affects 2of(kx))
11 steps
5 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)da(locl(a))?TopProp
5. ef : kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)d2(locl(a))?TopProp
14. e1 : kx:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22. x:Id. x  dom(ds)  ds(x)
23. k:Knd. k  dom(da)  Dec(da(k))
24. a:Id. a  dom(pre)  (s:State(ds). Dec(v:da(locl(a))?Top. pre(a)(s,v)))
25. kx:(KndId). 
25. kx  dom(ef)
25. 
25. <ds,da,init,pre,ef,send,frame,sframe,A8>.frame(1of(kx) affects 2of(kx))
26. kl:(KndIdLnk). 
26. kl  dom(send)
26. 
26. (tg:Id. 
26. ((tg  map(p.1of(p);send(kl)))
26. (
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <2of(
26. (<ds,da,init,pre,ef,send,frame,sframe,A8>.sframe(1of(kl) sends <kl),tg>))
27. x:Id. x  dom(d1)  d1(x)
28. k:Knd. k  dom(d2)  Dec(d2(k))
29. a:Id. a  dom(p1)  (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30. kx:(KndId). 
30. kx  dom(e1)  <d1,d2,i1,p1,e1,s1,f1,s2,B8>.frame(1of(kx) affects 2of(kx))
31. kl:(KndIdLnk). 
31. kl  dom(s1)
31. 
31. (tg:Id. 
31. ((tg  map(p.1of(p);s1(kl)))
31. (
31. (<d1,d2,i1,p1,e1,s1,f1,s2,B8>.sframe(1of(kl) sends <2of(kl),tg>))
  kl:(KndIdLnk). 
  kl  dom(send  s1)
  
  (tg:Id. 
  ((tg  map(p.1of(p);send  s1(kl)))
  (
  (<ds  d1
  (,da  d2
  (,init  i1
  (,pre  p1
  (,ef  e1
  (,send  s1
  (,frame  f1
  (,sframe  s2
  (,>.sframe(1of(kl) sends <2of(kl),tg>))
28 steps

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

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