Definition: before
before(u;ps) ==  null(ps) ∨b(hd(ps) <b u)

Lemma: before_wf
a:DSet. ∀ps:|a| List. ∀u:|a|.  (before(u;ps) ∈ 𝔹)

Lemma: comb_for_before_wf
λa,ps,u,z. before(u;ps) ∈ a:DSet ⟶ ps:(|a| List) ⟶ u:|a| ⟶ (↓True) ⟶ 𝔹

Lemma: before_nil_lemma
u,a:Top.  (before(u;[]) tt)

Lemma: before_cons_lemma
vs,v,u,a:Top.  (before(u;[v vs]) v <b u)

Lemma: before_trans
a:LOSet. ∀u,v:|a|. ∀ws:|a| List.  ((v <u)  (↑before(v;ws))  (↑before(u;ws)))

Definition: sd_ordered
sd_ordered(as) ==  sd_ordered,as. case as of [] => tt a::bs => before(a;bs) ∧b (sd_ordered bs) esac) as

Lemma: sd_ordered_wf
s:DSet. ∀as:|s| List.  (sd_ordered(as) ∈ 𝔹)

Lemma: comb_for_sd_ordered_wf
λs,as,z. sd_ordered(as) ∈ s:DSet ⟶ as:(|s| List) ⟶ (↓True) ⟶ 𝔹

Lemma: sd_ordered_nil_lemma
s:Top. (sd_ordered([]) tt)

Lemma: sd_ordered_cons_lemma
as,a,s:Top.  (sd_ordered([a as]) before(a;as) ∧b sd_ordered(as))

Lemma: sd_ordered_char
s:QOSet. ∀us:|s| List.  sd_ordered(us) HTFor{<𝔹,∧b>v::vs ∈ us. ∀bw(:|s|) ∈ vs. (w <b v)

Lemma: before_all_imp_count_zero
s:QOSet. ∀a:|s|. ∀cs:|s| List.  ((↑(∀bc(:|s|) ∈ cs. (c <b a)))  ((a #∈ cs) 0 ∈ ℤ))

Lemma: sd_ordered_count
s:QOSet. ∀as:|s| List.  ((↑sd_ordered(as))  (∀c:|s|. ((c #∈ as) ≤ 1)))

Definition: oalist
oal(a;b) ==  {ps:(a × (b↓set)) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))}

Lemma: oalist_wf
a:LOSet. ∀b:AbDMon.  (oal(a;b) ∈ DSet)

Lemma: oalist_subtype
[a:LOSet]. ∀[b1,b2:AbDMon].  |oal(a;b1)| ⊆|oal(a;b2)| supposing strong-subtype(|b1|;|b2|) ∧ (e e ∈ |b2|)

Lemma: oalist_strong-subtype
[a:LOSet]. ∀[b1,b2:AbDMon].
  strong-subtype(|oal(a;b1)|;|oal(a;b2)|) supposing strong-subtype(|b1|;|b2|) ∧ (e e ∈ |b2|)

Lemma: oalist_car_properties
a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|.  ((↑sd_ordered(map(λx.(fst(x));ws))) ∧ (¬↑(e ∈b map(λx.(snd(x));ws))))

Lemma: respects-equality-oalist1
[s:LOSet]. ∀[g:AbDMon].  respects-equality(|(s × (g↓set))| List;|oal(s;g)|)

Lemma: respects-equality-oalist2
[s:LOSet]. ∀[g:AbDMon].  respects-equality((|s| × |g|) List;|oal(s;g)|)

Lemma: before_imp_before_all
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.
  ((↑before(k;map(λz.(fst(z));ps)))  (↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps). (x <b k))))

Lemma: before_all_imp_before
a:LOSet. ∀b:AbMon. ∀k:|a|. ∀ps:(|a| × |b|) List.
  ((↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps). (x <b k)))  (↑before(k;map(λz.(fst(z));ps))))

Lemma: nil_in_oalist
a:LOSet. ∀b:AbDMon.  ([] ∈ |oal(a;b)|)

Lemma: cons_in_oalist
a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.
  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  ([<x, y> ws] ∈ |oal(a;b)|))

Lemma: cons_pr_in_oalist
a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.
  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  ([<x, y> ws] ∈ |oal(a;b)|))

