(7steps 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-compatible-join
  A,B,C:MsgA.
  A || B
  
  ma-frame-compatible(A; B)
  
  ma-sframe-compatible(A; B)
  
  C || A
  
  ma-frame-compatible(C; A)
  
  ma-sframe-compatible(C; A)
  
  C || B
  
  ma-frame-compatible(C; B)
  
  ma-sframe-compatible(C; B)
  
  C || A  B & ma-frame-compatible(C; A  B) & ma-sframe-compatible(C; A  B)
By: Auto THEN Unfold_MsgA -12 THEN Unfold_MsgA -11 THEN Unfold_MsgA -10
THEN
All (Unfolds [`ma-compatible`;`ma-frame-compatible`;`ma-sframe-compatible`])
THEN
All (Unfolds [`ma-compatible-decls`])
THEN
All Reduce
THEN
Unfold `guard` 0
THEN
SplitAndConcl
THEN
Try (BackThru Thm: fpf-compatible-join THEN Complete Auto)
THEN
Try
(Complete
((Auto THEN Inst Thm: fpf-compatible-triple [Id;IdDeq;ds;d1;d3]
((THEN
((Inst Thm: fpf-compatible-triple [Knd;KindDeq;da;d2;d4]
((THEN
((Try
(((Unfold `fpf-compatible` 0 THEN DupHyp -1
(((THEN
(((RWO
(((Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A.
(((Thm* x  dom(f  g)  x  dom(f)  x  dom(g)
(((-1
(((THEN
(((RWO
(((Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
(((Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi
(((0
(((THEN
(((SplitOnConclITE
(((THEN
(((SplitOrHyps
(((THEN
(((AllHyps (h.Unfold `fpf-compatible` h THEN InstHyp [x] h THENA Complete Auto)
(((THENL
((([Id;Thin -1;Id]
(((THEN
(((HypSubst -1 0
(((THEN
(((Try (Fold `member` 0)
(((THEN
(((Try (Analyze 0 THEN DoSubsume)
(((THEN
(((Try DoSubsume
(((THEN
(((Try (Unfold `ma-valtype` 0)
(((THEN
(((Try
((((BackThru
((((Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds)))
(((THEN
(((Try
((((BackThru
((((Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X.
((((Thm* g  f  (f(x)?T r g(x)?Top))
(((THEN
(((Try
((((BackThru
((((Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X.
((((Thm* f  g  (f(x)?Void r g(x)?T))
(((THEN
(((Try
((((BackThru
((((Thm* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
((((Thm* f  f  g))))

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. 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. Top
19. d3 : x:Id fp-> Type
20. d4 : a:Knd fp-> Type
21. i2 : x:Id fp-> d3(x)?Void
22. p2 : a:Id fp-> State(d3)d4(locl(a))?TopProp
23. e2 : kx:KndId fp-> State(d3)d4(1of(kx))?Topd3(2of(kx))?Void
24. s3 : 
24. kl:KndIdLnk fp-> (tg:Id
24. kl:KndIdLnk fp-> (State(d3)d4(1of(kl))?Top
24. kl:KndIdLnk fp-> ((d4(rcv(2of(kl); tg))?Void List)) List
25. f2 : x:Id fp-> Knd List
26. s4 : ltg:IdLnkId fp-> Knd List
27. Top
28. ds || d1 & da || d2
28. & init || i1
28. & pre || p1
28. & ef || e1
28. & send || s1
28. & frame || f1
28. & sframe || s2
29. kx:(KndId). 
29. (kx  dom(ef)
29. (
29. (2of(kx)  dom(frame)
29. (
29. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
29. & (kx  dom(e1)
29. & (
29. & (2of(kx)  dom(f1)
29. & (
29. & (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
30. kl:(KndIdLnk), tg:Id.
30. (kl  dom(send)
30. (
30. ((tg  map(p.1of(p);send(kl)))
30. (
30. (<2of(kl),tg>  dom(sframe)
30. (
30. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
30. & (kl  dom(s1)
30. & (
30. & ((tg  map(p.1of(p);s1(kl)))
30. & (
30. & (<2of(kl),tg>  dom(s2)
30. & (
30. & (<2of(kl),tg>  dom(sframe)
30. & (
30. & (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
31. d3 || ds & d4 || da
31. & i2 || init
31. & p2 || pre
31. & e2 || ef
31. & s3 || send
31. & f2 || frame
31. & s4 || sframe
32. kx:(KndId). 
32. (kx  dom(e2)
32. (
32. (2of(kx)  dom(f2)
32. (
32. (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
32. & (kx  dom(ef)
32. & (
32. & (2of(kx)  dom(frame)
32. & (
32. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
33. kl:(KndIdLnk), tg:Id.
33. (kl  dom(s3)
33. (
33. ((tg  map(p.1of(p);s3(kl)))
33. (
33. (<2of(kl),tg>  dom(s4)
33. (
33. (<2of(kl),tg>  dom(sframe)
33. (
33. (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
33. & (kl  dom(send)
33. & (
33. & ((tg  map(p.1of(p);send(kl)))
33. & (
33. & (<2of(kl),tg>  dom(sframe)
33. & (
33. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
34. d3 || d1 & d4 || d2
34. & i2 || i1
34. & p2 || p1
34. & e2 || e1
34. & s3 || s1
34. & f2 || f1
34. & s4 || s2
35. kx:(KndId). 
35. (kx  dom(e2)
35. (
35. (2of(kx)  dom(f2)
35. (
35. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
35. & (kx  dom(e1)
35. & (
35. & (2of(kx)  dom(f1)
35. & (
35. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
36. kl:(KndIdLnk), tg:Id.
36. (kl  dom(s3)
36. (
36. ((tg  map(p.1of(p);s3(kl)))
36. (
36. (<2of(kl),tg>  dom(s4)
36. (
36. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
36. & (kl  dom(s1)
36. & (
36. & ((tg  map(p.1of(p);s1(kl)))
36. & (
36. & (<2of(kl),tg>  dom(s2)
36. & (
36. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
  kx:(KndId). 
  (kx  dom(e2)
  (
  (2of(kx)  dom(f2)
  (
  (2of(kx)  dom(frame  f1)
  (
  (deq-member(KindDeq;1of(kx);frame  f1(2of(kx))))
  & (kx  dom(ef  e1)
  & (
  & (2of(kx)  dom(frame  f1)
  & (
  & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
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. 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. Top
19. d3 : x:Id fp-> Type
20. d4 : a:Knd fp-> Type
21. i2 : x:Id fp-> d3(x)?Void
22. p2 : a:Id fp-> State(d3)d4(locl(a))?TopProp
23. e2 : kx:KndId fp-> State(d3)d4(1of(kx))?Topd3(2of(kx))?Void
24. s3 : 
24. kl:KndIdLnk fp-> (tg:Id
24. kl:KndIdLnk fp-> (State(d3)d4(1of(kl))?Top
24. kl:KndIdLnk fp-> ((d4(rcv(2of(kl); tg))?Void List)) List
25. f2 : x:Id fp-> Knd List
26. s4 : ltg:IdLnkId fp-> Knd List
27. Top
28. ds || d1 & da || d2
28. & init || i1
28. & pre || p1
28. & ef || e1
28. & send || s1
28. & frame || f1
28. & sframe || s2
29. kx:(KndId). 
29. (kx  dom(ef)
29. (
29. (2of(kx)  dom(frame)
29. (
29. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
29. & (kx  dom(e1)
29. & (
29. & (2of(kx)  dom(f1)
29. & (
29. & (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
30. kl:(KndIdLnk), tg:Id.
30. (kl  dom(send)
30. (
30. ((tg  map(p.1of(p);send(kl)))
30. (
30. (<2of(kl),tg>  dom(sframe)
30. (
30. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
30. & (kl  dom(s1)
30. & (
30. & ((tg  map(p.1of(p);s1(kl)))
30. & (
30. & (<2of(kl),tg>  dom(s2)
30. & (
30. & (<2of(kl),tg>  dom(sframe)
30. & (
30. & (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
31. d3 || ds & d4 || da
31. & i2 || init
31. & p2 || pre
31. & e2 || ef
31. & s3 || send
31. & f2 || frame
31. & s4 || sframe
32. kx:(KndId). 
32. (kx  dom(e2)
32. (
32. (2of(kx)  dom(f2)
32. (
32. (2of(kx)  dom(frame)  deq-member(KindDeq;1of(kx);frame(2of(kx))))
32. & (kx  dom(ef)
32. & (
32. & (2of(kx)  dom(frame)
32. & (
32. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
33. kl:(KndIdLnk), tg:Id.
33. (kl  dom(s3)
33. (
33. ((tg  map(p.1of(p);s3(kl)))
33. (
33. (<2of(kl),tg>  dom(s4)
33. (
33. (<2of(kl),tg>  dom(sframe)
33. (
33. (deq-member(KindDeq;1of(kl);sframe(<2of(kl),tg>)))
33. & (kl  dom(send)
33. & (
33. & ((tg  map(p.1of(p);send(kl)))
33. & (
33. & (<2of(kl),tg>  dom(sframe)
33. & (
33. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
34. d3 || d1 & d4 || d2
34. & i2 || i1
34. & p2 || p1
34. & e2 || e1
34. & s3 || s1
34. & f2 || f1
34. & s4 || s2
35. kx:(KndId). 
35. (kx  dom(e2)
35. (
35. (2of(kx)  dom(f2)
35. (
35. (2of(kx)  dom(f1)  deq-member(KindDeq;1of(kx);f1(2of(kx))))
35. & (kx  dom(e1)
35. & (
35. & (2of(kx)  dom(f1)
35. & (
35. & (2of(kx)  dom(f2)  deq-member(KindDeq;1of(kx);f2(2of(kx))))
36. kl:(KndIdLnk), tg:Id.
36. (kl  dom(s3)
36. (
36. ((tg  map(p.1of(p);s3(kl)))
36. (
36. (<2of(kl),tg>  dom(s4)
36. (
36. (<2of(kl),tg>  dom(s2)  deq-member(KindDeq;1of(kl);s2(<2of(kl),tg>)))
36. & (kl  dom(s1)
36. & (
36. & ((tg  map(p.1of(p);s1(kl)))
36. & (
36. & (<2of(kl),tg>  dom(s2)
36. & (
36. & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
  kl:(KndIdLnk), tg:Id.
  (kl  dom(s3)
  (
  ((tg  map(p.1of(p);s3(kl)))
  (
  (<2of(kl),tg>  dom(s4)
  (
  (<2of(kl),tg>  dom(sframe  s2)
  (
  (deq-member(KindDeq;1of(kl);sframe  s2(<2of(kl),tg>)))
  & (kl  dom(send  s1)
  & (
  & ((tg  map(p.1of(p);send  s1(kl)))
  & (
  & (<2of(kl),tg>  dom(sframe  s2)
  & (
  & (<2of(kl),tg>  dom(s4)  deq-member(KindDeq;1of(kl);s4(<2of(kl),tg>)))
5 steps

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

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