---

Step * of Lemma filter-equal

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List].
  (filter(P;L1) = filter(P;L2) ∈ (T List)) supposing 
     ((∀i:ℕ||L1||. ((L1[i] = L2[i] ∈ T) ∨ ((¬↑(P L1[i])) ∧ (¬↑(P L2[i]))))) and 
     (||L1|| = ||L2|| ∈ ℤ))
BY
{ ((InductionOnList
    THEN Reduce 0
    THEN (D 0 THENA Auto)
    THEN ListInd (-1)
    THEN Reduce 0
    THEN Try (QuickAuto)
    THEN Try (Complete ((Auto THEN (Assert ⌜¬(0 = (||v|| + 1) ∈ ℤ)⌝⋅ THEN Auto) THEN All Thin THEN Auto'))))
   THEN Thin (-1)
   THEN (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert ||v|| = ||v1|| ∈ ℤ BY Auto))
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN (InstHyp [⌜0⌝] (-4)⋅ THENA Auto')
   THEN Reduce (-1)
   THEN D -1
   THEN Try (Complete (Auto))) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[L2:T List]
     (filter(P;v) = filter(P;L2) ∈ (T List)) supposing 
        ((∀i:ℕ||v||. ((v[i] = L2[i] ∈ T) ∨ ((¬↑(P v[i])) ∧ (¬↑(P L2[i]))))) and 
        (||v|| = ||L2|| ∈ ℤ))
6. u1 : T
7. v1 : T List
8. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
9. ∀i:ℕ||v|| + 1. (([u / v][i] = [u1 / v1][i] ∈ T) ∨ ((¬↑(P [u / v][i])) ∧ (¬↑(P [u1 / v1][i]))))
10. ||v|| = ||v1|| ∈ ℤ
11. ↑(P u)
12. ↑(P u1)
13. u = u1 ∈ T
⊢ [u / filter(P;v)] = [u1 / filter(P;v1)] ∈ (T List)

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[L2:T List]
     (filter(P;v) = filter(P;L2) ∈ (T List)) supposing 
        ((∀i:ℕ||v||. ((v[i] = L2[i] ∈ T) ∨ ((¬↑(P v[i])) ∧ (¬↑(P L2[i]))))) and 
        (||v|| = ||L2|| ∈ ℤ))
6. u1 : T
7. v1 : T List
8. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
9. ∀i:ℕ||v|| + 1. (([u / v][i] = [u1 / v1][i] ∈ T) ∨ ((¬↑(P [u / v][i])) ∧ (¬↑(P [u1 / v1][i]))))
10. ||v|| = ||v1|| ∈ ℤ
11. ¬↑(P u)
12. ¬↑(P u1)
13. u = u1 ∈ T
⊢ filter(P;v) = filter(P;v1) ∈ (T List)

3
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[L2:T List]
     (filter(P;v) = filter(P;L2) ∈ (T List)) supposing 
        ((∀i:ℕ||v||. ((v[i] = L2[i] ∈ T) ∨ ((¬↑(P v[i])) ∧ (¬↑(P L2[i]))))) and 
        (||v|| = ||L2|| ∈ ℤ))
6. u1 : T
7. v1 : T List
8. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
9. ∀i:ℕ||v|| + 1. (([u / v][i] = [u1 / v1][i] ∈ T) ∨ ((¬↑(P [u / v][i])) ∧ (¬↑(P [u1 / v1][i]))))
10. ||v|| = ||v1|| ∈ ℤ
11. ¬↑(P u)
12. ¬↑(P u1)
13. (¬↑(P u)) ∧ (¬↑(P u1))
⊢ filter(P;v) = filter(P;v1) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L1,L2:T  List].
    (filter(P;L1)  =  filter(P;L2))  supposing 
          ((\mforall{}i:\mBbbN{}||L1||.  ((L1[i]  =  L2[i])  \mvee{}  ((\mneg{}\muparrow{}(P  L1[i]))  \mwedge{}  (\mneg{}\muparrow{}(P  L2[i])))))  and 
          (||L1||  =  ||L2||))


By

---

Latex:
((InductionOnList
    THEN  Reduce  0
    THEN  (D  0  THENA  Auto)
    THEN  ListInd  (-1)
    THEN  Reduce  0
    THEN  Try  (QuickAuto)
    THEN  Try  (Complete  ((Auto
                                              THEN  (Assert  \mkleeneopen{}\mneg{}(0  =  (||v||  +  1))\mkleeneclose{}\mcdot{}  THEN  Auto)
                                              THEN  All  Thin
                                              THEN  Auto'))))
  THEN  Thin  (-1)
  THEN  (RepeatFor  2  ((D  0  THENA  Auto))  THEN  (Assert  ||v||  =  ||v1||  BY  Auto))
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto')
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  Try  (Complete  (Auto)))

---

Home Index