Definition: oal_nil
00 ==  []

Lemma: oal_nil_wf
a:LOSet. ∀b:AbDMon.  (00 ∈ |oal(a;b)|)

Definition: oal_cons_pr
oal_cons_pr(x;y;ws) ==  [<x, y> ws]

Lemma: oal_cons_pr_wf
a:LOSet. ∀b:AbDMon. ∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.
  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  (oal_cons_pr(x;y;ws) ∈ |oal(a;b)|))

Lemma: oalist_cases
a:LOSet. ∀b:AbDMon. ∀Q:((|a| × |b|) List) ⟶ ℙ.
   (∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  Q[[<x, y> ws]]))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: oalist_cases_a
a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
   (∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  Q[[<x, y> ws]]))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: oalist_cases_c
a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
   (∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  Q[oal_cons_pr(x;y;ws)]))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: oalist_cases_b
a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
   (∀ws:|oal(a;b)|. ∀k:|a|. ∀v:|b|.
        ((↑(∀bx(:|a|) ∈ map(λz.(fst(z));ws). (x <b k)))  (v e ∈ |b|))  Q[[<k, v> ws]]))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: oalist_ind
a:LOSet. ∀b:AbDMon. ∀Q:((|a| × |b|) List) ⟶ ℙ.
        (Q[ws]  (∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  Q[[<x, y> ws]]))))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: oalist_ind_a
a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
        (Q[ws]  (∀x:|a|. ∀y:|b|.  ((↑before(x;map(λx.(fst(x));ws)))  (y e ∈ |b|))  Q[[<x, y> ws]]))))
   {∀ws:|oal(a;b)|. Q[ws]})

Lemma: list_pr_length_ind
T:Type. ∀Q:(T List) ⟶ (T List) ⟶ ℙ.
  ((∀ps,qs:T List.  ((∀us,vs:T List.  (||us|| ||vs|| < ||ps|| ||qs||  Q[us;vs]))  Q[ps;qs]))
   {∀ps,qs:T List.  Q[ps;qs]})

Lemma: oalist_pr_length_ind
a:LOSet. ∀b:AbDMon. ∀Q:((|a| × |b|) List) ⟶ ((|a| × |b|) List) ⟶ ℙ.
  ((∀ps,qs:|oal(a;b)|.  ((∀us,vs:|oal(a;b)|.  (||us|| ||vs|| < ||ps|| ||qs||  Q[us;vs]))  Q[ps;qs]))
   {∀ps,qs:|oal(a;b)|.  Q[ps;qs]})

Definition: oal_dom
dom(ps) ==  mk_mset(map(λz.(fst(z));ps))

Lemma: oal_dom_wf
a:LOSet. ∀b:AbMon. ∀ps:(|a| × |b|) List.  (dom(ps) ∈ MSet{a})

Lemma: oal_dom_wf2
a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  (dom(ps) ∈ FiniteSet{a})

Definition: lookup
as[k] ==  lookup,as. case as of [] => b::bs => let bk,bv in if bk (=bthen bv else lookup bs fi  esac) as

Lemma: lookup_wf
a:PosetSig. ∀B:Type. ∀z:B. ∀k:|a|. ∀xs:(|a| × B) List.  (xs[k] ∈ B)

Lemma: comb_for_lookup_wf
λa,B,z,k,xs,z1. (xs[k]) ∈ a:PosetSig ⟶ B:Type ⟶ z:B ⟶ k:|a| ⟶ xs:((|a| × B) List) ⟶ (↓True) ⟶ B

Lemma: lookup_nil_lemma
k,z,s:Top.  ([][k] z)

