---

Step * of Lemma mFOLeffect_wf

∀[sr:mFOL-sequent() × FOLRule()]. (mFOLeffect(sr) ∈ mFOL-sequent() List?)
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (D 1)
   THEN Unfold `mFOLeffect` 0
   THEN Reduce 0
   THEN MemCD
   THEN Try ((BoolCase ⌜i <z ||s3||⌝⋅ THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[sr:mFOL-sequent()  \mtimes{}  FOLRule()].  (mFOLeffect(sr)  \mmember{}  mFOL-sequent()  List?)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (D  1)
  THEN  Unfold  `mFOLeffect`  0
  THEN  Reduce  0
  THEN  MemCD
  THEN  Try  ((BoolCase  \mkleeneopen{}i  <z  ||s3||\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index