---

Step * 1 of Lemma bag-filter-trivial2


1. T : Type
2. p : T ⟶ 𝔹
3. u : T
4. v : T List
5. (∀x:T. (x ↓∈ v ⇒ (↑p[x]))) ⇒ permutation(T;filter(λx.p[x];v);v)
6. ∀x:T. (x ↓∈ [u / v] ⇒ (↑p[x]))
7. ↑p[u]
⊢ permutation(T;if p[u] then [u / filter(λx.p[x];v)] else filter(λx.p[x];v) fi ;[u / v])
BY
{ ((Subst ⌜p[u] ~ tt⌝ 0⋅ THENA Auto) THEN Reduce 0 THEN D (-3) THEN EAuto 1)⋅ }

1
1. T : Type
2. p : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀x:T. (x ↓∈ [u / v] ⇒ (↑p[x]))
6. ↑p[u]
7. x : T
8. x ↓∈ v
⊢ ↑p[x]

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (\muparrow{}p[x])))  {}\mRightarrow{}  permutation(T;filter(\mlambda{}x.p[x];v);v)
6.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  [u  /  v]  {}\mRightarrow{}  (\muparrow{}p[x]))
7.  \muparrow{}p[u]
\mvdash{}  permutation(T;if  p[u]  then  [u  /  filter(\mlambda{}x.p[x];v)]  else  filter(\mlambda{}x.p[x];v)  fi  ;[u  /  v])


By

---

Latex:
((Subst  \mkleeneopen{}p[u]  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  D  (-3)  THEN  EAuto  1)\mcdot{}

---

Home Index