Lemma: lookup_cons_pr_lemma
cs,b,a,k,z,s:Top.  ([<a, b> cs][k] if (=bthen else cs[k] fi )

Lemma: lookup_fails
a:DSet. ∀B:Type. ∀z:B. ∀k:|a|. ∀ps:(|a| × B) List.  ((¬↑(k ∈b map(λx.(fst(x));ps)))  ((ps[k]) z ∈ B))

Lemma: lookup_non_zero
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.  ((ps[k]) e ∈ |b|) ⇐⇒ ↑(k ∈b dom(ps)))

Lemma: lookup_oal_eq_id
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.  ((¬↑(k ∈b dom(ps)))  ((ps[k]) e ∈ |b|))

Lemma: lookup_before_start
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.  ((↑before(k;map(λz.(fst(z));ps)))  ((ps[k]) e ∈ |b|))

Lemma: lookup_oal_cons
a:LOSet. ∀b:OCMon. ∀k,kp:|a|. ∀vp:|b|. ∀ps:|oal(a;b)|.
  ((↑before(kp;map(λz.(fst(z));ps)))  (([<kp, vp> ps][k]) ((when kp (=bk. vp) (ps[k])) ∈ |b|))

Lemma: lookup_before_start_a
a:QOSet. ∀b:AbMon. ∀k:|a|. ∀ps:(|a| × |b|) List.
  ((↑(∀bk'(:|a|) ∈ map(λz.(fst(z));ps). (k' <b k)))  ((ps[k]) e ∈ |b|))

Lemma: lookups_same
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  ((∀u:|a|. ((ps[u]) (qs[u]) ∈ |b|))  (ps qs ∈ ((|a| × |b|) List)))

Lemma: lookups_same_a
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  ((∀u:|a|. ((ps[u]) (qs[u]) ∈ |b|))  (ps qs ∈ |oal(a;b)|))

Lemma: oal_equal_char
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  (ps qs ∈ |oal(a;b)| ⇐⇒ ∀u:|a|. ((ps[u]) (qs[u]) ∈ |b|))

Definition: oal_merge
ps ++ qs ==
  oal_merge,ps,qs. if null(ps) then qs
                    if null(qs) then ps
                    if (fst(hd(qs))) <b (fst(hd(ps))) then [hd(ps) (oal_merge tl(ps) qs)]
                    if (fst(hd(ps))) <b (fst(hd(qs))) then [hd(qs) (oal_merge ps tl(qs))]
                    if ((snd(hd(ps))) (snd(hd(qs)))) =b then oal_merge tl(ps) tl(qs)
                    else [<fst(hd(ps)), (snd(hd(ps))) (snd(hd(qs)))> (oal_merge tl(ps) tl(qs))]

Lemma: oal_merge_left_nil_lemma
qs,b,a:Top.  ([] ++ qs qs)

Lemma: oal_merge_right_nil_lemma
ps,p,b,a:Top.  ([p ps] ++ [] [p ps])

Lemma: oal_merge_conses_lemma
  ([<kp, vp> ps] ++ [<kq, vq> qs] if kq <b kp then [<kp, vp> (ps ++ [<kq, vq> qs])]
  if kp <b kq then [<kq, vq> ([<kp, vp> ps] ++ qs)]
  if (vp vq) =b then ps ++ qs
  else [<kp, vp vq> (ps ++ qs)]
  fi )

Lemma: oal_merge_wf
a:LOSet. ∀b:AbDMon. ∀ps,qs:(|a| × |b|) List.  (ps ++ qs ∈ (|a| × |b|) List)

