---

Step * 1 3 of Lemma K-uforces-monotone


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)
BY
{ ((Assert filter(λx.(¬b(x =z var));mFOL-freevars(body)) ⊆ mFOL-freevars(∀var;body)) BY
          (Unfold `l_contains` 0 THEN RWO "l_all_iff" 0 THEN Auto))
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0) }

1
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))
11. filter(λx.(¬b(x =z var));mFOL-freevars(body)) ⊆ mFOL-freevars(∀var;body))
12. ↑isall
⊢ (∀[j:World]. ∀v:Dom(j). (K-uforces(K;body) j a[var := v]) supposing i ≤ j) ⊆r (∀[j@0:World]
                                                                                   ∀v:Dom(j@0)
                                                                                     (K-uforces(K;body) j@0 
                                                                                      a[var := v]) 
                                                                                   supposing j ≤ j@0)

2
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))
11. filter(λx.(¬b(x =z var));mFOL-freevars(body)) ⊆ mFOL-freevars(∀var;body))
12. ¬↑isall
⊢ (∃v:Dom(i). (K-uforces(K;body) i a[var := v])) ⊆r (∃v:Dom(j). (K-uforces(K;body) j a[var := v]))

---

Latex:

---

Latex:

1.  K  :  mKripkeStruct
2.  fmla  :  mFOL()
3.  isall  :  \mBbbB{}
4.  var  :  \mBbbZ{}
5.  body  :  mFOL()
6.  \mforall{}i,j:World.
          (i  \mleq{}  j
          {}\mRightarrow{}  (\mforall{}a:FOAssignment(mFOL-freevars(body),Dom(i))
                      ((K-uforces(K;body)  i  a)  \msubseteq{}r  (K-uforces(K;body)  j  a))))
7.  i  :  World
8.  j  :  World
9.  i  \mleq{}  j
10.  a  :  FOAssignment(mFOL-freevars(mFOquant(isall;var;body)),Dom(i))
\mvdash{}  (if  isall
      then  \mlambda{}i,a.  \mforall{}[j:World].  \mforall{}v:Dom(j).  (K-uforces(K;body)  j  a[var  :=  v])  supposing  i  \mleq{}  j
      else  \mlambda{}i,a.  \mexists{}v:Dom(i).  (K-uforces(K;body)  i  a[var  :=  v])
      fi   
      i 
      a)  \msubseteq{}r  (if  isall
                    then  \mlambda{}i,a.  \mforall{}[j:World].  \mforall{}v:Dom(j).  (K-uforces(K;body)  j  a[var  :=  v])  supposing  i  \mleq{}  j
                    else  \mlambda{}i,a.  \mexists{}v:Dom(i).  (K-uforces(K;body)  i  a[var  :=  v])
                    fi   
                    j 
                    a)


By

---

Latex:
((Assert  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body))  \msubseteq{}  mFOL-freevars(\mforall{}var;body))  BY
                (Unfold  `l\_contains`  0  THEN  RWO  "l\_all\_iff"  0  THEN  Auto))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0)

---

Home Index