---

Step * of Lemma fl-filter-decomp

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:Point(face-lattice(T;eq))].
∀[Q:{x:fset(T + T)| ↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))}  ⟶ 𝔹].
  (s = fl-filter(s;x.Q[x]) ∨ fl-filter(s;x.¬bQ[x]) ∈ Point(face-lattice(T;eq)))
BY
{ (RepeatFor 2 (Intro)
   THEN (InstLemma `cal-filter-decomp` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;
         ⌜λ2s.fset-contains-none(union-deq(T;T;eq;eq);s;x.face-lattice-constraints(x))⌝]⋅
         THENA Auto
         )
   THEN (Subst' constrained-antichain-lattice(T + T;union-deq(T;T;eq;
                                                              eq);λ2s.fset-contains-none(union-deq(T;T;eq;
                                                                                                   eq);s;x....)) 
         ~ face-lattice(T;eq) -1
         THENA (All (RepUR ``so_lambda face-lattice free-dist-lattice-with-constraints fl-filter``) THEN Auto)
         )
   THEN Fold `fl-filter` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[s:Point(face-lattice(T;eq))].
\mforall{}[Q:\{x:fset(T  +  T)|  \muparrow{}fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))\} 
        {}\mrightarrow{}  \mBbbB{}].
    (s  =  fl-filter(s;x.Q[x])  \mvee{}  fl-filter(s;x.\mneg{}\msubb{}Q[x]))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (InstLemma  `cal-filter-decomp`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}s.fset-contains-none(union-deq(T;T;eq;eq);s;x.face-lattice-constraints(x))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (Subst'  constrained-antichain-lattice(T  +  T;union-deq(T;T;eq;
                                                                                                                        eq);\mlambda{}\msubtwo{}s....)  \msim{}  face-lattice(T;eq)  -1
              THENA  (All  (RepUR  ``so\_lambda  face-lattice  free-dist-lattice-with-constraints  fl-filter``)
                            THEN  Auto
                            )
              )
  THEN  Fold  `fl-filter`  (-1)
  THEN  Trivial)

---

Home Index