---

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


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)))
BY
{ (InductionOnLast THEN Reduce 0) }

1
1. T : Type
2. eq : EqDecider(T)@i
⊢ ∀bs:bag(T). (bs = ([] + bs) ∈ bag(T))

2
1. T : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. ¬↑null(as)
5. ||as|| ≥ 1 
6. ∀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:
            firstn(||as|| - 1;as)
          with starting value:
           inl bs)
      of inl(cs) =>
      bs = (firstn(||as|| - 1;as) + cs) ∈ bag(T)
      | inr(z@0) =>
      ∀cs:bag(T). (¬(bs = (firstn(||as|| - 1;as) + cs) ∈ bag(T)))
⊢ ∀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:
           firstn(||as|| - 1;as) @ [last(as)]
         with starting value:
          inl bs)
     of inl(cs) =>
     bs = ((firstn(||as|| - 1;as) @ [last(as)]) + cs) ∈ bag(T)
     | inr(z@0) =>
     ∀cs:bag(T). (¬(bs = ((firstn(||as|| - 1;as) @ [last(as)]) + cs) ∈ bag(T)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)@i
\mvdash{}  \mforall{}as:T  List.  \mforall{}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)
          |  inr(z@0)  =>
          \mforall{}cs:bag(T).  (\mneg{}(bs  =  (as  +  cs)))


By

---

Latex:
(InductionOnLast  THEN  Reduce  0)

---

Home Index