Definition: bag
`bag(T) ==  as,bs:T List//permutation(T;as;bs)`

Lemma: bag_wf
`∀[T:Type]. (bag(T) ∈ Type)`

Lemma: bag-valueall-type
`∀[T:Type]. valueall-type(bag(T)) supposing valueall-type(T)`

Lemma: bag-value-type
`∀[T:Type]. value-type(bag(T))`

Lemma: list-subtype-bag
`∀[A,B:Type].  (A List) ⊆r bag(B) supposing A ⊆r B`

Lemma: bag-subtype-fset
`∀[A:Type]. (bag(A) ⊆r fset(A))`

Lemma: bag-subtype-list
`∀T:Type. (bag(T) ⊆r (Top List))`

Lemma: bag-equality
`∀[A,B:Type]. ∀[f,g:bag(A) ⟶ bag(B)].  ∀[b:bag(A)]. (f[b] = g[b] ∈ bag(B)) supposing ∀[b:A List]. (f[b] = g[b] ∈ bag(B))`

Lemma: bag_to_squash_list
`∀[T:Type]. ∀[b:bag(T)].  (↓∃L:T List. (b = L ∈ bag(T)))`

Lemma: respects-equality-bag
`∀[A,B:Type].  respects-equality(bag(A);bag(B)) supposing respects-equality(A;B)`

Lemma: respects-equality-list-bag
`∀[A,B:Type].  respects-equality(A List;bag(B)) supposing respects-equality(A;B)`

Definition: eval_bag
`eval_bag(b) ==  eval_list(b)`

Lemma: eval_bag_wf
`∀[T:Type]. ∀[b:bag(T)].  (eval_bag(b) ∈ bag(T))`

Definition: mk_bag
`mk_bag(L) ==  L`

Lemma: mk_bag_wf
`∀[T:Type]. ∀[L:T List].  (mk_bag(L) ∈ bag(T))`

Definition: empty-bag
`{} ==  []`

Lemma: empty-bag_wf
`∀[T:Type]. ({} ∈ bag(T))`

Lemma: empty-bag-wf-list-test
`∀[T:Type]. ({} ∈ T List)`

Lemma: equal-empty-bag
`∀[T:Type]. ∀x:bag(T). ((x = {} ∈ bag(T)) `` (x ~ {}))`

Lemma: bag-void-sq-empty
`∀[T:Type]. ∀x:bag(T). x ~ {} supposing ¬T`

Definition: single-bag
`{x} ==  [x]`

Lemma: single-bag_wf
`∀T:Type. ∀x:T.  ({x} ∈ bag(T))`

Definition: cons-bag
`x.b ==  [x / b]`

Lemma: cons-bag_wf
`∀[T:Type]. ∀[x:T]. ∀[b:bag(T)].  (x.b ∈ bag(T))`

Lemma: cons_bag_empty_lemma
`∀x:Top. (x.{} ~ {x})`

Lemma: reverse-bag
`∀[T:Type]. ∀[b:bag(T)].  (rev(b) = b ∈ bag(T))`

Definition: bag-upto
`bag-upto(n) ==  upto(n)`

Lemma: bag-upto_wf
`∀[n:ℤ]. (bag-upto(n) ∈ bag(ℤ))`

Definition: bag-map
`bag-map(f;bs) ==  map(f;bs)`

Lemma: bag-map_wf
`∀[B,A:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (bag-map(f;bs) ∈ bag(B))`

Lemma: bag_map_empty_lemma
`∀f:Top. (bag-map(f;{}) ~ {})`

Lemma: bag_map_single_lemma
`∀x,f:Top.  (bag-map(f;{x}) ~ {f x})`

Lemma: subtype_rel_bag
`∀[B,A:Type].  bag(A) ⊆r bag(B) supposing A ⊆r B`

Definition: bag-append
`as + bs ==  as @ bs`

Lemma: bag-append_wf
`∀[T:Type]. ∀[as,bs:bag(T)].  (as + bs ∈ bag(T))`

Lemma: bag-append-comm
`∀[T:Type]. ∀[as,bs:bag(T)].  ((as + bs) = (bs + as) ∈ bag(T))`

Lemma: bag-append-assoc
`∀[as,bs,cs:Top].  ((as + bs) + cs ~ as + bs + cs)`

Lemma: bag-append-assoc2
`∀[as,bs,cs:Top].  (as + bs + cs ~ (as + bs) + cs)`

Lemma: bag-append-assoc-comm
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  ((as + bs + cs) = (bs + as + cs) ∈ bag(T))`

Lemma: bag-append-comm-assoc
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  ((as + bs + cs) = ((as + cs) + bs) ∈ bag(T))`

Lemma: bag-append-empty
`∀[as:Top List]. (as + {} ~ as)`

Lemma: bag-append-cancel
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  uiff((as + bs) = (as + cs) ∈ bag(T);bs = cs ∈ bag(T))`

Lemma: empty_bag_append_lemma
`∀b:Top. ({} + b ~ b)`

Lemma: cons_bag_append_lemma
`∀b2,b1,x:Top.  (x.b1 + b2 ~ x.b1 + b2)`

Lemma: bag-empty-append
`∀[as:Top]. ({} + as ~ as)`

Lemma: bag-append-ident
`∀[T:Type]. ∀[as:bag(T)].  (((as + {}) = as ∈ bag(T)) ∧ (({} + as) = as ∈ bag(T)))`

Lemma: bag-append-eq-empty
`∀[T:Type]. ∀[b1,b2:bag(T)].  uiff((b1 + b2) = {} ∈ bag(T);(b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T)))`

Lemma: bag-append-ac
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  ((as + bs + cs) = (bs + as + cs) ∈ bag(T))`

Lemma: cons-bag-as-append
`∀[x,b:Top].  (x.b ~ {x} + b)`

Lemma: bag-function
`∀[T,A:Type]. ∀[f:(T List) ⟶ bag(A)].`
`  f ∈ bag(T) ⟶ bag(A) supposing ∀as,bs:T List.  (f[as @ bs] = (f[as] + f[bs]) ∈ bag(A))`

Definition: bag-product
`bs × cs ==  rec-case(bs) of [] => {} | b::as => r.bag-map(λx.<b, x>;cs) + r`

Lemma: bag-product_wf
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)].  (as × bs ∈ bag(A × B))`

Lemma: bag-product-empty
`∀[bs:Top]. ({} × bs ~ {})`

Lemma: bag-product-single
`∀[bs:Top List]. ∀[a:Top].  ({a} × bs ~ bag-map(λx.<a, x>;bs))`

Lemma: bag-product-append
`∀[as,bs,cs:Top List].  (as + bs × cs ~ as × cs + bs × cs)`

Definition: bag-filter
`[x∈b|p[x]] ==  filter(λx.p[x];b)`

Lemma: bag-filter_wf
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  ([x∈bs|p[x]] ∈ bag({x:T| ↑p[x]} ))`

Lemma: bag-filter-wf3
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  ([x∈bs|p[x]] ∈ bag(T))`

Lemma: bag-filter-is-nil
`∀[T:Type]. ∀[p:T ⟶ 𝔹].  ∀[bs:bag(T)]. ([x∈bs|p[x]] ~ []) supposing ∀x:T. (¬↑p[x])`

Lemma: bag-filter-trivial
`∀[T:Type]. ∀[p:T ⟶ 𝔹].  ∀[bs:bag(T)]. ([x∈bs|p[x]] = bs ∈ bag(T)) supposing ∀x:T. (↑p[x])`

Lemma: bag-filter-append
`∀[p,as,bs:Top].  ([x∈as + bs|p[x]] ~ [x∈as|p[x]] + [x∈bs|p[x]])`

Lemma: bag-filter-filter
`∀[p,q,bs:Top].  ([x∈[x∈bs|p[x]]|q[x]] ~ [x∈bs|p[x] ∧b q[x]])`

Lemma: bag-filter-filter2
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[q:{x:T| ↑p[x]}  ⟶ 𝔹]. ∀[bs:bag(T)].`
`  ([x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} ))`

Lemma: bag-filter-singleton
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[v:T].  ([x∈{v}|p[x]] ~ if p[v] then {v} else {} fi )`

Lemma: bag-filter-split
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (([x∈bs|p[x]] + [x∈bs|¬bp[x]]) = bs ∈ bag(T))`

Lemma: bag-filter-map
`∀[f,p,as:Top].  ([x∈bag-map(f;as)|p[x]] ~ bag-map(f;[x∈as|p[f x]]))`

Lemma: bag-filter-map2
`∀[T,A:Type]. ∀[f:A ⟶ T]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(A)].`
`  ([x∈bag-map(f;as)|p[x]] = bag-map(f;[x∈as|p[f x]]) ∈ bag({x:T| ↑p[x]} ))`

Lemma: bag_filter_empty_lemma
`∀p:Top. ([x∈{}|p[x]] ~ {})`

Lemma: bag_filter_cons_lemma
`∀p,v,u:Top.  ([x∈u.v|p[x]] ~ if p[u] then u.[x∈v|p[x]] else [x∈v|p[x]] fi )`

Lemma: test-bag-filter-empty
`∀[p:Top]. ([b∈{}|p[b]] ~ {})`

Lemma: bag-split
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(T)].  (as = ([x∈as|p[x]] + [x∈as|¬bp[x]]) ∈ bag(T))`

Lemma: bag-map-null
`∀f,bs:Top.  (null(bag-map(f;bs)) ~ null(bs))`

Definition: bag-mapfilter
`bag-mapfilter(f;P;bs) ==  bag-map(f;[x∈bs|P x])`

Lemma: bag-mapfilter_wf
`∀[T,A:Type].  ∀P:T ⟶ 𝔹. ∀f:{x:T| ↑(P x)}  ⟶ A. ∀bs:bag(T).  (bag-mapfilter(f;P;bs) ∈ bag(A))`

Lemma: bag-mapfilter-null
`∀P,f,bs:Top.  (null(bag-mapfilter(f;P;bs)) ~ null([x∈bs|P x]))`

Lemma: bag-mapfilter-empty
`∀P,f:Top.  (bag-mapfilter(f;P;{}) ~ {})`

Definition: bag-null
`bag-null(bs) ==  null(bs)`

Lemma: bag-null_wf
`∀T:Type. ∀bs:bag(T).  (bag-null(bs) ∈ 𝔹)`

Lemma: bag_null_empty_lemma
`bag-null({}) ~ tt`

Lemma: bag_null_cons_lemma
`∀v,u:Top.  (bag-null(u.v) ~ ff)`

Lemma: bag-null-append
`∀[T:Type]. ∀[as,bs:bag(T)].  bag-null(as + bs) = bag-null(as) ∧b bag-null(bs)`

Lemma: assert-bag-null
`∀[T:Type]. ∀[bs:bag(T)].  uiff(↑bag-null(bs);bs = {} ∈ bag(T))`

Lemma: null-bag-mapfilter
`∀P,f,bs:Top.  (bag-null(bag-mapfilter(f;P;bs)) ~ bag-null([x∈bs|P x]))`

Lemma: bag-map-equal
`∀[T,A:Type].`
`  ∀f,g:T ⟶ A. ∀P:T ⟶ 𝔹.`
`    ((∀x:T. ((¬↑(P x)) `` ((f x) = (g x) ∈ A)))`
`    `` (∀as:bag(T). ((↑null([x∈as|P x])) `` (bag-map(f;as) = bag-map(g;as) ∈ bag(A)))))`

Lemma: null-bag-filter-map
`∀[T,A:Type]. ∀[f:A ⟶ T]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(A)].  null([x∈bag-map(f;as)|p[x]]) = null([x∈as|p[f x]])`

Definition: bag-size
`#(bs) ==  ||bs||`

Lemma: bag-size_wf
`∀[C:Type]. ∀[bs:bag(C)].  (#(bs) ∈ ℕ)`

Lemma: bag_size_single_lemma
`∀x:Top. (#({x}) ~ 1)`

Lemma: bag_size_cons_lemma
`∀b,x:Top.  (#(x.b) ~ #(b) + 1)`

Lemma: bag-size-map
`∀[bs,f:Top].  (#(bag-map(f;bs)) ~ #(bs))`

Lemma: bag-size-append
`∀[as,bs:Top].  (#(as + bs) ~ #(as) + #(bs))`

Lemma: bag-size-cons
`∀[b:bag(Top)]. ∀[x:Top].  (#(x.b) ~ 1 + #(b))`

Lemma: bag-size-zero
`∀[C:Type]. ∀[bs:bag(C)].  bs ~ {} supposing #(bs) ≤ 0`

Lemma: bag_size_empty_lemma
`#({}) ~ 0`

Lemma: bag-size-is-zero
`∀[C:Type]. ∀[bs:bag(C)].  bs ~ {} supposing #(bs) = 0 ∈ ℤ`

Lemma: bag-size-bound
`∀[T:Type]. ∀[as,bs:bag(T)]. ∀[n:ℕ].  #(as + bs) - n < #(bs) supposing #(as) < n`

