---

Step * of Lemma K-uforces_wf

∀[K:mKripkeStruct]. ∀[fmla:mFOL()].  (K-uforces(K;fmla) ∈ i:World ⟶ FOAssignment(mFOL-freevars(fmla),Dom(i)) ⟶ ℙ)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN SimpleDatatypeInduction 2⋅ THEN Reduce 0 THEN Auto) }

1
1. K : mKripkeStruct
2. isall : 𝔹
3. var : ℤ
4. f3 : mFOL()
5. K-uforces(K;f3) ∈ i:World ⟶ FOAssignment(mFOL-freevars(f3),Dom(i)) ⟶ ℙ
6. ↑isall
7. i : World
8. a : FOAssignment(mFOL-freevars(∀var;f3)),Dom(i))
9. j : World
10. i ≤ j
11. v : Dom(j)
⊢ a ∈ FOAssignment(filter(λx.(¬b(x =z var));mFOL-freevars(f3)),Dom(j))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  SimpleDatatypeInduction  2\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index