---

Step * 1 1 of Lemma K-uforces-monotone


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)
BY
{ (DKripke 1
   THEN All (RepUR ``K-sat K-le K-dom mFOL-abstract K-struct AbstractFOAtomic 
                 FOSatWith mFOL-freevars FOAssignment``)⋅
   THEN ExRepD
   THEN (InstHyp [⌜i⌝;⌜j⌝] 5⋅ THENA Auto)
   THEN D -1
   THEN InstHyp [⌜name⌝;⌜map(a;vars)⌝] (-1)⋅
   THEN Try (Complete (Auto))) }

1
.....wf..... 
1. G : Type
2. R : G ⟶ G ⟶ ℙ
3. D : G ⟶ Type
4. K5 : i:G ⟶ FOStruct(D i)
5. K6 : ∀i,j:G.  ((R i j) ⇒ (((D i) ⊆r (D j)) ∧ (∀A:Atom. ∀L:(D i) List.  ((K5 i A L) ⊆r (K5 j A L)))))
6. K8 : ∀i:G. (R i i)
7. K9 : ∀i,j,k:G.  ((R i j) ⇒ (R j k) ⇒ (R i k))
8. fmla : mFOL()
9. name : Atom
10. vars : ℤ List
11. i : World
12. j : World
13. R i j
14. a : {z:ℤ| (z ∈ remove-repeats(IntDeq;vars))}  ⟶ (D i)
15. (D i) ⊆r (D j)
16. ∀A:Atom. ∀L:(D i) List.  ((K5 i A L) ⊆r (K5 j A L))
⊢ map(a;vars) ∈ (D i) List

---

Latex:

---

Latex:

1.  K  :  mKripkeStruct
2.  fmla  :  mFOL()
3.  name  :  Atom
4.  vars  :  \mBbbZ{}  List
5.  i  :  World
6.  j  :  World
7.  i  \mleq{}  j
8.  a  :  FOAssignment(mFOL-freevars(name(vars)),Dom(i))
\mvdash{}  i,a  |=  name(vars)  \msubseteq{}r  j,a  |=  name(vars)


By

---

Latex:
(DKripke  1
  THEN  All  (RepUR  ``K-sat  K-le  K-dom  mFOL-abstract  K-struct  AbstractFOAtomic 
                              FOSatWith  mFOL-freevars  FOAssignment``)\mcdot{}
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  InstHyp  [\mkleeneopen{}name\mkleeneclose{};\mkleeneopen{}map(a;vars)\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Try  (Complete  (Auto)))

---

Home Index