---

Step * 1 1 1 1 2 1 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
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)))
BY
{ (D (-2) 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)@i
7. x : 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)
= (inl x)
∈ (bag(T)?)
⊢ (bs = (firstn(||as|| - 1;as) + x) ∈ bag(T))
⇒ case bag-remove1(eq;x;last(as))
    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)))

2
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. y : Unit@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)
= (inr y )
∈ (bag(T)?)
⊢ (∀cs:bag(T). (¬(bs = (firstn(||as|| - 1;as) + cs) ∈ bag(T))))
⇒ (∀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
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
\mvdash{}  case  v
  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  v  of  inl(b)  =>  bag-remove1(eq;b;last(as))  |  inr(z)  =>  v
        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:
(D  (-2)  THEN  Reduce  0)

---

Home Index