---

Step * 11 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. ∀[a,b,c:free-dl-type(X)].  (free-dl-meet(a;free-dl-meet(b;c)) = free-dl-meet(free-dl-meet(a;b);c) ∈ free-dl-type(X))
6. ∀[a,b,c:free-dl-type(X)].  (free-dl-join(a;free-dl-join(b;c)) = free-dl-join(free-dl-join(a;b);c) ∈ free-dl-type(X))
7. ∀[a,b:free-dl-type(X)].  (free-dl-join(a;free-dl-meet(a;b)) = a ∈ free-dl-type(X))
8. ∀[a,b:free-dl-type(X)].  (free-dl-meet(a;free-dl-join(a;b)) = a ∈ free-dl-type(X))
9. ∀[a:free-dl-type(X)]. (free-dl-meet(a;[[]]) = a ∈ free-dl-type(X))
10. ∀[a:free-dl-type(X)]. (free-dl-join(a;[]) = a ∈ free-dl-type(X))
11. X List List ∈ Type
12. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
13. ∀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))))))
14. X List List ∈ Type
15. ∀a1,b1:X List List.  (dlattice-eq(X;a1;b1) ∈ Type)
16. ∀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))))))
17. X List List ∈ Type
18. ∀a2,b2:X List List.  (dlattice-eq(X;a2;b2) ∈ Type)
19. ∀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))))))
20. as : X List List
21. bs : X List List
22. ∀x:X List. ((x ∈ bs) ⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))))
23. ∀x:X List. ((x ∈ as) ⇒ (∃y:X List. ((y ∈ bs) ∧ l_subset(X;y;x))))
24. free-dl-type(X) = free-dl-type(X) ∈ Type
25. a1 : X List List
26. b1 : X List List
27. ∀x:X List. ((x ∈ b1) ⇒ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;x))))
28. ∀x:X List. ((x ∈ a1) ⇒ (∃y:X List. ((y ∈ b1) ∧ l_subset(X;y;x))))
29. free-dl-type(X) = free-dl-type(X) ∈ Type
30. a2 : X List List
31. b2 : X List List
32. ∀x:X List. ((x ∈ b2) ⇒ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;x))))
33. ∀x:X List. ((x ∈ a2) ⇒ (∃y:X List. ((y ∈ b2) ∧ l_subset(X;y;x))))
34. free-dl-type(X) = free-dl-type(X) ∈ Type
35. x : X List
36. u : X List
37. v : X List
38. (u ∈ bs)
39. (v ∈ b2)
40. x = (u @ v) ∈ (X List)
41. y1 : X List
42. (y1 ∈ as)
43. l_subset(X;y1;u)
44. y : X List
45. (y ∈ a2)
46. l_subset(X;y;v)
⊢ ∃y:X List. ((∃u,v:X List. ((u ∈ as) ∧ ((v ∈ a1) ∨ (v ∈ a2)) ∧ (y = (u @ v) ∈ (X List)))) ∧ l_subset(X;y;u @ v))
BY
{ ((D 0 With ⌜y1 @ y⌝  THEN Auto) THEN 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.  \mforall{}[a,b,c:free-dl-type(X)].
          (free-dl-meet(a;free-dl-meet(b;c))  =  free-dl-meet(free-dl-meet(a;b);c))
6.  \mforall{}[a,b,c:free-dl-type(X)].
          (free-dl-join(a;free-dl-join(b;c))  =  free-dl-join(free-dl-join(a;b);c))
7.  \mforall{}[a,b:free-dl-type(X)].    (free-dl-join(a;free-dl-meet(a;b))  =  a)
8.  \mforall{}[a,b:free-dl-type(X)].    (free-dl-meet(a;free-dl-join(a;b))  =  a)
9.  \mforall{}[a:free-dl-type(X)].  (free-dl-meet(a;[[]])  =  a)
10.  \mforall{}[a:free-dl-type(X)].  (free-dl-join(a;[])  =  a)
11.  X  List  List  \mmember{}  Type
12.  \mforall{}as,bs:X  List  List.    (dlattice-eq(X;as;bs)  \mmember{}  Type)
13.  \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))))))
14.  X  List  List  \mmember{}  Type
15.  \mforall{}a1,b1:X  List  List.    (dlattice-eq(X;a1;b1)  \mmember{}  Type)
16.  \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))))))
17.  X  List  List  \mmember{}  Type
18.  \mforall{}a2,b2:X  List  List.    (dlattice-eq(X;a2;b2)  \mmember{}  Type)
19.  \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))))))
20.  as  :  X  List  List
21.  bs  :  X  List  List
22.  \mforall{}x:X  List.  ((x  \mmember{}  bs)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))))
23.  \mforall{}x:X  List.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  bs)  \mwedge{}  l\_subset(X;y;x))))
24.  free-dl-type(X)  =  free-dl-type(X)
25.  a1  :  X  List  List
26.  b1  :  X  List  List
27.  \mforall{}x:X  List.  ((x  \mmember{}  b1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a1)  \mwedge{}  l\_subset(X;y;x))))
28.  \mforall{}x:X  List.  ((x  \mmember{}  a1)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b1)  \mwedge{}  l\_subset(X;y;x))))
29.  free-dl-type(X)  =  free-dl-type(X)
30.  a2  :  X  List  List
31.  b2  :  X  List  List
32.  \mforall{}x:X  List.  ((x  \mmember{}  b2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  a2)  \mwedge{}  l\_subset(X;y;x))))
33.  \mforall{}x:X  List.  ((x  \mmember{}  a2)  {}\mRightarrow{}  (\mexists{}y:X  List.  ((y  \mmember{}  b2)  \mwedge{}  l\_subset(X;y;x))))
34.  free-dl-type(X)  =  free-dl-type(X)
35.  x  :  X  List
36.  u  :  X  List
37.  v  :  X  List
38.  (u  \mmember{}  bs)
39.  (v  \mmember{}  b2)
40.  x  =  (u  @  v)
41.  y1  :  X  List
42.  (y1  \mmember{}  as)
43.  l\_subset(X;y1;u)
44.  y  :  X  List
45.  (y  \mmember{}  a2)
46.  l\_subset(X;y;v)
\mvdash{}  \mexists{}y:X  List
      ((\mexists{}u,v:X  List.  ((u  \mmember{}  as)  \mwedge{}  ((v  \mmember{}  a1)  \mvee{}  (v  \mmember{}  a2))  \mwedge{}  (y  =  (u  @  v))))  \mwedge{}  l\_subset(X;y;u  @  v))


By

---

Latex:
((D  0  With  \mkleeneopen{}y1  @  y\mkleeneclose{}    THEN  Auto)  THEN  BLemma  `l\_subset\_append2`  THEN  Auto)

---

Home Index