---

Step * 1 1 1 of Lemma bag-diff-property


1. T : Type
2. eq : EqDecider(T)@i
3. as : T List
4. bs : bag(T)@i
⊢ ↓case bag-diff(eq;bs;as) of inl(cs) => bs = (as + cs) ∈ bag(T) | inr(z@0) => ∀cs:bag(T). (¬(bs = (as + cs) ∈ bag(T)))
BY
{ TACTIC:(D 0 THEN RepUR ``bag-diff bag-accum`` 0 THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. T : Type
2. eq : EqDecider(T)@i
⊢ ∀as:T List. ∀bs:bag(T).
    case accumulate (with value r and list item a):
          case r of inl(b) => bag-remove1(eq;b;a) | inr(z) => r
         over list:
           as
         with starting value:
          inl bs)
     of inl(cs) =>
     bs = (as + cs) ∈ bag(T)
     | inr(z@0) =>
     ∀cs:bag(T). (¬(bs = (as + cs) ∈ bag(T)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)@i
3.  as  :  T  List
4.  bs  :  bag(T)@i
\mvdash{}  \mdownarrow{}case  bag-diff(eq;bs;as)
        of  inl(cs)  =>
        bs  =  (as  +  cs)
        |  inr(z@0)  =>
        \mforall{}cs:bag(T).  (\mneg{}(bs  =  (as  +  cs)))


By

---

Latex:
TACTIC:(D  0  THEN  RepUR  ``bag-diff  bag-accum``  0  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index