Step
*
4
of Lemma
bag-filter_wf
.....antecedent.....
1. T : Type
2. p : T ⟶ 𝔹
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ permutation({x:T| ↑p[x]} ;filter(λx.p[x];as);filter(λx.p[x];bs))
BY
{ (InstLemma `permutation-filter` [⌜T⌝;⌜as⌝;⌜bs⌝;⌜λ2x.p[x]⌝]⋅ THEN Auto) }
Latex:
Latex:
.....antecedent.....
1. T : Type
2. p : T {}\mrightarrow{} \mBbbB{}
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
\mvdash{} permutation(\{x:T| \muparrow{}p[x]\} ;filter(\mlambda{}x.p[x];as);filter(\mlambda{}x.p[x];bs))
By
Latex:
(InstLemma `permutation-filter` [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.p[x]\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index