Lemma: null-bag
`∀[T:Type]. ∀[x:bag(T)].  uiff(↑null(x);x = {} ∈ bag(T))`

Lemma: assert-bag-null-sq
`∀bs:bag(Top). ((↑bag-null(bs)) `` (bs ~ {}))`

Lemma: smallbag-subtype-list
`∀T:Type. ({b:bag(T)| #(b) < 2}  ⊆r {b:T List| ||b|| < 2} )`

Lemma: bag-cases
`∀[T:Type]. ∀bs:bag(T). ((bs = {} ∈ bag(T)) ∨ (↓∃x:T. ∃bs':bag(T). (bs = ({x} + bs') ∈ bag(T))))`

Lemma: null-bag-size
`∀[T:Type]. ∀[x:bag(T)].  (bag-null(x) ~ (#(x) =z 0))`

Lemma: bag-map-append
`∀[as:bag(Top)]. ∀[bs,f:Top].  (bag-map(f;as + bs) ~ bag-map(f;as) + bag-map(f;bs))`

Lemma: bag-map-cons
`∀[b,x,f:Top].  (bag-map(f;x.b) ~ f x.bag-map(f;b))`

Lemma: bag-map-single
`∀[x,f:Top].  (bag-map(f;{x}) ~ {f x})`

Lemma: bag-map-map
`∀[as,f,g:Top].  (bag-map(f;bag-map(g;as)) ~ bag-map(f o g;as))`

Lemma: bag-map-filter
`∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].`
`  ∀[L:bag(T)]. (bag-map(f;[x∈L|P[x]]) = [x∈bag-map(f;L)|Q[x]] ∈ bag(A)) supposing ∀x:T. Q[f x] = P[x]`

Lemma: bag-map-trivial
`∀[A:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ A].  bag-map(f;as) = as ∈ bag(A) supposing ∀x:A. ((f x) = x ∈ A)`

Lemma: bag-mapfilter-append
`∀[T:Type]. ∀[a:bag(T)]. ∀[b:bag(Top)]. ∀[f:Top]. ∀[P:T ⟶ 𝔹].`
`  (bag-mapfilter(f;P;a + b) ~ bag-mapfilter(f;P;a) + bag-mapfilter(f;P;b))`

Lemma: bag-mapfilter-map
`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:B ⟶ 𝔹]. ∀[f:{x:B| ↑P[x]}  ⟶ C]. ∀[g:A ⟶ B].`
`  (bag-mapfilter(f;P;bag-map(g;b)) = bag-mapfilter(f o g;P o g;b) ∈ bag(C))`

Lemma: bag-map-mapfilter
`∀[b,P,f,g:Top].  (bag-map(g;bag-mapfilter(f;P;b)) ~ bag-mapfilter(g o f;P;b))`

Lemma: bag-mapfilter-mapfilter
`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B]. ∀[Q:B ⟶ 𝔹]. ∀[g:{x:B| ↑Q[x]}  ⟶ C].`
`  (bag-mapfilter(g;Q;bag-mapfilter(f;P;b)) = bag-mapfilter(g o f;λx.(P[x] ∧b Q[f[x]]);b) ∈ bag(C))`

Definition: bagp
`T Bag+ ==  {b:bag(T)| 0 < #(b)} `

Lemma: bagp_wf
`∀[T:Type]. (T Bag+ ∈ Type)`

Lemma: bagp_properties
`∀[T:Type]. ∀[b:T Bag+].  (#(b) ≥ 1 )`

Definition: bag-val
`bag-val(zero;+) ==  λb.accumulate (with value v and list item x): v + xover list:  bwith starting value: zero)`

Lemma: bag-val_wf
`∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].  (Comm(T;+) `` Assoc(T;+) `` Ident(T;+;zero) `` (bag-val(zero;+) ∈ bag(T) ⟶ T))`

Lemma: bag-val-empty
`∀[+,zero:Top].  (bag-val(zero;+) {} ~ zero)`

Lemma: bag-val-append
`∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].`
`  (Comm(T;+)`
`  `` Assoc(T;+)`
`  `` Ident(T;+;zero)`
`  `` (∀[as,bs:bag(T)].  ((bag-val(zero;+) (as + bs)) = ((bag-val(zero;+) as) + (bag-val(zero;+) bs)) ∈ T)))`

Definition: bag-union
`bag-union(bbs) ==  concat(bbs)`

Lemma: bag-union_wf
`∀[T:Type]. ∀[bbs:bag(bag(T))].  (bag-union(bbs) ∈ bag(T))`

Lemma: bag_union_empty_lemma
`bag-union({}) ~ {}`

Lemma: bag_union_cons_lemma
`∀v,u:Top.  (bag-union(u.v) ~ u + bag-union(v))`

Lemma: bag-union-bagp
`∀[T:Type]. ∀[bbs:bag(bag(T))].  (0 < #([b∈bbs|0 <z #(b)]) `` (bag-union(bbs) ∈ T Bag+))`

Lemma: bag-induction
`∀[T:Type]. ∀[P:bag(T) ⟶ ℙ].  ((∀x:T. P[[x]]) `` (∀bs:bag({b:bag(T)| P[b]} ). P[bag-union(bs)]) `` (∀b:bag(T). P[b]))`

Lemma: bag-filter-union
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bbs:bag(bag(T))].`
`  ([x∈bag-union(bbs)|p[x]] = bag-union(bag-map(λb.[x∈b|p[x]];bbs)) ∈ bag({x:T| ↑p[x]} ))`

Lemma: bag-filter-union2
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bbs:bag(bag(T))].  ([x∈bag-union(bbs)|p[x]] = bag-union(bag-map(λb.[x∈b|p[x]];bbs)) ∈ bag(T))`

Lemma: bag-map-union
`∀[T,S:Type]. ∀[f:T ⟶ bag(S)]. ∀[bbs:bag(bag(T))].`
`  (bag-map(f;bag-union(bbs)) = bag-union(bag-map(λb.bag-map(f;b);bbs)) ∈ bag(bag(S)))`

Lemma: bag-append-union
`∀[T:Type]. ∀as,bs:bag(bag(T)).  (bag-union(as + bs) = (bag-union(as) + bag-union(bs)) ∈ bag(T))`

Lemma: bag-union-single
`∀x:Top List. (bag-union({x}) ~ x)`

Lemma: bag-append-is-single
`∀[T:Type]. ∀[x:T].`
`  ∀as,bs:bag(T).`
`    ↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T))) ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))) `
`    supposing (as + bs) = {x} ∈ bag(T)`

Lemma: bag-append-is-single-iff
`∀[T:Type]. ∀[x:T].`
`  ∀as,bs:bag(T).`
`    uiff((as + bs) = {x} ∈ bag(T);↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))`
`                                   ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))))`

Lemma: bag-append-is-single-iff2
`∀[T:Type]. ∀[x:T].`
`  ∀as,bs:bag(T).`
`    uiff({x} = (as + bs) ∈ bag(T);↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))`
`                                   ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))))`

Lemma: bag-append-is-empty
`∀[T:Type]. ∀as,bs:bag(T).  uiff((as + bs) = {} ∈ bag(T);(as = {} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))`

Lemma: bag-union-is-single-if
`∀[T:Type]. ∀[x:T].  ∀bbs:bag(bag(T)). bag-union(bbs) = {x} ∈ bag(T) supposing bbs = {{x}} ∈ bag(bag(T))`

Lemma: bag-union-is-single
`∀[T:Type]. ∀[x:T].`
`  ∀bbs:bag(bag(T))`
`    uiff(bag-union(bbs) = {x} ∈ bag(T);↓∃bbs':bag(bag(T))`
`                                         ((bbs = {x}.bbs' ∈ bag(bag(T))) ∧ (bag-union(bbs') = {} ∈ bag(T))))`

Lemma: bag-union-cons
`∀[b,a:Top].  (bag-union(a.b) ~ a + bag-union(b))`

Lemma: bag-union-append
`∀[A:Type]. ∀[b1,b2:bag(bag(A))].  (bag-union(b1 + b2) = (bag-union(b1) + bag-union(b2)) ∈ bag(A))`

Lemma: non-empty-bag-union-of-list
`∀[T:Type]. ∀L:bag(T) List. (0 < #(bag-union(L)) `⇐⇒` (∃b∈L. 0 < #(b)))`

Lemma: non-empty-bag-mapfilter-union-of-list
`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀f:T ⟶ Top. ∀L:bag(T) List.  (0 < #(bag-mapfilter(f;λx.P[x];bag-union(L))) `⇐⇒` (∃b∈L. 0 < #([x∈b|P[x]])))`

Definition: bag-combine
`⋃x∈bs.f[x] ==  bag-union(bag-map(λx.f[x];bs))`

Lemma: bag-combine_wf
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)].  (⋃x∈bs.f[x] ∈ bag(B))`

Lemma: bag_combine_empty_lemma
`∀f:Top. (⋃x∈{}.f[x] ~ {})`

Lemma: strict4-bag-combine
`strict4(λx,y,z,w. ⋃b∈x.y[b])`

Lemma: bag-combine-assoc
`∀[f,g:Top]. ∀[bs:bag(Top)].  (⋃y∈⋃x∈bs.f[x].g[y] ~ ⋃x∈bs.⋃y∈f[x].g[y])`

Lemma: bag-combine-unit-left
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A].  (⋃x∈[a].f[x] ~ f[a])`

Lemma: bag-combine-unit-left-top
`∀[f,a:Top].  (⋃x∈[a].f[x] ~ f[a] + {})`

Lemma: bag-combine-single-left
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A].  (⋃x∈{a}.f[x] ~ f[a])`

Lemma: bag-combine-empty-left
`∀[f:Top]. (⋃x∈{}.f[x] ~ {})`

Lemma: bag-combine-empty-right
`∀[T:Type]. ∀[bs:bag(T)].  (⋃x∈bs.{} ~ {})`

Lemma: bag-combine-unit-right
`∀[A:Type]. ∀[bs:bag(A)].  (⋃x∈bs.[x] ~ bs)`

Lemma: bag-combine-single-right
`∀[A:Type]. ∀[bs:bag(A)].  (⋃x∈bs.{x} ~ bs)`

Lemma: bag-combine-single-right-as-map
`∀[bs,f:Top].  (⋃x∈bs.{f[x]} ~ bag-map(λx.f[x];bs))`

Lemma: bag-combine-append-left
`∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)].  (⋃x∈ba + bb.f[x] = (⋃x∈ba.f[x] + ⋃x∈bb.f[x]) ∈ bag(B))`

Lemma: bag-combine-append-right
`∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].  (⋃x∈ba.F[x] + G[x] = (⋃x∈ba.F[x] + ⋃x∈ba.G[x]) ∈ bag(B))`

Lemma: bag-combine-cons-left
`∀[b,a,f:Top].  (⋃x∈a.b.f[x] ~ f[a] + ⋃x∈b.f[x])`

Lemma: bag-combine-com
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[ba:bag(A)]. ∀[bb:bag(B)].  (⋃a∈ba.⋃b∈bb.f[a;b] = ⋃b∈bb.⋃a∈ba.f[a;b] ∈ bag(C))`

Lemma: bag-combine-filter
`∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]}  ⟶ bag(B)]. ∀[ba:bag(A)].`
`  (⋃a∈[a∈ba|p[a]].f[a] = ⋃a∈ba.if p[a] then f[a] else {} fi  ∈ bag(B))`

Lemma: bag-map-combine
`∀[A,B,C:Type]. ∀[g:A ⟶ bag(B)]. ∀[f:B ⟶ C]. ∀[bs:bag(A)].  (bag-map(f;⋃x∈bs.g[x]) = ⋃x∈bs.bag-map(f;g[x]) ∈ bag(C))`

Lemma: bag-combine-map
`∀[A,B,C:Type]. ∀[g:B ⟶ bag(C)]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (⋃x∈bag-map(f;bs).g[x] = ⋃x∈bs.g[f x] ∈ bag(C))`

