---

Step * 2 1 1 1 2 1 1 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)
11. ∀[a,b,c:Point(L)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(L))
⊢ 0 ∨ accumulate (with value b and list item x):
       b ∧ f x
      over list:
        u
      with starting value:
       1) ∨ fdl-hom(L;f) v
= 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
{ (GenConcl ⌜accumulate (with value b and list item x): b ∧ f xover list:  uwith starting value: 1) = uu ∈ Point(L)⌝⋅
   THENA 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))
12. uu : Point(L)
13. accumulate (with value b and list item x): b ∧ f xover list:  uwith starting value: 1) = uu ∈ Point(L)
⊢ 0 ∨ uu ∨ fdl-hom(L;f) v = uu ∨ 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)
11.  \mforall{}[a,b,c:Point(L)].    (a  \mvee{}  b  \mvee{}  c  =  a  \mvee{}  b  \mvee{}  c)
\mvdash{}  0  \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
=  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:
(GenConcl  \mkleeneopen{}accumulate  (with  value  b  and  list  item  x):
                        b  \mwedge{}  f  x
                      over  list:
                          u
                      with  starting  value:
                        1)
                      =  uu\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index