---

Definition: mset
MSet{s} ==  as,bs:|s| List//(as ≡(|s|) bs)

Lemma: mset_wf
∀s:DSet. (MSet{s} ∈ Type)

Lemma: mset_qinc
∀s:DSet. ((|s| List) ⊆r MSet{s})

Definition: mk_mset
mk_mset(as) ==  as

Lemma: mk_mset_wf
∀s:DSet. ∀as:|s| List.  (mk_mset(as) ∈ MSet{s})

Lemma: comb_for_mk_mset_wf
λs,as,z. mk_mset(as) ∈ s:DSet ⟶ as:(|s| List) ⟶ (↓True) ⟶ MSet{s}

Lemma: all_mset_elim
∀s:DSet. ∀F:MSet{s} ⟶ ℙ.  ((∀a:MSet{s}. SqStable(F[a])) ⇒ (∀a:MSet{s}. F[a] ⇐⇒ ∀a:|s| List. F[mk_mset(a)]))

Definition: null_mset
0{s} ==  []

Lemma: null_mset_wf
∀s:DSet. (0{s} ∈ MSet{s})

Definition: mset_count
x #∈ a ==  x #∈ a

Lemma: mset_count_wf
∀s:DSet. ∀x:|s|. ∀a:MSet{s}.  (x #∈ a ∈ ℕ)

Lemma: comb_for_mset_count_wf
λs,x,a,z. (x #∈ a) ∈ s:DSet ⟶ x:|s| ⟶ a:MSet{s} ⟶ (↓True) ⟶ ℕ

Definition: finite_set
FiniteSet{s} ==  {a:MSet{s}| ∀x:|s|. ((x #∈ a) ≤ 1)} 

Lemma: finite_set_wf
∀[s:DSet]. (FiniteSet{s} ∈ Type)

Lemma: mk_mset_wf2
∀s:DSet. ∀as:DisList{s}.  (mk_mset(as) ∈ FiniteSet{s})

Lemma: all_fset_elim
∀s:DSet. ∀F:MSet{s} ⟶ ℙ.
  ((∀a:FiniteSet{s}. SqStable(F[a])) ⇒ (∀a:FiniteSet{s}. F[a] ⇐⇒ ∀a:DisList{s}. F[mk_mset(a)]))

Definition: mset_inj
mset_inj{s}(x) ==  mk_mset([x])

Lemma: mset_inj_wf
∀s:DSet. ∀x:|s|.  (mset_inj{s}(x) ∈ MSet{s})

Lemma: comb_for_mset_inj_wf
λs,x,z. mset_inj{s}(x) ∈ s:DSet ⟶ x:|s| ⟶ (↓True) ⟶ MSet{s}

Definition: mset_sum
a + b ==  a @ b

Lemma: mset_sum_wf
∀s:DSet. ∀a,b:MSet{s}.  (a + b ∈ MSet{s})

Lemma: comb_for_mset_sum_wf
λs,a,b,z. (a + b) ∈ s:DSet ⟶ a:MSet{s} ⟶ b:MSet{s} ⟶ (↓True) ⟶ MSet{s}

Lemma: mset_sum_comm
∀s:DSet. Comm(MSet{s};λa,b. (a + b))

Lemma: mset_sum_assoc
∀s:DSet. Assoc(MSet{s};λa,b. (a + b))

Lemma: mk_mset_cons
∀s:DSet. ∀a:|s|. ∀as:|s| List.  (mk_mset([a / as]) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s})

Definition: eq_mset
eq_mset{s}(a,b) ==  a ≡b b

Lemma: eq_mset_wf
∀s:DSet. ∀a,b:MSet{s}.  (eq_mset{s}(a,b) ∈ 𝔹)

Lemma: assert_of_eq_mset
∀s:DSet. ∀a,b:MSet{s}.  (↑eq_mset{s}(a,b) ⇐⇒ a = b ∈ MSet{s})

Lemma: equal_mset_elim
∀s:DSet. ∀as,bs:|s| List.  (mk_mset(as) = mk_mset(bs) ∈ MSet{s} ⇐⇒ as ≡(|s|) bs)

Definition: mset_mon
mset_mon{s} ==  <MSet{s}, λx,y. eq_mset{s}(x,y), λx,y. tt, λx,y. (x + y), 0{s}, λx.x>

Lemma: mset_mon_wf
∀s:DSet. (mset_mon{s} ∈ AbMon)

Lemma: mset_sum_ident_r
∀s:DSet. ∀a:MSet{s}.  ((a + 0{s}) = a ∈ MSet{s})

Definition: mset_mem
x ∈b a ==  x ∈b a

Lemma: mset_mem_wf
∀s:DSet. ∀x:|s|. ∀a:MSet{s}.  (x ∈b a ∈ 𝔹)

Lemma: comb_for_mset_mem_wf
λs,x,a,z. (x ∈b a) ∈ s:DSet ⟶ x:|s| ⟶ a:MSet{s} ⟶ (↓True) ⟶ 𝔹

Lemma: mset_mem_null_lemma
∀x,s:Top.  (x ∈b 0{s} ~ ff)

Lemma: mset_mem_inj_sum_lemma
∀a,y,x,s:Top.  (x ∈b mset_inj{s}(y) + a ~ (y (=b) x) ∨b(x ∈b a))

Lemma: mset_mem_iff_count_nzero
∀s:DSet. ∀x:|s|. ∀a:MSet{s}.  (↑(x ∈b a) ⇐⇒ (x #∈ a) > 0)

Definition: ftype
FTy{s}(a) ==  {x:|s|| ↑(x ∈b a)} 

Lemma: ftype_wf
∀s:DSet. ∀a:MSet{s}.  (FTy{s}(a) ∈ Type)

Lemma: ftype_properties
∀s:DSet. ∀a:MSet{s}. ∀x:FTy{s}(a).  (↑(x ∈b a))

Lemma: mset_mon_for_elim
∀s:DSet. ∀T:Type. ∀f:T ⟶ (|s| List). ∀as:T List.
  ((For{mset_mon{s}} x ∈ as. mk_mset(f[x])) = mk_mset(For{<s List, @>} x ∈ as. f[x]) ∈ MSet{s})

Definition: mset_for
msFor{m} x ∈ a. f[x] ==  For{m} x ∈ a. f[x]

Lemma: mset_for_wf
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀a:MSet{s}.  (msFor{g} x ∈ a. f[x] ∈ |g|)

Lemma: comb_for_mset_for_wf
λs,g,f,a,z. (msFor{g} x ∈ a. f[x]) ∈ s:DSet ⟶ g:IAbMonoid ⟶ f:(|s| ⟶ |g|) ⟶ a:MSet{s} ⟶ (↓True) ⟶ |g|

Lemma: mset_for_functionality
∀s:DSet. ∀g:IAbMonoid. ∀f,f':|s| ⟶ |g|. ∀a,a':MSet{s}.
  ((a = a' ∈ MSet{s})
  ⇒ (∀x:|s|. ((↑(x ∈b a)) ⇒ (f[x] = f'[x] ∈ |g|)))
  ⇒ ((msFor{g} x ∈ a. f[x]) = (msFor{g} x ∈ a'. f'[x]) ∈ |g|))

Lemma: mset_for_mset_sum
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀a,b:MSet{s}.
  ((msFor{g} x ∈ a + b. f[x]) = ((msFor{g} x ∈ a. f[x]) * (msFor{g} x ∈ b. f[x])) ∈ |g|)

Lemma: mset_for_mset_inj
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀u:|s|.  ((msFor{g} x ∈ mset_inj{s}(u). f[x]) = f[u] ∈ |g|)

Lemma: mset_for_null_lemma
∀f,g,s:Top.  (msFor{g} x ∈ 0{s}. f[x] ~ e)

Lemma: mset_for_inj_lemma
∀f,a,y,g,s:Top.  (msFor{g} x ∈ mset_inj{s}(y) + a. f[x] ~ f[y] * (msFor{g} x ∈ a. f[x]))

Lemma: mset_for_elim_lemma
∀F,as,g,s:Top.  (msFor{g} x ∈ mk_mset(as). F[x] ~ For{g} x ∈ as. F[x])

Lemma: mset_for_of_id
∀s:DSet. ∀g:IAbMonoid. ∀a:MSet{s}.  ((msFor{g} x ∈ a. e) = e ∈ |g|)

Lemma: mset_for_of_op
∀g:IAbMonoid. ∀s:DSet. ∀e,f:|s| ⟶ |g|. ∀a:MSet{s}.
  ((msFor{g} x ∈ a. (e[x] * f[x])) = ((msFor{g} x ∈ a. e[x]) * (msFor{g} x ∈ a. f[x])) ∈ |g|)

Lemma: dist_hom_over_mset_for
∀s:DSet. ∀m,n:IAbMonoid. ∀f:MonHom(m,n). ∀a:MSet{s}. ∀g:|s| ⟶ |m|.
  ((f (msFor{m} x ∈ a. g[x])) = (msFor{n} x ∈ a. (f g[x])) ∈ |n|)

Lemma: mset_for_swap
∀g:IAbMonoid. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ |g|. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((msFor{g} x ∈ a. msFor{g} y ∈ b. f[x;y]) = (msFor{g} y ∈ b. msFor{g} x ∈ a. f[x;y]) ∈ |g|)

Lemma: bmsexists_char
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  ((∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x]))) ⇒ (↑(∃b{s} x ∈ a. f[x])))

Lemma: bmsexists_char_a
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  ((↑(∃b{s} x ∈ a. f[x])) ⇒ (↓∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x]))))

Lemma: bmsexists_char_a_rw
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  {(↑(∃b{s} x ∈ a. f[x])) ⇒ (↓∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x])))}

Lemma: bmsexists_char_rw
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  {(∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x]))) ⇒ (↑(∃b{s} x ∈ a. f[x]))}

