---

Step * 1 2 3 of Lemma K-forces-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-forces(K;left) i a) ⊆r (K-forces(K;left) j a))))
7. ∀i,j:World.
     (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(right),Dom(i)). ((K-forces(K;right) i a) ⊆r (K-forces(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-forces(K;left) i a) ⊆r (K-forces(K;left) j a)
13. (K-forces(K;right) i a) ⊆r (K-forces(K;right) j a)
14. ¬(knd = "and" ∈ Atom)
15. ¬(knd = "or" ∈ Atom)
⊢ (∀j:{j:World| i ≤ j} . ((K-forces(K;left) j a) ⇒ (K-forces(K;right) j a))) ⊆r (∀j:{j@0:World| j ≤ j@0} 
                                                                                   ((K-forces(K;left) j a)
                                                                                   ⇒ (K-forces(K;right) j a)))
BY
{ (Unfold `all` 0
   THEN SubtypeReasoning1
   THEN Auto
   THEN Try ((DSetVars THEN InstLemma `K-le_transitivity` [⌜K⌝;⌜i⌝;⌜j⌝;⌜j1⌝]⋅ THEN Auto))) }

1
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-forces(K;left) i a) ⊆r (K-forces(K;left) j a))))
7. ∀i,j:World.
     (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(right),Dom(i)). ((K-forces(K;right) i a) ⊆r (K-forces(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-forces(K;left) i a) ⊆r (K-forces(K;left) j a)
13. (K-forces(K;right) i a) ⊆r (K-forces(K;right) j a)
14. ¬(knd = "and" ∈ Atom)
15. ¬(knd = "or" ∈ Atom)
⊢ {j@0:World| j ≤ j@0}  ⊆r {j:World| i ≤ j} 

---

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-forces(K;left)  i  a)  \msubseteq{}r  (K-forces(K;left)  j  a))))
7.  \mforall{}i,j:World.
          (i  \mleq{}  j
          {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(right),Dom(i))
                      ((K-forces(K;right)  i  a)  \msubseteq{}r  (K-forces(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-forces(K;left)  i  a)  \msubseteq{}r  (K-forces(K;left)  j  a)
13.  (K-forces(K;right)  i  a)  \msubseteq{}r  (K-forces(K;right)  j  a)
14.  \mneg{}(knd  =  "and")
15.  \mneg{}(knd  =  "or")
\mvdash{}  (\mforall{}j:\{j:World|  i  \mleq{}  j\}  .  ((K-forces(K;left)  j  a)  {}\mRightarrow{}  (K-forces(K;right)  j  a)))
        \msubseteq{}r  (\mforall{}j:\{j@0:World|  j  \mleq{}  j@0\}  .  ((K-forces(K;left)  j  a)  {}\mRightarrow{}  (K-forces(K;right)  j  a)))


By

---

Latex:
(Unfold  `all`  0
  THEN  SubtypeReasoning1
  THEN  Auto
  THEN  Try  ((DSetVars  THEN  InstLemma  `K-le\_transitivity`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}j1\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index