---

Step * of Lemma fset-ac-le-iff

∀[T:Type]
  ∀eq:EqDecider(T). ∀ac1,ac2:fset(fset(T)).
    (fset-ac-le(eq;ac1;ac2) ⇐⇒ ∀[a:fset(T)]. ↓∃b:fset(T). (b ∈ ac2 ∧ b ⊆ a) supposing a ∈ ac1)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `fset-ac-le` 0
   THEN Fold `ac-covers` 0
   THEN ((InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto) THEN (RWO "-1" 0 THENA Auto))
   THEN Thin (-1)
   THEN skip{(RWO "assert-ac-covers" 0 THEN Auto)}) }

1
1. T : Type
2. eq : EqDecider(T)
3. ac1 : fset(fset(T))
4. ac2 : fset(fset(T))
⊢ ∀[x:fset(T)]. ↑ac-covers(eq;ac2;x) supposing x ∈ ac1
⇐⇒ ∀[a:fset(T)]. ↓∃b:fset(T). (b ∈ ac2 ∧ b ⊆ a) supposing a ∈ ac1

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}ac1,ac2:fset(fset(T)).
        (fset-ac-le(eq;ac1;ac2)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}[a:fset(T)].  \mdownarrow{}\mexists{}b:fset(T).  (b  \mmember{}  ac2  \mwedge{}  b  \msubseteq{}  a)  supposing  a  \mmember{}  ac1)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fset-ac-le`  0
  THEN  Fold  `ac-covers`  0
  THEN  ((InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO  "-1"  0  THENA  Auto)
              )
  THEN  Thin  (-1)
  THEN  skip\{(RWO  "assert-ac-covers"  0  THEN  Auto)\})

---

Home Index