Step
*
1
of Lemma
filter-union
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. P : T ⟶ 𝔹
5. u : T
6. v : T List
7. filter(P;reduce(λa,L. insert(a;L);as;v)) = reduce(λa,L. insert(a;L);filter(P;as);filter(P;v)) ∈ (T List)
8. ↑(P u)
⊢ filter(P;insert(u;reduce(λa,L. insert(a;L);as;v))) = insert(u;reduce(λa,L. insert(a;L);filter(P;as);filter(P;v))) ∈ (T\000C List)
BY
{ (RevHypSubst' (-2) 0 THEN Auto) }
1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. P : T ⟶ 𝔹
5. u : T
6. v : T List
7. filter(P;reduce(λa,L. insert(a;L);as;v)) = reduce(λa,L. insert(a;L);filter(P;as);filter(P;v)) ∈ (T List)
8. ↑(P u)
⊢ filter(P;insert(u;reduce(λa,L. insert(a;L);as;v))) = insert(u;filter(P;reduce(λa,L. insert(a;L);as;v))) ∈ (T List)
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. P : T {}\mrightarrow{} \mBbbB{}
5. u : T
6. v : T List
7. filter(P;reduce(\mlambda{}a,L. insert(a;L);as;v)) = reduce(\mlambda{}a,L. insert(a;L);filter(P;as);filter(P;v))
8. \muparrow{}(P u)
\mvdash{} filter(P;insert(u;reduce(\mlambda{}a,L. insert(a;L);as;v)))
= insert(u;reduce(\mlambda{}a,L. insert(a;L);filter(P;as);filter(P;v)))
By
Latex:
(RevHypSubst' (-2) 0 THEN Auto)
Home
Index