---

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


1. X : Type
2. L : BoundedDistributiveLattice
3. f : X ⟶ Point(L)
4. (fdl-hom(L;f) 0) = 0 ∈ Point(L)
5. (fdl-hom(L;f) 1) = 1 ∈ Point(L)
6. as : X List List
7. u : X List
8. v : X List List
9. ∀aa:Point(L)
     (aa ∨ fdl-hom(L;f) v
     = accumulate (with value a and list item xs):
        a ∨ accumulate (with value b and list item x):
             b ∧ f x
            over list:
              xs
            with starting value:
             1)
       over list:
         v
       with starting value:
        aa)
     ∈ Point(L))
10. aa : Point(L)
⊢ aa ∨ fdl-hom(L;f) [u / v]
= aa ∨ accumulate (with value b and list item x):
        b ∧ f x
       over list:
         u
       with starting value:
        1) ∨ fdl-hom(L;f) v
∈ Point(L)
BY
{ (Assert ∀[a,b,c:Point(L)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(L)) BY
         (InstLemma `lattice_properties` [⌜L⌝]⋅ THEN Auto)) }

1
1. X : Type
2. L : BoundedDistributiveLattice
3. f : X ⟶ Point(L)
4. (fdl-hom(L;f) 0) = 0 ∈ Point(L)
5. (fdl-hom(L;f) 1) = 1 ∈ Point(L)
6. as : X List List
7. u : X List
8. v : X List List
9. ∀aa:Point(L)
     (aa ∨ fdl-hom(L;f) v
     = accumulate (with value a and list item xs):
        a ∨ accumulate (with value b and list item x):
             b ∧ f x
            over list:
              xs
            with starting value:
             1)
       over list:
         v
       with starting value:
        aa)
     ∈ Point(L))
10. aa : Point(L)
11. ∀[a,b,c:Point(L)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(L))
⊢ aa ∨ fdl-hom(L;f) [u / v]
= aa ∨ accumulate (with value b and list item x):
        b ∧ f x
       over list:
         u
       with starting value:
        1) ∨ fdl-hom(L;f) v
∈ Point(L)

---

Latex:

---

Latex:

1.  X  :  Type
2.  L  :  BoundedDistributiveLattice
3.  f  :  X  {}\mrightarrow{}  Point(L)
4.  (fdl-hom(L;f)  0)  =  0
5.  (fdl-hom(L;f)  1)  =  1
6.  as  :  X  List  List
7.  u  :  X  List
8.  v  :  X  List  List
9.  \mforall{}aa:Point(L)
          (aa  \mvee{}  fdl-hom(L;f)  v
          =  accumulate  (with  value  a  and  list  item  xs):
                a  \mvee{}  accumulate  (with  value  b  and  list  item  x):
                          b  \mwedge{}  f  x
                        over  list:
                            xs
                        with  starting  value:
                          1)
              over  list:
                  v
              with  starting  value:
                aa))
10.  aa  :  Point(L)
\mvdash{}  aa  \mvee{}  fdl-hom(L;f)  [u  /  v]
=  aa  \mvee{}  accumulate  (with  value  b  and  list  item  x):
                b  \mwedge{}  f  x
              over  list:
                  u
              with  starting  value:
                1)  \mvee{}  fdl-hom(L;f)  v


By

---

Latex:
(Assert  \mforall{}[a,b,c:Point(L)].    (a  \mvee{}  b  \mvee{}  c  =  a  \mvee{}  b  \mvee{}  c)  BY
              (InstLemma  `lattice\_properties`  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index