Lemma: oal_merge_dom_pred
a:LOSet. ∀b:AbDMon. ∀Q:|a| ⟶ 𝔹. ∀ps,qs:(|a| × |b|) List.
  ((↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps)
   (↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs)
   (↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps ++ qs)

Lemma: oal_merge_sd_ordered
a:LOSet. ∀b:AbDMon. ∀ps,qs:(|a| × |b|) List.
  ((↑sd_ordered(map(λx.(fst(x));ps)))  (↑sd_ordered(map(λx.(fst(x));qs)))  (↑sd_ordered(map(λx.(fst(x));ps ++ qs))))

Lemma: oal_merge_non_id_vals
a:LOSet. ∀b:AbDMon. ∀ps,qs:(|a| × |b|) List.
  ((¬↑(e ∈b map(λx.(snd(x));ps)))  (¬↑(e ∈b map(λx.(snd(x));qs)))  (¬↑(e ∈b map(λx.(snd(x));ps ++ qs))))

Lemma: oal_merge_wf2
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  (ps ++ qs ∈ |oal(a;b)|)

Lemma: oal_dom_merge
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  (↑(dom(ps ++ qs) ⊆b (dom(ps) ⋃ dom(qs))))

Lemma: lookup_merge
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps,qs:|oal(a;b)|.  (((ps ++ qs)[k]) ((ps[k]) (qs[k])) ∈ |b|)

Lemma: oal_nil_ident_r
a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  ((ps ++ 00) ps ∈ |oal(a;b)|)

Lemma: oal_nil_ident_l
a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  ((00 ++ ps) ps ∈ |oal(a;b)|)

Lemma: oal_merge_comm
a:LOSet. ∀b:AbDMon. ∀ps,qs:|oal(a;b)|.  ((ps ++ qs) (qs ++ ps) ∈ |oal(a;b)|)

Lemma: oal_merge_assoc
a:LOSet. ∀b:AbDMon. ∀ps,qs,rs:|oal(a;b)|.  ((ps ++ qs ++ rs) ((ps ++ qs) ++ rs) ∈ |oal(a;b)|)

Definition: oal_mon
oal_mon(a;b) ==  <|oal(a;b)|, =b, λx,y. tt, λx,y. (x ++ y), 00, λx.x>

Lemma: oal_mon_wf
a:LOSet. ∀b:AbDMon.  (oal_mon(a;b) ∈ AbDMon)

Lemma: oalist_subtype_oal_mon
a:LOSet. ∀b:AbDMon.  (|oal(a;b)| ⊆|oal_mon(a;b)|)

Definition: oal_inj
inj(k,v) ==  if =b then [] else [<k, v>fi 

Lemma: oal_inj_wf
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀v:|b|.  (inj(k,v) ∈ |oal(a;b)|)

Lemma: comb_for_oal_inj_wf
λa,b,k,v,z. inj(k,v) ∈ a:LOSet ⟶ b:AbDMon ⟶ k:|a| ⟶ v:|b| ⟶ (↓True) ⟶ |oal(a;b)|

Lemma: lookup_oal_inj
a:LOSet. ∀b:AbDMon. ∀k,k':|a|. ∀v:|b|.  ((inj(k,v)[k']) (when (=bk'. v) ∈ |b|)

Lemma: oal_dom_inj
a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀v:|b|.  (dom(inj(k,v)) if =b then 0{a} else mset_inj{a}(k) fi  ∈ FiniteSet{a})

Lemma: oalist_fact
a:LOSet. ∀b:AbDMon. ∀ps:|oal(a;b)|.  (ps (msFor{oal_mon(a;b)} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |oal(a;b)|)

Definition: oal_neg
--ps ==  map(λkv.<fst(kv), (snd(kv))>;ps)

Lemma: oal_neg_wf
a:PosetSig. ∀b:GrpSig. ∀ps:(|a| × |b|) List.  (--ps ∈ (|a| × |b|) List)

Lemma: oal_neg_keys_invar
a:PosetSig. ∀b:GrpSig. ∀ps:(|a| × |b|) List.  (map(λz.(fst(z));--ps) map(λz.(fst(z));ps) ∈ (|a| List))

Lemma: oal_neg_sd_ordered
a:LOSet. ∀b:AbMon. ∀ps:(|a| × |b|) List.  ((↑sd_ordered(map(λx.(fst(x));ps)))  (↑sd_ordered(map(λx.(fst(x));--ps))))

Lemma: oal_neg_non_id_vals
a:LOSet. ∀b:AbDGrp. ∀ps:(|a| × |b|) List.  ((¬↑(e ∈b map(λx.(snd(x));ps)))  (¬↑(e ∈b map(λx.(snd(x));--ps))))

Lemma: oal_neg_wf2
a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (--ps ∈ |oal(a;b)|)

Lemma: lookup_oal_neg
a:DSet. ∀b:IGroup. ∀k:|a|. ∀ps:(|a| × |b|) List.  (((--ps)[k]) (~ (ps[k])) ∈ |b|)

Lemma: oal_dom_neg
a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (dom(--ps) dom(ps) ∈ FiniteSet{a})

Lemma: oal_neg_left_inv
a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (((--ps) ++ ps) 00 ∈ |oal(a;b)|)

Lemma: oal_neg_right_inv
a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  ((ps ++ (--ps)) 00 ∈ |oal(a;b)|)

Lemma: oal_neg_eq_nil
a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  ((--ps) 00 ∈ |oal(a;b)| ⇐⇒ ps 00 ∈ |oal(a;b)|)

Definition: oal_null
null(ps) ==  null(ps)

Lemma: oal_null_wf
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  (null(ps) ∈ 𝔹)

Lemma: assert_of_oal_null
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  (↑null(ps) ⇐⇒ ps 00 ∈ |oal(s;g)|)

Definition: oal_lk
lk(ps) ==  fst(hd(ps))

Lemma: oal_lk_wf
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lk(ps) ∈ |s|))

Lemma: oal_lk_in_dom
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (↑(lk(ps) ∈b dom(ps))))

