---

Step * 1 of Lemma K-uforces_wf


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))
BY
{ Assert ⌜filter(λx.(¬b(x =z var));mFOL-freevars(f3)) ⊆ mFOL-freevars(∀var;f3))⌝⋅ }

1
.....assertion..... 
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)
⊢ filter(λx.(¬b(x =z var));mFOL-freevars(f3)) ⊆ mFOL-freevars(∀var;f3))

2
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)
12. filter(λx.(¬b(x =z var));mFOL-freevars(f3)) ⊆ mFOL-freevars(∀var;f3))
⊢ a ∈ FOAssignment(filter(λx.(¬b(x =z var));mFOL-freevars(f3)),Dom(j))

---

Latex:

---

Latex:

1.  K  :  mKripkeStruct
2.  isall  :  \mBbbB{}
3.  var  :  \mBbbZ{}
4.  f3  :  mFOL()
5.  K-uforces(K;f3)  \mmember{}  i:World  {}\mrightarrow{}  FOAssignment(mFOL-freevars(f3),Dom(i))  {}\mrightarrow{}  \mBbbP{}
6.  \muparrow{}isall
7.  i  :  World
8.  a  :  FOAssignment(mFOL-freevars(\mforall{}var;f3)),Dom(i))
9.  j  :  World
10.  i  \mleq{}  j
11.  v  :  Dom(j)
\mvdash{}  a  \mmember{}  FOAssignment(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(f3)),Dom(j))


By

---

Latex:
Assert  \mkleeneopen{}filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(f3))  \msubseteq{}  mFOL-freevars(\mforall{}var;f3))\mkleeneclose{}\mcdot{}

---

Home Index