---

Step * 1 2 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))
⊢ (if knd =a "and" then λi,a. ((K-uforces(K;left) i a) ∧ (K-uforces(K;right) i a))
   if knd =a "or" then λi,a. ((K-uforces(K;left) i a) ∨ (K-uforces(K;right) i a))
   else λi,a. ∀[j:World]. (K-uforces(K;left) j a) ⇒ (K-uforces(K;right) j a) supposing i ≤ j
   fi  
   i 
   a) ⊆r (if knd =a "and" then λi,a. ((K-uforces(K;left) i a) ∧ (K-uforces(K;right) i a))
          if knd =a "or" then λi,a. ((K-uforces(K;left) i a) ∨ (K-uforces(K;right) i a))
          else λi,a. ∀[j:World]. (K-uforces(K;left) j a) ⇒ (K-uforces(K;right) j a) supposing i ≤ j
          fi  
          j 
          a)
BY
{ (((InstHyp [⌜i⌝;⌜j⌝;⌜a⌝] 6⋅ THENA Auto) THEN (InstHyp [⌜i⌝;⌜j⌝;⌜a⌝] 7⋅ THENA Auto))
   THEN Repeat (((SplitOnConclITE THENA Auto) THEN Reduce 0))
   ) }

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-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))

2
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)
15. knd = "or" ∈ 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))

3
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)
15. ¬(knd = "or" ∈ Atom)
⊢ (∀[j:World]. (K-uforces(K;left) j a) ⇒ (K-uforces(K;right) j a) supposing i ≤ j) ⊆r (∀[j@0:World]
                                                                                          (K-uforces(K;left) j@0 a)
                                                                                          ⇒ (K-uforces(K;right) j@0 a) 
                                                                                          supposing j ≤ j@0)

---

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))
\mvdash{}  (if  knd  =a  "and"  then  \mlambda{}i,a.  ((K-uforces(K;left)  i  a)  \mwedge{}  (K-uforces(K;right)  i  a))
      if  knd  =a  "or"  then  \mlambda{}i,a.  ((K-uforces(K;left)  i  a)  \mvee{}  (K-uforces(K;right)  i  a))
      else  \mlambda{}i,a.  \mforall{}[j:World].  (K-uforces(K;left)  j  a)  {}\mRightarrow{}  (K-uforces(K;right)  j  a)  supposing  i  \mleq{}  j
      fi   
      i 
      a)  \msubseteq{}r  (if  knd  =a  "and"  then  \mlambda{}i,a.  ((K-uforces(K;left)  i  a)  \mwedge{}  (K-uforces(K;right)  i  a))
                    if  knd  =a  "or"  then  \mlambda{}i,a.  ((K-uforces(K;left)  i  a)  \mvee{}  (K-uforces(K;right)  i  a))
                    else  \mlambda{}i,a.  \mforall{}[j:World].  (K-uforces(K;left)  j  a)  {}\mRightarrow{}  (K-uforces(K;right)  j  a)  supposing  i  \mleq{}  j
                    fi   
                    j 
                    a)


By

---

Latex:
(((InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  6\mcdot{}  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  7\mcdot{}  THENA  Auto))
  THEN  Repeat  (((SplitOnConclITE  THENA  Auto)  THEN  Reduce  0))
  )

---

Home Index