---

Step * 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)) ∧ ((fdl-hom(L;f) 1) = 1 ∈ Point(L))
5. as : X List List
6. bs : X List List
7. aa : Point(L)
8. (fdl-hom(L;f) as) = aa ∈ Point(L)
⊢ aa ∨ fdl-hom(L;f) bs
= 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:
    bs
  with starting value:
   aa)
∈ Point(L)
BY
{ (Thin (-1) THEN MoveToConcl (-1) THEN ListInd (-1) THEN Reduce 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. aa : Point(L)
⊢ aa ∨ fdl-hom(L;f) [] = aa ∈ Point(L)

2
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)

---

Latex:

---

Latex:

1.  X  :  Type
2.  L  :  BoundedDistributiveLattice
3.  f  :  X  {}\mrightarrow{}  Point(L)
4.  ((fdl-hom(L;f)  0)  =  0)  \mwedge{}  ((fdl-hom(L;f)  1)  =  1)
5.  as  :  X  List  List
6.  bs  :  X  List  List
7.  aa  :  Point(L)
8.  (fdl-hom(L;f)  as)  =  aa
\mvdash{}  aa  \mvee{}  fdl-hom(L;f)  bs
=  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:
        bs
    with  starting  value:
      aa)


By

---

Latex:
(Thin  (-1)  THEN  MoveToConcl  (-1)  THEN  ListInd  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index