---

Step * of Lemma filter_is_singleton2

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀L:T List.
    (||filter(P;L)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||L||. ((↑(P L[i])) ∧ (∀j:ℕ||L||. i = j ∈ ℤ supposing ↑(P L[j]))))
BY
{ TACTIC:((InductionOnList THEN Reduce 0 THEN Try (Complete ((Auto THEN ExRepD THEN Auto'))) THEN SplitOnConclITE)
          THENA Auto
          ) }

1
.....truecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ||filter(P;v)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||v||. ((↑(P v[i])) ∧ (∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])))
6. ↑(P u)
⊢ ||[u / filter(P;v)]|| = 1 ∈ ℤ
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))

2
.....falsecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ||filter(P;v)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||v||. ((↑(P v[i])) ∧ (∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])))
6. ¬↑(P u)
⊢ ||filter(P;v)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
        (||filter(P;L)||  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||L||.  ((\muparrow{}(P  L[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}||L||.  i  =  j  supposing  \muparrow{}(P  L[j]))))


By

---

Latex:
TACTIC:((InductionOnList
                  THEN  Reduce  0
                  THEN  Try  (Complete  ((Auto  THEN  ExRepD  THEN  Auto')))
                  THEN  SplitOnConclITE)
                THENA  Auto
                )

---

Home Index