---

Step * 2 of Lemma CLK-prop


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
BY
{ ((D (-5) THENA Auto)
   THEN D (-1)
   THEN RepUR ``make-msg-interface`` (-1)
   THEN (RWO "CLK-ilf" (-1) THENA Auto)
   THEN RepD) }

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. e = e1 ∈ E@i
18. clock1 ∈ CLK_Clock(MsgType;f)(e1)@i
19. clock2 ∈ CLK_Clock(MsgType;f)(e2)@i
20. ¬(loc(e) = loc(e2) ∈ Id)
21. delay : ℤ@i
22. loc(e) ↓∈ locs
23. header(e) = ``CLK msg`` ∈ Name
24. has-es-info-type(es;e;f;MsgType × ℤ)
25. delay = 0 ∈ ℤ
26. loc(e2) = (snd((reply loc(e) (fst(msgval(e)))))) ∈ Id
27. info(e2) = make-Msg(``CLK msg``;<fst((reply loc(e) (fst(msgval(e))))), CLK_ClockVal(MsgType;f)@e>) ∈ Message(f)
⊢ clock1 < clock2

---

Latex:

---

Latex:

1.  MsgType  :  \{T:Type|  valueall-type(T)\}  @i'
2.  locs  :  bag(Id)@i
3.  reply  :  Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id)@i
4.  f  :  CLK\_headers\_type\{i:l\}(MsgType)@i'
5.  (f  ``CLK  msg``)  =  (MsgType  \mtimes{}  \mBbbZ{})
6.  f  \mmember{}  Name  {}\mrightarrow{}  Type
7.  es  :  EO+(Message(f))@i'
8.  e1  :  E@i
9.  CLK\_message-constraint\{i:l\}(MsgType;locs;reply;f)@i'
10.  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f))@i
11.  e2  :  E@i
12.  \mforall{}e3:E
            ((e3  <  e2)
            {}\mRightarrow{}  (\mforall{}clock1,clock2:\mBbbZ{}.
                        (e1  {}\mrightarrow{}  e3
                        {}\mRightarrow{}  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)
                        {}\mRightarrow{}  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e3)
                        {}\mRightarrow{}  clock1  <  clock2)))
13.  clock1  :  \mBbbZ{}@i
14.  clock2  :  \mBbbZ{}@i
15.  e  :  E@i
16.  (e  <  e2)@i
17.  (\mneg{}(loc(e)  =  loc(e2)))  {}\mRightarrow{}  e2  caused  by  e  in  CLK\_main(MsgType;locs;reply;f)@i
18.  e  =  e1@i
19.  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)@i
20.  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e2)@i
21.  \mneg{}(loc(e)  =  loc(e2))
\mvdash{}  clock1  <  clock2


By

---

Latex:
((D  (-5)  THENA  Auto)
  THEN  D  (-1)
  THEN  RepUR  ``make-msg-interface``  (-1)
  THEN  (RWO  "CLK-ilf"  (-1)  THENA  Auto)
  THEN  RepD)

---

Home Index