---

Step * 1 1 of Lemma K-uforces_wf

.....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))
BY
{ (Unfold `l_contains` 0 THEN RWO "l_all_iff" 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(f3))  \msubseteq{}  mFOL-freevars(\mforall{}var;f3))


By

---

Latex:
(Unfold  `l\_contains`  0  THEN  RWO  "l\_all\_iff"  0  THEN  Auto)

---

Home Index