---

Step * 1 of Lemma CLK_stric_inc


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)
BY
{ (ReduceAutoMemory THEN RepeatFor 2 (SimpleReasoningStep) THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  MsgType  :  \{T:Type|  valueall-type(T)\}  @i'
2.  f  :  CLK\_headers\_type\{i:l\}(MsgType)@i'
3.  (f  ``CLK  msg``)  =  (MsgType  \mtimes{}  \mBbbZ{})
4.  f  \mmember{}  Name  {}\mrightarrow{}  Type
5.  es  :  EO+(Message(f))@i'
6.  e1  :  E@i
7.  e2  :  E@i
8.  clock1  :  \mBbbZ{}@i
9.  clock2  :  \mBbbZ{}@i
10.  \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))@i
11.  (e1  <loc  e2)@i
12.  clock1  \mmember{}  State-loc-comb(\mlambda{}loc.\{0\};CLK\_upd\_clock(MsgType);CLK\_msg'base(MsgType;f))(e1)
13.  clock2  \mmember{}  State-loc-comb(\mlambda{}loc.\{0\};CLK\_upd\_clock(MsgType);CLK\_msg'base(MsgType;f))(e2)
14.  a  :  MsgType  \mtimes{}  \mBbbZ{}@i
15.  e  :  E@i
16.  (e1  <loc  e)@i
17.  e  \mleq{}loc  e2  @i
18.  a  \mmember{}  CLK\_msg'base(MsgType;f)(e)@i
19.  s  :  \mBbbZ{}@i
20.  s  \mmember{}  State-loc-comb(\mlambda{}loc.\{0\};CLK\_upd\_clock(MsgType);CLK\_msg'base(MsgType;f))(pred(e))@i
\mvdash{}  (\mlambda{}clock2.s  <  clock2)  (CLK\_upd\_clock(MsgType)  loc(e)  a  s)


By

---

Latex:
(ReduceAutoMemory
  THEN  RepeatFor  2  (SimpleReasoningStep)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index