---

Step * 1 1 1 of Lemma K-uforces-monotone

.....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
BY
{ (GenConcl ⌜vars = L ∈ ({z:ℤ| (z ∈ vars)}  List)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  G  :  Type
2.  R  :  G  {}\mrightarrow{}  G  {}\mrightarrow{}  \mBbbP{}
3.  D  :  G  {}\mrightarrow{}  Type
4.  K5  :  i:G  {}\mrightarrow{}  FOStruct(D  i)
5.  K6  :  \mforall{}i,j:G.
                    ((R  i  j)  {}\mRightarrow{}  (((D  i)  \msubseteq{}r  (D  j))  \mwedge{}  (\mforall{}A:Atom.  \mforall{}L:(D  i)  List.    ((K5  i  A  L)  \msubseteq{}r  (K5  j  A  L)))))
6.  K8  :  \mforall{}i:G.  (R  i  i)
7.  K9  :  \mforall{}i,j,k:G.    ((R  i  j)  {}\mRightarrow{}  (R  j  k)  {}\mRightarrow{}  (R  i  k))
8.  fmla  :  mFOL()
9.  name  :  Atom
10.  vars  :  \mBbbZ{}  List
11.  i  :  World
12.  j  :  World
13.  R  i  j
14.  a  :  \{z:\mBbbZ{}|  (z  \mmember{}  remove-repeats(IntDeq;vars))\}    {}\mrightarrow{}  (D  i)
15.  (D  i)  \msubseteq{}r  (D  j)
16.  \mforall{}A:Atom.  \mforall{}L:(D  i)  List.    ((K5  i  A  L)  \msubseteq{}r  (K5  j  A  L))
\mvdash{}  map(a;vars)  \mmember{}  (D  i)  List


By

---

Latex:
(GenConcl  \mkleeneopen{}vars  =  L\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index