---

Step * 1 1 1 of Lemma bag-remove1_wf

.....antecedent..... 
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) ⇐ (x ∈ bs)
10. as@0 : T List
11. b1 : T List
12. as = ((as@0 @ [x]) @ b1) ∈ (T List)
13. bag-remove1(eq;as;x) = (inl (rev(as@0) @ b1)) ∈ (T List?)
14. a1 : T List
15. bs@0 : T List
16. bs = ((a1 @ [x]) @ bs@0) ∈ (T List)
17. bag-remove1(eq;bs;x) = (inl (rev(a1) @ bs@0)) ∈ (T List?)
⊢ permutation(T;as@0 @ b1;a1 @ bs@0)
BY
{ xxx(Assert ⌜permutation(T;(as@0 @ [x]) @ b1;(a1 @ [x]) @ bs@0)⌝⋅ THEN Auto)xxx }

1
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) ⇐ (x ∈ bs)
10. as@0 : T List
11. b1 : T List
12. as = ((as@0 @ [x]) @ b1) ∈ (T List)
13. bag-remove1(eq;as;x) = (inl (rev(as@0) @ b1)) ∈ (T List?)
14. a1 : T List
15. bs@0 : T List
16. bs = ((a1 @ [x]) @ bs@0) ∈ (T List)
17. bag-remove1(eq;bs;x) = (inl (rev(a1) @ bs@0)) ∈ (T List?)
18. permutation(T;(as@0 @ [x]) @ b1;(a1 @ [x]) @ bs@0)
⊢ permutation(T;as@0 @ b1;a1 @ bs@0)

---

Latex:

---

Latex:
.....antecedent..... 
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)  {}\mRightarrow{}  (x  \mmember{}  bs)
9.  (x  \mmember{}  as)  \mLeftarrow{}{}  (x  \mmember{}  bs)
10.  as@0  :  T  List
11.  b1  :  T  List
12.  as  =  ((as@0  @  [x])  @  b1)
13.  bag-remove1(eq;as;x)  =  (inl  (rev(as@0)  @  b1))
14.  a1  :  T  List
15.  bs@0  :  T  List
16.  bs  =  ((a1  @  [x])  @  bs@0)
17.  bag-remove1(eq;bs;x)  =  (inl  (rev(a1)  @  bs@0))
\mvdash{}  permutation(T;as@0  @  b1;a1  @  bs@0)


By

---

Latex:
xxx(Assert  \mkleeneopen{}permutation(T;(as@0  @  [x])  @  b1;(a1  @  [x])  @  bs@0)\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index