---

Step * of Lemma mFOL-abstract-has-value

∀[fmla:mFOL()]. (mFOL-abstract(fmla))↓
BY
{ xxx((D 0 THENA Auto) THEN SimpleDatatypeInduction (-1) THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[fmla:mFOL()].  (mFOL-abstract(fmla))\mdownarrow{}


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  SimpleDatatypeInduction  (-1)  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index