Step
*
11
4
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 ∈ as)
39. (v ∈ a2)
40. x = (u @ v) ∈ (X List)
41. y1 : X List
42. (y1 ∈ bs)
43. l_subset(X;y1;u)
44. y : X List
45. (y ∈ b2)
46. l_subset(X;y;v)
⊢ ∃y:X List
(((∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b1) ∧ (y = (u @ v) ∈ (X List))))
∨ (∃u,v:X List. ((u ∈ bs) ∧ (v ∈ b2) ∧ (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{} as)
39. (v \mmember{} a2)
40. x = (u @ v)
41. y1 : X List
42. (y1 \mmember{} bs)
43. l\_subset(X;y1;u)
44. y : X List
45. (y \mmember{} b2)
46. l\_subset(X;y;v)
\mvdash{} \mexists{}y:X List
(((\mexists{}u,v:X List. ((u \mmember{} bs) \mwedge{} (v \mmember{} b1) \mwedge{} (y = (u @ v))))
\mvee{} (\mexists{}u,v:X List. ((u \mmember{} bs) \mwedge{} (v \mmember{} b2) \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