---

Step * of Lemma K-uforces-umonotone

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

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

---

Latex:

---

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


By

---

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

---

Home Index