---

Step * 1 1 1 1 2 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 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)))
BY
{ ((RWO "list_accum_append" 0 THENA Auto) THEN Reduce 0) }

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

---

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


By

---

Latex:
((RWO  "list\_accum\_append"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index