Step
*
of Lemma
bag-filter-wf2
∀[T:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs} ⟶ 𝔹]. ([x∈bs|p[x]] ∈ bag({x:{b:T| b ↓∈ bs} | ↑p[x]} ))
BY
{ ((UnivCD THENA Auto)
THEN (InstLemma `bag-filter_wf` [⌜{b:T| b ↓∈ bs} ⌝]⋅ THENA Auto)
THEN BHyp (-1)
THEN Try (Complete (Auto))
THEN BLemma `bag-subtype`
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[bs:bag(T)]. \mforall{}[p:\{b:T| b \mdownarrow{}\mmember{} bs\} {}\mrightarrow{} \mBbbB{}]. ([x\mmember{}bs|p[x]] \mmember{} bag(\{x:\{b:T| b \mdownarrow{}\mmember{} bs\} | \muparrow{}p[x]\} )\000C)
By
Latex:
((UnivCD THENA Auto)
THEN (InstLemma `bag-filter\_wf` [\mkleeneopen{}\{b:T| b \mdownarrow{}\mmember{} bs\} \mkleeneclose{}]\mcdot{} THENA Auto)
THEN BHyp (-1)
THEN Try (Complete (Auto))
THEN BLemma `bag-subtype`
THEN Auto)
Home
Index