Lemma: bag-combine-is-single-if
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)]. ∀[x:B].`
`  ⋃x∈bs.f[x] = {x} ∈ bag(B) supposing ↓∃y:A. ((bs = {y} ∈ bag(A)) ∧ (f[y] = {x} ∈ bag(B)))`

Lemma: bag-combine-combine
`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)].  (⋃x∈⋃y∈b.f[y].g[x] = ⋃x∈b.⋃y∈f[x].g[y] ∈ bag(C))`

Lemma: bag-map-union2
`∀[A,B:Type]. ∀[g:A ⟶ B]. ∀[x:bag(bag(A))].  (bag-map(g;bag-union(x)) = bag-union(bag-map(λz.bag-map(g;z);x)) ∈ bag(B))`

Lemma: bag-union-as-combine
`∀[A:Type]. ∀[x:bag(bag(A))].  (bag-union(x) = ⋃b∈x.b ∈ bag(A))`

Lemma: bag-union-union-as-combine
`∀[X:Type]. ∀[x:bag(bag(bag(X)))].  (bag-union(bag-union(x)) = ⋃z∈x.bag-union(z) ∈ bag(X))`

`BagMonad ==  mk_monad(λT.bag(T);λx.{x};λba,f. ⋃x∈ba.f x)`

`BagMonad ∈ Monad`

Lemma: bag-combine-mapfilter
`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B]. ∀[g:B ⟶ bag(C)].`
`  (⋃x∈bag-mapfilter(f;P;b).g[x] = ⋃x∈b.if P[x] then g[f[x]] else {} fi  ∈ bag(C))`

Lemma: bag-combine-is-map
`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ B].  (⋃x∈b.{f[x]} = bag-map(f;b) ∈ bag(B))`

Definition: bag-sum
`bag-sum(ba;x.f[x]) ==  accumulate (with value s and list item x): f[x] + sover list:  bawith starting value: 0)`

Lemma: bag-sum_wf
`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)].  (bag-sum(ba;x.f[x]) ∈ ℤ)`

Lemma: bag-sum_wf_nat
`∀[A:Type]. ∀[f:A ⟶ ℕ]. ∀[ba:bag(A)].  (bag-sum(ba;x.f[x]) ∈ ℕ)`

Lemma: bag-sum-nonneg
`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)].  0 ≤ bag-sum(ba;x.f[x]) supposing ∀x:A. (0 ≤ f[x])`

Lemma: bag-combine-size
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[ba:bag(A)].  (#(⋃a∈ba.f[a]) = bag-sum(ba;a.#(f[a])) ∈ ℕ)`

Lemma: bag-combine-size-bound
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[L:A List]. ∀[a:A].  #(f[a]) ≤ #(⋃a∈L.f[a]) supposing (a ∈ L)`

Definition: bag-reduce
`bag-reduce(x,y.f[x; y];zero;bs) ==  reduce(λx,y. f[x; y];zero;bs)`

Lemma: bag-reduce_wf
`∀[T:Type]. ∀[zero:T]. ∀[f:T ⟶ T ⟶ T].`
`  (∀[bs:bag(T)]. (bag-reduce(x,y.f[x;y];zero;bs) ∈ T)) supposing (Assoc(T;λx,y. f[x;y]) and Comm(T;λx,y. f[x;y]))`

Definition: bag-accum
`bag-accum(v,x.f[v; x];init;bs) ==`
`  accumulate (with value v and list item x):`
`   f[v; x]`
`  over list:`
`    bs`
`  with starting value:`
`   init)`

Lemma: bag-accum_wf
`∀[T,S:Type]. ∀[init:S]. ∀[f:S ⟶ T ⟶ S]. ∀[bs:bag(T)].`
`  bag-accum(v,x.f[v;x];init;bs) ∈ S supposing ∀v:S. ∀x,y:T.  (f[f[v;y];x] = f[f[v;x];y] ∈ S)`

Lemma: bag-accum-map
`∀[L,y,f,g:Top].  (bag-accum(x,a.f[x;a];y;bag-map(g;L)) ~ bag-accum(x,a.f[x;g a];y;L))`

Lemma: bag-accum-single
`∀[init,f,x:Top].  (bag-accum(v,x.f[v;x];init;{x}) ~ f[init;x])`

Lemma: bag-map-as-accum
`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (bag-map(f;bs) = bag-accum(b,x.f[x].b;{};bs) ∈ bag(B))`

Lemma: bag-combine-as-accum
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)].  (⋃b∈bs.f[b] = bag-accum(c,b.f[b] + c;{};bs) ∈ bag(B))`

Lemma: sum-as-bag-accum
`∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) ~ bag-accum(x,y.x + y;0;[x∈bag-map(λx.f[x];upto(n))|¬b(x =z 0)]))`

Lemma: bag-filter-as-accum
`∀[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[bs:bag(A)].`
`  ([x∈bs|p[x]] = bag-accum(b,x.if p[x] then x.b else b fi ;{};bs) ∈ bag({x:A| ↑p[x]} ))`

Definition: bag-maximal?
`bag-maximal?(bg;x;R) ==  bag-accum(b,y.b ∧b R[x;y];tt;bg)`

Lemma: bag-maximal?_wf
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].  (bag-maximal?(b;x;R) ∈ 𝔹)`

Lemma: bag-maximal?-single
`∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[v,x:T].  uiff(↑bag-maximal?({v};x;R);↑(R x v))`

Lemma: bag-maximal?-append
`∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[b1,b2:bag(T)]. ∀[x:T].`
`  uiff(↑bag-maximal?(b1 + b2;x;R);(↑bag-maximal?(b1;x;R)) ∧ (↑bag-maximal?(b2;x;R)))`

Lemma: bag-maximal?-cons
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,v:T].  uiff(↑bag-maximal?(v.b;x;R);(↑bag-maximal?(b;x;R)) ∧ (↑(R x v)))`

Definition: bag-maximals
`bag-maximals(bg;R) ==  [x∈bg|bag-maximal?(bg;x;R)]`

Lemma: bag-maximals_wf
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹].  (bag-maximals(b;R) ∈ bag(T))`

Definition: imax-bag
`imax-bag(bs) ==  imax-list(bs)`

Lemma: imax-bag_wf
`∀[bs:bag(ℤ)]. imax-bag(bs) ∈ ℤ supposing 0 < #(bs)`

Definition: bag-summation
`Σ(x∈b). f[x] ==  bag-accum(c,x.add f[x] c;zero;b)`

Lemma: bag-summation_wf
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f:T ⟶ R]. ∀[b:bag(T)].`
`  Σ(x∈b). f[x] ∈ R supposing Assoc(R;add) ∧ Comm(R;add)`

Lemma: bag-summation-empty
`∀[add,zero,f:Top].  (Σ(x∈{}). f[x] ~ zero)`

Lemma: bag-summation-append
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T:Type]. ∀[f:T ⟶ R]. ∀[b,c:bag(T)].  (Σ(x∈b + c). f[x] = (Σ(x∈b). f[x] add Σ(x∈c). f[x]) ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-single-sq
`∀[add,zero,f,a:Top].  (Σ(x∈{a}). f[x] ~ add f[a] zero)`

Lemma: bag-summation-single
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T:Type]. ∀[f:T ⟶ R]. ∀[a:T].  (Σ(x∈{a}). f[x] = f[a] ∈ R) supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-cons
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T:Type]. ∀[f:T ⟶ R]. ∀[b:bag(T)]. ∀[a:T].  (Σ(x∈a.b). f[x] = (f[a] add Σ(x∈b). f[x]) ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-linear
`∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].`
`  ∀a:R. (Σ(x∈b). a mul (f[x] add g[x]) = (a mul (Σ(x∈b). f[x] add Σ(x∈b). g[x])) ∈ R) `
`  supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)`

`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f,g:T ⟶ R]. ∀[b:bag(T)].`
`  Σ(x∈b). f[x] add g[x] = (Σ(x∈b). f[x] add Σ(x∈b). g[x]) ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-linear-right
`∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].`
`  ∀a:R. (Σ(x∈b). (f[x] add g[x]) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). g[x]) mul a) ∈ R) `
`  supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)`

Lemma: bag-summation-zero
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)].`
`  Σ(x∈b). zero = zero ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-linear1
`∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  ∀a:R. (Σ(x∈b). a mul f[x] = (a mul Σ(x∈b). f[x]) ∈ R) `
`  supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)`

Lemma: bag-summation-constant
`∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)].  ∀a:|r|. (Σ(x∈b). a = (#(b) ⋅r a) ∈ |r|)`

Lemma: bag-summation-minus
`∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].  (Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|)`

Lemma: bag-summation-linear1-right
`∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  ∀a:R. (Σ(x∈b). f[x] mul a = (Σ(x∈b). f[x] mul a) ∈ R) `
`  supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)`

Lemma: bag-summation-ring-linear1
`∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].`
`  ∀a:|r|. ((Σ(x∈b). f[x] * a = (Σ(x∈b). f[x] * a) ∈ |r|) ∧ (Σ(x∈b). a * f[x] = (a * Σ(x∈b). f[x]) ∈ |r|))`

Lemma: bag-summation-map
`∀[add,zero:Top]. ∀[b:Top List]. ∀[f,g:Top].  (Σ(x∈bag-map(g;b)). f[x] ~ Σ(x∈b). f[g x])`

