---

Step * of Lemma not-self-starting_wf

∀[Info,A:Type]. ∀[Y:A ⟶ EClass(A)].  (not-self-starting{i:l}(Info;A;Y) ∈ ℙ')
BY
{ (Auto
   THEN Unfold `not-self-starting` 0
   THEN (Assert ⌜A ∈ 𝕌'⌝⋅ THENA Auto)
   THEN RepeatFor 5 ((MemCD THEN Try (Complete (Auto))))
   THEN Thin 4
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(A)].    (not-self-starting\{i:l\}(Info;A;Y)  \mmember{}  \mBbbP{}')


By

---

Latex:
(Auto
  THEN  Unfold  `not-self-starting`  0
  THEN  (Assert  \mkleeneopen{}A  \mmember{}  \mBbbU{}'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  5  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Thin  4
  THEN  Auto)\mcdot{}

---

Home Index