---

Step * 1 1 of Lemma free-dl-generators


1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. X List List ∈ Type
15. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
16. ∀as:X List List. dlattice-eq(X;as;as)
17. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
18. as : X List List
⊢ (f as) = (g as) ∈ Point(L)
BY
{ (MoveToConcl (-1) THEN BLemma `accum_induction` THEN Auto) }

1
1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. X List List ∈ Type
15. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
16. ∀as:X List List. dlattice-eq(X;as;as)
17. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
18. ys : X List List
19. (f ys) = (g ys) ∈ Point(L)
20. y : X List
⊢ (f (ys @ [y])) = (g (ys @ [y])) ∈ Point(L)

2
1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. X List List ∈ Type
15. ∀as,bs:X List List.  (dlattice-eq(X;as;bs) ∈ Type)
16. ∀as:X List List. dlattice-eq(X;as;as)
17. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
⊢ (f []) = (g []) ∈ Point(L)

---

Latex:

---

Latex:

1.  X  :  Type
2.  free-dl-type(X)  \msim{}  free-dl-type(X)
3.  free-dl-type(X)  =  free-dl-type(X)
4.  L  :  BoundedDistributiveLattice
5.  f  :  free-dl-type(X)  {}\mrightarrow{}  Point(L)
6.  \mforall{}[a,b:free-dl-type(X)].    ((f  a  \mwedge{}  f  b  =  (f  a  \mwedge{}  b))  \mwedge{}  (f  a  \mvee{}  f  b  =  (f  a  \mvee{}  b)))
7.  (f  0)  =  0
8.  (f  1)  =  1
9.  g  :  free-dl-type(X)  {}\mrightarrow{}  Point(L)
10.  \mforall{}[a,b:free-dl-type(X)].    ((g  a  \mwedge{}  g  b  =  (g  a  \mwedge{}  b))  \mwedge{}  (g  a  \mvee{}  g  b  =  (g  a  \mvee{}  b)))
11.  (g  0)  =  0
12.  (g  1)  =  1
13.  \mforall{}x:X.  ((f  free-dl-generator(x))  =  (g  free-dl-generator(x)))
14.  X  List  List  \mmember{}  Type
15.  \mforall{}as,bs:X  List  List.    (dlattice-eq(X;as;bs)  \mmember{}  Type)
16.  \mforall{}as:X  List  List.  dlattice-eq(X;as;as)
17.  EquivRel(X  List  List;as,bs.dlattice-eq(X;as;bs))
18.  as  :  X  List  List
\mvdash{}  (f  as)  =  (g  as)


By

---

Latex:
(MoveToConcl  (-1)  THEN  BLemma  `accum\_induction`  THEN  Auto)

---

Home Index