Lemma: bag-summation-reindex
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[h:A ⟶ T]. ∀[f:T ⟶ R].`
`    ∀[b:bag(T)]. (Σ(x∈b). f[x] = Σ(x∈bag-map(g;b)). f[h x] ∈ R) supposing ∀x:T. (x = (h (g x)) ∈ T) `
`  supposing Comm(R;add) ∧ Assoc(R;add)`

Lemma: bag-summation-split
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹]. ∀[f:T ⟶ R].`
`  Σ(x∈b). f[x] = (Σ(x∈[x∈b|p[x]]). f[x] add Σ(x∈[x∈b|¬bp[x]]). f[x]) ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-product
`∀[r:Rng]. ∀[A,B:Type]. ∀[f:A ⟶ |r|]. ∀[c:bag(B)]. ∀[g:B ⟶ |r|]. ∀[b:bag(A)].`
`  ((Σ(x∈b). f[x] * Σ(y∈c). g[y]) = Σ(p∈b × c). f[fst(p)] * g[snd(p)] ∈ |r|)`

Lemma: bag-summation-hom
`∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].`
`  ∀[A:Type]. ∀[g:A ⟶ |r|]. ∀[b:bag(A)].  (Σ(x∈b). f[g[x]] = f[Σ(x∈b). g[x]] ∈ |s|) supposing rng_hom_p(r;s;f)`

Lemma: bag-double-summation1
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ R]. ∀[b:bag(T)].`
`    (Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-double-summation
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T,A,B:Type]. ∀[f:T ⟶ bag(A)]. ∀[g:T ⟶ B]. ∀[h:B ⟶ A ⟶ R]. ∀[b:bag(T)].`
`    (Σ(x∈b). Σ(y∈f[x]). h[g[x];y] = Σ(p∈⋃x∈b.bag-map(λy.<g[x], y>;f[x])). h[fst(p);snd(p)] ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-double-summation2
`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T,A:Type]. ∀[f:T ⟶ bag(A)]. ∀[h:T ⟶ A ⟶ R]. ∀[b:bag(T)].`
`    (Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Definition: bag-product
`Πx ∈ b. f[x] ==  Σ(x∈b). f[x]`

Lemma: bag-product_wf
`∀[T,R:Type]. ∀[mul:R ⟶ R ⟶ R]. ∀[one:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  Πx ∈ b. f[x] ∈ R supposing Assoc(R;mul) ∧ Comm(R;mul)`

Definition: int-bag-product
`Π(b) ==  Πx ∈ b. x`

Lemma: int-bag-product_wf
`∀[b:bag(ℤ)]. (Π(b) ∈ ℤ)`

Lemma: int-bag-product-append
`∀[b1,b2:bag(ℤ)].  (Π(b1 + b2) ~ Π(b1) * Π(b2))`

Definition: int-bag-sum
`Σ(b) ==  Σ(x∈b). x`

Lemma: int-bag-sum_wf
`∀[b:bag(ℤ)]. (Σ(b) ∈ ℤ)`

Lemma: int-bag-sum-append
`∀[b1,b2:bag(ℤ)].  (Σ(b1 + b2) ~ Σ(b1) + Σ(b2))`

Definition: bag-no-repeats
`bag-no-repeats(T;bs) ==  ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ no_repeats(T;L))`

Lemma: bag-no-repeats_wf
`∀[T:Type]. ∀[bs:bag(T)].  (bag-no-repeats(T;bs) ∈ ℙ)`

Lemma: sq_stable__bag-no-repeats
`∀[T:Type]. ∀[bs:bag(T)].  SqStable(bag-no-repeats(T;bs))`

Lemma: bag-single-no-repeats
`∀[T:Type]. ∀[x:T].  bag-no-repeats(T;{x})`

Lemma: empty-bag-no-repeats
`∀[T:Type]. bag-no-repeats(T;{})`

Lemma: bag-map-no-repeats
`∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[bs:bag(T1)].`
`  uiff(bag-no-repeats(T2;bag-map(f;bs));bag-no-repeats(T1;bs)) supposing Inj(T1;T2;f)`

Lemma: bag-filter-no-repeats
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats(T;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)`

Definition: bag-rep
`bag-rep(n;x) ==  primrec(n;{};λi,r. x.r)`

Lemma: bag-rep_wf
`∀[T:Type]. ∀[n:ℕ]. ∀[x:T].  (bag-rep(n;x) ∈ T List)`

Lemma: bag-size-rep
`∀[n:ℕ]. ∀[x:Top].  (#(bag-rep(n;x)) ~ n)`

Lemma: bag-null-rep
`∀[n:ℕ]. ∀[x:Top].  (bag-null(bag-rep(n;x)) ~ (n =z 0))`

`∀x:Top. ∀n,m:ℕ.  (bag-rep(n + m;x) ~ bag-rep(n;x) + bag-rep(m;x))`

Lemma: empty-bag-union
`∀T:Type. ∀bs:bag(bag(T)).  ((bag-union(bs) = {} ∈ bag(T)) `` (bs ~ bag-rep(#(bs);{})))`

Definition: bag-all
`bag-all(x.p[x];bs) ==  bag-reduce(x,y.x ∧b y;tt;bag-map(λx.p[x];bs))`

Lemma: bag-all_wf
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (bag-all(x.p[x];bs) ∈ 𝔹)`

Definition: bag_all
`bag_all(b;f) ==  bag-accum(a,x.a ∧b f[x];tt;b)`

Lemma: bag_all_wf
`∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[b:bag(T)].  (bag_all(b;f) ∈ 𝔹)`

Lemma: bag_all-empty
`∀[f:Top]. (bag_all({};f) ~ tt)`

Lemma: bag_all-cons
`∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. ∀[f:T ⟶ 𝔹].  (bag_all(x.b;f) ~ (f x) ∧b bag_all(b;f))`

Lemma: bag_all-map
`∀[b,f,g:Top].  (bag_all(bag-map(g;b);f) ~ bag_all(b;f o g))`

Definition: bag-only
`only(bs) ==  hd(bs)`

Lemma: bag-only_wf
`∀[T:Type]. ∀[bs:bag(T)].  only(bs) ∈ T supposing #(bs) = 1 ∈ ℤ`

Lemma: bag_only_single_lemma
`∀x:Top. (only({x}) ~ x)`

Lemma: bag-size-one
`∀[T:Type]. ∀[bs:bag(T)].  bs ~ {only(bs)} supposing #(bs) = 1 ∈ ℤ`

Lemma: subtype-bag-only
`∀[T:Type]. ∀[bs:bag(T)].  bs ∈ bag({x:T| x = only(bs) ∈ T} ) supposing #(bs) = 1 ∈ ℤ`

Lemma: subtype-bag-empty
`∀[T:Type]. ∀[bs:bag(T)].  bs ∈ bag(Void) supposing #(bs) = 0 ∈ ℤ`

Lemma: only-bag-map
`∀[f:Top]. ∀[T:Type]. ∀[b:bag(T)].  only(bag-map(f;b)) ~ f only(b) supposing #(b) = 1 ∈ ℤ`

Lemma: equal-bag-size-le1
`∀[T:Type]. ∀[as,bs:bag(T)].`
`  uiff(as = bs ∈ bag(T);(as = {} ∈ bag(T) `⇐⇒` bs = {} ∈ bag(T))`
`  ∧ ((#(as) = 1 ∈ ℤ) `` (#(bs) = 1 ∈ ℤ) `` (only(as) = only(bs) ∈ T))) `
`  supposing (#(as) ≤ 1) ∧ (#(bs) ≤ 1)`

Definition: bag-merge
`bag-merge(as;bs) ==  bag-map(λx.(inl x);as) + bag-map(λx.(inr x );bs)`

Lemma: bag-merge_wf
`∀A,B:Type. ∀as:bag(A). ∀bs:bag(B).  (bag-merge(as;bs) ∈ bag(A + B))`

Definition: bag-separate
`bag-separate(bs) ==  <bag-mapfilter(λt.outl(t);λt.isl(t);bs), bag-mapfilter(λt.outr(t);λt.(¬bisl(t));bs)>`

Lemma: bag-separate_wf
`∀[A,B:Type]. ∀[bs:bag(A + B)].  (bag-separate(bs) ∈ bag(A) × bag(B))`

Lemma: bag-separate-merge
`∀[as,bs:Top List].  (bag-separate(bag-merge(as;bs)) ~ <as, bs>)`

Definition: sub-bag
`sub-bag(T;as;bs) ==  ∃cs:bag(T). (bs = (as + cs) ∈ bag(T))`

Lemma: sub-bag_wf
`∀[T:Type]. ∀[as,bs:bag(T)].  (sub-bag(T;as;bs) ∈ ℙ)`

Lemma: sub-bag_weakening
`∀[T:Type]. ∀[as,bs:bag(T)].  ((as = bs ∈ bag(T)) `` sub-bag(T;as;bs))`

Lemma: sub-bag_transitivity
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  (sub-bag(T;as;bs) `` sub-bag(T;bs;cs) `` sub-bag(T;as;cs))`

Lemma: sub-bag_antisymmetry
`∀[T:Type]. ∀[as,bs:bag(T)].  (as = bs ∈ bag(T)) supposing (sub-bag(T;as;bs) and sub-bag(T;bs;as))`

Lemma: sub-bag-rep
`∀[T:Type]. ∀x:T. ∀n,m:ℕ.  uiff(sub-bag(T;bag-rep(n;x);bag-rep(m;x));n ≤ m)`

Lemma: sub-bag-combine
`∀[T,U:Type].  ∀f:T ⟶ bag(U). ∀b1,b2:bag(T).  (sub-bag(T;b1;b2) `` sub-bag(U;⋃x∈b1.f[x];⋃x∈b2.f[x]))`

Lemma: sub-bag-append-trivial1
`∀[T:Type]. ∀[b,x:bag(T)].  ∀y:bag(T). (sub-bag(T;b;x) `` sub-bag(T;b;x + y))`

Lemma: sub-bag-append-trivial2
`∀[T:Type]. ∀[b,y:bag(T)].  ∀x:bag(T). (sub-bag(T;b;y) `` sub-bag(T;b;x + y))`

Lemma: sub-bag-append-left
`∀[T:Type]. ∀b1,b2,b:bag(T).  (sub-bag(T;b1 + b2;b) `` sub-bag(T;b1;b))`

Lemma: sub-bag-append-left2
`∀[T:Type]. ∀b1,b2,b:bag(T).  (sub-bag(T;b1 + b2;b) `` sub-bag(T;b2;b))`

Lemma: sub-bag-cancel-right
`∀[T:Type]. ∀b1,b2,b:bag(T).  (sub-bag(T;b1 + b;b2 + b) `⇐⇒` sub-bag(T;b1;b2))`

Lemma: sub-bag-equal
`∀[T:Type]. ∀[b1,b2:bag(T)].  (b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b1;b2) and sub-bag(T;b2;b1))`

Lemma: empty-sub-bag
`∀T:Type. ∀b:bag(T).  sub-bag(T;{};b)`

Lemma: sub-bag-empty
`∀[T:Type]. ∀[b:bag(T)].  uiff(sub-bag(T;b;{});b = {} ∈ bag(T))`

Definition: maximal-sub-bag
`maximal-sub-bag(T;m;b;s.P[s]) ==  (∀s:bag(T). (sub-bag(T;s;b) `` P[s] `` sub-bag(T;s;m))) ∧ P[m]`

Lemma: maximal-sub-bag_wf
`∀[T:Type]. ∀[b,m:bag(T)]. ∀[P:bag(T) ⟶ ℙ].  (maximal-sub-bag(T;m;b;s.P[s]) ∈ ℙ)`

Definition: bag-member
`x ↓∈ bs ==  ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ (x ∈ L))`

Lemma: bag-member_wf
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)].  (x ↓∈ bs ∈ ℙ)`

Lemma: squash-bag-member
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)].  uiff(↓x ↓∈ bs;x ↓∈ bs)`

Lemma: sq_stable__bag-member
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)].  SqStable(x ↓∈ bs)`

Lemma: bag-member-subtype
`∀[A,B:Type].  ∀b:bag(A). ∀x:A.  (x ↓∈ b `` x ↓∈ b) supposing A ⊆r B`

Lemma: bag-member-strong-subtype
`∀[A,B:Type].  ∀b:bag(A). ∀x:B.  (x ↓∈ b `` (x ∈ A)) supposing strong-subtype(A;B)`

Lemma: bag-member-empty
`∀[T:Type]. ∀[x:T].  False supposing x ↓∈ {}`

Lemma: bag-member-empty-iff
`∀[T:Type]. ∀[x:T].  uiff(x ↓∈ {};False)`

Lemma: bag-member-empty-weak
`∀[T:Type]. ∀[x:T].  (x ↓∈ {} `⇐⇒` False)`

Lemma: empty-bag-iff-no-member
`∀[T:Type]. ∀[bs:bag(T)].  uiff(bs = {} ∈ bag(T);∀x:T. (¬x ↓∈ bs))`

Lemma: bag-member-iff-size
`∀[T:Type]. ∀[bs:bag(T)].  uiff(↓∃x:T. x ↓∈ bs;0 < #(bs))`

Lemma: empty-bag-iff-size
`∀[T:Type]. ∀[bs:bag(T)].  uiff(bs = {} ∈ bag(T);#(bs) ≤ 0)`

Lemma: non-empty-bag-implies-non-void
`∀[T:Type]. ∀[bs:bag(T)].  ((¬(bs = {} ∈ bag(T))) `` (↓T))`

Lemma: bag-member-single
`∀[T:Type]. ∀[x,y:T].  uiff(x ↓∈ {y};x = y ∈ T)`

Lemma: single-bags-equal
`∀[T:Type]. ∀[x,y:T].  uiff({x} = {y} ∈ bag(T);x = y ∈ T)`

Lemma: bag-member-single-weak
`∀[T:Type]. ∀[x,y:T].  (x ↓∈ {y} `⇐⇒` x = y ∈ T)`

Lemma: bag-member-list
`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀x:T. ∀L:T List.  (x ↓∈ L `⇐⇒` (x ∈ L))))`

Lemma: l_member-bag-member
`∀[T:Type]. ∀x:T. ∀L:T List.  (x ↓∈ L `⇐⇒` ↓(x ∈ L))`

Lemma: bag-member-iff-hd
`∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;↓∃L:T List. (bs = [x / L] ∈ bag(T)))`

Lemma: bag-member-append
`∀[T:Type]. ∀x:T. ∀as,bs:bag(T).  (x ↓∈ as + bs `⇐⇒` x ↓∈ as ↓∨ x ↓∈ bs)`

Lemma: bag-member-iff
`∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T].  uiff(x ↓∈ bs;↓∃as:bag(T). (bs = ({x} + as) ∈ bag(T)))`

Lemma: bag-in-subtype
`∀[A,B:Type].  ∀[b:bag(B)]. b ∈ bag(A) supposing ∀x:B. (x ↓∈ b `` (x ∈ A)) supposing strong-subtype(A;B)`

Lemma: bag-in-subtype2
`∀[A,B:Type].  ∀[b:bag(B)]. b ∈ bag(A) supposing ∀x:B. (x ↓∈ b `` (∃a:bag(A). x ↓∈ a)) supposing strong-subtype(A;B)`

Lemma: bag-member-combine
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[b:B].  uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))`

Lemma: bag-member-select
`∀[A:Type]. ∀[L:A List]. ∀[i:ℕ||L||].  L[i] ↓∈ L`

Lemma: bag-map-list-map
`∀[T,U:Type].  ∀L1:T List. ∀L2:U List. ∀f:T ⟶ U.  ((L2 = map(f;L1) ∈ bag(U)) `` (∃L:U List. (L = map(f;L1) ∈ (U List))))`

Lemma: bag-member-cons
`∀[T:Type]. ∀[x,u:T]. ∀[v:bag(T)].  uiff(x ↓∈ u.v;(x = u ∈ T) ↓∨ x ↓∈ v)`

Lemma: bag-member-map
`∀[T,U:Type].  ∀x:U. ∀f:T ⟶ U. ∀bs:bag(T).  uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))`

Lemma: bag-member-filter
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))`

Lemma: bag-member-filter-set
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:{x:T| ↑P[x]} ]. ∀[bs:bag(T)].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs)`

Lemma: bag-member-mapfilter
`∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:U]. ∀[bs:bag(T)]. ∀[f:{x:T| ↑(P x)}  ⟶ U].`
`  uiff(x ↓∈ bag-mapfilter(f;P;bs);↓∃v:{x:T| ↑(P x)} . (v ↓∈ bs ∧ (x = (f v) ∈ U)))`

Lemma: bag-member-union
`∀[T:Type]. ∀[x:T]. ∀[bbs:bag(bag(T))].  uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))`

Lemma: bag-member-list-member
`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀L:T List. ∀b:bag(T). ∀x:T.  ((L = b ∈ bag(T)) `` x ↓∈ b `` (x ∈ L))))`

Lemma: bag-member-from-upto
`∀[n,m,x:ℤ].  uiff(x ↓∈ [n, m);(n ≤ x) ∧ x < m)`

Lemma: bag-member-ifthenelse
`∀[T:Type]. ∀[as,bs:bag(T)]. ∀[x:T].  ∀b:𝔹. uiff(x ↓∈ if b then as else bs fi ;if b then x ↓∈ as else x ↓∈ bs fi )`

Lemma: bag-member-not-bag-null
`∀[T:Type]. ∀[bs:bag(T)].  uiff(↓∃x:T. x ↓∈ bs;¬↑bag-null(bs))`

Lemma: bag-member-product
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[p:A × B].  uiff(p ↓∈ as × bs;fst(p) ↓∈ as ∧ snd(p) ↓∈ bs)`

