---

Step * 1 2 1 of Lemma K-uforces-monotone


1. K : mKripkeStruct
2. fmla : mFOL()
3. knd : Atom
4. left : mFOL()
5. right : mFOL()
6. ∀i,j:World.
     (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(left),Dom(i)). ((K-uforces(K;left) i a) ⊆r (K-uforces(K;left) j a))))
7. ∀i,j:World.
     (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(right),Dom(i)). ((K-uforces(K;right) i a) ⊆r (K-uforces(K;right) j a))))
8. i : World
9. j : World
10. i ≤ j
11. a : FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom(i))
12. (K-uforces(K;left) i a) ⊆r (K-uforces(K;left) j a)
13. (K-uforces(K;right) i a) ⊆r (K-uforces(K;right) j a)
14. knd = "and" ∈ Atom
⊢ ((K-uforces(K;left) i a) ∧ (K-uforces(K;right) i a)) ⊆r ((K-uforces(K;left) j a) ∧ (K-uforces(K;right) j a))
BY
{ ((Unfold `and` 0 THEN SubtypeReasoning1) THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  mKripkeStruct
2.  fmla  :  mFOL()
3.  knd  :  Atom
4.  left  :  mFOL()
5.  right  :  mFOL()
6.  \mforall{}i,j:World.
          (i  \mleq{}  j
          {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(left),Dom(i))
                      ((K-uforces(K;left)  i  a)  \msubseteq{}r  (K-uforces(K;left)  j  a))))
7.  \mforall{}i,j:World.
          (i  \mleq{}  j
          {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(right),Dom(i))
                      ((K-uforces(K;right)  i  a)  \msubseteq{}r  (K-uforces(K;right)  j  a))))
8.  i  :  World
9.  j  :  World
10.  i  \mleq{}  j
11.  a  :  FOAssignment(mFOL-freevars(mFOconnect(knd;left;right)),Dom(i))
12.  (K-uforces(K;left)  i  a)  \msubseteq{}r  (K-uforces(K;left)  j  a)
13.  (K-uforces(K;right)  i  a)  \msubseteq{}r  (K-uforces(K;right)  j  a)
14.  knd  =  "and"
\mvdash{}  ((K-uforces(K;left)  i  a)  \mwedge{}  (K-uforces(K;right)  i  a))  \msubseteq{}r  ((K-uforces(K;left)  j  a)
        \mwedge{}  (K-uforces(K;right)  j  a))


By

---

Latex:
((Unfold  `and`  0  THEN  SubtypeReasoning1)  THEN  Auto)

---

Home Index