---

Step * 1 of Lemma cal-filter-decomp


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))
BY
{ ((InstLemma `fset-ac-order` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
   THEN InstLemma `least-upper-bound-unique` 
   [⌜{ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} ⌝
   ; ⌜λ2ac1 ac2.fset-ac-le(eq;ac1;ac2)⌝;⌜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]))⌝]⋅
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Try ((Unfold `cal-filter` 0
              THEN Fold `cal-filter` 0
              THEN BLemma `fset-ac-le_weakening_f-subset`
              THEN Auto
              THEN Unfold `cal-filter` 0
              THEN BLemma `fset-filter-subset2`
              THEN Auto
              THEN MemTypeCD
              THEN Auto
              THEN (InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝;⌜P⌝;⌜s⌝]⋅ THENA Auto)
              THEN BHyp -1 
              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])))
11. Order({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);s)
13. x : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P[a])} 
14. fset-ac-le(eq;cal-filter(s;x.Q[x]);x)
15. fset-ac-le(eq;cal-filter(s;x.¬bQ[x]);x)
⊢ fset-ac-le(eq;s;x)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  P  :  fset(T)  {}\mrightarrow{}  \mBbbB{}
4.  s  :  fset(fset(T))
5.  \muparrow{}fset-antichain(eq;s)
6.  fset-all(s;a.P  a)
7.  Q  :  \{x:fset(T)|  \muparrow{}P[x]\}    {}\mrightarrow{}  \mBbbB{}
8.  cal-filter(s;x.Q[x])  \mmember{}  \{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P  a)\} 
9.  cal-filter(s;x.\mneg{}\msubb{}Q[x])  \mmember{}  \{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P  a)\} 
10.  least-upper-bound(\{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P[a])\}  ;
                                            ac1,ac2.fset-ac-le(eq;ac1;ac2);
                                            cal-filter(s;x.Q[x]);cal-filter(s;x.\mneg{}\msubb{}Q[x]);lub(P;cal-filter(s;x.Q[x]);...))
\mvdash{}  s  =  lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.\mneg{}\msubb{}Q[x]))


By

---

Latex:
((InstLemma  `fset-ac-order`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `least-upper-bound-unique` 
  [\mkleeneopen{}\{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P[a])\}  \mkleeneclose{}
  ;  \mkleeneopen{}\mlambda{}\msubtwo{}ac1  ac2.fset-ac-le(eq;ac1;ac2)\mkleeneclose{};\mkleeneopen{}cal-filter(s;x.Q[x])\mkleeneclose{};\mkleeneopen{}cal-filter(s;x.\mneg{}\msubb{}Q[x])\mkleeneclose{}
  ;  \mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}lub(P;cal-filter(s;x.Q[x]);cal-filter(s;x.\mneg{}\msubb{}Q[x]))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Try  ((Unfold  `cal-filter`  0
                        THEN  Fold  `cal-filter`  0
                        THEN  BLemma  `fset-ac-le\_weakening\_f-subset`
                        THEN  Auto
                        THEN  Unfold  `cal-filter`  0
                        THEN  BLemma  `fset-filter-subset2`
                        THEN  Auto
                        THEN  MemTypeCD
                        THEN  Auto
                        THEN  (InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
                        THEN  BHyp  -1 
                        THEN  Auto)))

---

Home Index