---

Step * 4 of Lemma CLK-prop2


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. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))@i
10. e2 : E@i
11. ∀e3:E
      ((e3 < e2)
      ⇒ (∀clock1,clock2:ℤ.
            (e1 ⟶ e3 ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1) ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e3) ⇒ clock1 < clock2)))
12. clock1 : ℤ@i
13. clock2 : ℤ@i
14. e : E@i
15. (e < e2)@i
16. (¬(loc(e) = loc(e2) ∈ Id))
⇒ (∃delay:ℤ. make-msg-interface(delay;loc(e2);info(e2)) ∈ CLK_main(MsgType;locs;reply;f)(e))@i
17. 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)
⊢ clock1 < clock2
BY
{ ((InstHyp [⌜e⌝;⌜clock1⌝;⌜CLK_ClockVal(MsgType;f)@e⌝] (-10)⋅ THENA (Auto THEN RWO "CLK_Clock-classrel" 0 THEN Auto))
   THEN Assert ⌜CLK_ClockVal(MsgType;f)@e < clock2⌝⋅
   THEN Auto
   THEN ExRepD
   THEN RepUR ``make-msg-interface`` (-1)
   THEN (RWO "CLK-ilf" (-1) THENA Auto)
   THEN RepD
   THEN (RWO "CLK_Clock-classrel" (-10) THENA Auto)
   THEN SimpleSubstVar `clock2' 0
   THEN (RW (AddrC [2] (LemmaC `CLK_ClockFun-eq`)) 0 THENA Auto)
   THEN AutoSplit
   THEN If (\p.opid_of_term(h (-1) p) = `assert`) (Thin (-1)) Id
   THEN RepUR ``CLK_msg'base`` 0
   THEN (RWO "classfun-res-member-base" 0 THENA Auto)
   THEN Try (Complete (((InstHyp [⌜e2⌝] 9⋅ THENA Auto) THEN RepUR ``CLK_msg'base`` (-1) THEN Auto)))
   THEN (Assert ⌜msgval(e2) = <fst((reply loc(e) (fst(msgval(e))))), CLK_ClockVal(MsgType;f)@e> ∈ (MsgType × ℤ)⌝⋅
   THENM ((HypSubst (-1) 0 THENA Auto) THEN Reduce 0 THEN BLemma `le_to_lt` THEN Auto')
   )
   THEN UnfoldAtAddr [2] 0
   THEN (RW (AddrC [2] (LemmaC `Message-eta`)) (-1) THENA Auto)
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Try (Complete ((RepUR ``make-Authentic-Msg make-Msg`` (-2) THEN EqHD (-2) THEN Auto)))
   THEN (RWO "make-Msg-equal" (-2) THENA Auto)
   THEN Try ((RWO "msg-has-type-encodes" 0 THEN Auto THEN D 0 THEN Auto))
   THEN Try (Complete ((GenConclAtAddr [2] THEN Try (ProveEncodesMsgType) THEN Auto)))
   THEN D (-2)
   THEN (Assert ⌜(f msg-header(info(e2))) ⊆r (MsgType × ℤ)⌝⋅ THENM Auto)
   THEN Fold `msg-type` 0
   THEN Fold `msg-has-type` 0
   THEN (RWO "msg-has-type-encodes" 0 THENA Auto)
   THEN ProveEncodesMsgType) }

---

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.  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f))@i
10.  e2  :  E@i
11.  \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)))
12.  clock1  :  \mBbbZ{}@i
13.  clock2  :  \mBbbZ{}@i
14.  e  :  E@i
15.  (e  <  e2)@i
16.  (\mneg{}(loc(e)  =  loc(e2)))
{}\mRightarrow{}  (\mexists{}delay:\mBbbZ{}.  make-msg-interface(delay;loc(e2);info(e2))  \mmember{}  CLK\_main(MsgType;locs;reply;f)(e))@i
17.  e1  {}\mrightarrow{}  e@i
18.  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)@i
19.  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e2)@i
20.  \mneg{}(loc(e)  =  loc(e2))
\mvdash{}  clock1  <  clock2


By

---

Latex:
((InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}clock1\mkleeneclose{};\mkleeneopen{}CLK\_ClockVal(MsgType;f)@e\mkleeneclose{}]  (-10)\mcdot{}
    THENA  (Auto  THEN  RWO  "CLK\_Clock-classrel"  0  THEN  Auto)
    )
  THEN  Assert  \mkleeneopen{}CLK\_ClockVal(MsgType;f)@e  <  clock2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  RepUR  ``make-msg-interface``  (-1)
  THEN  (RWO  "CLK-ilf"  (-1)  THENA  Auto)
  THEN  RepD
  THEN  (RWO  "CLK\_Clock-classrel"  (-10)  THENA  Auto)
  THEN  SimpleSubstVar  `clock2'  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `CLK\_ClockFun-eq`))  0  THENA  Auto)
  THEN  AutoSplit
  THEN  If  (\mbackslash{}p.opid\_of\_term(h  (-1)  p)  =  `assert`)  (Thin  (-1))  Id
  THEN  RepUR  ``CLK\_msg'base``  0
  THEN  (RWO  "classfun-res-member-base"  0  THENA  Auto)
  THEN  Try  (Complete  (((InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  9\mcdot{}  THENA  Auto)  THEN  RepUR  ``CLK\_msg'base``  (-1)  THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}msgval(e2)  =  <fst((reply  loc(e)  (fst(msgval(e))))),  CLK\_ClockVal(MsgType;f)@e>\mkleeneclose{}\mcdot{}
  THENM  ((HypSubst  (-1)  0  THENA  Auto)  THEN  Reduce  0  THEN  BLemma  `le\_to\_lt`  THEN  Auto')
  )
  THEN  UnfoldAtAddr  [2]  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `Message-eta`))  (-1)  THENA  Auto)
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Try  (Complete  ((RepUR  ``make-Authentic-Msg  make-Msg``  (-2)  THEN  EqHD  (-2)  THEN  Auto)))
  THEN  (RWO  "make-Msg-equal"  (-2)  THENA  Auto)
  THEN  Try  ((RWO  "msg-has-type-encodes"  0  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  Try  (Complete  ((GenConclAtAddr  [2]  THEN  Try  (ProveEncodesMsgType)  THEN  Auto)))
  THEN  D  (-2)
  THEN  (Assert  \mkleeneopen{}(f  msg-header(info(e2)))  \msubseteq{}r  (MsgType  \mtimes{}  \mBbbZ{})\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  Fold  `msg-type`  0
  THEN  Fold  `msg-has-type`  0
  THEN  (RWO  "msg-has-type-encodes"  0  THENA  Auto)
  THEN  ProveEncodesMsgType)

---

Home Index