Step
*
5
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. u1 : X List
33. v1 : X List
34. (u1 ∈ bs)
35. (v1 ∈ b1)
36. u = (u1 @ v1) ∈ (X List)
37. (v ∈ b2)
38. x = (u @ v) ∈ (X List)
⊢ ∃y:X List
((∃u,v:X List
((u ∈ as) ∧ (∃u,v1:X List. ((u ∈ a1) ∧ (v1 ∈ a2) ∧ (v = (u @ v1) ∈ (X List)))) ∧ (y = (u @ v) ∈ (X List))))
∧ l_subset(X;y;x))
BY
{ ((Assert (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;u1)))
∧ (∃y:X List. ((y ∈ a1) ∧ l_subset(X;y;v1)))
∧ (∃y:X List. ((y ∈ a2) ∧ l_subset(X;y;v))) BY
Auto)
THEN ExRepD
THEN (D 0 With ⌜y2 @ y1 @ y⌝ THENW Auto)) }
1
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. u1 : X List
33. v1 : X List
34. (u1 ∈ bs)
35. (v1 ∈ b1)
36. u = (u1 @ v1) ∈ (X List)
37. (v ∈ b2)
38. x = (u @ v) ∈ (X List)
39. y2 : X List
40. (y2 ∈ as)
41. l_subset(X;y2;u1)
42. y1 : X List
43. (y1 ∈ a1)
44. l_subset(X;y1;v1)
45. y : X List
46. (y ∈ a2)
47. l_subset(X;y;v)
⊢ (∃u,v:X List
((u ∈ as)
∧ (∃u,v1:X List. ((u ∈ a1) ∧ (v1 ∈ a2) ∧ (v = (u @ v1) ∈ (X List))))
∧ ((y2 @ y1 @ y) = (u @ v) ∈ (X List))))
∧ l_subset(X;y2 @ y1 @ y;x)
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. u1 : X List
33. v1 : X List
34. (u1 \mmember{} bs)
35. (v1 \mmember{} b1)
36. u = (u1 @ v1)
37. (v \mmember{} b2)
38. x = (u @ v)
\mvdash{} \mexists{}y:X List
((\mexists{}u,v:X List
((u \mmember{} as) \mwedge{} (\mexists{}u,v1:X List. ((u \mmember{} a1) \mwedge{} (v1 \mmember{} a2) \mwedge{} (v = (u @ v1)))) \mwedge{} (y = (u @ v))))
\mwedge{} l\_subset(X;y;x))
By
Latex:
((Assert (\mexists{}y:X List. ((y \mmember{} as) \mwedge{} l\_subset(X;y;u1)))
\mwedge{} (\mexists{}y:X List. ((y \mmember{} a1) \mwedge{} l\_subset(X;y;v1)))
\mwedge{} (\mexists{}y:X List. ((y \mmember{} a2) \mwedge{} l\_subset(X;y;v))) BY
Auto)
THEN ExRepD
THEN (D 0 With \mkleeneopen{}y2 @ y1 @ y\mkleeneclose{} THENW Auto))
Home
Index