---

Step * of Lemma K-assignment_subtype

∀[K:mKripkeStruct]. ∀[i,j:World].
  ∀vs1,vs2:ℤ List.  FOAssignment(vs1,Dom(i)) ⊆r FOAssignment(vs2,Dom(j)) supposing vs2 ⊆ vs1 supposing i ≤ j
BY
{ (Auto THEN Unfold `l_contains` -1 THEN (RWO "l_all_iff" (-1) THENA Auto) THEN Unfold `FOAssignment` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:mKripkeStruct].  \mforall{}[i,j:World].
    \mforall{}vs1,vs2:\mBbbZ{}  List.    FOAssignment(vs1,Dom(i))  \msubseteq{}r  FOAssignment(vs2,Dom(j))  supposing  vs2  \msubseteq{}  vs1 
    supposing  i  \mleq{}  j


By

---

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

---

Home Index