---

Step * 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)) ∧ ((fdl-hom(L;f) 1) = 1 ∈ Point(L))
5. as : X List List
6. bs : X List List
⊢ fdl-hom(L;f) as ∨ fdl-hom(L;f) bs = (fdl-hom(L;f) (as @ bs)) ∈ Point(L)
BY
{ ((Subst' fdl-hom(L;f) (as @ 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:
                                     fdl-hom(L;f) as) 0
    THENA (RepUR ``fdl-hom`` 0 THEN RWO "list_accum_append" 0 THEN Auto)
    )
   THEN (GenConcl ⌜(fdl-hom(L;f) as) = aa ∈ 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)) ∧ ((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)

---

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
\mvdash{}  fdl-hom(L;f)  as  \mvee{}  fdl-hom(L;f)  bs  =  (fdl-hom(L;f)  (as  @  bs))


By

---

Latex:
((Subst'  fdl-hom(L;f)  (as  @  bs)  \msim{}  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:
                                                                      fdl-hom(L;f)  as)  0
    THENA  (RepUR  ``fdl-hom``  0  THEN  RWO  "list\_accum\_append"  0  THEN  Auto)
    )
  THEN  (GenConcl  \mkleeneopen{}(fdl-hom(L;f)  as)  =  aa\mkleeneclose{}\mcdot{}  THENA  Auto)
  )

---

Home Index