Step
*
of Lemma
fset-minimals-ac-le
∀[T:Type]. ∀eq:EqDecider(T). ∀s:fset(fset(T)). fset-ac-le(eq;s;fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s))
BY
{ (Auto
THEN Unfold `fset-ac-le` 0
THEN (InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
THEN RWO "-1" 0
THEN Auto
THEN (RW assert_pushdownC 0 THENA Auto)
THEN RWO "assert-fset-null" 0
THEN Auto) }
1
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))]. uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. x : fset(T)
6. x ∈ s
⊢ ¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T). \mforall{}s:fset(fset(T)).
fset-ac-le(eq;s;fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s))
By
Latex:
(Auto
THEN Unfold `fset-ac-le` 0
THEN (InstLemma `fset-all-iff` [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{} THENA Auto)
THEN RWO "-1" 0
THEN Auto
THEN (RW assert\_pushdownC 0 THENA Auto)
THEN RWO "assert-fset-null" 0
THEN Auto)
Home
Index