---

Step * of Lemma CLK-prop

∀MsgType:ValueAllType. ∀locs:bag(Id). ∀reply:Id ⟶ MsgType ⟶ (MsgType × Id). ∀f:CLK_headers_type{i:l}(MsgType).
∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
  (CLK_message-constraint{i:l}(MsgType;locs;reply;f)
  ⇒ (∀e:E. (↑e ∈b CLK_msg'base(MsgType;f)))
  ⇒ e1 ⟶ e2
  ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
  ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
  ⇒ clock1 < clock2)
BY
{ (StartEmlProof
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN RepeatFor 3 (MoveToConcl (-3))
   THEN CausalInd'
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `es-happened-before` (-3)
   THEN DProdsAndUnions
   THEN (Decide ⌜loc(e) = loc(e2) ∈ Id⌝⋅ THENA Auto)) }

1
1. MsgType : {T:Type| valueall-type(T)} @i'
2. locs : bag(Id)@i
3. reply : Id ⟶ MsgType ⟶ (MsgType × Id)@i
4. f : CLK_headers_type{i:l}(MsgType)@i'
5. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
6. f ∈ Name ⟶ Type
7. es : EO+(Message(f))@i'
8. e1 : E@i
9. CLK_message-constraint{i:l}(MsgType;locs;reply;f)@i'
10. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))@i
11. e2 : E@i
12. ∀e3:E
      ((e3 < e2)
      ⇒ (∀clock1,clock2:ℤ.
            (e1 ⟶ e3 ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1) ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e3) ⇒ clock1 < clock2)))
13. clock1 : ℤ@i
14. clock2 : ℤ@i
15. e : E@i
16. (e < e2)@i
17. (¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in CLK_main(MsgType;locs;reply;f)@i
18. e = e1 ∈ E@i
19. clock1 ∈ CLK_Clock(MsgType;f)(e1)@i
20. clock2 ∈ CLK_Clock(MsgType;f)(e2)@i
21. loc(e) = loc(e2) ∈ Id
⊢ clock1 < clock2

2
1. MsgType : {T:Type| valueall-type(T)} @i'
2. locs : bag(Id)@i
3. reply : Id ⟶ MsgType ⟶ (MsgType × Id)@i
4. f : CLK_headers_type{i:l}(MsgType)@i'
5. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
6. f ∈ Name ⟶ Type
7. es : EO+(Message(f))@i'
8. e1 : E@i
9. CLK_message-constraint{i:l}(MsgType;locs;reply;f)@i'
10. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))@i
11. e2 : E@i
12. ∀e3:E
      ((e3 < e2)
      ⇒ (∀clock1,clock2:ℤ.
            (e1 ⟶ e3 ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1) ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e3) ⇒ clock1 < clock2)))
13. clock1 : ℤ@i
14. clock2 : ℤ@i
15. e : E@i
16. (e < e2)@i
17. (¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in CLK_main(MsgType;locs;reply;f)@i
18. e = e1 ∈ E@i
19. clock1 ∈ CLK_Clock(MsgType;f)(e1)@i
20. clock2 ∈ CLK_Clock(MsgType;f)(e2)@i
21. ¬(loc(e) = loc(e2) ∈ Id)
⊢ clock1 < clock2

3
1. MsgType : {T:Type| valueall-type(T)} @i'
2. locs : bag(Id)@i
3. reply : Id ⟶ MsgType ⟶ (MsgType × Id)@i
4. f : CLK_headers_type{i:l}(MsgType)@i'
5. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
6. f ∈ Name ⟶ Type
7. es : EO+(Message(f))@i'
8. e1 : E@i
9. CLK_message-constraint{i:l}(MsgType;locs;reply;f)@i'
10. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))@i
11. e2 : E@i
12. ∀e3:E
      ((e3 < e2)
      ⇒ (∀clock1,clock2:ℤ.
            (e1 ⟶ e3 ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1) ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e3) ⇒ clock1 < clock2)))
13. clock1 : ℤ@i
14. clock2 : ℤ@i
15. e : E@i
16. (e < e2)@i
17. (¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in CLK_main(MsgType;locs;reply;f)@i
18. e1 ⟶ e@i
19. clock1 ∈ CLK_Clock(MsgType;f)(e1)@i
20. clock2 ∈ CLK_Clock(MsgType;f)(e2)@i
21. loc(e) = loc(e2) ∈ Id
⊢ clock1 < clock2

4
1. MsgType : {T:Type| valueall-type(T)} @i'
2. locs : bag(Id)@i
3. reply : Id ⟶ MsgType ⟶ (MsgType × Id)@i
4. f : CLK_headers_type{i:l}(MsgType)@i'
5. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
6. f ∈ Name ⟶ Type
7. es : EO+(Message(f))@i'
8. e1 : E@i
9. CLK_message-constraint{i:l}(MsgType;locs;reply;f)@i'
10. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))@i
11. e2 : E@i
12. ∀e3:E
      ((e3 < e2)
      ⇒ (∀clock1,clock2:ℤ.
            (e1 ⟶ e3 ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1) ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e3) ⇒ clock1 < clock2)))
13. clock1 : ℤ@i
14. clock2 : ℤ@i
15. e : E@i
16. (e < e2)@i
17. (¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in CLK_main(MsgType;locs;reply;f)@i
18. e1 ⟶ e@i
19. clock1 ∈ CLK_Clock(MsgType;f)(e1)@i
20. clock2 ∈ CLK_Clock(MsgType;f)(e2)@i
21. ¬(loc(e) = loc(e2) ∈ Id)
⊢ clock1 < clock2

---

Latex:

---

Latex:
\mforall{}MsgType:ValueAllType.  \mforall{}locs:bag(Id).  \mforall{}reply:Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id).
\mforall{}f:CLK\_headers\_type\{i:l\}(MsgType).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.  \mforall{}clock1,clock2:\mBbbZ{}.
    (CLK\_message-constraint\{i:l\}(MsgType;locs;reply;f)
    {}\mRightarrow{}  (\mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f)))
    {}\mRightarrow{}  e1  {}\mrightarrow{}  e2
    {}\mRightarrow{}  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)
    {}\mRightarrow{}  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e2)
    {}\mRightarrow{}  clock1  <  clock2)


By

---

Latex:
(StartEmlProof
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  RepeatFor  3  (MoveToConcl  (-3))
  THEN  CausalInd'
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `es-happened-before`  (-3)
  THEN  DProdsAndUnions
  THEN  (Decide  \mkleeneopen{}loc(e)  =  loc(e2)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index