---

Step * 3 1 of Lemma free-dl_wf

.....antecedent..... 
1. X : Type
2. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
3. X List List ∈ Type
4. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
5. ∀as:X List List. dlattice-eq(X;as;as)
6. X List List ∈ Type
7. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
8. ∀a1:X List List. dlattice-eq(X;a1;a1)
9. as : X List List
10. bs : X List List
11. dlattice-eq(X;as;bs)
12. free-dl-type(X) = free-dl-type(X) ∈ Type
13. a1 : X List List
14. b1 : X List List
15. dlattice-eq(X;a1;b1)
16. free-dl-type(X) = free-dl-type(X) ∈ Type
⊢ dlattice-eq(X;free-dl-meet(as;a1);free-dl-meet(b1;bs))
BY
{ (Thin (-1)
   THEN Lemmaize [11;15]
   THEN Unfold `dlattice-eq` 0
   THEN RepeatFor 5 (Intro)
   THEN (RWO  "dlattice-order-iff" 0 THENA Auto)
   THEN (RWO "member-free-dl-meet" 0 THEN Auto)
   THEN ExRepD) }

1
1. X : Type
2. as : X List List
3. bs : X List List
4. a1 : X List List
5. b1 : X List List
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. x : X List
11. u : X List
12. v : X List
13. (u ∈ b1)
14. (v ∈ bs)
15. x = (u @ v) ∈ (X List)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))

2
1. X : Type
2. as : X List List
3. bs : X List List
4. a1 : X List List
5. b1 : X List List
6. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
7. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
8. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
9. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
10. ∀x:X List
      ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
      ⇒ (∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ (v ∈ a1) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))))
11. x : X List
12. u : X List
13. v : X List
14. (u ∈ as)
15. (v ∈ a1)
16. x = (u @ v) ∈ (X List)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ b1) ∧ (v ∈ bs) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;x))

---

Latex:

---

Latex:
.....antecedent..... 
1.  X  :  Type
2.  EquivRel(X  List  List;as,bs.dlattice-eq(X;as;bs))
3.  X  List  List  \mmember{}  Type
4.  \mforall{}as,bs:X  List  List.    (dlattice-eq(X;as;bs)  \mmember{}  Type)
5.  \mforall{}as:X  List  List.  dlattice-eq(X;as;as)
6.  X  List  List  \mmember{}  Type
7.  \mforall{}a1,b1:X  List  List.    (dlattice-eq(X;a1;b1)  \mmember{}  Type)
8.  \mforall{}a1:X  List  List.  dlattice-eq(X;a1;a1)
9.  as  :  X  List  List
10.  bs  :  X  List  List
11.  dlattice-eq(X;as;bs)
12.  free-dl-type(X)  =  free-dl-type(X)
13.  a1  :  X  List  List
14.  b1  :  X  List  List
15.  dlattice-eq(X;a1;b1)
16.  free-dl-type(X)  =  free-dl-type(X)
\mvdash{}  dlattice-eq(X;free-dl-meet(as;a1);free-dl-meet(b1;bs))


By

---

Latex:
(Thin  (-1)
  THEN  Lemmaize  [11;15]
  THEN  Unfold  `dlattice-eq`  0
  THEN  RepeatFor  5  (Intro)
  THEN  (RWO    "dlattice-order-iff"  0  THENA  Auto)
  THEN  (RWO  "member-free-dl-meet"  0  THEN  Auto)
  THEN  ExRepD)

---

Home Index