---

Step * 2 1 of Lemma bag-remove1-equal


1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. a : T
6. b : T
7. ({a} + bs) = ({b} + as) ∈ bag(T)
⊢ bag-remove1(eq;as;a) = bag-remove1(eq;bs;b) ∈ (bag(T)?)
BY
{ ((ApFunToHypEquands `Z' ⌜bag-remove1(eq;Z;a)⌝ ⌜bag(T)?⌝ (-1)⋅ THENA Auto)
   THEN (RWO  "bag-remove1-member" (-1) THENA Auto)
   THEN (RWO "bag-remove1-append1" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜bag-remove1(eq;as;a)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  bag(T)
4.  bs  :  bag(T)
5.  a  :  T
6.  b  :  T
7.  (\{a\}  +  bs)  =  (\{b\}  +  as)
\mvdash{}  bag-remove1(eq;as;a)  =  bag-remove1(eq;bs;b)


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}bag-remove1(eq;Z;a)\mkleeneclose{}  \mkleeneopen{}bag(T)?\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO    "bag-remove1-member"  (-1)  THENA  Auto)
  THEN  (RWO  "bag-remove1-append1"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}bag-remove1(eq;as;a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index