---

Step * of Lemma CLK_stric_inc

∀MsgType:ValueAllType. ∀f:CLK_headers_type{i:l}(MsgType). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
  ((∃a:MsgType × ℤ. ∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ a ∈ CLK_msg'base(MsgType;f)(e)))
  ⇒ (e1 <loc e2)
  ⇒ clock1 ∈ CLK_Clock(MsgType;f)(e1)
  ⇒ clock2 ∈ CLK_Clock(MsgType;f)(e2)
  ⇒ clock1 < clock2)
BY
{ ((GenMemoryTrans1 2 ProgressLemmas⋅⋅ THENA Auto) THEN Try (WithRuleCount 10000 GenMemoryTrans2⋅⋅)) }

1
1. MsgType : {T:Type| valueall-type(T)} @i'
2. f : CLK_headers_type{i:l}(MsgType)@i'
3. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
4. f ∈ Name ⟶ Type
5. es : EO+(Message(f))@i'
6. e1 : E@i
7. e2 : E@i
8. clock1 : ℤ@i
9. clock2 : ℤ@i
10. ∃a:MsgType × ℤ. ∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ a ∈ CLK_msg'base(MsgType;f)(e))@i
11. (e1 <loc e2)@i
12. clock1 ∈ State-loc-comb(λloc.{0};CLK_upd_clock(MsgType);CLK_msg'base(MsgType;f))(e1)
13. clock2 ∈ State-loc-comb(λloc.{0};CLK_upd_clock(MsgType);CLK_msg'base(MsgType;f))(e2)
14. a : MsgType × ℤ@i
15. e : E@i
16. (e1 <loc e)@i
17. e ≤loc e2 @i
18. a ∈ CLK_msg'base(MsgType;f)(e)@i
19. s : ℤ@i
20. s ∈ State-loc-comb(λloc.{0};CLK_upd_clock(MsgType);CLK_msg'base(MsgType;f))(pred(e))@i
⊢ (λclock2.s < clock2) (CLK_upd_clock(MsgType) loc(e) a s)

---

Latex:

---

Latex:
\mforall{}MsgType:ValueAllType.  \mforall{}f:CLK\_headers\_type\{i:l\}(MsgType).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}clock1,clock2:\mBbbZ{}.
    ((\mexists{}a:MsgType  \mtimes{}  \mBbbZ{}.  \mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  a  \mmember{}  CLK\_msg'base(MsgType;f)(e)))
    {}\mRightarrow{}  (e1  <loc  e2)
    {}\mRightarrow{}  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)
    {}\mRightarrow{}  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e2)
    {}\mRightarrow{}  clock1  <  clock2)


By

---

Latex:
((GenMemoryTrans1  2  ProgressLemmas\mcdot{}\mcdot{}  THENA  Auto)  THEN  Try  (WithRuleCount  10000  GenMemoryTrans2\mcdot{}\mcdot{}))

---

Home Index