`∀[P:Top × Top]. ∀[C,p,T:Top].  (p ↓∈ let x,y = P in C[x;y] ~ let x,y = P in p ↓∈ C[x;y])`

`∀[P:Top × Top]. ∀[C,p,T:Top].  (p ↓∈ let x,y = P in C[x;y] ~ p ↓∈ C[fst(P);snd(P)])`

Lemma: bag-member-evidence
`∀[T:Type]. ∀[b:bag(T)]. ∀[x:T].  Ax ∈ x ↓∈ b supposing x ↓∈ b`

Lemma: list-member-bag-member
`∀[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L) `` x ↓∈ L)`

Lemma: bag-member-sq-list-member
`∀[T:Type]. ∀L:T List. ∀x:T.  ↓(x ∈ L) supposing x ↓∈ L`

Lemma: bag-member-iff-sq-list-member
`∀[T:Type]. ∀L:T List. ∀x:T.  uiff(x ↓∈ L;↓(x ∈ L))`

Lemma: not-list-member-not-bag-member
`∀[T:Type]. ∀[L:T List]. ∀[x:T].  ((¬(x ∈ L)) `` (¬x ↓∈ L))`

Lemma: int-bag-product-positive
`∀[b:bag(ℤ)]. 0 < Π(b) supposing ∀[x:ℤ]. (x ↓∈ b `` 0 < x)`

Lemma: map-member-wf
`∀[A,B:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)}  ⟶ B].  (map(f;L) ∈ B List)`

Lemma: bag-combine-null
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[b:bag(A)].  uiff(↑bag-null(⋃x∈b.f[x]);∀x:A. (x ↓∈ b `` (↑bag-null(f[x]))))`

Lemma: bag-combine-size-bound2
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[L:bag(A)]. ∀[a:A].  #(f[a]) ≤ #(⋃a∈L.f[a]) supposing a ↓∈ L`

Lemma: bag-size-bag-member
`∀[T:Type]. ∀[bs:bag(T)].  (0 < #(bs) `⇐⇒` ↓∃b:T. b ↓∈ bs)`

Lemma: bag-member-size
`∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T].  0 < #(bs) supposing x ↓∈ bs`

Lemma: sub-bag-union-of-list
`∀[T:Type]. ∀[x:bag(T)].  ∀bs:bag(T) List. ((x ∈ bs) `` sub-bag(T;x;bag-union(bs)))`

Lemma: member-bag-rep
`∀[T:Type]. ∀[n:ℕ]. ∀[x,y:T].  y = x ∈ T supposing y ↓∈ bag-rep(n;x)`

Lemma: select-bag-rep
`∀[T:Type]. ∀[n:ℕ]. ∀[x:T]. ∀[i:ℕn].  (bag-rep(n;x)[i] = x ∈ T)`

Lemma: assert-bag_all
`∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[b:bag(T)].  (∀x:T. (x ↓∈ b `` (↑f[x])) `⇐⇒` ↑bag_all(b;f))`

Lemma: bag-null-bag-union
`∀[T:Type]. ∀[bbs:bag(bag(T))].  ↑bag-null(bag-union(bbs)) supposing ∀bs:bag(T). (bs ↓∈ bbs `` (↑bag-null(bs)))`

Lemma: bag-null-filter
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(↑bag-null([x∈b|p[x]]);∀x:T. (x ↓∈ b `` (¬↑p[x])))`

Definition: b_all
`b_all(T;b;x.P[x]) ==  ∀x:T. (x ↓∈ b `` P[x])`

Lemma: b_all_wf
`∀[T:Type]. ∀[b:bag(T)]. ∀[P:T ⟶ ℙ].  (b_all(T;b;x.P[x]) ∈ ℙ)`

Lemma: b_all-wf2
`∀[T:Type]. ∀[b:bag(T)]. ∀[P:{x:T| x ↓∈ b}  ⟶ ℙ].  (b_all(T;b;x.P[x]) ∈ ℙ)`

Lemma: b_all-map
`∀[A,B:Type].`
`  ∀f:A ⟶ B. ∀b:bag(A). ∀P:B ⟶ ℙ.  ((∀b:B. SqStable(P[b])) `` (b_all(B;bag-map(f;b);x.P[x]) `⇐⇒` b_all(A;b;x.P[f x])))`

Lemma: b_all-inst
`∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  (x ↓∈ b `` b_all(B;b;x.P[x]) `` P[x])`

Lemma: b_all-cons
`∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B.  ((∀b:B. SqStable(P[b])) `` (b_all(B;x.b;x.P[x]) `⇐⇒` P[x] ∧ b_all(B;b;x.P[x])))`

Lemma: b_all-squash-exists-bag
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].`
`  ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b])) `
`  supposing b_all(A;as;x.↓∃y:B. P[x;y])`

Lemma: b_all-squash-exists-bag2
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].`
`  ↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.↓P[fst(x);snd(x)])) `
`  supposing b_all(A;as;x.↓∃y:B. P[x;y])`

Lemma: b_all-squash-exists-list
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].`
`  ↓∃bs:(A × B) List. ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ (∀x∈bs.↓P[fst(x);snd(x)])) `
`  supposing b_all(A;as;x.↓∃y:B. P[x;y])`

Lemma: l_all-squash-exists-list
`∀[A,B:Type]. ∀[as:A List]. ∀[P:A ⟶ B ⟶ ℙ].`
`  ↓∃bs:(A × B) List. ((map(λx.(fst(x));bs) = as ∈ (A List)) ∧ (∀x∈bs.↓P[fst(x);snd(x)])) supposing (∀x∈as.↓∃y:B. P[x;y])`

Lemma: l_all_implies_b_all
`∀[A:Type]. ∀as:A List. ∀P:A ⟶ ℙ.  ((∀x,y:A.  Dec(x = y ∈ A)) `` (∀x∈as.P[x]) `` b_all(A;as;x.P[x]))`

Definition: bag-inject
`bag-inject(A;b;B;f) ==  Inj({x:A| x ↓∈ b} ;B;f)`

Lemma: bag-inject_wf
`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ B].  (bag-inject(A;b;B;f) ∈ ℙ)`

Definition: similar-bags
`similar-bags(A;as;bs) ==  ∀a:A. (a ↓∈ as ∧ 0 < #(bs) `⇐⇒` a ↓∈ bs ∧ 0 < #(as))`

Lemma: similar-bags_wf
`∀[A:Type]. ∀[as,bs:bag(A)].  (similar-bags(A;as;bs) ∈ ℙ)`

Definition: single-valued-bag
`single-valued-bag(b;T) ==  ∀x,y:T.  (x ↓∈ b `` y ↓∈ b `` (x = y ∈ T))`

Lemma: single-valued-bag_wf
`∀[T:Type]. ∀[b:bag(T)].  (single-valued-bag(b;T) ∈ ℙ)`

Lemma: single-valued-bag-hd
`∀[T:Type]. ∀[b:bag(T)].  (hd(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))`

Lemma: single-valued-bag-if-le1
`∀[T:Type]. ∀[b:bag(T)].  single-valued-bag(b;T) supposing #(b) ≤ 1`

Lemma: single-valued-bag-single
`∀[T:Type]. ∀[b:T].  single-valued-bag({b};T)`

Lemma: single-valued-bag-empty
`∀[T:Type]. single-valued-bag({};T)`

Lemma: single-valued-bag-combine
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ bag(B)].`
`  (single-valued-bag(⋃x∈as.f[x];B)) supposing ((∀a:A. single-valued-bag(f[a];B)) and single-valued-bag(as;A))`

Lemma: single-valued-bag-append
`∀[A:Type]. ∀[as,bs:bag(A)].`
`  (single-valued-bag(as + bs;A)) supposing `
`     (similar-bags(A;as;bs) and `
`     single-valued-bag(as;A) and `
`     single-valued-bag(bs;A))`

Lemma: single-valued-bag-map
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ B].  single-valued-bag(bag-map(f;as);B) supposing single-valued-bag(as;A)`

Lemma: single-valued-bag-list
`∀[T:Type]. ∀[L:T List].  single-valued-list(L;T) supposing single-valued-bag(L;T)`

Lemma: single-valued-bag-is-rep
`∀[A:Type]. ∀[as:bag(A)].  ∀a:A. (a ↓∈ as `` (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)`

Definition: sv-bag-only
`sv-bag-only(b) ==  hd(b)`

Lemma: sv-bag-only_wf
`∀[T:Type]. ∀[b:bag(T)].  (sv-bag-only(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))`

Lemma: bag-member-sv-bag-only
`∀[T:Type]. ∀[b:bag(T)].  (sv-bag-only(b) ↓∈ b) supposing (0 < #(b) and single-valued-bag(b;T))`

Lemma: bag-member-implies-hd-append
`∀[T:Type]. ∀[x:T]. ∀[b:bag(T)].  ↓∃c:bag(T). (b = ({x} + c) ∈ bag(T)) supposing x ↓∈ b`

Lemma: sv-bag-only-single
`∀[x:Top]. (sv-bag-only({x}) ~ x)`

Lemma: sv_bag_only_single_lemma
`∀x:Top. (sv-bag-only({x}) ~ x)`

Lemma: sv-bag-only-append
`∀[A:Type]. ∀[as,bs:bag(A)].`
`  (sv-bag-only(as + bs) = sv-bag-only(as) ∈ A) supposing `
`     (similar-bags(A;as;bs) and `
`     0 < #(as) and `
`     single-valued-bag(as;A) and `
`     single-valued-bag(bs;A))`

Lemma: sv-bag-only-combine
`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)].`
`  (sv-bag-only(⋃x∈b.f[x]) = sv-bag-only(f[sv-bag-only(b)]) ∈ B) supposing `
`     ((∀a:A. 0 < #(f[a])) and `
`     (∀a:A. single-valued-bag(f[a];B)) and `
`     0 < #(b) and `
`     single-valued-bag(b;A))`

Lemma: sv-bag-only-map
`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].`
`  (sv-bag-only(bag-map(f;b)) = f[sv-bag-only(b)] ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))`

Lemma: sv-bag-only-map2
`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].`
`  (sv-bag-only(bag-map(f;b)) = (f sv-bag-only(b)) ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))`

Definition: bag-disjoint
`bag-disjoint(T;as;bs) ==  ∀x:T. (¬(x ↓∈ as ∧ x ↓∈ bs))`

Lemma: bag-disjoint_wf
`∀[T:Type]. ∀[as,bs:bag(T)].  (bag-disjoint(T;as;bs) ∈ ℙ)`

Lemma: bag-combine-eq-right
`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f1,f2:A ⟶ bag(B)].`
`  ⋃x∈b.f1[x] = ⋃x∈b.f2[x] ∈ bag(B) supposing ∀x:{x:A| x ↓∈ b} . (f1[x] = f2[x] ∈ bag(B))`

Lemma: bag-filter-empty
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  ∀x:T. (x ↓∈ b `` (¬↑P[x])) supposing ↑bag-null([x∈b|P[x]])`

Lemma: bag-filter-empty-iff
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(∀x:T. (x ↓∈ b `` (¬↑P[x]));↑bag-null([x∈b|P[x]]))`

Lemma: bag-filter-is-empty
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(∀x:T. (x ↓∈ b `` (¬↑P[x]));[x∈b|P[x]] = {} ∈ bag(T))`

Lemma: bag-filter-trivial2
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs `` (↑p[x]))`

Lemma: bag-filter-equal
`∀[T:Type]. ∀[p1,p2:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff([x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T);∀x:T. (x ↓∈ b `` (↑p1[x] `⇐⇒` ↑p2[x])))`

Lemma: sub-bag-member
`∀[T:Type]. ∀[b1,b2:bag(T)]. ∀[x:T].  (x ↓∈ b2) supposing (sub-bag(T;b1;b2) and x ↓∈ b1)`

Lemma: sub-bag-filter
`∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b,c:bag(T).  (sub-bag(T;b;[x∈c|p[x]]) `⇐⇒` sub-bag(T;b;c) ∧ (∀x:T. (x ↓∈ b `` (↑p[x]))))`

Lemma: bag-filter-is-sub-bag
`∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b:bag(T).  sub-bag(T;[x∈b|p[x]];b)`

Lemma: sub-bag-filter2
`∀T:Type. ∀p1,p2:T ⟶ 𝔹. ∀b,c:bag(T).`
`  (sub-bag(T;b;[x∈c|p1[x]]) `` sub-bag(T;b;[x∈c|p2[x]]) `` sub-bag(T;b;[x∈c|p1[x] ∧b p2[x]]))`

Lemma: sub-bag-filter3
`∀T:Type. ∀p:T ⟶ 𝔹. ∀b,c:bag(T).  (sub-bag(T;b;c) `` sub-bag(T;[x∈b|p[x]];[x∈c|p[x]]))`

Lemma: single-valued-sub-bag
`∀[T:Type]. ∀[as,bs:bag(T)].  (single-valued-bag(bs;T) `` sub-bag(T;as;bs) `` single-valued-bag(as;T))`

