---

Step * 1 1 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. ys : X List List
19. (f ys) = (g ys) ∈ Point(L)
20. y : X List
⊢ (f ys ∨ [y]) = (g ys ∨ [y]) ∈ Point(L)
BY
{ ((RWO "6.2< 10.2<" 0 THEN Auto) THEN EqCD THEN Auto) }

1
.....subterm..... T:t
3:n
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 [y]) = (g [y]) ∈ 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.  ys  :  X  List  List
19.  (f  ys)  =  (g  ys)
20.  y  :  X  List
\mvdash{}  (f  ys  \mvee{}  [y])  =  (g  ys  \mvee{}  [y])


By

---

Latex:
((RWO  "6.2<  10.2<"  0  THEN  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index