Step
*
1
1
of Lemma
fpf-vals-nil
.....assertion.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
⊢ ∀L:A List. (no_repeats(A;L) ⇒ (filter(P;L) = if a ∈b L) then [a] else [] fi ∈ (A List)))
BY
{ (((((((((InductionOnList THEN SplitOnConclITE) THENA Auto)
THEN Try (((RWO "nil_member" (-1)) THEN Auto))
THEN Try (((RWO "cons_member" (-1)) THENA Auto))
THEN All Reduce
THEN Try (Complete (Auto))
THEN (ParallelOp (-2))
THEN Try (((RWO "no_repeats_cons" (-1)) THEN Complete (Auto)))
THEN SplitOnConclITE)
THENA Auto
)
THEN (HypSubst (-2) 0)
)
THENA Auto
)
THEN SplitOnConclITE
)
THENA Auto
)
THEN Try (Complete (Auto))
THEN (RW assert_pushdownC (-5))
THEN Auto) }
1
.....truecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. (a = u ∈ A) ∨ (a ∈ v)
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ↑(P u)
16. (a ∈ v)
⊢ [u; a] = [a] ∈ (A List)
2
.....falsecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. (a = u ∈ A) ∨ (a ∈ v)
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ↑(P u)
16. ¬(a ∈ v)
⊢ [u] = [a] ∈ (A List)
3
.....falsecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. (a = u ∈ A) ∨ (a ∈ v)
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ¬↑(P u)
16. ¬(a ∈ v)
⊢ [] = [a] ∈ (A List)
4
.....truecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. ¬((a = u ∈ A) ∨ (a ∈ v))
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ↑(P u)
16. (a ∈ v)
⊢ [u; a] = [] ∈ (A List)
5
.....falsecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. ¬((a = u ∈ A) ∨ (a ∈ v))
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ↑(P u)
16. ¬(a ∈ v)
⊢ [u] = [] ∈ (A List)
6
.....truecase.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. d : A List
6. f1 : x:{x:A| (x ∈ d)} ─→ B[x]
7. a : A
8. ¬↑a ∈ dom(<d, f1>)
9. ∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)
10. u : A@i
11. v : A List@i
12. ¬((a = u ∈ A) ∨ (a ∈ v))
13. no_repeats(A;[u / v])@i
14. filter(P;v) = if a ∈b v) then [a] else [] fi ∈ (A List)@i
15. ¬↑(P u)
16. (a ∈ v)
⊢ [a] = [] ∈ (A List)
Latex:
.....assertion.....
1. A : Type
2. eq : EqDecider(A)
3. B : A {}\mrightarrow{} Type
4. P : A {}\mrightarrow{} \mBbbB{}
5. d : A List
6. f1 : x:\{x:A| (x \mmember{} d)\} {}\mrightarrow{} B[x]
7. a : A
8. \mneg{}\muparrow{}a \mmember{} dom(<d, f1>)
9. \mforall{}b:A. (\muparrow{}(P b) \mLeftarrow{}{}\mRightarrow{} b = a)
\mvdash{} \mforall{}L:A List. (no\_repeats(A;L) {}\mRightarrow{} (filter(P;L) = if a \mmember{}\msubb{} L) then [a] else [] fi ))
By
(((((((((InductionOnList THEN SplitOnConclITE) THENA Auto)
THEN Try (((RWO "nil\_member" (-1)) THEN Auto))
THEN Try (((RWO "cons\_member" (-1)) THENA Auto))
THEN All Reduce
THEN Try (Complete (Auto))
THEN (ParallelOp (-2))
THEN Try (((RWO "no\_repeats\_cons" (-1)) THEN Complete (Auto)))
THEN SplitOnConclITE)
THENA Auto
)
THEN (HypSubst (-2) 0)
)
THENA Auto
)
THEN SplitOnConclITE
)
THENA Auto
)
THEN Try (Complete (Auto))
THEN (RW assert\_pushdownC (-5))
THEN Auto)
Home
Index