Lemma: bag-subtype
`∀[A:Type]. ∀b:bag(A). (b ∈ bag({x:A| x ↓∈ b} ))`

Lemma: bag-subtype2
`∀[A:Type]. ∀P:A ⟶ ℙ. ∀b:bag({x:A| P[x]} ). ∀x:{x:A| P[x]} .  (x ↓∈ b `⇐⇒` x ↓∈ b)`

Lemma: bag-member-subtype-2
`∀[A:Type]. ∀b:bag(A). ∀x:A.  (x ↓∈ b `` x ↓∈ b)`

Lemma: strong-subtype-bag
`∀[A,B:Type].  strong-subtype(bag(A);bag(B)) supposing strong-subtype(A;B)`

Definition: bag-to-list
`bag-to-list(cmp;b) ==  comparison-sort(cmp;b)`

Lemma: bag-to-list_wf
`∀[T:Type]`
`  ∀[b:bag(T)]. ∀[cmp:comparison({x:T| x ↓∈ b} )].`
`    bag-to-list(cmp;b) ∈ T List supposing ∀x,y:{x:T| x ↓∈ b} .  (((cmp x y) = 0 ∈ ℤ) `` (x = y ∈ T)) `
`  supposing valueall-type(T)`

Lemma: sub-bag-of-bag-rep
`∀[T:Type]. ∀x:T. ∀n:ℕ.  ∀[b:bag(T)]. b = bag-rep(#(b);x) ∈ bag(T) supposing sub-bag(T;b;bag-rep(n;x))`

Lemma: bag-append-equal-bag-rep
`∀[T:Type]. ∀[x:T]. ∀[n:ℕ]. ∀[a,b:bag(T)].`
`  uiff((a + b) = bag-rep(n;x) ∈ bag(T);(n = (#(a) + #(b)) ∈ ℤ)`
`  ∧ (a = bag-rep(#(a);x) ∈ bag(T))`
`  ∧ (b = bag-rep(#(b);x) ∈ bag(T)))`

Lemma: bag-no-repeats-subtype
`∀[T,A:Type]. ∀[bs:bag(A)].  (bag-no-repeats(A;bs)) supposing (bag-no-repeats(T;bs) and strong-subtype(A;T))`

Lemma: bag-filter-no-repeats2
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats({x:T| ↑p[x]} ;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)`

Lemma: bag-combine-eq-out
`∀[A,B,C:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[f:A ⟶ bag(C)]. ∀[g:B ⟶ bag(C)]. ∀[h:A ⟶ B].`
`  (⋃a∈as.f[a] = ⋃b∈bs.g[b] ∈ bag(C)) supposing `
`     ((∀a:A. (a ↓∈ as `` (g[h[a]] = f[a] ∈ bag(C)))) and `
`     (bs = bag-map(h;as) ∈ bag(B)))`

Lemma: bag-map-member-wf
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs}  ⟶ B].  (bag-map(f;bs) ∈ bag(B))`

Lemma: bag-combine-member-wf
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs}  ⟶ bag(B)].  (⋃x∈bs.f[x] ∈ bag(B))`

Lemma: bag-filter-wf2
`∀[T:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs}  ⟶ 𝔹].  ([x∈bs|p[x]] ∈ bag({x:{b:T| b ↓∈ bs} | ↑p[x]} ))`

Lemma: bag-mapfilter-wf2
`∀[T,A:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs}  ⟶ 𝔹]. ∀[f:{x:{b:T| b ↓∈ bs} | ↑p[x]}  ⟶ A].`
`  (bag-mapfilter(f;p;bs) ∈ bag(A))`

Lemma: bag-member-map2
`∀[T,U:Type].  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.  uiff(x ↓∈ bag-map(f;bs);↓∃v:{v:T| v ↓∈ bs} . (x = (f v) ∈ U))`

Lemma: bag-member-map3
`∀[T,U:Type].  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.  uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))`

Lemma: bag-member-filter-implies1
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  x ↓∈ [x∈bs|P[x]] supposing x ↓∈ bs ∧ (↑P[x])`

Lemma: bag-member-filter-implies2
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]`

Lemma: bag-member-filter2
`∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))`

Lemma: single-valued-bag-filter
`∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].`
`  single-valued-bag([x∈b|p[x]];A) supposing ∀x,y:A.  (x ↓∈ b `` y ↓∈ b `` (↑p[x]) `` (↑p[y]) `` (x = y ∈ A))`

Lemma: bag-eq-subtype1
`∀[A:Type]. ∀[B:A ⟶ ℙ]. ∀[d1,d2:bag({a:A| B[a]} )].  d1 = d2 ∈ bag({a:A| B[a]} ) supposing d1 = d2 ∈ bag(A)`

Lemma: bag-eq-subtype
`∀[A:Type]. ∀[d1,d2:bag(A)].  d1 = d2 ∈ bag({a:A| a ↓∈ d1} ) supposing d1 = d2 ∈ bag(A)`

Lemma: sv-bag-only-filter
`∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].`
`  ∀x:A. (sv-bag-only([x∈b|p[x]]) = x ∈ A) supposing ((↑p[x]) and x ↓∈ b and (∀y:A. (y ↓∈ b `` (↑p[y]) `` (y = x ∈ A))))`

Lemma: bag-member-map3-deq
`∀[T,U:Type].`
`  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.`
`    (Inj({v:T| v ↓∈ bs} ;U;f) `` (∀x,y:U.  Dec(x = y ∈ U)) `` uiff(x ↓∈ bag-map(f;bs);∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))\000C)`

Lemma: b_all-map2
`∀[A,B:Type].`
`  ∀b:bag(A). ∀f:{a:A| a ↓∈ b}  ⟶ B. ∀P:B ⟶ ℙ.`
`    ((∀b:B. SqStable(P[b])) `` (b_all(B;bag-map(f;b);x.P[x]) `⇐⇒` b_all(A;b;x.P[f x])))`

Definition: bag-combine-restrict
`bag-combine-restrict(b;x.f[x]) ==  ⋃x∈b.f[x]`

Lemma: bag-combine-restrict_wf
`∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:{a:A| a ↓∈ b}  ⟶ bag(B)].  (bag-combine-restrict(b;x.f[x]) ∈ bag(B))`

Lemma: bag-only_wf2
`∀[T:Type]. ∀[b:bag(T)].  only(b) ∈ T supposing single-valued-bag(b;T) ∧ 0 < #(b)`

Lemma: bag-filter-combine
`∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[f:U ⟶ bag(T)]. ∀[b:bag(U)].  ([x∈⋃z∈b.f[z]|P[x]] = ⋃z∈b.[x∈f[z]|P[x]] ∈ bag(T))`

Lemma: bag-filter-combine2
`∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[f:U ⟶ bag(T)]. ∀[b:bag(U)].  ([x∈⋃z∈b.f[z]|P[x]] = ⋃z∈b.[x∈f[z]|P[x]] ∈ bag({x:T| ↑P[x]} ))`

Lemma: bag-mapfilter-combine
`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[P:B ⟶ 𝔹]. ∀[g:{x:B| ↑P[x]}  ⟶ C].`
`  (bag-mapfilter(g;P;⋃x∈b.f[x]) = ⋃x∈b.bag-mapfilter(g;P;f[x]) ∈ bag(C))`

Definition: bag-mapfilter-fast
`bag-mapfilter-fast(f;P;bs) ==  bag-accum(b,x.if P[x] then f[x].b else b fi ;{};bs)`

Lemma: bag-mapfilter-fast_wf
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].  (bag-mapfilter-fast(f;P;bs) ∈ bag(B))`

Lemma: bag-mapfilter-fast-eq
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].`
`  (bag-mapfilter-fast(f;P;bs) = bag-mapfilter(f;P;bs) ∈ bag(B))`

Lemma: bag-mapfilter-fast-eq2
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].`
`  (bag-mapfilter(f;P;bs) = bag-mapfilter-fast(f;P;bs) ∈ bag(B))`

Lemma: bag-mapfilter-fast-map
`∀[bs:bag(Top)]. ∀[P,f,g:Top].  (bag-mapfilter-fast(f;P;bag-map(g;bs)) ~ bag-mapfilter-fast(f o g;P o g;bs))`

Lemma: bag-maximals-not-max
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].`
`  (¬↑(R x y)) supposing `
`     (y ↓∈ bag-maximals(b;R) and `
`     x ↓∈ bag-maximals(b;R) and `
`     (∀x,y:T.  ((↑(R x y)) `` (↑(R y x)) `` (x = y ∈ T))) and `
`     (∀x:T. (¬↑(R x x))))`

Lemma: bag-maximal?-max
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].  (↑(R x y)) supposing ((↑bag-maximal?(b;x;R)) and y ↓∈ b)`

Lemma: bag-maximal?-iff
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T].  uiff(↑bag-maximal?(b;x;R);∀y:T. (y ↓∈ b `` (↑(R x y))))`

Lemma: bag-maximals-max
`∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].  (↑(R x y)) supposing (x ↓∈ bag-maximals(b;R) and y ↓∈ b)`

Lemma: imax-bag-ub
`∀[bs:bag(ℤ)]. ∀[x:ℤ].  (x ↓∈ bs `` (x ≤ imax-bag(bs)))`

Lemma: imax-bag-lb
`∀[bs:bag(ℤ)]. (0 < #(bs) `` imax-bag(bs) ↓∈ bs)`

Definition: bag-max
`bag-max(f;bs) ==  imax-bag(bag-map(f;bs))`

Lemma: bag-max_wf
`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)].  bag-max(f;bs) ∈ ℤ supposing 0 < #(bs)`

Lemma: bag-max-ub
`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)]. ∀[x:A].  (f x) ≤ bag-max(f;bs) supposing x ↓∈ bs`

Lemma: bag-max-lb
`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)].  bag-max(f;bs) ↓∈ bag-map(f;bs) supposing 0 < #(bs)`

Lemma: bag-append-no-repeats1
`∀[T:Type]. ∀[as,bs:bag(T)].`
`  bag-no-repeats(T;as + bs) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as `` (¬z ↓∈ bs)))`

Lemma: bag-append-no-repeats
`∀[T:Type]. ∀[as,bs:bag(T)].`
`  uiff(bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as `` (¬z ↓∈ bs)));bag-no-repeats(T;as + bs))`

Lemma: bag-product-no-repeats
`∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)].`
`  bag-no-repeats(A × B;as × bs) supposing bag-no-repeats(A;as) ∧ bag-no-repeats(B;bs)`

Lemma: bag-no-repeats-implies-disjoint
`∀[T:Type]. ∀[as,bs:bag(T)].  bag-disjoint(T;as;bs) supposing bag-no-repeats(T;as + bs)`

Lemma: bag-settype
`∀[T:Type]. ∀[bs:bag(T)]. ∀[P:T ⟶ ℙ].  bs ∈ bag({x:T| P[x]} ) supposing ∀x:T. (x ↓∈ bs `` P[x])`

Lemma: bag-filter-same
`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs `` (↑p[x]))`

Lemma: bag-extensionality-no-repeats
`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀[as,bs:bag(T)].`
`        uiff(as = bs ∈ bag(T);∀x:T. uiff(x ↓∈ as;x ↓∈ bs)) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs)))`

Lemma: bag-extensionality1
`∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].`
`  ∀[as,bs:bag(T)].  uiff(as = bs ∈ bag(T);∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ)) `
`  supposing ∀[x,y:T].  (↑(eq x y) `⇐⇒` x = y ∈ T)`

Lemma: bag-intersection
`∀[A:Type]. ∀[as,as',bs,bs':bag(A)].`
`  (↓∃x:A. (x ↓∈ as ∧ x ↓∈ bs)) supposing (#(as') < #(as) and #(bs') < #(bs) and ((as + as') = (bs + bs') ∈ bag(A)))`

Definition: bag-splits
`bag-splits(b) ==  rec-case(b) of [] => {<{}, {}>} | a::as => r.bag-map(λp.<{a} + (fst(p)), snd(p)>;r) + bag-map(λp.<fst(\000Cp), {a} + (snd(p))>;r)`

Lemma: bag-splits_wf_list
`∀T:Type. ∀b:T List.  (bag-splits(b) ∈ (bag(T) × bag(T)) List)`

Lemma: bag-splits-permutation1
`∀T:Type. ∀L:T List. ∀a,b:T.  permutation(bag(T) × bag(T);bag-splits([a; [b / L]]);bag-splits([b; [a / L]]))`

Lemma: bag-splits-permutation
`∀T:Type. ∀L1,L2:T List.  (permutation(T;L1;L2) `` permutation(bag(T) × bag(T);bag-splits(L1);bag-splits(L2)))`

Lemma: bag-splits_wf
`∀T:Type. ∀b:bag(T).  (bag-splits(b) ∈ bag(bag(T) × bag(T)))`

Lemma: bag-member-splits
`∀[T:Type]. ∀[as,bs,cs:bag(T)].  uiff(<as, bs> ↓∈ bag-splits(cs);(as + bs) = cs ∈ bag(T))`

