---

Step * 1 1 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. y1 : X List
21. (f [y1]) = (g [y1]) ∈ Point(L)
22. y : X
⊢ (f [y1 @ [y]]) = (g [y1 @ [y]]) ∈ Point(L)
BY
{ (Subst' [y1 @ [y]] ~ [y1] ∧ free-dl-generator(y) 0
   THENA (RW  (SubC (TagC (mk_tag_term 100))) 0
          THEN Reduce 0
          THEN EqCD
          THEN Try (Trivial)
          THEN RW  (SubC (TagC (mk_tag_term 100))) 0
          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. y1 : X List
21. (f [y1]) = (g [y1]) ∈ Point(L)
22. y : X
⊢ (f [y1] ∧ free-dl-generator(y)) = (g [y1] ∧ free-dl-generator(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.  y1  :  X  List
21.  (f  [y1])  =  (g  [y1])
22.  y  :  X
\mvdash{}  (f  [y1  @  [y]])  =  (g  [y1  @  [y]])


By

---

Latex:
(Subst'  [y1  @  [y]]  \msim{}  [y1]  \mwedge{}  free-dl-generator(y)  0
  THENA  (RW    (SubC  (TagC  (mk\_tag\_term  100)))  0
                THEN  Reduce  0
                THEN  EqCD
                THEN  Try  (Trivial)
                THEN  RW    (SubC  (TagC  (mk\_tag\_term  100)))  0
                THEN  Auto)
  )

---

Home Index