Step
*
1
1
1
of Lemma
filter-fpf-vals
1. A : Type
2. eq : EqDecider(A)
3. B : A ⟶ Type
4. P : A ⟶ 𝔹
5. Q : A ⟶ 𝔹
6. d : A List
7. f1 : x:{x:A| (x ∈ d)} ⟶ B[x]
8. L : {x:A| (x ∈ d)} List
9. remove-repeats(eq;d) = L ∈ ({x:A| (x ∈ d)} List)
⊢ filter(λpL.Q[fst(pL)];zip(filter(P;L);map(f1;filter(P;L))))
~ zip(filter(λa.((P a) ∧b (Q a));L);map(f1;filter(λa.((P a) ∧b (Q a));L)))
BY
{ xxx((Thin (-1)) THEN (ListInd (-1)) THEN Reduce 0 THEN Try (Trivial))xxx }
1
1. A : Type
2. eq : EqDecider(A)
3. B : A ⟶ Type
4. P : A ⟶ 𝔹
5. Q : A ⟶ 𝔹
6. d : A List
7. f1 : x:{x:A| (x ∈ d)} ⟶ B[x]
8. u : {x:A| (x ∈ d)}
9. v : {x:A| (x ∈ d)} List
10. filter(λpL.Q[fst(pL)];zip(filter(P;v);map(f1;filter(P;v))))
~ zip(filter(λa.((P a) ∧b (Q a));v);map(f1;filter(λa.((P a) ∧b (Q a));v)))
⊢ filter(λpL.Q[fst(pL)];zip(if P u then [u / filter(P;v)] else filter(P;v) fi ;map(f1;if P u
then [u / filter(P;v)]
else filter(P;v)
fi )))
~ zip(if (P u) ∧b (Q u) then [u / filter(λa.((P a) ∧b (Q a));v)] else filter(λa.((P a) ∧b (Q a));v) fi ;
map(f1;if (P u) ∧b (Q u) then [u / filter(λa.((P a) ∧b (Q a));v)] else filter(λa.((P a) ∧b (Q a));v) fi ))
Latex:
Latex:
1. A : Type
2. eq : EqDecider(A)
3. B : A {}\mrightarrow{} Type
4. P : A {}\mrightarrow{} \mBbbB{}
5. Q : A {}\mrightarrow{} \mBbbB{}
6. d : A List
7. f1 : x:\{x:A| (x \mmember{} d)\} {}\mrightarrow{} B[x]
8. L : \{x:A| (x \mmember{} d)\} List
9. remove-repeats(eq;d) = L
\mvdash{} filter(\mlambda{}pL.Q[fst(pL)];zip(filter(P;L);map(f1;filter(P;L))))
\msim{} zip(filter(\mlambda{}a.((P a) \mwedge{}\msubb{} (Q a));L);map(f1;filter(\mlambda{}a.((P a) \mwedge{}\msubb{} (Q a));L)))
By
Latex:
xxx((Thin (-1)) THEN (ListInd (-1)) THEN Reduce 0 THEN Try (Trivial))xxx
Home
Index