---

Step * 1 of Lemma K-uforces-umonotone


1. K : mKripkeStruct
2. fmla : mFOL()
⊢ ∀i:World
    ∀[j:World]
      ∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a)) supposing i ≤ j
BY
{ (((InstLemma `mFOL-induction` [⌜λ2fmla.∀i:World
                                           ∀[j:World]
                                             ∀a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                                               ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a)) 
                                             supposing i ≤ j⌝]⋅
    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:World
     ∀[j:World]
       ∀a:FOAssignment(mFOL-freevars(left),Dom(i)). ((K-uforces(K;left) i a) ⊆r (K-uforces(K;left) j a)) supposing i ≤ j
7. ∀i:World
     ∀[j:World]
       ∀a:FOAssignment(mFOL-freevars(right),Dom(i)). ((K-uforces(K;right) i a) ⊆r (K-uforces(K;right) j a)) 
       supposing i ≤ j
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:World
     ∀[j:World]
       ∀a:FOAssignment(mFOL-freevars(body),Dom(i)). ((K-uforces(K;body) i a) ⊆r (K-uforces(K;body) j a)) supposing i ≤ j
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:World
        \mforall{}[j:World]
            \mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom(i))
                ((K-uforces(K;fmla)  i  a)  \msubseteq{}r  (K-uforces(K;fmla)  j  a)) 
            supposing  i  \mleq{}  j


By

---

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

---

Home Index