Definition: mset_size
size{s}(a) ==  ||a||

Lemma: mset_size_wf
∀s:DSet. ∀a:MSet{s}.  (size{s}(a) ∈ ℤ)

Lemma: non_neg_mset_size
∀s:DSet. ∀a:MSet{s}.  (size{s}(a) ≥ 0 )

Lemma: mset_fact
∀s:DSet. ∀a:MSet{s}.  (a = (msFor{mset_mon{s}} x ∈ a. mset_inj{s}(x)) ∈ MSet{s})

Definition: free_abmonoid
FAbMon(S) ==
  mon:AbMon
  × inj:|S| ⟶ |mon|
  × (mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)})

Lemma: free_abmonoid_wf
∀S:DSet. (FAbMon(S) ∈ 𝕌')

Definition: free_abmon_mon
f.mon ==  fst(f)

Lemma: free_abmon_mon_wf
∀S:DSet. ∀f:FAbMon(S).  (f.mon ∈ AbMon)

Definition: free_abmon_inj
f.inj ==  fst(snd(f))

Lemma: free_abmon_inj_wf
∀S:DSet. ∀f:FAbMon(S).  (f.inj ∈ |S| ⟶ |f.mon|)

Definition: free_abmon_umap
f.umap ==  snd(snd(f))

Lemma: free_abmon_umap_wf
∀S:DSet. ∀f:FAbMon(S).
  (f.umap ∈ mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(f.mon,mon') | (g o f.inj) = f' ∈ (|S| ⟶ |mon'|)})

Definition: mset_fmon
mset_fmon(s) ==  <mset_mon{s}, λx:|s|. mset_inj{s}(x), λm.(λf:|s| ⟶ |m|. λy:MSet{s}. msFor{m} z ∈ y. (f z))>

Lemma: mset_fmon_wf
∀s:DSet. (mset_fmon(s) ∈ FAbMon(s))

Lemma: mset_mem_char
∀s:DSet. ∀x:|s|. ∀a:MSet{s}.  x ∈b a = ∃b{s} y ∈ a. (y (=b) x)

Definition: mset_map
msmap{s,s'}(f;a) ==  msFor{mset_mon{s'}} x ∈ a. mset_inj{s'}(f x)

Lemma: mset_map_wf
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀a:MSet{s}.  (msmap{s,s'}(f;a) ∈ MSet{s'})

Lemma: comb_for_mset_map_wf
λs,s',f,a,z. msmap{s,s'}(f;a) ∈ s:DSet ⟶ s':DSet ⟶ f:(|s| ⟶ |s'|) ⟶ a:MSet{s} ⟶ (↓True) ⟶ MSet{s'}

Lemma: mset_map_char
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀as:|s| List.  (msmap{s,s'}(f;mk_mset(as)) = mk_mset(map(f;as)) ∈ MSet{s'})

Lemma: mset_map_id
∀s:DSet. ∀a:MSet{s}.  (msmap{s,s}(Id{|s|};a) = a ∈ MSet{s})

Definition: mset_union
a ⋃ b ==  lmax(s;a;b)

Lemma: mset_union_wf
∀s:DSet. ∀a,b:MSet{s}.  (a ⋃ b ∈ MSet{s})

Definition: mset_inter
a ⋂s b ==  lmin(s;a;b)

Lemma: mset_inter_wf
∀s:DSet. ∀a,b:MSet{s}.  (a ⋂s b ∈ MSet{s})

Definition: mset_diff
a - b ==  a - b

Lemma: mset_diff_wf
∀s:DSet. ∀a,b:MSet{s}.  (a - b ∈ MSet{s})

Lemma: eq_mset_iff_eq_counts
∀s:DSet. ∀a,b:MSet{s}.  (a = b ∈ MSet{s} ⇐⇒ ∀x:|s|. ((x #∈ a) = (x #∈ b) ∈ ℤ))

Lemma: mset_count_inj
∀s:DSet. ∀a,x:|s|.  ((x #∈ mset_inj{s}(a)) = b2i(a (=b) x) ∈ ℤ)

Lemma: mset_count_sum
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  ((c #∈ (as + bs)) = ((c #∈ as) + (c #∈ bs)) ∈ ℤ)

Lemma: mset_count_union
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  ((c #∈ (as ⋃ bs)) = imax(c #∈ as;c #∈ bs) ∈ ℤ)

Lemma: mset_union_assoc
∀s:DSet. ∀a,b,c:MSet{s}.  ((a ⋃ (b ⋃ c)) = ((a ⋃ b) ⋃ c) ∈ MSet{s})

Lemma: mset_union_comm
∀s:DSet. ∀a,b:MSet{s}.  ((a ⋃ b) = (b ⋃ a) ∈ MSet{s})

Lemma: mset_union_ident_l
∀s:DSet. ∀a:MSet{s}.  ((0{s} ⋃ a) = a ∈ MSet{s})

Lemma: mset_union_ident_r
∀s:DSet. ∀a:MSet{s}.  ((a ⋃ 0{s}) = a ∈ MSet{s})

Definition: mset_union_mon
<MSet{s},⋃,0> ==  <MSet{s}, λx,y. eq_mset{s}(x,y), λx,y. tt, λx,y. (x ⋃ y), 0{s}, λx.x>

Lemma: mset_union_mon_wf
∀s:DSet. (<MSet{s},⋃,0> ∈ AbMon)

Lemma: mset_count_inter
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  ((c #∈ (as ⋂s bs)) = imin(c #∈ as;c #∈ bs) ∈ ℤ)

Lemma: mset_inter_assoc
∀s:DSet. ∀a,b,c:MSet{s}.  ((a ⋂s (b ⋂s c)) = ((a ⋂s b) ⋂s c) ∈ MSet{s})

Lemma: mset_inter_comm
∀s:DSet. ∀a,b:MSet{s}.  ((a ⋂s b) = (b ⋂s a) ∈ MSet{s})

Lemma: mset_count_diff
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  ((c #∈ (as - bs)) = ((c #∈ as) -- (c #∈ bs)) ∈ ℤ)

Lemma: fset_mem_union
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  c ∈b as ⋃ bs = (c ∈b as) ∨b(c ∈b bs)

Lemma: mset_mem_inter
∀s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  c ∈b as ⋂s bs = (c ∈b as) ∧b (c ∈b bs)

Lemma: mset_mem_sum
∀s:DSet. ∀a,b:MSet{s}. ∀u:|s|.  u ∈b a + b = (u ∈b a) ∨b(u ∈b b)

Lemma: mset_mem_diff
∀s:DSet. ∀as:FiniteSet{s}. ∀bs:MSet{s}. ∀c:|s|.  c ∈b as - bs = (c ∈b as) ∧b (¬b(c ∈b bs))

Lemma: mset_union_bor_mon_hom
∀s:DSet. ∀x:|s|.  IsMonHom{<MSet{s},⋃,0>,<𝔹,∨b>}(λu.(x ∈b u))

Lemma: mset_sum_bor_mon_hom
∀s:DSet. ∀x:|s|.  IsMonHom{mset_mon{s},<𝔹,∨b>}(λu.(x ∈b u))

Lemma: mset_mem_mon_for_union
∀s,s':DSet. ∀a:MSet{s}. ∀e:|s| ⟶ MSet{s'}. ∀x:|s'|.  x ∈b msFor{<MSet{s'},⋃,0>} y ∈ a. e[y] = ∃b{s} y ∈ a. (x ∈b e[y])

Lemma: mset_ind_a
∀s:DSet. ∀Q:MSet{s} ⟶ ℙ.
  ((∀w:MSet{s}. SqStable(Q[w]))
  ⇒ Q[0{s}]
  ⇒ (∀x:|s|. Q[mset_inj{s}(x)])
  ⇒ (∀ys,ys':MSet{s}.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys + ys']))
  ⇒ {∀zs:MSet{s}. Q[zs]})

Lemma: mset_count_bound_for_union
∀s,s':DSet. ∀n:ℕ. ∀e:|s| ⟶ MSet{s'}. ∀x:|s'|.
  ((∀y:|s|. ((x #∈ e[y]) ≤ n)) ⇒ (∀a:MSet{s}. ((x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ a. e[y])) ≤ n)))

Lemma: mset_mem_map
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀x:|s|. ∀a:MSet{s}.  ((↑(x ∈b a)) ⇒ (↑((f x) ∈b msmap{s,s'}(f;a))))

Definition: fset_of_mset
fset_of_mset(s;a) ==  msFor{<MSet{s},⋃,0>} x ∈ a. mset_inj{s}(x)

Lemma: fset_of_mset_wf
∀s:DSet. ∀a:MSet{s}.  (fset_of_mset(s;a) ∈ MSet{s})

Lemma: fset_of_mset_count_bound
∀s:DSet. ∀a:MSet{s}. ∀c:|s|.  ((c #∈ fset_of_mset(s;a)) ≤ 1)

Lemma: fset_of_mset_wf2
∀s:DSet. ∀a:MSet{s}.  (fset_of_mset(s;a) ∈ FiniteSet{s})

Lemma: fset_of_mset_mem
∀s:DSet. ∀a:MSet{s}. ∀c:|s|.  c ∈b fset_of_mset(s;a) = c ∈b a

Definition: fset_map
fs-map(f, a) ==  fset_of_mset(s';msmap{s,s'}(f;a))

Lemma: fset_map_wf
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀a:MSet{s}.  (fs-map(f, a) ∈ FiniteSet{s'})

Lemma: mset_mem_fmap
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀x:|s|. ∀a:MSet{s}.  ((↑(x ∈b a)) ⇒ (↑((f x) ∈b fs-map(f, a))))

Definition: bsubmset
a ⊆b b ==  bsublist(s;a;b)

Lemma: bsubmset_wf
∀s:DSet. ∀a,b:MSet{s}.  (a ⊆b b ∈ 𝔹)

Definition: bsupmset
a ⊇bs b ==  b ⊆b a

Lemma: bsupmset_wf
∀s:DSet. ∀a,b:MSet{s}.  (a ⊇bs b ∈ 𝔹)

Lemma: bsubmset_elim
∀s:DSet. ∀as,bs:|s| List.  mk_mset(as) ⊆b mk_mset(bs) = bsublist(s;as;bs)

Lemma: bsubmset_weakening
∀s:DSet. ∀a,b:MSet{s}.  ((a = b ∈ MSet{s}) ⇒ (↑(a ⊆b b)))

Lemma: bsubmset_transitivity
∀s:DSet. ∀a,b,c:MSet{s}.  ((↑(a ⊆b b)) ⇒ (↑(b ⊆b c)) ⇒ (↑(a ⊆b c)))

Lemma: bsubmset_functionality_wrt_bsubmset
∀s:DSet. ∀a,a',b,b':MSet{s}.  ((↑(a ⊇bs b)) ⇒ (↑(a' ⊆b b')) ⇒ (↑(a ⊆b a' ⇒b (b ⊆b b'))))

Lemma: count_bsubmset
∀s:DSet. ∀a,b:MSet{s}.  (↑(a ⊆b b) ⇐⇒ ∀x:|s|. ((x #∈ a) ≤ (x #∈ b)))

Lemma: fset_properties
∀s:DSet. ∀a:FiniteSet{s}.  {∀x:|s|. ((x #∈ a) ≤ 1)}

Lemma: mem_bsubmset
∀s:DSet. ∀a:FiniteSet{s}. ∀b:MSet{s}.  (↑(a ⊆b b) ⇐⇒ ∀x:|s|. ((↑(x ∈b a)) ⇒ (↑(x ∈b b))))

Lemma: mset_mem_functionality_wrt_bsubmset
∀s:DSet. ∀a:FiniteSet{s}. ∀b:MSet{s}. ∀u:|s|.  ((↑(a ⊆b b)) ⇒ (↑(u ∈b a ⇒b (u ∈b b))))

Lemma: detach_msubset
∀s:DSet. ∀a,b:MSet{s}.  ((↑(a ⊆b b)) ⇒ (b = ((b - a) + a) ∈ MSet{s}))

Lemma: comb_for_mk_mset_wf2
λs,as,z. mk_mset(as) ∈ s:DSet ⟶ as:DisList{s} ⟶ (↓True) ⟶ FiniteSet{s}

Lemma: null_mset_wf_f
∀s:DSet. (0{s} ∈ FiniteSet{s})

Lemma: mset_union_wf_f
∀s:DSet. ∀a,b:FiniteSet{s}.  (a ⋃ b ∈ FiniteSet{s})

Lemma: mset_inter_wf_f
∀s:DSet. ∀a,b:FiniteSet{s}.  (a ⋂s b ∈ FiniteSet{s})

Lemma: mset_diff_wf_f
∀s:DSet. ∀a,b:FiniteSet{s}.  (a - b ∈ FiniteSet{s})

Lemma: mset_inj_wf_f
∀s:DSet. ∀x:|s|.  (mset_inj{s}(x) ∈ FiniteSet{s})

Lemma: comb_for_mset_inj_wf_f
λs,x,z. mset_inj{s}(x) ∈ s:DSet ⟶ x:|s| ⟶ (↓True) ⟶ FiniteSet{s}

Definition: ffor
ffor(b0;b1;up;zs) ==  Y (λffor,zs. case zs of [] => b0 | z::zs' => up [z] zs' (b1 z) (ffor zs') esac) zs

Lemma: ffor_wf
∀T:Type. ∀Q:(T List) ⟶ Type. ∀b0:Q[[]]. ∀b1:∀x:T. Q[[x]]. ∀up:∀ys,ys':T List.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys']).
∀zs:T List.
  (ffor(b0;b1;up;zs) ∈ Q[zs])

Lemma: mset_for_when_none
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀as:MSet{s}.
  ((∀x:|s|. ((↑(x ∈b as)) ⇒ (¬↑b[x]))) ⇒ ((msFor{g} x ∈ as. when b[x]. f[x]) = e ∈ |g|))

Lemma: mset_for_when_unique
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.
  ((↑b[u])
  ⇒ (∀as:MSet{s}
        ((∀x:|s|. ((x #∈ as) ≤ 1))
        ⇒ (↑(u
           ∈b as))
        ⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
        ⇒ ((msFor{g} x ∈ as. when b[x]. f[x]) = f[u] ∈ |g|))))

Lemma: fset_for_when_unique
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.
  ((↑b[u])
  ⇒ (∀as:FiniteSet{s}
        ((↑(u
         ∈b as))
        ⇒ (∀v:|s|. ((↑b[v]) ⇒ (↑(v ∈b as)) ⇒ (v = u ∈ |s|)))
        ⇒ ((msFor{g} x ∈ as. when b[x]. f[x]) = f[u] ∈ |g|))))

Lemma: fset_for_when_eq
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀e:|s|. ∀as:FiniteSet{s}.
  ((↑(e ∈b as)) ⇒ ((msFor{g} x ∈ as. when x (=b) e. f[x]) = f[e] ∈ |g|))

Lemma: mset_for_when_dom_shift
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀c:|s| ⟶ 𝔹. ∀p,q:MSet{s}.
  ((↑(p ⊆b q))
  ⇒ (∀x:|s|. ((↑(x ∈b q - p)) ⇒ (¬↑c[x])))
  ⇒ ((msFor{g} x ∈ p. when c[x]. f[x]) = (msFor{g} x ∈ q. when c[x]. f[x]) ∈ |g|))

Lemma: mset_for_dom_shift
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀p,q:MSet{s}.
  ((↑(p ⊆b q))
  ⇒ (∀x:|s|. ((↑(x ∈b q - p)) ⇒ (f[x] = e ∈ |g|)))
  ⇒ ((msFor{g} x ∈ p. f[x]) = (msFor{g} x ∈ q. f[x]) ∈ |g|))

Lemma: mset_for_functionality_wrt_bsubmset
∀s:DSet. ∀g:IAbMonoid. ∀f,f':|s| ⟶ |g|. ∀p,q:MSet{s}.
  ((∀x:|s|. ((↑(x ∈b q - p)) ⇒ (f'[x] = e ∈ |g|)))
  ⇒ (↑(p ⊆b q))
  ⇒ (∀x:|s|. ((↑(x ∈b p)) ⇒ (f[x] = f'[x] ∈ |g|)))
  ⇒ ((msFor{g} x ∈ p. f[x]) = (msFor{g} x ∈ q. f'[x]) ∈ |g|))

Definition: mset_prod
a × b ==  msFor{<MSet{g↓set},⋃,0>} u ∈ a. msFor{<MSet{g↓set},⋃,0>} v ∈ b. mset_inj{g↓set}(u * v)

Lemma: mset_prod_wf
∀g:DMon. ∀a,b:MSet{g↓set}.  (a × b ∈ MSet{g↓set})

Lemma: mset_prod_wf2
∀g:DMon. ∀a,b:FiniteSet{g↓set}.  (a × b ∈ FiniteSet{g↓set})

Lemma: mset_prod_mem
∀g:DMon. ∀a,b:MSet{g↓set}. ∀u:|g|.  u ∈b a × b = ∃b{g↓set} v ∈ a. ∃b{g↓set} w ∈ b. (u =b (v * w))

Lemma: prod_in_mset_prod
∀g:DMon. ∀a,b:MSet{g↓set}. ∀u,v:|g|.  ((↑(u ∈b a)) ⇒ (↑(v ∈b b)) ⇒ (↑((u * v) ∈b a × b)))



Home Index