Nuprl - Proof: ESAxioms wf

(5steps 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: ESAxioms wf

E:Type{i}, T,V:(Id

Type{i}), M:(IdLnk

Type{i}), loc:(E

Id),

kind:(E

Knd), val:(e:E

eventtype(kind;loc;V;M;e)),

when,after:(x:Id

e:E

T(loc(e),x)),

sends:(l:IdLnk

(Msg_sub(l; M) List)),

sender:({e:E| isrcv(kind(e)) }

E),

index:(e:{e:E| isrcv(kind(e)) }

||sends(lnk(kind(e)),sender(e))||),

first:(E

), pred:({e':E|

first(e') }

E), causl:(E

Prop{i}).

ESAxioms{i:l}

ESAxioms(E;

ESAxioms(T;

ESAxioms(M;

ESAxioms(loc;

ESAxioms(kind;

ESAxioms(val;

ESAxioms(when;

ESAxioms(after;

ESAxioms(sends;

ESAxioms(sender;

ESAxioms(index;

ESAxioms(first;

ESAxioms(pred;

ESAxioms(causl)

Prop{i'}

By:	Auto THEN Try (Analyze -1 THEN Unhide) THEN Unfold `ESAxioms` 0 THEN Unfold `and` 0 THEN Fold `cand` 0 THEN Try (Unfold `Msg_sub` -1 THEN Analyze -1 THEN Complete Auto)

Generated subgoals:

1 1. E : Type
2. T : IdIdType
3. V : IdIdType
4. M : IdLnkIdType
5. loc : EId
6. kind : EKnd
7. e:Eeventtype(kind;loc;V;M;e)
8. x:Ide:ET(loc(e),x)
9. after : x:Ide:ET(loc(e),x)
10. sends : l:IdLnkE(Msg_sub(l; M) List)
11. sender : {e:E| isrcv(kind(e)) }E
12. e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
13. first : E
14. pred : {e':E| first(e') }E
15. causl : EEProp
16. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
17. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
18. e:E.
18. first(e)
18.
18. loc(pred(e)) = loc(e) & causl(pred(e),e)
18. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
19. e : E
20. first(e)
21. x : Id
  after(x,pred(e))  T(loc(e),x)
3 steps

2 1. E : Type
2. T : IdIdType
3. V : IdIdType
4. M : IdLnkIdType
5. loc : EId
6. kind : EKnd
7. val : e:Eeventtype(kind;loc;V;M;e)
8. when : x:Ide:ET(loc(e),x)
9. after : x:Ide:ET(loc(e),x)
10. sends : l:IdLnkE(Msg_sub(l; M) List)
11. sender : {e:E| isrcv(kind(e)) }E
12. e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
13. first : E
14. pred : {e':E| first(e') }E
15. causl : EEProp
16. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
17. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
18. e:E.
18. first(e)
18.
18. loc(pred(e)) = loc(e) & causl(pred(e),e)
18. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
19. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x))
20. Trans e,e':E. causl(e,e')
21. SWellFounded(causl(e,e'))
22. e : E
23. isrcv(kind(e))
  val(e)  M(lnk(kind(e)),tag(kind(e)))
1 step

About:

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

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

1	1. E : Type 2. T : IdIdType 3. V : IdIdType 4. M : IdLnkIdType 5. loc : EId 6. kind : EKnd 7. e:Eeventtype(kind;loc;V;M;e) 8. x:Ide:ET(loc(e),x) 9. after : x:Ide:ET(loc(e),x) 10. sends : l:IdLnkE(Msg_sub(l; M) List) 11. sender : {e:E\| isrcv(kind(e)) }E 12. e:{e:E\| isrcv(kind(e)) }\|\|sends(lnk(kind(e)),sender(e))\|\| 13. first : E 14. pred : {e':E\| first(e') }E 15. causl : EEProp 16. e,e':E. loc(e) = loc(e') causl(e,e') e = e' causl(e',e) 17. e:E. first(e) (e':E. loc(e') = loc(e) causl(e',e)) 18. e:E. 18. first(e) 18. 18. loc(pred(e)) = loc(e) & causl(pred(e),e) 18. & (e':E. loc(e') = loc(e) (causl(pred(e),e') & causl(e',e))) 19. e : E 20. first(e) 21. x : Id after(x,pred(e)) T(loc(e),x)	3 steps
2	1. E : Type 2. T : IdIdType 3. V : IdIdType 4. M : IdLnkIdType 5. loc : EId 6. kind : EKnd 7. val : e:Eeventtype(kind;loc;V;M;e) 8. when : x:Ide:ET(loc(e),x) 9. after : x:Ide:ET(loc(e),x) 10. sends : l:IdLnkE(Msg_sub(l; M) List) 11. sender : {e:E\| isrcv(kind(e)) }E 12. e:{e:E\| isrcv(kind(e)) }\|\|sends(lnk(kind(e)),sender(e))\|\| 13. first : E 14. pred : {e':E\| first(e') }E 15. causl : EEProp 16. e,e':E. loc(e) = loc(e') causl(e,e') e = e' causl(e',e) 17. e:E. first(e) (e':E. loc(e') = loc(e) causl(e',e)) 18. e:E. 18. first(e) 18. 18. loc(pred(e)) = loc(e) & causl(pred(e),e) 18. & (e':E. loc(e') = loc(e) (causl(pred(e),e') & causl(e',e))) 19. e:E. first(e) (x:Id. when(x,e) = after(x,pred(e)) T(loc(e),x)) 20. Trans e,e':E. causl(e,e') 21. SWellFounded(causl(e,e')) 22. e : E 23. isrcv(kind(e)) val(e) M(lnk(kind(e)),tag(kind(e)))	1 step