Lemma: oal_lk_bounds_dom
s:LOSet. ∀g:AbDMon. ∀k:|s|. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (↑(k ∈b dom(ps)))  (k ≤ lk(ps)))

Definition: oal_lv
lv(ps) ==  snd(hd(ps))

Lemma: oal_lv_wf
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lv(ps) ∈ |g|))

Lemma: oal_lv_nid
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lv(ps) e ∈ |g|)))

Lemma: oal_lk_merge_1
s:LOSet. ∀g:AbDMon. ∀ps,qs:|oal(s;g)|.
  ((¬(ps 00 ∈ |oal(s;g)|))
   (qs 00 ∈ |oal(s;g)|))
   ((ps ++ qs) 00 ∈ |oal(s;g)|))
   (lk(ps) <lk(qs))
   (lk(ps ++ qs) lk(qs) ∈ |s|))

Lemma: oal_lk_merge_2
s:LOSet. ∀g:AbDMon. ∀ps,qs:|oal(s;g)|.
  ((¬(ps 00 ∈ |oal(s;g)|))
   (qs 00 ∈ |oal(s;g)|))
   ((ps ++ qs) 00 ∈ |oal(s;g)|))
   (lk(ps) lk(qs) ∈ |s|)
   ((lv(ps) lv(qs)) e ∈ |g|))
   (lk(ps ++ qs) lk(qs) ∈ |s|))

Lemma: oal_lk_neg
s:LOSet. ∀g:AbDGrp. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lk(--ps) lk(ps) ∈ |s|))

Lemma: lookup_oal_lk
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  ((ps[lk(ps)]) lv(ps) ∈ |g|))

Lemma: oal_lv_neg
s:LOSet. ∀g:AbDGrp. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lv(--ps) (~ lv(ps)) ∈ |g|))

Definition: oal_bpos
pos(ps) ==  bnull(ps)) ∧b (e <b lv(ps))

Lemma: oal_bpos_wf
s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  (pos(ps) ∈ 𝔹)

Lemma: comb_for_oal_bpos_wf
λs,g,ps,z. pos(ps) ∈ s:LOSet ⟶ g:AbDMon ⟶ ps:|oal(s;g)| ⟶ (↓True) ⟶ 𝔹

Definition: oal_blt
ps <<b qs ==  pos(qs ++ (--ps))

Lemma: oal_blt_wf
s:LOSet. ∀g:AbDGrp. ∀ps,qs:|oal(s;g)|.  (ps <<b qs ∈ 𝔹)

