---

Definition: omralist
omral(g;r) ==  oal(g↓oset;r↓+gp)

Lemma: omralist_wf
∀g:OCMon. ∀r:CDRng.  (omral(g;r) ∈ DSet)

Definition: omral_dom
dom(ps) ==  dom(ps)

Lemma: omral_dom_wf
∀g:OCMon. ∀r:CRng. ∀ps:(|g| × |r|) List.  (dom(ps) ∈ MSet{g↓oset})

Lemma: omral_dom_wf2
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (dom(ps) ∈ FiniteSet{g↓oset})

Definition: omral_plus
ps ++ qs ==  ps ++ qs

Lemma: omral_plus_wf
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.  (ps ++ qs ∈ (|g| × |r|) List)

Lemma: omralist_car_properties
∀g:OCMon. ∀r:CDRng. ∀ws:|omral(g;r)|.  ((↑sd_ordered(map(λx.(fst(x));ws))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ws))))

Lemma: rng_before_imp_before_all
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.
  ((↑before(k;map(λz.(fst(z));ps))) ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). (x <b k))))

Lemma: rng_before_all_imp_before
∀g:OCMon. ∀r:CRng. ∀k:|g|. ∀ps:(|g| × |r|) List.
  ((↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). (x <b k))) ⇒ (↑before(k;map(λz.(fst(z));ps))))

Lemma: omralist_cases
∀g:OCMon. ∀r:CDRng. ∀Q:|omral(g;r)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|omral(g;r)|. ∀x:|g|. ∀y:|r|.  ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = 0 ∈ |r|)) ⇒ Q[[<x, y> / ws]]))
  ⇒ {∀ws:|omral(g;r)|. Q[ws]})

Lemma: omralist_ind_a
∀g:OCMon. ∀r:CDRng. ∀Q:|omral(g;r)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|omral(g;r)|
        (Q[ws] ⇒ (∀x:|g|. ∀y:|r|.  ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = 0 ∈ |r|)) ⇒ Q[[<x, y> / ws]]))))
  ⇒ {∀ws:|omral(g;r)|. Q[ws]})

Lemma: omral_lookups_same_a
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  ((∀u:|g|. ((ps[u]) = (qs[u]) ∈ |r|)) ⇒ (ps = qs ∈ |omral(g;r)|))

Lemma: rng_lookup_before_start
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = 0 ∈ |r|))

Lemma: lookup_omral_eq_zero
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.  ((¬↑(k ∈b dom(ps))) ⇒ ((ps[k]) = 0 ∈ |r|))

Lemma: omral_plus_sd_ordered
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.
  ((↑sd_ordered(map(λx.(fst(x));ps))) ⇒ (↑sd_ordered(map(λx.(fst(x));qs))) ⇒ (↑sd_ordered(map(λx.(fst(x));ps ++ qs))))

Lemma: omral_plus_non_zero_vals
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.
  ((¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));qs))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));ps ++ qs))))

Lemma: omral_plus_wf2
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  (ps ++ qs ∈ |omral(g;r)|)

Lemma: omral_plus_dom
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  (↑(dom(ps ++ qs) ⊆b (dom(ps) ⋃ dom(qs))))

Lemma: lookup_omral_plus
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps,qs:|omral(g;r)|.  (((ps ++ qs)[k]) = ((ps[k]) +r (qs[k])) ∈ |r|)

Definition: omral_zero
00g,r ==  00

Lemma: omral_zero_wf
∀g:OCMon. ∀r:CDRng.  (00g,r ∈ |omral(g;r)|)

Definition: omral_minus
--ps ==  --ps

Lemma: omral_minus_wf
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (--ps ∈ |omral(g;r)|)

Definition: omral_inj
inj(k,v) ==  inj(k,v)

Lemma: omral_inj_wf
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|.  (inj(k,v) ∈ |omral(g;r)|)

Lemma: omral_plus_comm
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  ((ps ++ qs) = (qs ++ ps) ∈ |omral(g;r)|)

Lemma: omral_plus_assoc
∀g:OCMon. ∀r:CDRng. ∀ps,qs,rs:|omral(g;r)|.  ((ps ++ (qs ++ rs)) = ((ps ++ qs) ++ rs) ∈ |omral(g;r)|)

