Step
*
1
2
2
1
of Lemma
pRun_functionality
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
⊢ system-equiv(P.M[P];snd(let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm));snd(let n,m,nm = env t
pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)))
∧ (let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm)
= let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ HypSubst (-4) 0 }
1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
⊢ system-equiv(P.M[P];snd(let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm));snd(let n,m,nm = env t
pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)))
∧ (let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm)
= let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
2
.....wf.....
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
15. z : ℕ × ℕ × Id
⊢ system-equiv(P.M[P];snd(let n,m,nm = z in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm));snd(let n,m,nm = env t
pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)))
∧ (let n,m,nm = z in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm)
= let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))) ∈ ℙ
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. nat2msg : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])
4. loc2msg : Id {}\mrightarrow{} pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : \{1...\}
10. \mforall{}t:\mBbbN{}t
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg)
t)))
\mwedge{} ((pRun(S1;env;nat2msg;loc2msg) t) = (pRun(S2;env;nat2msg;loc2msg) t)))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg))
12. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
\mvdash{} system-equiv(P.M[P];snd(let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm));
snd(let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm)))
\mwedge{} (let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P2;n;m;nm)
= let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
do-chosen-command(nat2msg;loc2msg;t;P4;n;m;nm))
By
Latex:
HypSubst (-4) 0
Home
Index