---

Step * 1 of Lemma fset-filter_wf

.....antecedent..... 
1. T : Type
2. P : T ⟶ 𝔹
3. s : Base
4. s1 : Base
5. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
6. s ∈ T List
7. s1 ∈ T List
8. set-equal(T;s;s1)
⊢ set-equal(T;filter(λx.P[x];s);filter(λx.P[x];s1))
BY
{ (RepeatFor 2 (ParallelLast) THEN ((RWO "member_filter" 0 THENM Reduce 0) THENA (Reduce 0 THEN Auto))⋅) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. s : Base
4. s1 : Base
5. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
6. s ∈ T List
7. s1 ∈ T List
8. t : T@i
9. (t ∈ s) ⇐⇒ (t ∈ s1)
⊢ (t ∈ s) ∧ (↑P[t]) ⇐⇒ (t ∈ s1) ∧ (↑P[t])

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  s  :  Base
4.  s1  :  Base
5.  s  =  s1
6.  s  \mmember{}  T  List
7.  s1  \mmember{}  T  List
8.  set-equal(T;s;s1)
\mvdash{}  set-equal(T;filter(\mlambda{}x.P[x];s);filter(\mlambda{}x.P[x];s1))


By

---

Latex:
(RepeatFor  2  (ParallelLast)
  THEN  ((RWO  "member\_filter"  0  THENM  Reduce  0)  THENA  (Reduce  0  THEN  Auto))\mcdot{}
  )

---

Home Index