---

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 <a u) ⇒ (↑before(v;ws)) ⇒ (↑before(u;ws)))

Definition: sd_ordered
sd_ordered(as) ==  Y (λ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)| ⊆r |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) ⟶ ℙ.
  (Q[[]]
  ⇒ (∀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)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀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)| ⟶ ℙ.
  (Q[00]
  ⇒ (∀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)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀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:|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: oalist_ind_a
∀a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
  (Q[[]]
  ⇒ (∀ws:|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] ==  Y (λlookup,as. case as of [] => z | b::bs => let bk,bv = b in if bk (=b) k then 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 a (=b) k then b 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 (=b) k. 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 ==
  Y 
  (λ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 e then oal_merge tl(ps) tl(qs)
                    else [<fst(hd(ps)), (snd(hd(ps))) * (snd(hd(qs)))> / (oal_merge tl(ps) tl(qs))]
                    fi ) 
  ps 
  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
∀qs,vq,kq,ps,vp,kp,b,a:Top.
  ([<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 e 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)
         Q[x]))
  ⇒ (↑(∀bx(:|a|) ∈ map(λx.(fst(x));qs)
           Q[x]))
  ⇒ (↑(∀bx(:|a|) ∈ map(λx.(fst(x));ps ++ qs)
           Q[x])))

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)| ⊆r |oal_mon(a;b)|)

Definition: oal_inj
inj(k,v) ==  if v =b e 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 k (=b) k'. v) ∈ |b|)

Lemma: oal_dom_inj
∀a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀v:|b|.  (dom(inj(k,v)) = if v =b e 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) <s 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 (=b) qs) ∨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 <s 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.ps << qs)

Lemma: oal_lt_trans
∀s:LOSet. ∀g:OCMon.  Trans(|oal(s;g)|;ps,qs.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,qs.ps ≤{s,g} qs)

Lemma: oal_le_connex
∀s:LOSet. ∀g:OGrp.  Connex(|oal(s;g)|;ps,qs.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:  I gave a new proof using ~ reasoning and ⌜[Type] ⊆r [Type]⌝ 

Lemma: set_car_inc
∀s:LOSet. ∀g:OGrp.  (|oal(s;g↓hgrp)| ⊆r |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)| ⊆r |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 a 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 ⊆r B⌝ as a "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 ⌜ℤ ⊆r 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 k (ps[k]))) = !v:|oal(s;g)| ⟶ |h|
                                        (IsMonHom{oal_mon(s;g),h}(v)
                                        ∧ (∀j:|s|. ((f j) = (v o (λw.inj(j,w))) ∈ (|g| ⟶ |h|))))

Definition: oal_umap
umap(h,f) ==  λps:|oal(s;g)|. msFor{h} k ∈ dom(ps). (f k (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 o (λ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 k (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