---

Step * of Lemma mFOLeffect_wf

∀[sr:mFOL-sequent() × mFOLRule()]. (mFOLeffect(sr) ∈ mFOL-sequent() List?)
BY
{ (Auto
   THEN D -1
   THEN D -2
   THEN Unfold `mFOLeffect` 0
   THEN Reduce 0
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN AutoBoolCase ⌈i <z ||s3||⌉⋅) }

---

Latex:


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


By

(Auto
  THEN  D  -1
  THEN  D  -2
  THEN  Unfold  `mFOLeffect`  0
  THEN  Reduce  0
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  AutoBoolCase  \mkleeneopen{}i  <z  ||s3||\mkleeneclose{}\mcdot{})

---

Home Index