---

Step * 5 2 2 1 of Lemma free-dl_wf


1. X : Type
2. EquivRel(X List List;as,bs.(∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))))
3. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;b) = free-dl-meet(b;a) ∈ free-dl-type(X))
4. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;b) = free-dl-join(b;a) ∈ free-dl-type(X))
5. X List List ∈ Type
6. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
7. ∀as:X List List
     ((∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
     ∧ (∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))))
8. X List List ∈ Type
9. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
10. ∀a1:X List List
      ((∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))))
11. X List List ∈ Type
12. ∀a2,b2:X List List.  (dlattice-eq(X;a2;b2) ∈ Type)
13. ∀a2:X List List
      ((∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x)))))
      ∧ (∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))))
14. as : X List List
15. bs : X List List
16. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
17. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
18. free-dl-type(X) = free-dl-type(X) ∈ Type
19. a1 : X List List
20. b1 : X List List
21. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
22. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
23. free-dl-type(X) = free-dl-type(X) ∈ Type
24. a2 : X List List
25. b2 : X List List
26. ∀x:X List. ((x ∈ b2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))
27. ∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ b2) ∧ l_subset(X;y;x))))
28. free-dl-type(X) = free-dl-type(X) ∈ Type
29. x : X List
30. u : X List
31. v : X List
32. (u ∈ as)
33. u1 : X List
34. v1 : X List
35. (u1 ∈ a1)
36. (v1 ∈ a2)
37. v = (u1 @ v1) ∈ (X List)
38. x = (u @ v) ∈ (X List)
39. y2 : X List
40. (y2 ∈ bs)
41. l_subset(X;y2;u)
42. y1 : X List
43. (y1 ∈ b1)
44. l_subset(X;y1;u1)
45. y : X List
46. (y ∈ b2)
47. l_subset(X;y;v1)
⊢ l_subset(X;y2 @ y1 @ y;u @ u1 @ v1)
BY
{ RepeatFor 2 ((BLemma  `l_subset_append2` THEN Auto)) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  EquivRel(X  List  List;as,bs.(\mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x)))))
\mwedge{}  (\mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  l\_subset(X;y;x))))))
3.  \mforall{}[a,b:free-dl-type(X)].    (free-dl-meet(a;b)  =  free-dl-meet(b;a))
4.  \mforall{}[a,b:free-dl-type(X)].    (free-dl-join(a;b)  =  free-dl-join(b;a))
5.  X  List  List  \mmember{}  Type
6.  \mforall{}as,bs:X  List  List.    (dlattice-eq(X;as;bs)  \mmember{}  Type)
7.  \mforall{}as:X  List  List
          ((\mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x)))))
          \mwedge{}  (\mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))))))
8.  X  List  List  \mmember{}  Type
9.  \mforall{}a1,b1:X  List  List.    (dlattice-eq(X;a1;b1)  \mmember{}  Type)
10.  \mforall{}a1:X  List  List
            ((\mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x)))))
            \mwedge{}  (\mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x))))))
11.  X  List  List  \mmember{}  Type
12.  \mforall{}a2,b2:X  List  List.    (dlattice-eq(X;a2;b2)  \mmember{}  Type)
13.  \mforall{}a2:X  List  List
            ((\mforall{}x:X  List.  ((x  \mmember{}  a2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a2)  \mwedge{}  l\_subset(X;y;x)))))
            \mwedge{}  (\mforall{}x:X  List.  ((x  \mmember{}  a2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a2)  \mwedge{}  l\_subset(X;y;x))))))
14.  as  :  X  List  List
15.  bs  :  X  List  List
16.  \mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))))
17.  \mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  l\_subset(X;y;x))))
18.  free-dl-type(X)  =  free-dl-type(X)
19.  a1  :  X  List  List
20.  b1  :  X  List  List
21.  \mforall{}x:X  List.  ((x  \mmember{}  b1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x))))
22.  \mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b1)  \mwedge{}  l\_subset(X;y;x))))
23.  free-dl-type(X)  =  free-dl-type(X)
24.  a2  :  X  List  List
25.  b2  :  X  List  List
26.  \mforall{}x:X  List.  ((x  \mmember{}  b2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a2)  \mwedge{}  l\_subset(X;y;x))))
27.  \mforall{}x:X  List.  ((x  \mmember{}  a2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b2)  \mwedge{}  l\_subset(X;y;x))))
28.  free-dl-type(X)  =  free-dl-type(X)
29.  x  :  X  List
30.  u  :  X  List
31.  v  :  X  List
32.  (u  \mmember{}  as)
33.  u1  :  X  List
34.  v1  :  X  List
35.  (u1  \mmember{}  a1)
36.  (v1  \mmember{}  a2)
37.  v  =  (u1  @  v1)
38.  x  =  (u  @  v)
39.  y2  :  X  List
40.  (y2  \mmember{}  bs)
41.  l\_subset(X;y2;u)
42.  y1  :  X  List
43.  (y1  \mmember{}  b1)
44.  l\_subset(X;y1;u1)
45.  y  :  X  List
46.  (y  \mmember{}  b2)
47.  l\_subset(X;y;v1)
\mvdash{}  l\_subset(X;y2  @  y1  @  y;u  @  u1  @  v1)


By

---

Latex:
RepeatFor  2  ((BLemma    `l\_subset\_append2`  THEN  Auto))

---

Home Index