Proof of Nuprl Lemma : pRun

Step * 1 2 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
⊢ system-equiv(P.M[P];snd(let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in

                      do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S1;env;nat2msg;loc2msg) (t - 1)));n;m;nm));

snd(let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in

                      do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S2;env;nat2msg;loc2msg) (t - 1)));n;m;nm)))

∧ (let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in
  do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S1;env;nat2msg;loc2msg) (t - 1)));n;m;nm)
  = let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in
    do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S2;env;nat2msg;loc2msg) (t - 1)));n;m;nm)
  ∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
BY

{ Assert ⌈(env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)⌉⋅ }

1
.....assertion.....
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
⊢ (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)

2
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)
⊢ system-equiv(P.M[P];snd(let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in

                      do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S1;env;nat2msg;loc2msg) (t - 1)));n;m;nm));

snd(let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in

                      do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S2;env;nat2msg;loc2msg) (t - 1)));n;m;nm)))

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 \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;snd((pRun(S1;env;nat2msg;loc2msg) (t - 1)));n;m;nm)); snd(let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S2;env;nat2msg;loc2msg) (t - 1)));n;m;nm))) \mwedge{} (let n,m,nm = env t pRun(S1;env;nat2msg;loc2msg) in do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S1;env;nat2msg;loc2msg) (t - 1)));n;m;nm) = let n,m,nm = env t pRun(S2;env;nat2msg;loc2msg) in do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S2;env;nat2msg;loc2msg) (t - 1)));n;m;nm)) By Latex: Assert \mkleeneopen{}(env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg))\mkleeneclose{}\mcdot{} Home Index