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 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 then else fi  ∈ ℤ)

Lemma: bag-count-cons
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[b:bag(T)].
  ((#x in y.b) if eq then (#x in b) 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) 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 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 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 then else 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 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
  ∀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 <(#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 <(#x in bs) then else 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 <(#x in bs) then else 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 ==  [y∈bs|¬b(eq 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 as bs x)

Lemma: bag-remove-trivial
[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  bs 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
  ∀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
  ∀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' then inl (checked as') else bag_remove1_aux [a' checked] as' fi  

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

Lemma: bag_remove1_aux_property
  ∀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) ∈ List?)

Lemma: bag-remove1-property1
  ∀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
  ∀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 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
  ∀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
  ∀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
  ∀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
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
     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). (#(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, 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
  ∀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
  ∀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
  ∀[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
  ∀[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
  ∀[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
  ∀[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
  ∀[eq:EqDecider(X)]. ∀[x:X]. ∀[b:bag(X)].
    (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 = Π(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 )) 

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
  ∀[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)]

Lemma: bag-parts'_wf
  ∀[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'
  ∀[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
  ∀[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
  ∀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
  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    ∧ 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
  ∀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 ~ ℕ (∀A:ℕ ⟶ bag(T). ∃j:ℕ. ∃i:ℕj. sub-bag(T;A[i];A[j])))

Lemma: bag-ordering-wellfounded
    (T ~ ℕp
     (∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]
           (∀a,b:bag(T).  Dec(R[a;b]))
           (∀a,b:bag(T).  (sub-bag(T;a;b)  R[b;a])))

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

Definition: bag-restrict
(b|x) ==  [z∈b|eq 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 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 ~ ℕn
     (UnorderedCombination(m;T) ~ ℕchoose(n;m) supposing m ≤ n ∧ UnorderedCombination(m;T) ~ ℕsupposing n < m))

Definition: bag-moebius
bag-moebius(eq;b) ==  if bag-has-no-repeats(eq;b) then if (#(b) rem =z 0) then else -1 fi  else 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 =z 0) then else -1 fi  supposing ↑bag-has-no-repeats(eq;b)

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

Lemma: bag-moebius-property
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
    if bag-null(b) then 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 (#g in as) in eval (#g in bs) in   else v)

Home Index