---

Step * of Lemma pRun-System-invariant

∀[M:Type ⟶ Type]
  ∀[Q:ℕ ⟶ System(P.M[P]) ⟶ ℙ]
    ∀nat2msg:ℕ ⟶ pMsg(P.M[P]). ∀loc2msg:Id ⟶ pMsg(P.M[P]). ∀S0:System(P.M[P]).
      (Q[0;S0]
      ⇒ (∀t:ℕ. ∀S:System(P.M[P]).
            (Q[t;S]
            ⇒ (∀env:pEnvType(P.M[P])
                  let n,m,nm = env (t + 1) pRun(S0;env;nat2msg;loc2msg) in 
                  Q[t + 1;snd(do-chosen-command(nat2msg;loc2msg;t + 1;S;n;m;nm))])))
      ⇒ {∀env:pEnvType(P.M[P]). ∀t:ℕ.  Q[t;snd((pRun(S0;env;nat2msg;loc2msg) t))]}) 
  supposing Continuous+(P.M[P])
BY
{ (RepeatFor 7 ((D 0 THENA Auto))
   THEN (At ⌜Type⌝ (D 0)⋅ THENA (Auto THEN GenConclAtAddr [2;1] THEN Auto THEN DoSubsume THEN Auto THEN Auto))
   THEN (Unfold `guard` 0 THEN Auto THEN CompNatInd (-1) THEN RecUnfold `pRun` 0 THEN Reduce 0 THEN AutoSplit)⋅) }

1
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. [Q] : ℕ ⟶ System(P.M[P]) ⟶ ℙ
4. nat2msg : ℕ ⟶ pMsg(P.M[P])@i
5. loc2msg : Id ⟶ pMsg(P.M[P])@i
6. S0 : System(P.M[P])@i
7. Q[0;S0]@i
8. ∀t:ℕ. ∀S:System(P.M[P]).
     (Q[t;S]
     ⇒ (∀env:pEnvType(P.M[P])
           let n,m,nm = env (t + 1) pRun(S0;env;nat2msg;loc2msg) in 
           Q[t + 1;snd(do-chosen-command(nat2msg;loc2msg;t + 1;S;n;m;nm))]))@i
9. env : pEnvType(P.M[P])@i
10. t : {1...}
11. ∀t:ℕt. Q[t;snd((pRun(S0;env;nat2msg;loc2msg) t))]@i
⊢ Q[t;snd(let n,m,nm = env t pRun(S0;env;nat2msg;loc2msg) in 
  do-chosen-command(nat2msg;loc2msg;t;snd((pRun(S0;env;nat2msg;loc2msg) (t - 1)));n;m;nm))]

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[Q:\mBbbN{}  {}\mrightarrow{}  System(P.M[P])  {}\mrightarrow{}  \mBbbP{}]
        \mforall{}nat2msg:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}loc2msg:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S0:System(P.M[P]).
            (Q[0;S0]
            {}\mRightarrow{}  (\mforall{}t:\mBbbN{}.  \mforall{}S:System(P.M[P]).
                        (Q[t;S]
                        {}\mRightarrow{}  (\mforall{}env:pEnvType(P.M[P])
                                    let  n,m,nm  =  env  (t  +  1)  pRun(S0;env;nat2msg;loc2msg)  in 
                                    Q[t  +  1;snd(do-chosen-command(nat2msg;loc2msg;t  +  1;S;n;m;nm))])))
            {}\mRightarrow{}  \{\mforall{}env:pEnvType(P.M[P]).  \mforall{}t:\mBbbN{}.    Q[t;snd((pRun(S0;env;nat2msg;loc2msg)  t))]\}) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(RepeatFor  7  ((D  0  THENA  Auto))
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}
              THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  Auto  THEN  DoSubsume  THEN  Auto  THEN  Auto)
              )
  THEN  (Unfold  `guard`  0
              THEN  Auto
              THEN  CompNatInd  (-1)
              THEN  RecUnfold  `pRun`  0
              THEN  Reduce  0
              THEN  AutoSplit)\mcdot{})

---

Home Index