---

Step * 1 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)
⊢ bag-remove1(eq;as;x) = bag-remove1(eq;bs;x) ∈ (bag(T)?)
BY
{ xxx((InstLemma `member-permutation` [⌜T⌝;⌜as⌝;⌜bs⌝]⋅ THENA Auto)
      THEN (InstHyp [⌜x⌝] (-1)⋅ THENA Auto)
      THEN ((InstLemma `bag-remove1-property1` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜as⌝]⋅ THENA Auto)
            THEN (InstLemma `bag-remove1-property1` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto)
            )
      THEN SplitOrHyps
      THEN ExRepD)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. as@0 : T List
10. b1 : T List
11. as = ((as@0 @ [x]) @ b1) ∈ (T List)
12. bag-remove1(eq;as;x) = (inl (rev(as@0) @ b1)) ∈ (T List?)
13. a1 : T List
14. bs@0 : T List
15. bs = ((a1 @ [x]) @ bs@0) ∈ (T List)
16. bag-remove1(eq;bs;x) = (inl (rev(a1) @ bs@0)) ∈ (T List?)
⊢ bag-remove1(eq;as;x) = bag-remove1(eq;bs;x) ∈ (bag(T)?)

2
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. a1 : T List
12. bs@0 : T List
13. bs = ((a1 @ [x]) @ bs@0) ∈ (T List)
14. bag-remove1(eq;bs;x) = (inl (rev(a1) @ bs@0)) ∈ (T List?)
⊢ bag-remove1(eq;as;x) = bag-remove1(eq;bs;x) ∈ (bag(T)?)

3
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. as@0 : T List
10. b1 : T List
11. as = ((as@0 @ [x]) @ b1) ∈ (T List)
12. bag-remove1(eq;as;x) = (inl (rev(as@0) @ b1)) ∈ (T List?)
13. ¬(x ∈ bs)
14. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (T List?)
⊢ bag-remove1(eq;as;x) = bag-remove1(eq;bs;x) ∈ (bag(T)?)

4
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)?)

---

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)
\mvdash{}  bag-remove1(eq;as;x)  =  bag-remove1(eq;bs;x)


By

---

Latex:
xxx((InstLemma  `member-permutation`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
        THEN  ((InstLemma  `bag-remove1-property1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
                    THEN  (InstLemma  `bag-remove1-property1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
                    )
        THEN  SplitOrHyps
        THEN  ExRepD)xxx

---

Home Index