---

Step * 1 1 2 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])))
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)
16. s ∈ fset({x:fset(T)| ↑P[x]} )
⊢ fset-ac-le(eq;s;x)
BY
{ ((InstLemma `fset-all-iff` [⌜{x:fset(T)| ↑P[x]} ⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
   THEN RepUR ``fset-ac-le cal-filter`` -4
   THEN (RWO "-1" (-4) THENA Auto)
   THEN RepUR ``fset-ac-le cal-filter`` -3
   THEN (RWO "-1" (-3) THENA Auto)
   THEN RepUR ``fset-ac-le cal-filter`` 0
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RenameVar `z' (-2)
   THEN (BoolCase ⌜Q[z]⌝⋅ THENA Auto)
   THEN OnMaybeHyp 15 (\h. (BHyp h  THEN Auto THEN BLemma `member-fset-filter` THEN Complete (Auto)))) }

---

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]);...))
11.  Order(\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ;ac1,ac2.fset-ac-le(eq;ac1;ac2))
12.  fset-ac-le(eq;cal-filter(s;x.\mneg{}\msubb{}Q[x]);s)
13.  x  :  \{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  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.\mneg{}\msubb{}Q[x]);x)
16.  s  \mmember{}  fset(\{x:fset(T)|  \muparrow{}P[x]\}  )
\mvdash{}  fset-ac-le(eq;s;x)


By

---

Latex:
((InstLemma  `fset-all-iff`  [\mkleeneopen{}\{x:fset(T)|  \muparrow{}P[x]\}  \mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``fset-ac-le  cal-filter``  -4
  THEN  (RWO  "-1"  (-4)  THENA  Auto)
  THEN  RepUR  ``fset-ac-le  cal-filter``  -3
  THEN  (RWO  "-1"  (-3)  THENA  Auto)
  THEN  RepUR  ``fset-ac-le  cal-filter``  0
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RenameVar  `z'  (-2)
  THEN  (BoolCase  \mkleeneopen{}Q[z]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  OnMaybeHyp  15  (\mbackslash{}h.  (BHyp  h    THEN  Auto  THEN  BLemma  `member-fset-filter`  THEN  Complete  (Auto))))

---

Home Index