Lemma: omral_dom_inj
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|.
  (dom(inj(k,v)) = if v =b 0 then 0{g↓oset} else mset_inj{g↓oset}(k) fi  ∈ FiniteSet{g↓oset})

Lemma: lookup_omral_inj
∀g:OCMon. ∀r:CDRng. ∀k,k':|g|. ∀v:|r|.  ((inj(k,v)[k']) = (when k =b k'. v) ∈ |r|)

Lemma: comb_for_omral_inj_wf
λg,r,k,v,z. inj(k,v) ∈ g:OCMon ⟶ r:CDRng ⟶ k:|g| ⟶ v:|r| ⟶ (↓True) ⟶ |omral(g;r)|

Lemma: omral_fact
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (ps = (msFor{oal_mon(g↓oset;r↓+gp)} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)

Definition: omral_alg
omral_alg(g;r) ==  <|omral(g;r)|, =b, λx,y. tt, λx,y. (x ++ y), 00g,r, λx.(--x), λx,y. (x ** y), 11, λx,y. (inr ⋅ ), λa,\000Cx. (a ⋅⋅ x)>

Lemma: omral_fact_a
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (ps = (msFor{omral_alg(g;r)↓grp} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)

Definition: omral_scale
<k,v>* ps ==
  Y 
  (λomral_scale,ps. case ps of 
                      [] => [] 
                      p::ps' =>
                       if (v * (snd(p))) =b 0
                      then omral_scale ps'
                      else [<k * (fst(p)), v * (snd(p))> / (omral_scale ps')]
                      fi  
                   esac) 
  ps

Lemma: omral_scale_wf
∀g:GrpSig. ∀r:RngSig. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.  (<k,v>* ps ∈ (|g| × |r|) List)

Lemma: omral_scale_dom_pred
∀g:OCMon. ∀r:CDRng. ∀Q:|g| ⟶ 𝔹. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). Q[k * x])) ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps). Q[x])))

Lemma: omral_scale_dom_bound
∀g:OCMon. ∀r:CDRng. ∀bound,k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps)
         (x <b bound)))
  ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));<k,v>* ps)
           (x <b (k * bound)))))

Lemma: omral_scale_sd_ordered
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((↑sd_ordered(map(λz.(fst(z));ps))) ⇒ (↑sd_ordered(map(λz.(fst(z));<k,v>* ps))))

Lemma: omral_scale_non_zero_vals
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((¬↑(0 ∈b map(λx.(snd(x));ps))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));<k,v>* ps))))

Lemma: omral_scale_wf2
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.  (<k,v>* ps ∈ |omral(g;r)|)

Lemma: omral_dom_scale
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.  (↑(dom(<k,v>* ps) ⊆b fs-map(λk'.(k' * k), dom(ps))))

