---

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


1. T : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. ¬↑null(as)
5. ||as|| ≥ 1 
6. bs : bag(T)@i
⊢ 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)))
⇒ case 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(b) =>
         bag-remove1(eq;b;last(as))
         | inr(z) =>
         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) @ [last(as)]) + cs) ∈ bag(T)
    | inr(z@0) =>
    ∀cs:bag(T). (¬(bs = ((firstn(||as|| - 1;as) @ [last(as)]) + cs) ∈ bag(T)))
BY
{ (GenConclAtAddrType ⌜bag(T)?⌝ [1;1]⋅ THENA Auto) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. as : T List@i
4. ¬↑null(as)
5. ||as|| ≥ 1 
6. bs : bag(T)@i
7. v : bag(T)?@i
8. 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)
= v
∈ (bag(T)?)
⊢ case v
 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)))
⇒ case case v of inl(b) => bag-remove1(eq;b;last(as)) | inr(z) => v
    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
3.  as  :  T  List@i
4.  \mneg{}\muparrow{}null(as)
5.  ||as||  \mgeq{}  1 
6.  bs  :  bag(T)@i
\mvdash{}  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)
  |  inr(z@0)  =>
  \mforall{}cs:bag(T).  (\mneg{}(bs  =  (firstn(||as||  -  1;as)  +  cs)))
{}\mRightarrow{}  case  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(b)  =>
                  bag-remove1(eq;b;last(as))
                  |  inr(z)  =>
                  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)  @  [last(as)])  +  cs)
        |  inr(z@0)  =>
        \mforall{}cs:bag(T).  (\mneg{}(bs  =  ((firstn(||as||  -  1;as)  @  [last(as)])  +  cs)))


By

---

Latex:
(GenConclAtAddrType  \mkleeneopen{}bag(T)?\mkleeneclose{}  [1;1]\mcdot{}  THENA  Auto)

---

Home Index