Definition: oal_ble
ps ≤≤b qs ==  (ps (=bqs) ∨b(ps <<b qs)

Lemma: oal_ble_wf
s:LOSet. ∀g:AbDGrp. ∀ps,qs:|oal(s;g)|.  (ps ≤≤b qs ∈ 𝔹)

Definition: oal_le
ps ≤{s,g} qs ==  ↑ps ≤≤b qs

Lemma: oal_le_wf
s:LOSet. ∀g:AbDGrp. ∀ps,qs:|oal(s;g)|.  (ps ≤{s,g} qs ∈ ℙ1)

Definition: oal_grp
oal_grp(s;g) ==  <|oal(s;g)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.(--x)>

Lemma: oal_grp_wf
s:LOSet. ∀g:AbDGrp.  (oal_grp(s;g) ∈ AbDGrp)

Definition: oal_lt
ps << qs ==  ∃k:|s|. ((∀k':|s|. ((k <k')  ((ps[k']) (qs[k']) ∈ |g|))) ∧ ((ps[k]) < (qs[k])))

Lemma: oal_lt_wf
s:LOSet. ∀g:OCMon. ∀ps,qs:|oal(s;g)|.  (ps << qs ∈ ℙ)

Lemma: assert_of_oal_blt
s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  (↑(ps <<b qs) ⇐⇒ ps << qs)

Lemma: decidable__oal_lt
s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  Dec(ps << qs)

Lemma: oal_lt_irrefl
s:LOSet. ∀g:OCMon.  Irrefl(|oal(s;g)|;ps, << qs)

Lemma: oal_lt_trans
s:LOSet. ∀g:OCMon.  Trans(|oal(s;g)|;ps, << qs)

Lemma: oal_bpos_trichot
s:LOSet. ∀g:OGrp. ∀rs:|oal(s;g)|.  ((↑pos(rs)) ∨ (rs 00 ∈ |oal(s;g)|) ∨ (↑pos(--rs)))

Lemma: oal_lt_trichot
s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  ((ps << qs) ∨ (ps qs ∈ |oal(s;g)|) ∨ (qs << ps))

Lemma: oal_merge_preserves_lt
s:LOSet. ∀g:OCMon. ∀ps,qs,rs:|oal(s;g)|.  ((qs << rs)  ((ps ++ qs) << (ps ++ rs)))

Lemma: oal_le_char
s:LOSet. ∀g:OGrp.  ((ps,qs:|oal(s;g)|. ps ≤{s,g} qs) <≡>{|oal(s;g)|} ((ps,qs:|oal(s;g)|. ps << qs)o))

Lemma: oal_lt_char
s:LOSet. ∀g:OGrp.  ((ps,qs:|oal(s;g)|. ps << qs) <≡>{|oal(s;g)|} ((ps,qs:|oal(s;g)|. ps ≤{s,g} qs)\))

Lemma: oal_le_is_order
s:LOSet. ∀g:OGrp.  Order(|oal(s;g)|;ps, ≤{s,g} qs)

Lemma: oal_le_connex
s:LOSet. ∀g:OGrp.  Connex(|oal(s;g)|;ps, ≤{s,g} qs)

Lemma: oal_grp_wf1
s:LOSet. ∀g:OGrp.  (oal_grp(s;g) ∈ OMon)

Lemma: oal_lt_iff_grp_lt
s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  (ps << qs ⇐⇒ ps < qs)

Lemma: oal_grp_wf2
s:LOSet. ∀g:OGrp.  (oal_grp(s;g) ∈ OGrp)

Lemma: oal_merge_preserves_le
s:LOSet. ∀g:OGrp. ∀ps,qs,rs:|oal(s;g)|.  ((qs ≤{s,g} rs)  ((ps ++ qs) ≤{s,g} (ps ++ rs)))

Comment: set_car_inc_tcom
This inclusion lemma is needed in proof of oal_hgp_wf.