Lemma: lookup_omral_scale_a
∀g:OCMon. ∀r:CDRng. ∀k,k':|g|. ∀v:|r|. ∀ps:|omral(g;r)|.  (((<k,v>* ps)[k * k']) = (v * (ps[k'])) ∈ |r|)

Lemma: lookup_omral_scale_b
∀g:OCMon. ∀r:CDRng. ∀k,k':|g|. ∀v:|r|. ∀ps:(|g| × |r|) List.
  ((¬(∃d:|g|. ((↑(d ∈b dom(ps))) ∧ ((k * d) = k' ∈ |g|)))) ⇒ (((<k,v>* ps)[k']) = 0 ∈ |r|))

Lemma: lookup_omral_scale_c
∀g:OCMon. ∀r:CDRng. ∀z,k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.
  (((<k,v>* ps)[z]) = (msFor{r↓+gp} y ∈ dom(ps). when (k * y) =b z. (v * (ps[y]))) ∈ |r|)

Lemma: lookup_omral_scale_d
∀g:OCMon. ∀r:CDRng. ∀z,k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.
  (((<k,v>* ps)[z]) = (Σy ∈ dom(ps). (when (k * y) =b z. (v * (ps[y])))) ∈ |r|)

Definition: omral_times
ps ** qs ==  Y (λomral_times,ps. case ps of [] => [] | p::ps' => (<fst(p),snd(p)>* qs) ++ (omral_times ps') esac) ps

Lemma: omral_times_wf
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.  (ps ** qs ∈ (|g| × |r|) List)

Lemma: omral_times_sd_ordered
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.
  ((↑sd_ordered(map(λz.(fst(z));qs))) ⇒ (↑sd_ordered(map(λz.(fst(z));ps ** qs))))

Lemma: omral_times_non_zero_vals
∀g:OCMon. ∀r:CDRng. ∀ps,qs:(|g| × |r|) List.  ((¬↑(0 ∈b map(λx.(snd(x));qs))) ⇒ (¬↑(0 ∈b map(λx.(snd(x));ps ** qs))))

Lemma: omral_times_wf2
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  (ps ** qs ∈ |omral(g;r)|)

Lemma: lookup_omral_times
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|. ∀z:|g|.
  (((ps ** qs)[z]) = (msFor{r↓+gp} x ∈ dom(ps). msFor{r↓+gp} y ∈ dom(qs). when (x * y) =b z. ((ps[x]) * (qs[y]))) ∈ |r|)

Lemma: lookup_omral_times_a
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|. ∀z:|g|.
  (((ps ** qs)[z]) = (Σx ∈ dom(ps). Σy ∈ dom(qs). (when (x * y) =b z. ((ps[x]) * (qs[y])))) ∈ |r|)

Lemma: mset_on_grp_eq
∀g:Top. (MSet{g↓set} ~ MSet{g↓oset})

Lemma: mset_inc
∀g:OCMon. (MSet{g↓set} ⊆r MSet{g↓oset})

Lemma: mset_inc_a
∀g:OCMon. (MSet{g↓oset} ⊆r MSet{g↓set})

Lemma: omral_times_dom
∀g:OCMon. ∀r:CDRng. ∀ps,qs:|omral(g;r)|.  (↑(dom(ps ** qs) ⊆b (dom(ps) × dom(qs))))

Lemma: omral_times_assoc
∀g:OCMon. ∀a:CDRng.  Assoc(|omral(g;a)|;λps,qs. (ps ** qs))

Lemma: omral_times_assoc_a
∀[g:OCMon]. ∀[a:CDRng]. ∀[ps,qs,rs:|omral(g;a)|].  ((ps ** (qs ** rs)) = ((ps ** qs) ** rs) ∈ |omral(g;a)|)

Lemma: omral_times_comm
∀g:OCMon. ∀a:CDRng.  Comm(|omral(g;a)|;λps,qs. (ps ** qs))

Lemma: omral_times_comm_a
∀g:OCMon. ∀a:CDRng.  ∀[ps,qs:|omral(g;a)|].  ((ps ** qs) = (qs ** ps) ∈ |omral(g;a)|)

Lemma: omral_bilinear
∀g:OCMon. ∀a:CDRng.  BiLinear(|omral(g;a)|;λps,qs. (ps ++ qs);λps,qs. (ps ** qs))

Lemma: omral_bilinear_a
∀g:OCMon. ∀a:CDRng.
  ∀[ps,qs,rs:|omral(g;a)|].
    (((ps ** (qs ++ rs)) = ((ps ** qs) ++ (ps ** rs)) ∈ |omral(g;a)|)
    ∧ (((qs ++ rs) ** ps) = ((qs ** ps) ++ (rs ** ps)) ∈ |omral(g;a)|))

Definition: omral_one
11 ==  inj(e,1)

Lemma: omral_one_wf
∀g:OCMon. ∀r:CDRng.  (11 ∈ |omral(g;r)|)

Lemma: omral_dom_one
∀g:OCMon. ∀r:CDRng.  ((¬(0 = 1 ∈ |r|)) ⇒ (dom(11) = mset_inj{g↓oset}(e) ∈ FiniteSet{g↓oset}))

Definition: omral_action
v ⋅⋅ ps ==  <e,v>* ps

Lemma: omral_action_wf
∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps:|omral(g;r)|.  (v ⋅⋅ ps ∈ |omral(g;r)|)

Lemma: comb_for_omral_action_wf
λg,r,v,ps,z. (v ⋅⋅ ps) ∈ g:OCMon ⟶ r:CDRng ⟶ v:|r| ⟶ ps:|omral(g;r)| ⟶ (↓True) ⟶ |omral(g;r)|

Lemma: omral_dom_action
∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps:|omral(g;r)|.  (↑(dom(v ⋅⋅ ps) ⊆b dom(ps)))

Lemma: lookup_omral_action
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|. ∀ps:|omral(g;r)|.  (((v ⋅⋅ ps)[k]) = (v * (ps[k])) ∈ |r|)

Lemma: omral_times_ident_l
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  ((11 ** ps) = ps ∈ |omral(g;r)|)

Lemma: omral_times_ident_r
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  ((ps ** 11) = ps ∈ |omral(g;r)|)

Lemma: omral_action_one
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  ((1 ⋅⋅ ps) = ps ∈ |omral(g;r)|)

Lemma: omral_action_times
∀g:OCMon. ∀r:CDRng. ∀v,w:|r|. ∀ps:|omral(g;r)|.  (((v * w) ⋅⋅ ps) = (v ⋅⋅ (w ⋅⋅ ps)) ∈ |omral(g;r)|)

Lemma: omral_action_times_r1
∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps,qs:|omral(g;r)|.  ((v ⋅⋅ (ps ** qs)) = ((v ⋅⋅ ps) ** qs) ∈ |omral(g;r)|)

Lemma: omral_action_times_r2
∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps,qs:|omral(g;r)|.  ((v ⋅⋅ (ps ** qs)) = (ps ** (v ⋅⋅ qs)) ∈ |omral(g;r)|)

Lemma: omral_action_plus_l
∀g:OCMon. ∀r:CDRng. ∀v,w:|r|. ∀ps:|omral(g;r)|.  (((v +r w) ⋅⋅ ps) = ((v ⋅⋅ ps) ++ (w ⋅⋅ ps)) ∈ |omral(g;r)|)

Lemma: omral_action_plus_r
∀g:OCMon. ∀r:CDRng. ∀v:|r|. ∀ps,qs:|omral(g;r)|.  ((v ⋅⋅ (ps ++ qs)) = ((v ⋅⋅ ps) ++ (v ⋅⋅ qs)) ∈ |omral(g;r)|)

Lemma: omral_action_inj
∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v,v':|r|.  ((v ⋅⋅ inj(k,v')) = inj(k,v * v') ∈ |omral(g;r)|)

Lemma: omral_alg_wf
∀g:OCMon. ∀r:CDRng.  (omral_alg(g;r) ∈ algebra_sig{i:l}(|r|))

Lemma: omral_alg_wf2
∀g:OCMon. ∀r:CDRng.  (omral_alg(g;r) ∈ CAlg(r))

Lemma: omral_inj_mon_op
∀g:OCMon. ∀r:CDRng. ∀k,k':|g|.  (inj(k * k',1) = (inj(k,1) ** inj(k',1)) ∈ |omral(g;r)|)

Definition: omral_alg_umap
alg_umap(n,f) ==  λps:|omral(g;a)|. Σk ∈ dom(ps). ((ps[k]) n.act (f k))

Lemma: omral_alg_umap_wf
∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:|g| ⟶ n.car.  (alg_umap(n,f) ∈ |omral(g;a)| ⟶ n.car)

Lemma: omral_alg_umap_is_hom
∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:MonHom(g,n↓rg↓xmn).  alg_hom_p(a; omral_alg(g;a); n; alg_umap(n,f))

Lemma: omral_alg_umap_tri_comm
∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:|g| ⟶ n.car.  ((alg_umap(n,f) o (λk.inj(k,1))) = f ∈ (|g| ⟶ n.car))

Lemma: omral_alg_umap_unique
∀g:OCMon. ∀a:CDRng. ∀n:algebra{i:l}(a). ∀f:|g| ⟶ n.car. ∀f':algebra_hom(a; omral_alg(g;a); n).
  (((f' o (λk:|g|. inj(k,1))) = f ∈ (|g| ⟶ n.car)) ⇒ (f' = alg_umap(n,f) ∈ (|omral(g;a)| ⟶ n.car)))

Definition: omral_fma
omral_fma(g;a) ==  <omral_alg(g;a), λk.inj(k,1), λn,f. alg_umap(n,f)>

Lemma: omral_fma_wf
∀g:OCMon. ∀a:CDRng.  (omral_fma(g;a) ∈ fma_sig{i:l}(g;a))

Lemma: omral_fma_wf2
∀g:OCMon. ∀a:CDRng.  (omral_fma(g;a) ∈ FMonAlg(g;a))



Home Index