Step
*
5
2
2
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;x)
BY
{ ((SubstFor ⌜x⌝ 0⋅ THENA Auto) THEN (SubstFor ⌜v⌝ 0⋅ THENA 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. (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)
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;x)
By
Latex:
((SubstFor \mkleeneopen{}x\mkleeneclose{} 0\mcdot{} THENA Auto) THEN (SubstFor \mkleeneopen{}v\mkleeneclose{} 0\mcdot{} THENA Auto))
Home
Index