---

Step * of Lemma std-initial-property

∀[M:Type ⟶ Type]. ∀[S:System(P.M[P])].  ∀[r:pRunType(P.M[P])]. run-initialization(r;snd(S)) supposing std-initial(S)
BY
{ (Auto
   THEN DVar `S'
   THEN (D 0 THEN Auto)
   THEN All Reduce
   THEN (With ⌜n⌝ (D 4)⋅ THEN All Reduce THEN Auto)
   THEN (D 0 THENA Auto))⋅ }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[S:System(P.M[P])].
    \mforall{}[r:pRunType(P.M[P])].  run-initialization(r;snd(S))  supposing  std-initial(S)


By

---

Latex:
(Auto
  THEN  DVar  `S'
  THEN  (D  0  THEN  Auto)
  THEN  All  Reduce
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  4)\mcdot{}  THEN  All  Reduce  THEN  Auto)
  THEN  (D  0  THENA  Auto))\mcdot{}

---

Home Index