---

Step * 2 1 1 1 2 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]
= 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 ∨ accumulate (with value b and list item x):
         b ∧ f x
        over list:
          u
        with starting value:
         1))
∈ Point(L)
BY
{ (RWO "-2<" 0 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)
⊢ 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]
=  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  \mvee{}  accumulate  (with  value  b  and  list  item  x):
                  b  \mwedge{}  f  x
                over  list:
                    u
                with  starting  value:
                  1))


By

---

Latex:
(RWO  "-2<"  0  THEN  Auto)

---

Home Index