---

Step * 1 of Lemma K-uforces-monotone


1. K : mKripkeStruct
2. fmla : mFOL()
⊢ ∀i,j:World.
    (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a))))
BY
{ (((InstLemma `mFOL-induction` [⌜λ2fmla.∀i,j:World.
                                           (i ≤ j
                                           ⇒ (∀a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                                                 ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a))))⌝]⋅
    THENM (D -1 With ⌜fmla⌝  THEN Auto)
    )
    THENW Auto
    )
   THEN (UnivCD THENA Auto)
   THEN Reduce 0) }

1
1. K : mKripkeStruct
2. fmla : mFOL()
3. name : Atom
4. vars : ℤ List
5. i : World
6. j : World
7. i ≤ j
8. a : FOAssignment(mFOL-freevars(name(vars)),Dom(i))
⊢ i,a |= name(vars) ⊆r j,a |= name(vars)

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

3
1. K : mKripkeStruct
2. fmla : mFOL()
3. isall : 𝔹
4. var : ℤ
5. body : mFOL()
6. ∀i,j:World.
     (i ≤ j ⇒ (∀a:FOAssignment(mFOL-freevars(body),Dom(i)). ((K-uforces(K;body) i a) ⊆r (K-uforces(K;body) j a))))
7. i : World
8. j : World
9. i ≤ j
10. a : FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom(i))
⊢ (if isall
   then λi,a. ∀[j:World]. ∀v:Dom(j). (K-uforces(K;body) j a[var := v]) supposing i ≤ j
   else λi,a. ∃v:Dom(i). (K-uforces(K;body) i a[var := v])
   fi  
   i 
   a) ⊆r (if isall
          then λi,a. ∀[j:World]. ∀v:Dom(j). (K-uforces(K;body) j a[var := v]) supposing i ≤ j
          else λi,a. ∃v:Dom(i). (K-uforces(K;body) i a[var := v])
          fi  
          j 
          a)

---

Latex:

---

Latex:

1.  K  :  mKripkeStruct
2.  fmla  :  mFOL()
\mvdash{}  \mforall{}i,j:World.
        (i  \mleq{}  j
        {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                    ((K-uforces(K;fmla)  i  a)  \msubseteq{}r  (K-uforces(K;fmla)  j  a))))


By

---

Latex:
(((InstLemma  `mFOL-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}fmla.\mforall{}i,j:World.
                                                                                  (i  \mleq{}  j
                                                                                  {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                                                                                              ((K-uforces(K;fmla)  i  a)  \msubseteq{}r  (K-uforces(K;fmla)  j 
                                                                                                                                                        a))))\mkleeneclose{}]\mcdot{}
    THENM  (D  -1  With  \mkleeneopen{}fmla\mkleeneclose{}    THEN  Auto)
    )
    THENW  Auto
    )
  THEN  (UnivCD  THENA  Auto)
  THEN  Reduce  0)

---

Home Index