Step
*
1
1
3
1
of Lemma
std-component-property
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E ─→ (E?)
12. (∀C∈[<x, Q>].∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);≤loc(e)))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
⊢ ∀p∈last(data-stream(Q;map(λe.info(e);≤loc(e)))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((c1 e') = (inl e) ∈ (E?)))) ∈ ℙ
BY
{ GenConclAtAddrType ⌈pExt(P.M[P])⌉ [2;1]⋅ }
1
.....wf.....
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E ─→ (E?)
12. (∀C∈[<x, Q>].∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);≤loc(e)))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
⊢ last(data-stream(Q;map(λe.info(e);≤loc(e)))) ∈ pExt(P.M[P])
2
.....wf.....
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E ─→ (E?)
12. (∀C∈[<x, Q>].∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);≤loc(e)))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
⊢ pExt(P.M[P]) ∈ Type
3
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>;S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E ─→ (E?)
12. (∀C∈[<x, Q>].∀e:E
∀p∈last(data-stream(snd(C);map(λe.info(e);≤loc(e)))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
13. c1 : E ─→ (E?)
14. e : E@i
15. loc(e) = x ∈ Id@i
16. v : pExt(P.M[P])@i
17. last(data-stream(Q;map(λe.info(e);≤loc(e)))) = v ∈ pExt(P.M[P])@i
⊢ ∀p∈v.let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':E
((loc(e') = y ∈ Id)
∧ (e < e')
∧ (∃n:ℕ. ∃nm:Id. (info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((c1 e') = (inl e) ∈ (E?)))) ∈ ℙ
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i
4. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i
5. x : Id@i
6. Q : Process(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. sub-system(P.M[P];<[<x, Q>], lg-nil()>S2)@i
9. env : pEnvType(P.M[P])@i
10. reliable-env(env; pRun(S2;env;n2m;l2m))@i
11. cause : E {}\mrightarrow{} (E?)
12. (\mforall{}C\mmember{}[<x, Q>].\mforall{}e:E
\mforall{}p\mmember{}last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e)))).
let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':E
((loc(e') = y)
\mwedge{} (e < e')
\mwedge{} (\mexists{}n:\mBbbN{}. \mexists{}nm:Id. (info(e') = command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((cause e') = (inl e))))
supposing loc(e) = (fst(C)))
13. c1 : E {}\mrightarrow{} (E?)
14. e : E@i
15. loc(e) = x@i
\mvdash{} \mforall{}p\mmember{}last(data-stream(Q;map(\mlambda{}e.info(e);\mleq{}loc(e)))).let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':E
((loc(e') = y)
\mwedge{} (e < e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((c1 e') = (inl e)))) \mmember{} \mBbbP{}
By
Latex:
GenConclAtAddrType \mkleeneopen{}pExt(P.M[P])\mkleeneclose{} [2;1]\mcdot{}
Home
Index