---

Step * 2 1 1 1 2 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))
⊢ 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
{ ((RWO "-1<" 0 THENA Auto)
   THEN EqCDA
   THEN (RW  (AddrC [2] (UnfoldC `fdl-hom`)) 0 THEN Reduce 0)
   THEN (RWO  "-3<" 0 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))
⊢ 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)

---

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{}  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:
((RWO  "-1<"  0  THENA  Auto)
  THEN  EqCDA
  THEN  (RW    (AddrC  [2]  (UnfoldC  `fdl-hom`))  0  THEN  Reduce  0)
  THEN  (RWO    "-3<"  0  THENA  Auto))

---

Home Index