Need better way of finding appropriate inclusion lemmas.
Ideally, this lemma's proof should be completely automatic. 
Problem is that type information makes clauses look different, 
even though they eventually normalize to the same thing.

MSB:  gave new proof using reasoning and ⌜[Type] ⊆[Type]⌝ 

Lemma: set_car_inc
s:LOSet. ∀g:OGrp.  (|oal(s;g↓hgrp)| ⊆|oal(s;g)|)

Definition: oal_hgp
oal_hgp(s;g) ==  <|oal(s;g↓hgrp)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.x>

Lemma: oal_hgp_wf
s:LOSet. ∀g:OGrp.  (oal_hgp(s;g) ∈ GrpSig)

Lemma: oal_hgp_subtype_oal_grp
s:LOSet. ∀g:OGrp.  (|oal_hgp(s;g)| ⊆|oal_grp(s;g)|)

Comment: oalist_hgrp_eqs_com
Paul Jackson's comment
 "This lemma proves exactly that property
that should be true of subtypes, but that
isn't with the current definition of 
the subtype `predicate' because it
isn't fully fledged predicate well-formed
for any pair of types.

It also demonstrates proof patterns that could
be pulled out into `template proofs' "

Mark Bickford's comment
 We now have ⌜A ⊆B⌝ as "fully fledged predicate well-formed
       for any pair of types"
 But that does not imply that x,y:A are equal in A
 when they are equal in B.
 (Consider ⌜ℤ ⊆Top⌝)
 So what Paul was proving is what we have defined
 as ⌜strong-subtype(A;B)⌝..⋅

Lemma: oalist_hgrp_eqs
s:LOSet. ∀g:OGrp. ∀a1,a2:|oal(s;g↓hgrp)|.  ((a1 a2 ∈ |oal(s;g)|)  (a1 a2 ∈ |oal(s;g↓hgrp)|))

Lemma: oal_hgp_wf2
s:LOSet. ∀g:OGrp.  (oal_hgp(s;g) ∈ OCMon)

Lemma: oal_inj_mon_hom
a:LOSet. ∀b:AbDMon. ∀k:|a|.  IsMonHom{b,oal_mon(a;b)}(λv.inj(k,v))

Lemma: oal_umap_char
s:LOSet. ∀g:AbDMon. ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
  ps:|oal(s;g)|. msFor{h} k ∈ dom(ps)
                     (f (ps[k]))) !v:|oal(s;g)| ⟶ |h|
                                        ∧ (∀j:|s|. ((f j) (v w.inj(j,w))) ∈ (|g| ⟶ |h|))))

Definition: oal_umap
umap(h,f) ==  λps:|oal(s;g)|. msFor{h} k ∈ dom(ps). (f (ps[k]))

Lemma: oal_umap_wf
s:LOSet. ∀g:AbDMon. ∀h:AbMon. ∀f:|s| ⟶ |g| ⟶ |h|.  (umap(h,f) ∈ |oal(s;g)| ⟶ |h|)

Lemma: oal_umap_char_a
s:LOSet. ∀g:AbDMon. ∀h:AbMon. ∀f:|s| ⟶ MonHom(g,h).
  umap(h,f) !v:|oal(s;g)| ⟶ |h|
                (IsMonHom{oal_mon(s;g),h}(v) ∧ (∀j:|s|. ((f j) (v w.inj(j,w))) ∈ (|g| ⟶ |h|))))

Definition: oal_mcp
oal_mcp(s;g) ==  <oal_mon(s;g), λk,v. inj(k,v), λh,f,ps. (msFor{h} k ∈ dom(ps). (f (ps[k])))>

Lemma: oal_mcp_wf
s:LOSet. ∀g:AbDMon.  (oal_mcp(s;g) ∈ MCopower(s;g))

Definition: oal_omcp
oal_omcp{s,g} ==  <oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>

Lemma: oal_omcp_wf
s:LOSet. ∀g:OGrp.  (oal_omcp{s,g} ∈ MCopower(s;g↓hgrp))

Home Index