---

Step * of Lemma K-sat_wf

∀[K:mKripkeStruct]. ∀[i:World]. ∀[fmla:mFOL()]. ∀[a:FOAssignment(mFOL-freevars(fmla),Dom(i))].  (i,a |= fmla ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[K:mKripkeStruct].  \mforall{}[i:World].  \mforall{}[fmla:mFOL()].  \mforall{}[a:FOAssignment(mFOL-freevars(fmla),Dom(i))].
    (i,a  |=  fmla  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index