---

Step * 1 1 1 1 2 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)
     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 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
{ (ParallelLast THEN MoveToConcl (-1)) }

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
⊢ 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)))

---

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.  \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:
                        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)))
\mvdash{}  \mforall{}bs: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)
          |  inr(z@0)  =>
          \mforall{}cs:bag(T).  (\mneg{}(bs  =  ((firstn(||as||  -  1;as)  @  [last(as)])  +  cs)))


By

---

Latex:
(ParallelLast  THEN  MoveToConcl  (-1))

---

Home Index