---

Step * 2 2 2 1 1 1 1 1 1 2 1 2 1 1 1 2 1 2 1 1 1 of Lemma fdl-hom_wf

.....equality..... 
1. X : Type
2. L : BoundedDistributiveLattice
3. f : X ⟶ Point(L)
4. fdl-hom(L;f) ∈ free-dl-type(X) ⟶ Point(L)
5. (fdl-hom(L;f) 0) = 0 ∈ Point(L)
6. (fdl-hom(L;f) 1) = 1 ∈ Point(L)
7. ∀as,bs:X List List.  (fdl-hom(L;f) as ∨ fdl-hom(L;f) bs = (fdl-hom(L;f) as ∨ bs) ∈ Point(L))
8. ys : X List List
9. y : X List
10. ∀bs:X List List. (fdl-hom(L;f) ys ∧ fdl-hom(L;f) bs = (fdl-hom(L;f) free-dl-meet(ys;bs)) ∈ Point(L))
11. u : X List
12. v : X List List
13. (fdl-hom(L;f) map(λb.(y @ b);v)) = fdl-hom(L;f) [y] ∧ fdl-hom(L;f) v ∈ Point(L)
14. ∀a:X List. ∀as:X List List.  ((fdl-hom(L;f) [a / as]) = fdl-hom(L;f) [a] ∨ fdl-hom(L;f) as ∈ Point(L))
⊢ (fdl-hom(L;f) [y @ u]) = fdl-hom(L;f) [y] ∧ fdl-hom(L;f) [u] ∈ Point(L)
BY
{ (RepUR ``fdl-hom`` 0
   THEN (RWO "lattice-join-0.1" 0 THENA Auto)
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN (GenConcl 
         ⌜accumulate (with value b and list item x): b ∧ f xover list:  ywith starting value: 1) = a ∈ Point(L)⌝⋅
         THENA Auto
         )) }

1
1. X : Type
2. L : BoundedDistributiveLattice
3. f : X ⟶ Point(L)
4. fdl-hom(L;f) ∈ free-dl-type(X) ⟶ Point(L)
5. (fdl-hom(L;f) 0) = 0 ∈ Point(L)
6. (fdl-hom(L;f) 1) = 1 ∈ Point(L)
7. ∀as,bs:X List List.  (fdl-hom(L;f) as ∨ fdl-hom(L;f) bs = (fdl-hom(L;f) as ∨ bs) ∈ Point(L))
8. ys : X List List
9. y : X List
10. ∀bs:X List List. (fdl-hom(L;f) ys ∧ fdl-hom(L;f) bs = (fdl-hom(L;f) free-dl-meet(ys;bs)) ∈ Point(L))
11. u : X List
12. v : X List List
13. (fdl-hom(L;f) map(λb.(y @ b);v)) = fdl-hom(L;f) [y] ∧ fdl-hom(L;f) v ∈ Point(L)
14. ∀a:X List. ∀as:X List List.  ((fdl-hom(L;f) [a / as]) = fdl-hom(L;f) [a] ∨ fdl-hom(L;f) as ∈ Point(L))
15. a : Point(L)
16. accumulate (with value b and list item x): b ∧ f xover list:  ywith starting value: 1) = a ∈ Point(L)
⊢ accumulate (with value b and list item x):
   b ∧ f x
  over list:
    u
  with starting value:
   a)
= a ∧ accumulate (with value b and list item x):
       b ∧ f x
      over list:
        u
      with starting value:
       1)
∈ Point(L)

---

Latex:

---

Latex:
.....equality..... 
1.  X  :  Type
2.  L  :  BoundedDistributiveLattice
3.  f  :  X  {}\mrightarrow{}  Point(L)
4.  fdl-hom(L;f)  \mmember{}  free-dl-type(X)  {}\mrightarrow{}  Point(L)
5.  (fdl-hom(L;f)  0)  =  0
6.  (fdl-hom(L;f)  1)  =  1
7.  \mforall{}as,bs:X  List  List.    (fdl-hom(L;f)  as  \mvee{}  fdl-hom(L;f)  bs  =  (fdl-hom(L;f)  as  \mvee{}  bs))
8.  ys  :  X  List  List
9.  y  :  X  List
10.  \mforall{}bs:X  List  List.  (fdl-hom(L;f)  ys  \mwedge{}  fdl-hom(L;f)  bs  =  (fdl-hom(L;f)  free-dl-meet(ys;bs)))
11.  u  :  X  List
12.  v  :  X  List  List
13.  (fdl-hom(L;f)  map(\mlambda{}b.(y  @  b);v))  =  fdl-hom(L;f)  [y]  \mwedge{}  fdl-hom(L;f)  v
14.  \mforall{}a:X  List.  \mforall{}as:X  List  List.    ((fdl-hom(L;f)  [a  /  as])  =  fdl-hom(L;f)  [a]  \mvee{}  fdl-hom(L;f)  as)
\mvdash{}  (fdl-hom(L;f)  [y  @  u])  =  fdl-hom(L;f)  [y]  \mwedge{}  fdl-hom(L;f)  [u]


By

---

Latex:
(RepUR  ``fdl-hom``  0
  THEN  (RWO  "lattice-join-0.1"  0  THENA  Auto)
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}accumulate  (with  value  b  and  list  item  x):
                                    b  \mwedge{}  f  x
                                  over  list:
                                      y
                                  with  starting  value:
                                    1)
                                  =  a\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index