---

Step * of Lemma do-chosen-command_wf

∀[M:Type ⟶ Type]
  ∀[nat2msg:ℕ ⟶ pMsg(P.M[P])]. ∀[loc2msg:Id ⟶ pMsg(P.M[P])]. ∀[S:System(P.M[P])]. ∀[t,n,m:ℕ]. ∀[nm:Id].
    (do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm) ∈ ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])) 
  supposing Continuous+(P.M[P])
BY
{ ((ProveWfLemma THEN DVar `S2')
   THEN RepUR ``let`` 0
   THEN (Assert n < lg-size(S2) BY
               (RepUR ``lg-is-source`` -1 THEN SplitOnHypITE -1  THEN Auto))
   THEN (GenConclAtAddr [2;1] THENA Auto)
   THEN (RepeatFor 2 (D (-2)) THEN Reduce 0 THEN SplitOnConclITE THEN Try (Complete (Auto)) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[nat2msg:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[loc2msg:Id  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[S:System(P.M[P])].  \mforall{}[t,n,m:\mBbbN{}].
    \mforall{}[nm:Id].
        (do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm)  \mmember{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P])) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
((ProveWfLemma  THEN  DVar  `S2')
  THEN  RepUR  ``let``  0
  THEN  (Assert  n  <  lg-size(S2)  BY
                          (RepUR  ``lg-is-source``  -1  THEN  SplitOnHypITE  -1    THEN  Auto))
  THEN  (GenConclAtAddr  [2;1]  THENA  Auto)
  THEN  (RepeatFor  2  (D  (-2))  THEN  Reduce  0  THEN  SplitOnConclITE  THEN  Try  (Complete  (Auto))  THEN  Auto)
  \mcdot{})

---

Home Index