---

Step * 1 3 1 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))
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)
BY
{ ((D 0 THENA Auto)
   THEN (Unfolds ``uall uimplies`` (-1) THEN Unfolds ``uall uimplies`` 0)
   THEN RepeatFor 2 ((MemTypeCD THENA Auto))
   THEN (D -3 With ⌜j@0⌝  THENA Auto)
   THEN (InstLemma `K-le_transitivity` [⌜K⌝;⌜i⌝;⌜j⌝;⌜j@0⌝]⋅ THENA Auto)
   THEN RenameVar `p' (-1)
   THEN D -3 With ⌜p⌝ 
   THEN Auto) }

---

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))
11.  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  var));mFOL-freevars(body))  \msubseteq{}  mFOL-freevars(\mforall{}var;body))
12.  \muparrow{}isall
\mvdash{}  (\mforall{}[j:World].  \mforall{}v:Dom(j).  (K-uforces(K;body)  j  a[var  :=  v])  supposing  i  \mleq{}  j)
        \msubseteq{}r  (\mforall{}[j@0:World].  \mforall{}v:Dom(j@0).  (K-uforces(K;body)  j@0  a[var  :=  v])  supposing  j  \mleq{}  j@0)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Unfolds  ``uall  uimplies``  (-1)  THEN  Unfolds  ``uall  uimplies``  0)
  THEN  RepeatFor  2  ((MemTypeCD  THENA  Auto))
  THEN  (D  -3  With  \mkleeneopen{}j@0\mkleeneclose{}    THENA  Auto)
  THEN  (InstLemma  `K-le\_transitivity`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}j@0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RenameVar  `p'  (-1)
  THEN  D  -3  With  \mkleeneopen{}p\mkleeneclose{} 
  THEN  Auto)

---

Home Index