---

Step * 1 4 of Lemma bag-remove1_wf


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. as : T List
5. bs : T List
6. permutation(T;as;bs)
7. ∀a:T. ((a ∈ as) ⇐⇒ (a ∈ bs))
8. (x ∈ as) ⇐⇒ (x ∈ bs)
9. ¬(x ∈ as)
10. bag-remove1(eq;as;x) = (inr ⋅ ) ∈ (T List?)
11. ¬(x ∈ bs)
12. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (T List?)
⊢ bag-remove1(eq;as;x) = bag-remove1(eq;bs;x) ∈ (bag(T)?)
BY
{ xxx((HypSubst' -3 0 THEN Auto) THEN HypSubst' -1 0 THEN Auto)⋅xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  as  :  T  List
5.  bs  :  T  List
6.  permutation(T;as;bs)
7.  \mforall{}a:T.  ((a  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  bs))
8.  (x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs)
9.  \mneg{}(x  \mmember{}  as)
10.  bag-remove1(eq;as;x)  =  (inr  \mcdot{}  )
11.  \mneg{}(x  \mmember{}  bs)
12.  bag-remove1(eq;bs;x)  =  (inr  \mcdot{}  )
\mvdash{}  bag-remove1(eq;as;x)  =  bag-remove1(eq;bs;x)


By

---

Latex:
xxx((HypSubst'  -3  0  THEN  Auto)  THEN  HypSubst'  -1  0  THEN  Auto)\mcdot{}xxx

---

Home Index