---

Definition: bag-count
(#x in bs) ==  count(eq x;bs)

Lemma: bag-count_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  ((#x in bs) ∈ ℕ)

Lemma: bag-count-sqequal
∀[T:Type]. ∀[bs:bag(T)]. ∀[eq:EqDecider(T)]. ∀[x:T].  ((#x in bs) ~ #([y∈bs|eq x y]))

Lemma: bag-count-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[x:T].  ((#x in as + bs) = ((#x in as) + (#x in bs)) ∈ ℤ)

Lemma: bag-count-single
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T].  ((#x in [y]) = if eq x y then 1 else 0 fi  ∈ ℤ)

Lemma: bag-count-cons
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[b:bag(T)].
  ((#x in y.b) = if eq x y then (#x in b) + 1 else (#x in b) fi  ∈ ℤ)

Lemma: bag-count-empty
∀[eq,x:Top].  ((#x in {}) ~ 0)

Lemma: bag-member-count
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))

Lemma: bag-count-is-zero
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (#x in bs) ~ 0 supposing ¬x ↓∈ bs

Lemma: bag-count-ap-map
∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[x:T1]. ∀[bs:bag(T1)].
  (#f x in bag-map(f;bs)) ~ (#x in bs) supposing Inj(T1;T2;f)

Lemma: bag-count-map
∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[x:T2]. ∀[bs:bag(T1)]. ∀[g:T2 ⟶ T1].
  (#x in bag-map(f;bs)) ~ (#g x in bs) supposing (∀x:T2. ((f (g x)) = x ∈ T2)) ∧ (∀x:T1. ((g (f x)) = x ∈ T1))

Lemma: bag-count-filter
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  ((#x in [t∈bs|p[t]]) ≤ (#x in bs))

Lemma: bag-count-rep
∀[T:Type]. ∀[n:ℕ]. ∀[eq:EqDecider(T)]. ∀[x,y:T].  ((#x in bag-rep(n;y)) = if eq x y then n else 0 fi  ∈ ℤ)

Lemma: bag-count-combine
∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[eq:EqDecider(T2)]. ∀[z:T2]. ∀[bs:bag(T1)].
  ((#z in ⋃x∈bs.f[x]) ~ bag-sum(bs;x.(#z in f[x])))

Lemma: bag-sum-count
∀[A,B:Type]. ∀[f:B ⟶ bag(A)]. ∀[eq:EqDecider(A)]. ∀[bb:bag(B)]. ∀[z:A].
  (bag-sum(bb;b.(#z in f[b])) ~ bag-sum([b∈bb|1 ≤z (#z in f[b])];b.(#z in f[b])))

Lemma: decidable__bag-member
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀x:T. ∀bs:bag(T).  Dec(x ↓∈ bs)))

Lemma: decidable__bag-member2
∀[T:Type]. ∀x:T. ((∀y:T. Dec(x = y ∈ T)) ⇒ (∀bs:bag(T). Dec(x ↓∈ bs)))

Definition: bag-map'
bag-map'(f;b) ==  bag-map(f;b)

Lemma: bag-map'_wf
∀[B,A:Type]. ∀[b:bag(A)]. ∀[f:{x:A| x ↓∈ b}  ⟶ B].  (bag-map'(f;b) ∈ bag(B))

Lemma: bag-member-decidable2
∀T:Type. ∀P:T ⟶ ℙ. ∀b:bag(T). ∀x:{x:T| P[x]} .
  ((∀x,y:{x:T| P[x]} .  Dec(x = y ∈ {x:T| P[x]} )) ⇒ (∀x:{x:T| x ↓∈ b} . ∃y:{x:T| P[x]} . (x = y ∈ T)) ⇒ Dec(x ↓∈ b))

Lemma: permutation-iff-count
∀[T:Type]
  ∀eq:EqDecider(T). ∀a1,b1:T List.
    (∀x:T. (||filter(eqof(eq) x;a1)|| = ||filter(eqof(eq) x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))

Lemma: bag-no-repeats-count
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  uiff(bag-no-repeats(T;bs);∀[x:T]. uiff(1 ≤ (#x in bs);(#x in bs) = 1 ∈ ℤ))

Lemma: bag-count-member-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  ((#x in bs) = 1 ∈ ℤ) supposing (bag-no-repeats(T;bs) and x ↓∈ bs)

Lemma: bag-combine-no-repeats
∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(T2)]. ∀[bs:bag(T1)].
  (bag-no-repeats(T2;⋃x∈bs.f[x])) supposing 
     (bag-no-repeats(T1;bs) and 
     ((∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))) ∧ (∀x:T1. bag-no-repeats(T2;f[x]))))

Lemma: bag-combine-no-repeats2
∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[bs:bag(T1)].
  (bag-no-repeats(T2;⋃x∈bs.f[x])) supposing 
     (bag-no-repeats(T1;bs) and 
     ((∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1)))
     ∧ (∀x:T1. bag-no-repeats(T2;f[x]))
     ∧ (∀x,y:T1.  Dec(x = y ∈ T1))
     ∧ (∀x,y:T2.  Dec(x = y ∈ T2))))

Lemma: bag-extensionality
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  uiff(as = bs ∈ bag(T);∀x:T. ((#x in as) = (#x in bs) ∈ ℤ))

Lemma: bag-extensionality2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].
  uiff(as = bs ∈ bag(T);(∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))) ∧ (∀x:T. (x ↓∈ bs ⇒ x ↓∈ as)))

Lemma: assert-bag-all
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (∀x:T. (x ↓∈ bs ⇒ (↑p[x])) ⇐⇒ ↑bag-all(x.p[x];bs))

Definition: bag-deq-member
bag-deq-member(eq;x;b) ==  x ∈b b

Lemma: bag-deq-member_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[b:bag(A)]. ∀[x:A].  (bag-deq-member(eq;x;b) ∈ 𝔹)

Lemma: assert-bag-deq-member
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[b:bag(A)]. ∀[x:A].  uiff(↑bag-deq-member(eq;x;b);x ↓∈ b)

Definition: bag-eq
bag-eq(eq;as;bs) ==  bag-all(x.((#x in as) =z (#x in bs));as) ∧b bag-all(x.0 <z (#x in as);bs)

Lemma: bag-eq_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-eq(eq;as;bs) ∈ 𝔹)

Lemma: assert-bag-eq
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  uiff(↑bag-eq(eq;as;bs);as = bs ∈ bag(T))

Lemma: decidable__equal_bag
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀xs,ys:bag(T).  Dec(xs = ys ∈ bag(T))))

Definition: bag-deq
bag-deq(eq) ==  λas,bs. bag-eq(eq;as;bs)

Lemma: bag-deq_wf
∀[T:Type]. ∀[eq:EqDecider(T)].  (bag-deq(eq) ∈ EqDecider(bag(T)))

Definition: bag-remove-repeats
bag-remove-repeats(eq;bs) ==  list-to-set(eq;bs)

Lemma: bag-remove-repeats_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-remove-repeats(eq;bs) ∈ bag(T))

Lemma: bag-remove-repeats-eq-remove-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-remove-repeats(eq;bs) = remove-repeats(eq;bs) ∈ bag(T))

Lemma: count-bag-remove-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].
  ((#x in bag-remove-repeats(eq;bs)) ~ if 0 <z (#x in bs) then 1 else 0 fi )

Lemma: member-bag-remove-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-remove-repeats(eq;bs))

Lemma: bag-remove-repeats-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(T;bag-remove-repeats(eq;bs))

Lemma: bag-remove-repeats-if-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-remove-repeats(eq;bs) = bs ∈ bag(T) supposing bag-no-repeats(T;bs)

Lemma: bag-member-remove-repeats
∀[T:Type]. ∀[b:bag(T)]. ∀[eq:EqDecider(T)]. ∀[x:T].  uiff(x ↓∈ b;x ↓∈ bag-remove-repeats(eq;b))

Lemma: bag-remove-repeats-append
∀[T:Type]. ∀[as,bs:bag(T)]. ∀[eq:EqDecider(T)].
  (bag-remove-repeats(eq;as + bs)
  = (bag-remove-repeats(eq;as) + [x∈bag-remove-repeats(eq;bs)|¬bbag-deq-member(eq;x;as)])
  ∈ bag(T))

Lemma: bag-remove-repeats-filter
∀[T:Type]. ∀[b:bag(T)]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹].
  (bag-remove-repeats(eq;[x∈b|P[x]]) = [x∈bag-remove-repeats(eq;b)|P[x]] ∈ bag(T))

Definition: bag-to-set
bag-to-set(eq;bs) ==  bag-remove-repeats(eq;bs)

Lemma: bag-to-set_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-to-set(eq;bs) ∈ bag(T))

Lemma: count-bag-to-set
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  ((#x in bag-to-set(eq;bs)) ~ if 0 <z (#x in bs) then 1 else 0 fi )

Lemma: no-repeats-bag-to-set
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(T;bag-to-set(eq;bs))

Lemma: member-bag-to-set
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))

Lemma: equal-count-bag-to-set
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
  uiff((#x in bag-to-set(eq;bs)) = (#y in bag-to-set(eq;bs)) ∈ ℤ;x ↓∈ bs ⇐⇒ y ↓∈ bs)

Definition: bag-remove
bs - x ==  [y∈bs|¬b(eq x y)]

Lemma: bag-remove_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  (bs - x ∈ bag(T))

Lemma: bag-member-remove
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,z:T].  uiff(z ↓∈ bs - x;z ↓∈ bs ∧ (¬(z = x ∈ T)))

Lemma: bag-remove-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[x:T].  (as + bs - x ~ as - x + bs - x)

Lemma: bag-remove-trivial
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bs - x = bs ∈ bag(T) supposing ¬x ↓∈ bs

Lemma: sub-bag-remove-if
∀[T:Type]. ∀[bs:bag(T)].  ∀eq:EqDecider(T). ∀as:bag(T). ∀x:T.  (sub-bag(T;as;bs) ⇒ sub-bag(T;as - x;bs))

Lemma: bag-remove-size
∀[T:Type]
  ∀eq:EqDecider(T). ∀bs:bag(T). ∀x:T.
    ((x ↓∈ bs ∧ (#(bs - x) = (#(bs) - (#x in bs)) ∈ ℤ)) ∨ ((¬x ↓∈ bs) ∧ (#(bs - x) = #(bs) ∈ ℤ)))

Lemma: bag-remove-size-member-no-repeats
∀[T:Type]
  ∀eq:EqDecider(T). ∀bs:bag(T). ∀x:T.  (#(bs - x) = (#(bs) - 1) ∈ ℤ) supposing (x ↓∈ bs and bag-no-repeats(T;bs))

Definition: bag_remove1_aux
bag_remove1_aux(eq;checked;a;as) ==
  fix((λbag_remove1_aux,checked,as. case as of 
                                      [] => inr Ax  
                                      a'::as' =>
                                       if eq a' a then inl (checked @ as') else bag_remove1_aux [a' / checked] as' fi  
                                   esac)) 
  checked 
  as

Lemma: bag_remove1_aux_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs,checked:T List].  (bag_remove1_aux(eq;checked;x;bs) ∈ T List?)

Lemma: bag_remove1_aux_property
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀L,checked:T List.
    ((∃as,bs:T List
       ((L = ((as @ [x]) @ bs) ∈ (T List))
       ∧ (bag_remove1_aux(eq;checked;x;L) = (inl ((rev(as) @ checked) @ bs)) ∈ (T List?))))
    ∨ ((¬(x ∈ L)) ∧ (bag_remove1_aux(eq;checked;x;L) = (inr ⋅ ) ∈ (T List?))))

Definition: bag-remove1
bag-remove1(eq;bs;a) ==  bag_remove1_aux(eq;[];a;bs)

Lemma: bag-remove1_wf1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:T List].  (bag-remove1(eq;bs;x) ∈ T List?)

Lemma: bag-remove1-property1
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀L:T List.
    ((∃as,bs:T List. ((L = ((as @ [x]) @ bs) ∈ (T List)) ∧ (bag-remove1(eq;L;x) = (inl (rev(as) @ bs)) ∈ (T List?))))
    ∨ ((¬(x ∈ L)) ∧ (bag-remove1(eq;L;x) = (inr ⋅ ) ∈ (T List?))))

Lemma: bag-remove1_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-remove1(eq;bs;x) ∈ bag(T)?)

Lemma: bag-remove1-property
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
    ∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))

Lemma: bag-remove1-non-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?) supposing ¬x ↓∈ bs

Lemma: bag-remove1-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-remove1(eq;{x} + bs;x) = (inl bs) ∈ (bag(T)?))

Lemma: bag-remove1-append1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[bs:bag(T)].
  (bag-remove1(eq;{y} + bs;x)
  = if eq x y then inl bs else case bag-remove1(eq;bs;x) of inl(as) => inl ({y} + as) | inr(x) => inr ⋅  fi 
  ∈ (bag(T)?))

Lemma: bag-remove1-equal
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[a,b:T].
  uiff(bag-remove1(eq;as;a) = bag-remove1(eq;bs;b) ∈ (bag(T)?);(({a} + bs) = ({b} + as) ∈ bag(T))
  ↓∨ ((¬a ↓∈ as) ∧ (¬b ↓∈ bs)))

Lemma: bag-count-remove1
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((x ↓∈ bs ∧ ((#x in outl(bag-remove1(eq;bs;x))) = ((#x in bs) - 1) ∈ ℕ)) ∨ (¬x ↓∈ bs))

Definition: bag-drop
bag-drop(eq;bs;a) ==  case bag-remove1(eq;bs;a) of inl(as) => as | inr(_) => bs

Lemma: bag-drop_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[a:T].  (bag-drop(eq;bs;a) ∈ bag(T))

Lemma: bag-drop-property
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((bs = ({x} + bag-drop(eq;bs;x)) ∈ bag(T)) ∨ ((¬x ↓∈ bs) ∧ (bs = bag-drop(eq;bs;x) ∈ bag(T))))

Lemma: bag-drop-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs,cs:bag(T)].
  (bag-drop(eq;bs + cs;x) = if ((#x in bs) =z 0) then bs + bag-drop(eq;cs;x) else bag-drop(eq;bs;x) + cs fi  ∈ bag(T))

Lemma: bag-count-drop
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((x ↓∈ bs ∧ ((#x in bag-drop(eq;bs;x)) = ((#x in bs) - 1) ∈ ℕ))
    ∨ ((¬x ↓∈ bs) ∧ ((#x in bag-drop(eq;bs;x)) = (#x in bs) ∈ ℕ)))

Lemma: bag-count-drop-trivial
∀[T:Type]. ∀eq:EqDecider(T). ∀[x,y:T]. ∀[bs:bag(T)].  (#y in bag-drop(eq;bs;x)) = (#y in bs) ∈ ℕ supposing ¬(x = y ∈ T)

Lemma: bag-drop-commutes
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
  (bag-drop(eq;bag-drop(eq;bs;x);y) = bag-drop(eq;bag-drop(eq;bs;y);x) ∈ bag(T))

Lemma: bag-drop-head
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  (bag-drop(eq;[x / bs];x) ~ bs)

Lemma: bag-drop-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bag-no-repeats(T;bag-drop(eq;bs;x)) supposing bag-no-repeats(T;bs)

Lemma: bag-drop-property2
∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    (bag-no-repeats(T;bs)
    ⇒ x ↓∈ bs
    ⇒ {(bs = ({x} + bag-drop(eq;bs;x)) ∈ bag(T)) ∧ bag-no-repeats(T;bag-drop(eq;bs;x)) ∧ (¬x ↓∈ bag-drop(eq;bs;x))})

Lemma: bag-summation-constant-int
∀[T:Type]. ∀[a:ℤ]. ∀[bs:bag(T)].  (Σ(x∈bs). a = (#(bs) * a) ∈ ℤ)

Lemma: bag-size-as-summation
∀T:Type. ∀bs:bag(T).  (#(bs) = Σ(x∈bs). 1 ∈ ℤ)

Lemma: bag-size-partition
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (#(bs) = Σ(x∈bag-remove-repeats(eq;bs)). (#x in bs) ∈ ℤ)

Definition: bag-diff
bag-diff(eq;bs;as) ==  bag-accum(r,a.case r of inl(b) => bag-remove1(eq;b;a) | inr(z) => r;inl bs;as)

Lemma: bag-diff_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  (bag-diff(eq;bs;as) ∈ bag(T)?)

Lemma: bag-diff-property
∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    case bag-diff(eq;bs;as) of inl(cs) => bs = (as + cs) ∈ bag(T) | inr(z) => ∀cs:bag(T). (¬(bs = (as + cs) ∈ bag(T)))

Lemma: bag-diff-equal-inl
∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    ∀[cs:bag(T)]. uiff(bag-diff(eq;bs;as) = (inl cs) ∈ (bag(T)?);bs = (as + cs) ∈ bag(T))

Lemma: bag-member-bag-diff
∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).  uiff(x ↓∈ bs;↑isl(bag-diff(eq;bs;{x})))

Lemma: bag-deq-member-bag-diff
∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).  (bag-deq-member(eq;x;bs) ~ isl(bag-diff(eq;bs;{x})))

Definition: bag-subtract
bag-subtract(eq;bs;as) ==  bag-accum(r,a.bag-drop(eq;r;a);bs;as)

Lemma: bag-subtract_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  (bag-subtract(eq;bs;as) ∈ bag(T))

Lemma: bag-subtract-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-subtract(eq;as + bs;as) = bs ∈ bag(T))

Lemma: bag-subtract-size
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].
  #(bag-subtract(eq;bs;as)) = (#(bs) - #(as)) ∈ ℤ supposing sub-bag(T;as;bs)

Lemma: bag-subtract-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  bag-no-repeats(T;bag-subtract(eq;bs;as)) supposing bag-no-repeats(T;bs)

Lemma: bag-subtract-member-if-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)]. ∀[x:T].
  uiff(x ↓∈ bag-subtract(eq;bs;as);x ↓∈ bs ∧ (¬x ↓∈ as)) supposing bag-no-repeats(T;bs)

Lemma: bag-size-filter-member-bound
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].
  #([x∈as|bag-deq-member(eq;x;bs)]) ≤ #(bs) supposing bag-no-repeats(T;as)

Definition: bag-partitions
bag-partitions(eq;bs) ==  let splits ⟵ bag-splits(bs) in bag-to-set(proddeq(bag-deq(eq);bag-deq(eq));splits)

Lemma: bag-partitions_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-partitions(eq;bs) ∈ bag(bag(T) × bag(T))) supposing valueall-type(T)

Lemma: no-repeats-bag-partitions
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].
  bag-no-repeats(bag(T) × bag(T);bag-partitions(eq;bs)) supposing valueall-type(T)

Lemma: bag-member-partitions
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[as,bs,cs:bag(T)].  uiff(<as, bs> ↓∈ bag-partitions(eq;cs);(as + bs) = cs ∈ bag(T)) 
  supposing valueall-type(T)

Lemma: bag-partitions-with-one-given
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[as,bs,cs:bag(T)].
    ([p∈bag-partitions(eq;cs)|bag-eq(eq;fst(p);as)] = {<as, bs>} ∈ bag(bag(T) × bag(T)))
    ∧ ([p∈bag-partitions(eq;cs)|bag-eq(eq;snd(p);bs)] = {<as, bs>} ∈ bag(bag(T) × bag(T))) 
    supposing (as + bs) = cs ∈ bag(T) 
  supposing valueall-type(T)

Lemma: bag-partitions-symmetry
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].
    (bag-map(λp.<snd(p), fst(p)>;bag-partitions(eq;bs)) = bag-partitions(eq;bs) ∈ bag(bag(T) × bag(T))) 
  supposing valueall-type(T)

Lemma: bag-partitions-assoc
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].
    (⋃x∈bag-partitions(eq;bs).bag-map(λy.<fst(x), y>;bag-partitions(eq;snd(x)))
    = bag-map(λ2p.<fst(snd(p)), snd(snd(p)), fst(p)>;⋃x∈bag-partitions(eq;bs).bag-map(λy.<snd(x), y>;bag-partitions(eq;f\000Cst(x))))
    ∈ bag(bag(T) × bag(T) × bag(T))) 
  supposing valueall-type(T)

Lemma: bag-partitions-cons
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[x:X]. ∀[b:bag(X)].
    (bag-partitions(eq;x.b)
    = (bag-map(λp.<x.fst(p), snd(p)>;[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
      + bag-map(λp.<fst(p), x.snd(p)>;bag-partitions(eq;b)))
    ∈ bag(bag(X) × bag(X))) 
  supposing valueall-type(X)

Lemma: bag-summation-partitions-primes-general
∀[r:CRng]. ∀[h:ℕ+ ⟶ ℕ+ ⟶ |r|]. ∀[b:bag(Prime)].
  (Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))] = let n = Π(b) in Σ i|n. h[i;n ÷ i] ∈ |r|)

Lemma: bag-summation-partitions-primes
∀[h:ℕ+ ⟶ ℕ+ ⟶ ℤ]. ∀[b:bag(Prime)].
  (Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))] = Σ i|Π(b). h[i;Π(b) ÷ i]  ∈ ℤ)

Definition: bag-parts
bag-parts(eq;bs) ==
  fix((λbag-parts,bs. let splits ⟵ bag-partitions(eq;bs)
                      in ⋃p∈splits.if bag-null(fst(p)) then {}
                         if bag-null(snd(p)) then {[fst(p)]}
                         else let parts ⟵ bag-parts (snd(p))
                              in bag-map(λL.[fst(p) / L];parts)
                         fi )) 
  bs

Lemma: bag-parts_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-parts(eq;bs) ∈ bag(bag(T) List+)) supposing valueall-type(T)

Lemma: bag-member-parts
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[L:bag(T) List+].
    uiff(L ↓∈ bag-parts(eq;bs);(bag-union(L) = bs ∈ bag(T)) ∧ (∀x∈L.¬(x = {} ∈ bag(T)))) 
  supposing valueall-type(T)

Lemma: bag-parts-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(bag(T) List+;bag-parts(eq;bs)) supposing valueall-type(T)

Definition: bag-parts'
bag-parts'(eq;bs;x) ==
  if bag-null(bs)
  then {[bs]}
  else let pts ⟵ bag-parts(eq;bs)
       in bag-map(λL.[{} / L];pts) + [L∈pts|((#x in hd(L)) =z 0)]
  fi 

Lemma: bag-parts'_wf
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-parts'(eq;bs;x) ∈ bag(bag(T) List+)) supposing valueall-type(T)

Lemma: bag-member-parts'
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)]. ∀[L:bag(T) List+].
    uiff(L ↓∈ bag-parts'(eq;bs;x);(¬x ↓∈ hd(L)) ∧ (∀x∈tl(L).¬(x = {} ∈ bag(T))) ∧ (bag-union(L) = bs ∈ bag(T))) 
  supposing valueall-type(T)

Lemma: bag-parts'_wf2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-parts'(eq;bs;x) ∈ bag({L:bag(T) List+| ¬x ↓∈ hd(L)} )) suppos\000Cing valueall-type(T)

Lemma: bag-parts'-no-repeats
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  bag-no-repeats(bag(T) List+;bag-parts'(eq;bs;x)) supposing valueall-type(T)

Lemma: sub-bag-iff
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:bag(T).  (sub-bag(T;as;bs) ⇐⇒ ∀x:T. ((#x in as) ≤ (#x in bs)))

Lemma: bag-count-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  uiff(1 ≤ (#x in b);x ↓∈ b)

Lemma: sub-bag-no-repeats-iff
∀[T:Type]. ∀eq:EqDecider(T). ∀b1,b2:bag(T).  (bag-no-repeats(T;b1) ⇒ (∀x:T. (x ↓∈ b1 ⇒ x ↓∈ b2) ⇐⇒ sub-bag(T;b1;b2)))

Lemma: sub-bag-remove-repeats-if-no-repeats
∀[T:Type]
  ∀eq:EqDecider(T). ∀b1,b2:bag(T).
    (bag-no-repeats(T;b1) ⇒ sub-bag(T;b1;b2) ⇒ sub-bag(T;b1;bag-remove-repeats(eq;b2)))

Definition: bag-has-no-repeats
bag-has-no-repeats(eq;b) ==  (#(bag-remove-repeats(eq;b)) =z #(b))

Lemma: bag-has-no-repeats_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].  (bag-has-no-repeats(eq;b) ∈ 𝔹)

Lemma: assert-bag-has-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].  (↑bag-has-no-repeats(eq;b) ⇐⇒ bag-no-repeats(T;b))

Lemma: decidable__sub-bag
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀as,bs:bag(T).  Dec(sub-bag(T;as;bs))))

Definition: deq-sub-bag
deq-sub-bag(eq;as;bs) ==
  case TERMOF{decidable__sub-bag:o, 1:l, 1:l} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff

Lemma: deq-sub-bag_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (deq-sub-bag(eq;as;bs) ∈ 𝔹)

Lemma: assert-deq-sub-bag
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:bag(T).  (↑deq-sub-bag(eq;as;bs) ⇐⇒ sub-bag(T;as;bs))

Definition: bag-lub
bag-lub(eq;b1;b2) ==  ⋃x∈bag-to-set(eq;b1 + b2).bag-rep(imax((#x in b1);(#x in b2));x)

Lemma: bag-lub_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,as:bag(T)].  (bag-lub(eq;bs;as) ∈ bag(T))

Lemma: bag-lub-comm
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-lub(eq;as;bs) = bag-lub(eq;bs;as) ∈ bag(T))

Lemma: bag-count-bag-lub
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)]. ∀[x:T].  ((#x in bag-lub(eq;as;bs)) = imax((#x in as);(#x in bs)) ∈ ℤ)

Lemma: bag-lub-property
∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    (sub-bag(T;as;bag-lub(eq;as;bs))
    ∧ sub-bag(T;bs;bag-lub(eq;as;bs))
    ∧ (∀cs:bag(T). (sub-bag(T;as;cs) ⇒ sub-bag(T;bs;cs) ⇒ sub-bag(T;bag-lub(eq;as;bs);cs))))

Lemma: sub-bag-lub
∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs,cs:bag(T).  ((sub-bag(T;cs;as) ∨ sub-bag(T;cs;bs)) ⇒ sub-bag(T;cs;bag-lub(eq;as;bs)))

Definition: sub-bags
sub-bags(eq;bs) ==  bag-map(λp.(fst(p));bag-partitions(eq;bs))

Lemma: sub-bags_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (sub-bags(eq;bs) ∈ bag(bag(T))) supposing valueall-type(T)

Lemma: member-sub-bags
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,b:bag(T)].  uiff(b ↓∈ sub-bags(eq;bs);↓sub-bag(T;b;bs)) supposing valueall-type(T)

Lemma: sub-bags-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  bag-no-repeats(bag(T);sub-bags(eq;bs)) supposing valueall-type(T)

Lemma: bag-dickson-lemma
∀p:ℕ. ∀[T:Type]. (T ~ ℕp ⇒ (∀A:ℕ ⟶ bag(T). ∃j:ℕ. ∃i:ℕj. sub-bag(T;A[i];A[j])))

Lemma: bag-ordering-wellfounded
∀p:ℕ
  ∀[T:Type]
    (T ~ ℕp
    ⇒ (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]
          (Trans(bag(T);a,b.R[a;b])
          ⇒ (∀a,b:bag(T).  Dec(R[a;b]))
          ⇒ (∀a,b:bag(T).  (sub-bag(T;a;b) ⇒ (¬R[b;a])))
          ⇒ WellFnd{i}(bag(T);a,b.R[a;b]))))

Lemma: bag-admissable-well-founded
∀k:ℕ
  ∀[T:Type]
    (T ~ ℕk
    ⇒ (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]
          ((∀as,bs:bag(T).  Dec(R[as;bs]))
          ⇒ Order(bag(T);as,bs.R[as;bs])
          ⇒ bag-admissable(T;as,bs.R[as;bs])
          ⇒ WellFnd{i}(bag(T);as,bs.R[as;bs] ∧ (¬(as = bs ∈ bag(T)))))))

Definition: bag-restrict
(b|x) ==  [z∈b|eq x z]

Lemma: bag-restrict_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  ((b|x) ∈ bag(T))

Lemma: bag-restrict-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b,c:bag(T)].  ((b + c|x) ~ (b|x) + (c|x))

Lemma: bag-size-restrict
∀[T:Type]. ∀[b:bag(T)]. ∀[eq:EqDecider(T)]. ∀[x:T].  (#((b|x)) ~ (#x in b))

Lemma: bag-rep-size-restrict
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (bag-rep(#((b|x));x) = (b|x) ∈ bag(T))

Definition: bag-co-restrict
(b|¬x) ==  [z∈b|¬b(eq x z)]

Lemma: bag-co-restrict_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  ((b|¬x) ∈ bag(T))

Lemma: bag-co-restrict-property
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (¬x ↓∈ (b|¬x))

Lemma: bag-co-restrict-append
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b,c:bag(T)].  ((b + c|¬x) ~ (b|¬x) + (c|¬x))

Lemma: bag-co-restrict-rep
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[n:ℕ].  ((bag-rep(n;x)|¬x) ~ {})

Lemma: bag-co-restrict-disjoint
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b|¬x) = b ∈ bag(T) supposing ¬x ↓∈ b

Lemma: bag-drop-co-restrict
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[x:X]. ∀[b:bag(X)].  ((bag-drop(eq;b;x)|¬x) = (b|¬x) ∈ bag(X))

Lemma: bag-restrict-disjoint
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b|x) ~ {} supposing ¬x ↓∈ b

Lemma: bag-restrict-rep
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[n:ℕ].  ((bag-rep(n;x)|x) ~ bag-rep(n;x))

Lemma: bag-restrict-split
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b = ((b|x) + (b|¬x)) ∈ bag(T))

Lemma: bag-restrict-size-bound
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].
  (((#((b|x)) + #((b|¬x))) = #(b) ∈ ℤ) ∧ (#((b|¬x)) ≤ #(b)) ∧ (#((b|x)) ≤ #(b)))

Lemma: bag-no-repeats-supertype
∀[T,S:Type]. ∀[bs:bag(S)].  bag-no-repeats(T;bs) supposing strong-subtype(S;T) ∧ bag-no-repeats(S;bs)

Lemma: equipollent-choose
∀n,m:ℕ.  ((m ≤ n) ⇒ UnorderedCombination(m;ℕn) ~ ℕchoose(n;m))

Lemma: count-unordered-combinations
∀[T:Type]
  ∀n,m:ℕ.
    (T ~ ℕn
    ⇒ (UnorderedCombination(m;T) ~ ℕchoose(n;m) supposing m ≤ n ∧ UnorderedCombination(m;T) ~ ℕ0 supposing n < m))

Definition: bag-moebius
bag-moebius(eq;b) ==  if bag-has-no-repeats(eq;b) then if (#(b) rem 2 =z 0) then 1 else -1 fi  else 0 fi 

Lemma: bag-moebius_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].  (bag-moebius(eq;b) ∈ ℤ)

Lemma: bag-moebius-no-repeats
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
  bag-moebius(eq;b) ~ if (#(b) rem 2 =z 0) then 1 else -1 fi  supposing ↑bag-has-no-repeats(eq;b)

Lemma: bag-moebius-property1
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].  (Σ(c∈sub-bags(eq;b)). bag-moebius(eq;c) = if bag-null(b) then 1 else 0 fi  ∈ ℤ) 
  supposing valueall-type(T)

Lemma: bag-moebius-property
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
    (bag-moebius(eq;b)
    = if bag-null(b) then 1 else -Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p)) fi 
    ∈ ℤ) 
  supposing valueall-type(T)

Definition: bag-lex
bag-lex(n;f;g) ==
  λas,bs. primrec(n;0;λm,v. if v=0 then eval i = (#g m in as) in eval j = (#g m in bs) in   i - j else v)



Home Index