---

Step * of Lemma K-uforces-monotone

∀K:mKripkeStruct. ∀fmla:mFOL(). ∀i,j:World.
  (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a))))
BY
{ TACTIC:RepeatFor 2 ((D 0 THENA Auto)) }

1
1. K : mKripkeStruct
2. fmla : mFOL()
⊢ ∀i,j:World.
    (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a))))

---

Latex:

---

Latex:
\mforall{}K:mKripkeStruct.  \mforall{}fmla:mFOL().  \mforall{}i,j:World.
    (i  \mleq{}  j
    {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                ((K-uforces(K;fmla)  i  a)  \msubseteq{}r  (K-uforces(K;fmla)  j  a))))


By

---

Latex:
TACTIC:RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index