Definition: bag-decomp
`bag-decomp(bs) ==  map(λn.remove-nth(n;bs);upto(||bs||))`

Lemma: bag-decomp_wf
`∀[T:Type]. ∀[bs:bag(T)].  (bag-decomp(bs) ∈ bag(T × bag(T)))`

Lemma: bag-member-decomp
`∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. ∀[b:bag(T)].  uiff(<x, b> ↓∈ bag-decomp(bs);({x} + b) = bs ∈ bag(T))`

Lemma: bag-decomp_wf2
`∀[T:Type]. ∀[bs:bag(T)].  (bag-decomp(bs) ∈ bag({p:T × bag(T)| bs = ({fst(p)} + (snd(p))) ∈ bag(T)} ))`

Lemma: no_repeats-bag
`∀[T:Type]. ∀[as,bs:T List].  (no_repeats(T;as)) supposing (no_repeats(T;bs) and (as = bs ∈ bag(T)))`

Lemma: bag-no-repeats-settype
`∀[T:Type]. ∀[bs:bag(T)].  uiff(bag-no-repeats({x:T| x ↓∈ bs} ;bs);bag-no-repeats(T;bs)) supposing ∀x,y:T.  Dec(x = y ∈ T\000C)`

Lemma: bag-no-repeats-le-bag-size
`∀[T:Type]. ∀[locs,b:bag(T)].  #(b) ≤ #(locs) supposing bag-no-repeats(T;b) ∧ (∀x:T. (x ↓∈ b `` x ↓∈ locs))`

Lemma: bag-no-repeats-single
`∀[T:Type]. ∀[x:T].  bag-no-repeats(T;{x})`

Lemma: bag-no-repeats-append
`∀[T:Type]. ∀[as,bs:bag(T)].`
`  uiff(bag-no-repeats(T;as + bs);bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀x:T. (x ↓∈ as `` (¬x ↓∈ bs))))`

Lemma: bag-no-repeats-cons
`∀[T:Type]. ∀[b:bag(T)]. ∀[x:T].  uiff(bag-no-repeats(T;x.b);bag-no-repeats(T;b) ∧ (¬x ↓∈ b))`

Lemma: bag-no-repeats-list
`∀[T:Type]. ∀[L:T List].  uiff(bag-no-repeats(T;L);no_repeats(T;L))`

Lemma: bag-no-repeats-filter
`∀[T:Type]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹].  bag-no-repeats(T;[x∈b|p[x]]) supposing bag-no-repeats(T;b)`

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

Lemma: bag-summation-equal
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].`
`  Σ(x∈b). f[x] = Σ(x∈b). g[x] ∈ R supposing (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ R))) ∧ IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-equal2
`∀[T:Type]. ∀[r:Rng]. ∀[f,g:T ⟶ |r|]. ∀[b,c:bag(T)].`
`  Σ(x∈b). f[x] = Σ(x∈c). g[x] ∈ |r| supposing (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ |r|))) ∧ (b = c ∈ bag(T))`

Lemma: bag-summation-is-zero
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  Σ(x∈b). f[x] = zero ∈ R supposing (∀x:T. (x ↓∈ b `` (f[x] = zero ∈ R))) ∧ IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-single-non-zero
`∀[T,R:Type]. ∀[eq:EqDecider(T)]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  ∀z:T. Σ(x∈b). f[x] = Σ(x∈[x∈b|eq x z]). f[x] ∈ R supposing ∀x:T. (x ↓∈ b `` ((x = z ∈ T) ∨ (f[x] = zero ∈ R))) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-single-non-zero-no-repeats
`∀[T,R:Type]. ∀[eq:EqDecider(T)]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].`
`  ∀z:T`
`    (Σ(x∈b). f[x] = f[z] ∈ R) supposing `
`       ((bag-no-repeats(T;b) ∧ z ↓∈ b) and `
`       (∀x:T. (x ↓∈ b `` ((x = z ∈ T) ∨ (f[x] = zero ∈ R))))) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-filter
`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹]. ∀[f:T ⟶ R].`
`  Σ(x∈[x∈b|p[x]]). f[x] = Σ(x∈b). if p[x] then f[x] else zero fi  ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Lemma: bag-summation-from-upto
`∀[a,b:ℤ]. ∀[f:{a..b-} ⟶ ℤ].  (Σ(i∈[a, b)). f[i] = Σ(f[j + a] | j < b - a) ∈ ℤ)`

Lemma: bag-summation-partition
`∀[A:Type]`
`  ∀[R,T:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[case:T ⟶ A ⟶ 𝔹]. ∀[f:T ⟶ R]. ∀[c:bag(A)].`
`    Σ(x∈b). f[x] = Σ(z∈c). Σ(x∈[x∈b|case[x;z]]). f[x] ∈ R `
`    supposing (IsMonoid(R;add;zero) ∧ Comm(R;add))`
`    ∧ (∀x:{x:T| x ↓∈ b} . (∃z:A [(z ↓∈ c ∧ (↑case[x;z]))]))`
`    ∧ bag-no-repeats(A;c)`
`    ∧ (∀z1,z2:A. ∀x:T.  ((↑case[x;z1]) `` (↑case[x;z2]) `` (z1 = z2 ∈ A))) `
`  supposing ∀x,y:A.  Dec(x = y ∈ A)`

Lemma: bag-summation_functionality_wrt_le_1
`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:T ⟶ ℤ].  Σ(x∈b). f[x] ≤ Σ(x∈b). g[x] supposing ∀x:T. (f[x] ≤ g[x])`

Lemma: bag-summation_functionality_wrt_le
`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b}  ⟶ ℤ].`
`  Σ(x∈b). f[x] ≤ Σ(x∈b). g[x] supposing ∀x:T. (x ↓∈ b `` (f[x] ≤ g[x]))`

Lemma: bag-summation-equal-implies-all-equal-1
`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:T ⟶ ℤ].`
`  (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b `` (f[x] ≤ g[x]))))`

Lemma: bag-summation-equal-implies-all-equal
`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b}  ⟶ ℤ].`
`  (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b `` (f[x] ≤ g[x]))))`

Definition: strict-bag-function
`strict-bag-function(G;L;B;S) ==  ∀x:tuple-type(map(λT.bag(T);L)). ((∀i∈S.x.i = {} ∈ bag(L[i])) `` ((G x) = {} ∈ bag(B)))`

Lemma: strict-bag-function_wf
`∀[L:Type List]. ∀[B:Type]. ∀[G:tuple-type(map(λT.bag(T);L)) ⟶ bag(B)]. ∀[S:ℕ||L|| List].`
`  (strict-bag-function(G;L;B;S) ∈ ℙ)`

Lemma: bag-from-member-function
`∀[T:Type]`
`  ∀bs:bag(T). ∀P,Q:T ⟶ ℙ.`
`    ((∀i:T. Dec(Q[i]))`
`    `` (∀i:T. (i ↓∈ bs `` Q[i] `` P[i]))`
`    `` (∃b:bag(T). ((∀i:T. (i ↓∈ bs `` Q[i] `` i ↓∈ b)) ∧ (∀i:T. (i ↓∈ b `` P[i])))))`

Lemma: bag-from-member-function-exists
`∀[T,A:Type].`
`  ∀bs:bag(T). ∀P:T ⟶ A ⟶ ℙ.`
`    ((∀x,y:A.  Dec(x = y ∈ A))`
`    `` (∀x,y:T.  Dec(x = y ∈ T))`
`    `` (∀i:T. (i ↓∈ bs `` (∃a:A. P[i;a])))`
`    `` (∃b:bag(T × A). ((∀i:T. (i ↓∈ bs `` i ↓∈ bag-map(λx.(fst(x));b))) ∧ (∀x:T × A. (x ↓∈ b `` P[fst(x);snd(x)])))))`

Definition: lifting-gen-list-rev
`lifting-gen-list-rev(n;bags) ==`
`  fix((λlifting-gen-list-rev,m,g. if (n =z m) then {g} else ⋃x∈bags m.lifting-gen-list-rev (m + 1) (g x) fi ))`

Lemma: lifting-gen-list-rev_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].`
`  (lifting-gen-list-rev(n;bags) m g ∈ bag(B))`

Lemma: temp-lifting-gen-list-rev_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].`
`  (lifting-gen-list-rev(n;bags) m g ∈ bag(B))`

Definition: lifting-gen-rev
`lifting-gen-rev(n;f;bags) ==  lifting-gen-list-rev(n;bags) 0 f`

Lemma: lifting-gen-rev_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;B)].  (lifting-gen-rev(n;f;bags) ∈ bag(B))`

Definition: lifting-gen
`lifting-gen(n;f) ==  λbags.lifting-gen-rev(n;f;bags)`

Lemma: lifting-gen_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;B)].  (lifting-gen(n;f) ∈ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))`

Lemma: lifting-gen-strict
`∀[n:ℕ]. ∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)].  lifting-gen(n;f) a ~ {} supposing ∃k:ℕn. (↑bag-null(a k))`

Definition: lifting1
`lifting1(f;b) ==  lifting-gen-rev(1;f;λx.b)`

Lemma: lifting1_wf
`∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].  (lifting1(f;b) ∈ bag(B))`

Definition: lifting2
`lifting2(f;abag;bbag) ==  lifting-gen-rev(2;f;λx.[abag; bbag][x])`

Lemma: lifting2_wf
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].  (lifting2(f;abag;bbag) ∈ bag(C))`

Definition: lifting-0
`lifting-0(b) ==  lifting-gen-rev(0;b;λn.[][n])`

Lemma: lifting-0_wf
`∀[B:Type]. ∀[b:B].  (lifting-0(b) ∈ bag(B))`

Definition: lifting-1
`lifting-1(f) ==  λb.lifting1(f;b)`

Lemma: lifting-1_wf
`∀[A,B:Type]. ∀[f:A ⟶ B].  (lifting-1(f) ∈ bag(A) ⟶ bag(B))`

Lemma: lifting-1-strict
`∀[f:Top]. (lifting-1(f) {} ~ {})`

Definition: lifting-2
`lifting-2(f) ==  λa,b. lifting2(f;a;b)`

Lemma: lifting-2_wf
`∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C].  (lifting-2(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C))`

Lemma: lifting-2-strict
`∀[f:Top]. ∀[b:bag(Top)].  ((lifting-2(f) {} b ~ {}) ∧ (lifting-2(f) b {} ~ {}))`

Definition: lifting-3
`lifting-3(f) ==  λa,b,c. lifting-gen-rev(3;f;λn.[a; b; c][n])`

Lemma: lifting-3_wf
`∀[A,B,C,D:Type]. ∀[f:A ⟶ B ⟶ C ⟶ D].  (lifting-3(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))`

Lemma: lifting-3-strict
`∀[f:Top]. ∀[b:bag(Top)].`
`  ∀b':bag(Top). ((lifting-3(f) {} b b' ~ {}) ∧ (lifting-3(f) b {} b' ~ {}) ∧ (lifting-3(f) b b' {} ~ {}))`

Definition: uncurry-gen
`uncurry-gen(n) ==  fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (λx.(g x (x m))) fi ))`

Lemma: uncurry-gen_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].`
`  (uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)`

Lemma: uncurry-gen_wf2
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type].`
`∀[g:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].`
`  (uncurry-gen(n) m g ∈ (k:{q..n-} ⟶ (A k)) ⟶ B)`

Definition: uncurry-rev
`uncurry-rev(n;f) ==  uncurry-gen(n) 0 (λx.f)`

Lemma: uncurry-rev_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;B)].  (uncurry-rev(n;f) ∈ (k:ℕn ⟶ (A k)) ⟶ B)`

Definition: apply_gen
`apply_gen(n;lst) ==  fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (g (lst m)) fi ))`

Lemma: apply_gen_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - m;λx.(A (x + m));B)]. ∀[lst:k:{m..n-} ⟶ (A k)].`
`  (apply_gen(n;lst) m f ∈ B)`

Lemma: apply_gen_wf2
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - q;λx.(A (x + q));B)].`
`∀[lst:k:{q..n-} ⟶ (A k)].`
`  (apply_gen(m;lst) q f ∈ funtype(n - m;λx.(A (x + m));B))`

Lemma: apply_uncurry
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[lst:k:{q..n-} ⟶ (A k)].`
`∀[f:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].`
`  ((uncurry-gen(n) m f lst) = (apply_gen(n;lst) m (f lst)) ∈ B)`

Lemma: apply_larger_list
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[lst:k:{q..n-} ⟶ (A k)]. ∀[r:ℕm]. ∀[a:A r].`
`∀[f:funtype(n - m;λx.(A (x + m));B)].`
`  ((apply_gen(n;λx.if (x =z r) then a else lst x fi ) m f) = (apply_gen(n;lst) m f) ∈ B)`

Lemma: lifting-member
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n - m;λx.(A (x + m));B)]. ∀[b:B].`
`  (b ↓∈ lifting-gen-list-rev(n;bags) m f`
`  `⇐⇒` ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) m (λx.f) lst) = b ∈ B)))`

