(24steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: conditional-send1-rule 1
1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. rcv(l; tg) = k  T = B
9. f : ABT
10. c : AB
11. D : Dsys
12. D' : Dsys
13. D  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. vartype(source(l);x) r A
18. e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B)
19. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
20. (vartype(source(l);x) r A)
20. & (e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B))
20. & (e:E. kind(e) = rcv(l; tg)  (valtype(e) r T))
21. e : E
22. loc(e) = source(l)
23. kind(e) = k
24. L:{e':E| kind(e') = rcv(l; tg) } List. 
24. (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e)
24. & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
24. & map(e'.val(e');L)
24. & =
24. & if c((x when e),val(e)) [(f((x when e),val(e)))] else nil fi
  (c((x when e),val(e))
  (
  ((e':E. 
  ((kind(e') = rcv(l; tg)
  ((& sender(e') = e  E
  ((& & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e')
  ((& & val(e') = f((x when e),val(e))  T))
  & (c((x when e),val(e))
  & (
  & ((e':E. kind(e') = rcv(l; tg) & sender(e') = e  E))
By: Analyze 0 THEN Analyze 0 THENA MaAuto THEN SplitOnHypITE -2 THEN MaAuto

Generated subgoals:

1 20. vartype(source(l);x) r A
21. e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)
22. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
23. e : E
24. loc(e) = source(l)
25. kind(e) = k  Knd
26. L:{e':E| kind(e') = rcv(l; tg) } List. 
26. (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E)
26. & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
26. & map(e'.val(e');L) = [(f((x when e),val(e)))]  T List
27. c((x when e),val(e))
28. c((x when e),val(e))
  e':E. 
  kind(e') = rcv(l; tg)
  & sender(e') = e  E
  & & (e'':E. kind(e'') = rcv(l; tg)  sender(e'') = e  E  e'' = e')
  & & val(e') = f((x when e),val(e))  T
17 steps
2 20. vartype(source(l);x) r A
21. e:E. loc(e) = source(l)  kind(e) = k  Knd  (valtype(e) r B)
22. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
23. e : E
24. loc(e) = source(l)
25. kind(e) = k  Knd
26. L:{e':E| kind(e') = rcv(l; tg) } List. 
26. (e':E. (e'  L)  kind(e') = rcv(l; tg) & sender(e') = e  E)
26. & (e1,e2:E. e1 before e2  L  (e1 <loc e2))
26. & map(e'.val(e');L) = nil  T List
27. c((x when e),val(e))
28. c((x when e),val(e))
  (e':E. kind(e') = rcv(l; tg) & sender(e') = e  E)
5 steps

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

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