---

Step * of Lemma cal-filter-decomp

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)| 
                                                                                                          ↑P[x]}  ⟶ 𝔹].
  (s = cal-filter(s;x.Q[x]) ∨ cal-filter(s;x.¬bQ[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))
BY
{ (RepeatFor 3 ((Intro THENA Auto))
   THEN (RWO "cal-point" 0 THENA Auto)
   THEN Auto
   THEN (Assert cal-filter(s;x.Q[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)) BY
               (Auto THEN RWO "cal-point" 0 THEN Auto))
   THEN (Assert cal-filter(s;x.¬bQ[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)) BY
               (Auto THEN RWO "cal-point" 0 THEN Auto))
   THEN (All (RWO "cal-point") THENA Auto)
   THEN (InstLemma `fset-constrained-ac-lub-is-lub` 
         [⌜T⌝;⌜eq⌝;⌜P⌝;⌜cal-filter(s;x.Q[x])⌝;⌜cal-filter(s;x.¬bQ[x])⌝]⋅
         THENA Auto
         )
   THEN RepUR ``lattice-join lattice-point constrained-antichain-lattice`` 0
   THEN RepUR ``mk-bounded-distributive-lattice mk-bounded-lattice`` 0
   THEN DVar `s'
   THEN EqTypeCD
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. s : fset(fset(T))
5. ↑fset-antichain(eq;s)
6. fset-all(s;a.P a)
7. Q : {x:fset(T)| ↑P[x]}  ⟶ 𝔹
8. cal-filter(s;x.Q[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} 
9. cal-filter(s;x.¬bQ[x]) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} 
10. least-upper-bound({ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ;ac1,ac2.fset-ac-le(eq;ac1;ac2)\000C;
                      cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x]);lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x])))
⊢ s = lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.¬bQ[x])) ∈ fset(fset(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:Point(constrained-antichain-lattice(T;eq;P))].
\mforall{}[Q:\{x:fset(T)|  \muparrow{}P[x]\}    {}\mrightarrow{}  \mBbbB{}].
    (s  =  cal-filter(s;x.Q[x])  \mvee{}  cal-filter(s;x.\mneg{}\msubb{}Q[x]))


By

---

Latex:
(RepeatFor  3  ((Intro  THENA  Auto))
  THEN  (RWO  "cal-point"  0  THENA  Auto)
  THEN  Auto
  THEN  (Assert  cal-filter(s;x.Q[x])  \mmember{}  Point(constrained-antichain-lattice(T;eq;P))  BY
                          (Auto  THEN  RWO  "cal-point"  0  THEN  Auto))
  THEN  (Assert  cal-filter(s;x.\mneg{}\msubb{}Q[x])  \mmember{}  Point(constrained-antichain-lattice(T;eq;P))  BY
                          (Auto  THEN  RWO  "cal-point"  0  THEN  Auto))
  THEN  (All  (RWO  "cal-point")  THENA  Auto)
  THEN  (InstLemma  `fset-constrained-ac-lub-is-lub` 
              [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}cal-filter(s;x.Q[x])\mkleeneclose{};\mkleeneopen{}cal-filter(s;x.\mneg{}\msubb{}Q[x])\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepUR  ``lattice-join  lattice-point  constrained-antichain-lattice``  0
  THEN  RepUR  ``mk-bounded-distributive-lattice  mk-bounded-lattice``  0
  THEN  DVar  `s'
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index