(20steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: es-axioms
  the_es:ES. 
  (Trans e,e':E. (e <loc e'))
  & SWellFounded((e <loc e'))
  & (e,e':E. loc(e) = loc(e')  Id  (e <loc e')  e = e'  (e' <loc e))
  & (e:E. first(e)  (e':E. (e' <loc e)))
  & (e:E. 
  & (first(e)
  & (
  & ((pred(e) <loc e) & (e':E. ((pred(e) <loc e') & (e' <loc e))))
  & (e:E. 
  & (first(e)  (x:Id. (x when e) = (x after pred(e))  vartype(loc(e);x)))
  & (Trans e,e':E. (e < e'))
  & SWellFounded((e < e'))
  & (e:E. 
  & (isrcv(e)
  & (
  & (sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))  Msg)
  & (e,e':E. (e <loc e')  (e < e'))
  & (e:E. isrcv(e)  (sender(e) < e))
  & (e,e':E.
  & ((e < e')
  & (
  & (first(e') & (e < pred(e'))  e = pred(e')  E
  & ( isrcv(e') & (e < sender(e'))  e = sender(e')  E)
  & (e:E. isrcv(e)  loc(e) = destination(lnk(e)))
  & (e:E, l:IdLnk. loc(e) = source(l)  sends(l;e) = nil  (Msg on l) List)
  & (e,e':E.
  & (isrcv(e)
  & (
  & (isrcv(e')
  & (
  & (lnk(e) = lnk(e')
  & (
  & (((e <loc e')
  & ((
  & (((sender(e) <loc sender(e'))
  & (( sender(e) = sender(e')  E & index(e)<index(e')))
  & (e:E, l:IdLnk, n:||sends(l;e)||.
  & (e':E. isrcv(e') & lnk(e') = l & sender(e') = e  E & index(e') = n  )
By: All_ES THEN Analyze -2 THEN ExRepD THEN All (Unfold `Msg_sub`)
THEN
SplitAndConcl
THEN
Try Trivial

Generated subgoals:

1 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  Trans e,e':E. loc(e) = loc(e') & causl(e,e')
1 step
2 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  SWellFounded(loc(e) = loc(e') & causl(e,e'))
1 step
3 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e,e':E.
  loc(e) = loc(e')
  
  loc(e) = loc(e') & causl(e,e')  e = e'  loc(e') = loc(e) & causl(e',e)
1 step
4 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e:E. first(e)  (e':E. (loc(e') = loc(e) & causl(e',e)))
3 steps
5 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e:E. 
  first(e)
  
  loc(pred(e)) = loc(e) & causl(pred(e),e)
  & (e':E. 
  & ((loc(pred(e)) = loc(e') & causl(pred(e),e')
  & ((& loc(e') = loc(e)
  & ((& causl(e',e)))
1 step
6 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e,e':E. loc(e) = loc(e') & causl(e,e')  causl(e,e')
Auto
7 1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e,e':E.
  isrcv(kind(e))
  
  isrcv(kind(e'))
  
  lnk(kind(e)) = lnk(kind(e'))
  
  (loc(e) = loc(e') & causl(e,e')
  (
  (loc(sender(e)) = loc(sender(e')) & causl(sender(e),sender(e'))
  ( sender(e) = sender(e') & index(e)<index(e'))
11 steps

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

(20steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc