Step
*
1
2
1
of Lemma
global-order-pairwise-compat-msg-interface-constraint
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E. (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E. ((header(e) ∈ hdrs)
⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (msg-header(info(e)) ∈ hdrs)@i
12. e' : E
13. delay : ℤ
14. (e' < e)
15. make-msg-interface(delay;loc(e);info(e)) ∈ X(e')
16. (e' < e)
⊢ ∃delay:ℤ
make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))||
- 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))
BY
{ (With ⌈delay⌉ (D 0)⋅ THEN Auto) }
1
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E. (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E. ((header(e) ∈ hdrs)
⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (msg-header(info(e)) ∈ hdrs)@i
12. e' : E
13. delay : ℤ
14. (e' < e)
15. make-msg-interface(delay;loc(e);info(e)) ∈ X(e')
16. (e' < e)
⊢ make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))||
- 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))
2
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E. (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E. ((header(e) ∈ hdrs)
⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (msg-header(info(e)) ∈ hdrs)@i
12. e' : E
13. delay : ℤ
14. (e' < e)
15. make-msg-interface(delay;loc(e);info(e)) ∈ X(e')
16. (e' < e)
17. d1 : ℤ
⊢ ¬↑null(map(λx.info(x);≤loc(e')))
Latex:
Latex:
1. f : Name {}\mrightarrow{} Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id {}\mrightarrow{} hdataflow(Message(f);Interface)@i'
5. \mforall{}es:EO+(Message(f)). \mforall{}e:E. (X(e) = (snd(F loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))@i'
6. eo : EO+(Message(f))@i'
7. \mforall{}e:E
((header(e) \mmember{} hdrs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. \mexists{}delay:\mBbbZ{}. ((e' < e) \mwedge{} make-msg-interface(delay;loc(e);info(e)) \mmember{} X(e'))))@i
8. e : E@i
9. \mforall{}e:E. (last(map(\mlambda{}x.info(x);\mleq{}loc(e))) \msim{} info(e))
10. last(map(\mlambda{}x.info(x);\mleq{}loc(e))) \msim{} info(e)
11. (msg-header(info(e)) \mmember{} hdrs)@i
12. e' : E
13. delay : \mBbbZ{}
14. (e' < e)
15. make-msg-interface(delay;loc(e);info(e)) \mmember{} X(e')
16. (e' < e)
\mvdash{} \mexists{}delay:\mBbbZ{}
make-msg-interface(delay;loc(e);info(e)) \mdownarrow{}\mmember{} snd(F loc(e')*(firstn(||map(\mlambda{}x.info(x);\mleq{}loc(e'))||
- 1;map(\mlambda{}x.info(x);\mleq{}loc(e'))))(last(map(\mlambda{}x.info(x);\mleq{}loc(e')))))
By
Latex:
(With \mkleeneopen{}delay\mkleeneclose{} (D 0)\mcdot{} THEN Auto)
Home
Index