Lemma: lifting-member-simple
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;B)]. ∀[b:B].`
`  (b ↓∈ lifting-gen-rev(n;f;bags)`
`  `⇐⇒` ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ ((uncurry-rev(n;f) lst) = b ∈ B)))`

Lemma: bag-member-lifting-2
`∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[c:C].`
`  uiff(c ↓∈ lifting-2(f) as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C)))`

Definition: concat-lifting-list
`concat-lifting-list(n;bags) ==  λm,g. bag-union(lifting-gen-list-rev(n;bags) m g)`

Lemma: concat-lifting-list_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));bag(B))].`
`  (concat-lifting-list(n;bags) m g ∈ bag(B))`

Lemma: concat-lifting-list-member
`∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n - m;λx.(A (x + m));bag(B))].`
`∀[b:B].`
`  (b ↓∈ concat-lifting-list(n;bags) m f`
`  `⇐⇒` ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-gen(n) m (λx.f) lst))`

Definition: concat-lifting
`concat-lifting(n;f;bags) ==  concat-lifting-list(n;bags) 0 f`

Lemma: concat-lifting_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))].`
`  (concat-lifting(n;f;bags) ∈ bag(B))`

Lemma: concat-lifting-member
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))]. ∀[b:B].`
`  (b ↓∈ concat-lifting(n;f;bags) `⇐⇒` ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f) lst))`

Lemma: concat-lifting-strict
`∀[n:ℕ]. ∀[bags:k:ℕn ⟶ bag(Top)]. ∀[f:Top].  concat-lifting(n;f;bags) ~ {} supposing ∃k:ℕn. ((bags k) = {} ∈ bag(Top))`

Definition: concat-lifting-gen
`concat-lifting-gen(n;f) ==  λbags.concat-lifting(n;f;bags)`

Lemma: concat-lifting-gen_wf
`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;bag(B))].  (concat-lifting-gen(n;f) ∈ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))`

Definition: concat-lifting1
`concat-lifting1(f;bag) ==  concat-lifting(1;f;λx.bag)`

Lemma: concat-lifting1_wf
`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[b:bag(A)].  (concat-lifting1(f;b) ∈ bag(B))`

Definition: concat-lifting2
`concat-lifting2(f;abag;bbag) ==  concat-lifting(2;f;λn.[abag; bbag][n])`

Lemma: concat-lifting2_wf
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[abag:bag(A)]. ∀[bbag:bag(B)].  (concat-lifting2(f;abag;bbag) ∈ bag(C))`

Definition: concat-lifting-0
`concat-lifting-0(f) ==  concat-lifting(0;f;λn.[][n])`

Lemma: concat-lifting-0_wf
`∀[B:Type]. ∀[f:bag(B)].  (concat-lifting-0(f) ∈ bag(B))`

Definition: concat-lifting-1
`f@ ==  λb.concat-lifting1(f;b)`

Lemma: concat-lifting-1_wf
`∀[B,A:Type]. ∀[f:A ⟶ bag(B)].  (f@ ∈ bag(A) ⟶ bag(B))`

Lemma: concat-lifting-1-strict
`∀[f:Top]. (f@ {} ~ {})`

Definition: concat-lifting-2
`f@ ==  λa,b. concat-lifting2(f;a;b)`

Lemma: concat-lifting-2_wf
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)].  (f@ ∈ bag(A) ⟶ bag(B) ⟶ bag(C))`

Lemma: concat-lifting-2-strict
`∀[f:Top]. ∀[b:bag(Top)].  ((f@ {} b ~ {}) ∧ (f@ b {} ~ {}))`

Definition: concat-lifting-3
`concat-lifting-3(f) ==  λa,b,c. concat-lifting(3;f;λn.[a; b; c][n])`

Lemma: concat-lifting-3_wf
`∀[A,B,C,D:Type]. ∀[f:A ⟶ B ⟶ C ⟶ bag(D)].  (concat-lifting-3(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))`

Lemma: concat-lifting-3-strict
`∀[f:Top]. ∀[b:bag(Top)].`
`  ∀b':bag(Top)`
`    ((concat-lifting-3(f) {} b b' ~ {}) ∧ (concat-lifting-3(f) b {} b' ~ {}) ∧ (concat-lifting-3(f) b b' {} ~ {}))`

Lemma: bag-map-append-empty
`∀[f,b:Top].  (bag-map(f;b) + {} ~ bag-map(f;b))`

Lemma: bag-combine-append-empty
`∀[f,bs:Top].  (⋃x∈bs.f[x] @ [] ~ ⋃x∈bs.f[x])`

Lemma: bag-combine-bag-append-empty
`∀[f,bs:Top].  (⋃x∈bs.f[x] + [] ~ ⋃x∈bs.f[x])`

Definition: bag-monoid
`bag-monoid(T) ==  <bag(T), λx,y. tt, λx,y. tt, λx,y. (x + y), {}, λx.x>`

Lemma: bag-monoid_wf
`∀[T:Type]. (bag-monoid(T) ∈ AbMon)`

Lemma: single-bag-append-nil
`∀[a:Top]. ([a] + [] ~ [a])`

`∀[x,F,L:Top].  (let a,b = x in F[a;b] + L ~ let a,b = x in F[a;b] + L)`

Lemma: callbyvalueall-single-bag-combine1
`∀[F,a,as:Top].  (let x ⟵ [a] in let y ⟵ ⋃z∈x.map(z;as) in F[y] ~ let x ⟵ a in let y ⟵ map(x;as) in F[y])`

Lemma: callbyvalueall-single-bag-combine2
`∀[F,G,a:Top].  (let x ⟵ [a] in let y ⟵ ⋃z∈x.G[z] in F[y] ~ let x ⟵ a in let y ⟵ G[x] @ [] in F[y])`

Lemma: callbyvalueall-single-bag-combine3
`∀[F,G,a,b:Top].`
`  (let x ⟵ [a]`
`   in let z ⟵ b`
`      in let y ⟵ ⋃v∈x.G[z;v]`
`         in F[z;y] ~ let x ⟵ a`
`                     in let z ⟵ b`
`                        in let y ⟵ G[z;x] @ []`
`                           in F[z;y])`

Lemma: callbyvalueall-single-bag-combine4
`∀[F,a:Top].  (let x ⟵ [a] in F[x] ~ let x ⟵ a in F[[x]])`

Lemma: lifting-bag-combine-decide
`∀[a,F,G,f:Top].`
`  (⋃b∈case a of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case a of inl(x) => ⋃b∈F[x].f[b] | inr(x) => ⋃b∈G[x].f[b])`

Lemma: lifting-bag-combine-decide-name_eq
`∀[a,b,F,G,f:Top].`
`  (⋃b∈case name_eq(a;b) of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case name_eq(a;b)`
`   of inl(x) =>`
`   ⋃b∈F[x].f[b]`
`   | inr(x) =>`
`   ⋃b∈G[x].f[b])`

`bag-admissable(T;as,bs.R[as; bs]) ==  (∀bs:bag(T). R[{}; bs]) ∧ (∀as,bs,cs:bag(T).  (R[as; bs] `` R[as + cs; bs + cs]))`

`∀[T:Type]. ∀[R:bag(T) ⟶ bag(T) ⟶ ℙ].  (bag-admissable(T;as,bs.R[as;bs]) ∈ ℙ)`

`∀[T:Type]. ∀[R:bag(T) ⟶ bag(T) ⟶ ℙ].`
`  (bag-admissable(T;as,bs.R[as;bs]) `` (∀as,bs:bag(T).  (sub-bag(T;as;bs) `` R[as;bs])))`

Lemma: sub-bag-singleton-left
`∀[T:Type]. ∀[b:bag(T)]. ∀[x:T].  x ↓∈ b supposing sub-bag(T;{x};b)`

Lemma: sub-bag-map-equal
`∀[T,U:Type]. ∀[b1,b2:bag(T)]. ∀[f:T ⟶ U].`
`  (b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b2;b1) and sub-bag(U;bag-map(f;b1);bag-map(f;b2)))`

Lemma: sub-bag-mapfilter-implies
`∀[A,B:Type].`
`  ∀as:bag(A). ∀bs:bag(B). ∀f:A ⟶ B. ∀P:A ⟶ 𝔹.  (sub-bag(B;bag-map(f;as);bs) `` sub-bag(B;bag-mapfilter(f;P;as);bs))`

Lemma: sub-bag-size
`∀[T:Type]. ∀[a,b:bag(T)].  #(a) ≤ #(b) supposing sub-bag(T;a;b)`

Definition: bag-order
`bag-order(T) ==`
`  {cmp:bag(T) ⟶ bag(T) ⟶ ℤ| `
`   (∀as,bs:bag(T).  (((cmp as bs) = 0 ∈ ℤ `⇐⇒` as = bs ∈ bag(T)) ∧ (cmp as bs < 0 `⇐⇒` (cmp bs as) > 0)))`
`   ∧ Linorder(bag(T);as,bs.(cmp as bs) ≤ 0)} `

Lemma: bag-order_wf
`∀T:Type. (bag-order(T) ∈ Type)`

Definition: unordered-combination
`UnorderedCombination(n;T) ==  {b:bag(T)| bag-no-repeats(T;b) ∧ (#(b) = n ∈ ℤ)} `

Lemma: unordered-combination_wf
`∀[T:Type]. ∀[n:ℕ].  (UnorderedCombination(n;T) ∈ Type)`

Lemma: unordered-combination_functionality
`∀[A,B:Type].  ∀n,m:ℕ.  (A ~ B `` UnorderedCombination(n;A) ~ UnorderedCombination(m;B) supposing n = m ∈ ℤ)`

Lemma: subtype_rel_unordered-combination
`∀[A,B:Type].  ∀n:ℕ. UnorderedCombination(n;A) ⊆r UnorderedCombination(n;B) supposing strong-subtype(A;B)`

Definition: bag-incomparable
`bag-incomparable(T;R;b) ==  ∀x,y:T.  (x ↓∈ b `` y ↓∈ b `` (¬(x R y)))`

Lemma: bag-incomparable_wf
`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[b:bag(T)].  (bag-incomparable(T;R;b) ∈ ℙ)`

Definition: bag-covers
`bag-covers(T;R;cvr;b) ==  ∀x:T. (x ↓∈ b `` (x ↓∈ cvr ∨ (∃y:T. (y ↓∈ cvr ∧ (x R y)))))`

Lemma: bag-covers_wf
`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[cvr,b:bag(T)].  (bag-covers(T;R;cvr;b) ∈ ℙ)`

Definition: bag-cover
`bag-cover(T;R;mx;b) ==  sub-bag(T;mx;b) ∧ bag-covers(T;R;mx;b) ∧ bag-incomparable(T;R;mx)`

Lemma: bag-cover_wf
`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[cvr,b:bag(T)].  (bag-cover(T;R;cvr;b) ∈ ℙ)`

`monad-from(Mnd) ==`
`  mk-monad(functor(ob(T) = M-map(Mnd) T;`
`                   arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));`
`           λx.M-return(Mnd);`
`           λx,z. (M-bind(Mnd) z (λx.x)))`

`∀[Mnd:Monad]. (monad-from(Mnd) ∈ Monad(TypeCat))`

`bag-cat-monad() ==  mk-monad(functor(ob(x) = bag(x);arrow(x,y,f) = λz.bag-map(f;z));x |→ λz.{z};x |→ λz.bag-union(z))`

`bag-cat-monad() ∈ Monad(TypeCat)`

Definition: bag-bind
`bag-bind(bs;f) ==  bag-union(bag-map(f;bs))`

Lemma: bag-bind_wf
`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)].  (bag-bind(bs;f) ∈ bag(B))`

Lemma: bag-bind-assoc
`∀[A,B,C:Type]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)]. ∀[bs:bag(A)].`
`  (bag-bind(bag-bind(bs;f);g) = bag-bind(bs;λa.bag-bind(f a;g)) ∈ bag(C))`

Lemma: bag-bind-empty-right
`∀A:Type. ∀ba:bag(A).  (bag-bind(ba;λa.{}) ~ {})`

Lemma: bag-bind-append
`∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)].  (bag-bind(ba + bb;f) = (bag-bind(ba;f) + bag-bind(bb;f)) ∈ bag(B))`

Lemma: bag-bind-append2
`∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].`
`  (bag-bind(ba;λa.((F a) + (G a))) = (bag-bind(ba;F) + bag-bind(ba;G)) ∈ bag(B))`

Lemma: bag-bind-com
`∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[ba:bag(A)]. ∀[bb:bag(B)].`
`  (bag-bind(ba;λa.bag-bind(bb;λb.f[a;b])) = bag-bind(bb;λb.bag-bind(ba;λa.f[a;b])) ∈ bag(C))`

Lemma: bag-bind-filter
`∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]}  ⟶ bag(B)]. ∀[ba:bag(A)].`
`  (bag-bind([a∈ba|p[a]];λa.f[a]) = bag-bind(ba;λa.if p[a] then f[a] else {} fi ) ∈ bag(B))`

Home Index