Theory "canonical"

Parents semi_ring quote

Signature

Type	Arity
canonical_sum	1
spolynom	1
Constant	Type
Cons_monom	:α -> index list -> α canonical_sum -> α canonical_sum
Cons_varlist	:index list -> α canonical_sum -> α canonical_sum
Nil_monom	:α canonical_sum
SPconst	:α -> α spolynom
SPmult	:α spolynom -> α spolynom -> α spolynom
SPplus	:α spolynom -> α spolynom -> α spolynom
SPvar	:index -> α spolynom
canonical_sum_CASE	:α canonical_sum -> β -> (α -> index list -> α canonical_sum -> β) -> (index list -> α canonical_sum -> β) -> β
canonical_sum_merge	:α semi_ring -> α canonical_sum -> α canonical_sum -> α canonical_sum
canonical_sum_prod	:α semi_ring -> α canonical_sum -> α canonical_sum -> α canonical_sum
canonical_sum_scalar	:α semi_ring -> α -> α canonical_sum -> α canonical_sum
canonical_sum_scalar2	:α semi_ring -> index list -> α canonical_sum -> α canonical_sum
canonical_sum_scalar3	:α semi_ring -> α -> index list -> α canonical_sum -> α canonical_sum
canonical_sum_simplify	:α semi_ring -> α canonical_sum -> α canonical_sum
canonical_sum_size	:(α -> num) -> α canonical_sum -> num
ics_aux	:α semi_ring -> α varmap -> α -> α canonical_sum -> α
interp_cs	:α semi_ring -> α varmap -> α canonical_sum -> α
interp_m	:α semi_ring -> α varmap -> α -> index list -> α
interp_sp	:α semi_ring -> α varmap -> α spolynom -> α
interp_vl	:α semi_ring -> α varmap -> index list -> α
ivl_aux	:α semi_ring -> α varmap -> index -> index list -> α
monom_insert	:α semi_ring -> α -> index list -> α canonical_sum -> α canonical_sum
spolynom_CASE	:α spolynom -> (index -> β) -> (α -> β) -> (α spolynom -> α spolynom -> β) -> (α spolynom -> α spolynom -> β) -> β
spolynom_normalize	:α semi_ring -> α spolynom -> α canonical_sum
spolynom_simplify	:α semi_ring -> α spolynom -> α canonical_sum
spolynom_size	:(α -> num) -> α spolynom -> num
varlist_insert	:α semi_ring -> index list -> α canonical_sum -> α canonical_sum

Definitions

canonical_sum_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('canonical_sum').
             (∀a0'.
                (a0' = ind_type$CONSTR 0 (ARB,ARB) (λn. ind_type$BOTTOM)) ∨
                (∃a0 a1 a2.
                   (a0' =
                    (λa0 a1 a2.
                         ind_type$CONSTR (SUC 0) (a0,a1)
                           (ind_type$FCONS a2 (λn. ind_type$BOTTOM))) a0 a1 a2) ∧
                   $var$('canonical_sum') a2) ∨
                (∃a0 a1.
                   (a0' =
                    (λa0 a1.
                         ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
                           (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0 a1) ∧
                   $var$('canonical_sum') a1) ⇒
                $var$('canonical_sum') a0') ⇒
             $var$('canonical_sum') a0') rep

canonical_sum_case_def

⊢ (∀v f f1. canonical_sum_CASE Nil_monom v f f1 = v) ∧
  (∀a0 a1 a2 v f f1.
     canonical_sum_CASE (Cons_monom a0 a1 a2) v f f1 = f a0 a1 a2) ∧
  ∀a0 a1 v f f1. canonical_sum_CASE (Cons_varlist a0 a1) v f f1 = f1 a0 a1

canonical_sum_prod_def

⊢ (∀sr c1 l1 t1 s2.
     canonical_sum_prod sr (Cons_monom c1 l1 t1) s2 =
     canonical_sum_merge sr (canonical_sum_scalar3 sr c1 l1 s2)
       (canonical_sum_prod sr t1 s2)) ∧
  (∀sr l1 t1 s2.
     canonical_sum_prod sr (Cons_varlist l1 t1) s2 =
     canonical_sum_merge sr (canonical_sum_scalar2 sr l1 s2)
       (canonical_sum_prod sr t1 s2)) ∧
  ∀sr s2. canonical_sum_prod sr Nil_monom s2 = Nil_monom

canonical_sum_scalar2_def

⊢ (∀sr l0 c l t.
     canonical_sum_scalar2 sr l0 (Cons_monom c l t) =
     monom_insert sr c (list_merge index_lt l0 l)
       (canonical_sum_scalar2 sr l0 t)) ∧
  (∀sr l0 l t.
     canonical_sum_scalar2 sr l0 (Cons_varlist l t) =
     varlist_insert sr (list_merge index_lt l0 l)
       (canonical_sum_scalar2 sr l0 t)) ∧
  ∀sr l0. canonical_sum_scalar2 sr l0 Nil_monom = Nil_monom

canonical_sum_scalar3_def

⊢ (∀sr c0 l0 c l t.
     canonical_sum_scalar3 sr c0 l0 (Cons_monom c l t) =
     monom_insert sr (sr.SRM c0 c) (list_merge index_lt l0 l)
       (canonical_sum_scalar3 sr c0 l0 t)) ∧
  (∀sr c0 l0 l t.
     canonical_sum_scalar3 sr c0 l0 (Cons_varlist l t) =
     monom_insert sr c0 (list_merge index_lt l0 l)
       (canonical_sum_scalar3 sr c0 l0 t)) ∧
  ∀sr c0 l0. canonical_sum_scalar3 sr c0 l0 Nil_monom = Nil_monom

canonical_sum_scalar_def

⊢ (∀sr c0 c l t.
     canonical_sum_scalar sr c0 (Cons_monom c l t) =
     Cons_monom (sr.SRM c0 c) l (canonical_sum_scalar sr c0 t)) ∧
  (∀sr c0 l t.
     canonical_sum_scalar sr c0 (Cons_varlist l t) =
     Cons_monom c0 l (canonical_sum_scalar sr c0 t)) ∧
  ∀sr c0. canonical_sum_scalar sr c0 Nil_monom = Nil_monom

canonical_sum_simplify_def

⊢ (∀sr c l t.
     canonical_sum_simplify sr (Cons_monom c l t) =
     if c = sr.SR0 then canonical_sum_simplify sr t
     else if c = sr.SR1 then Cons_varlist l (canonical_sum_simplify sr t)
     else Cons_monom c l (canonical_sum_simplify sr t)) ∧
  (∀sr l t.
     canonical_sum_simplify sr (Cons_varlist l t) =
     Cons_varlist l (canonical_sum_simplify sr t)) ∧
  ∀sr. canonical_sum_simplify sr Nil_monom = Nil_monom

canonical_sum_size_def

⊢ (∀f. canonical_sum_size f Nil_monom = 0) ∧
  (∀f a0 a1 a2.
     canonical_sum_size f (Cons_monom a0 a1 a2) =
     1 + (f a0 + (list_size index_size a1 + canonical_sum_size f a2))) ∧
  ∀f a0 a1.
    canonical_sum_size f (Cons_varlist a0 a1) =
    1 + (list_size index_size a0 + canonical_sum_size f a1)

ics_aux_def

⊢ (∀sr vm a. ics_aux sr vm a Nil_monom = a) ∧
  (∀sr vm a l t.
     ics_aux sr vm a (Cons_varlist l t) =
     sr.SRP a (ics_aux sr vm (interp_vl sr vm l) t)) ∧
  ∀sr vm a c l t.
    ics_aux sr vm a (Cons_monom c l t) =
    sr.SRP a (ics_aux sr vm (interp_m sr vm c l) t)

interp_cs_def

⊢ (∀sr vm. interp_cs sr vm Nil_monom = sr.SR0) ∧
  (∀sr vm l t.
     interp_cs sr vm (Cons_varlist l t) = ics_aux sr vm (interp_vl sr vm l) t) ∧
  ∀sr vm c l t.
    interp_cs sr vm (Cons_monom c l t) = ics_aux sr vm (interp_m sr vm c l) t

interp_m_def

⊢ (∀sr vm c. interp_m sr vm c [] = c) ∧
  ∀sr vm c x t. interp_m sr vm c (x::t) = sr.SRM c (ivl_aux sr vm x t)

interp_sp_def

⊢ (∀sr vm c. interp_sp sr vm (SPconst c) = c) ∧
  (∀sr vm i. interp_sp sr vm (SPvar i) = varmap_find i vm) ∧
  (∀sr vm p1 p2.
     interp_sp sr vm (SPplus p1 p2) =
     sr.SRP (interp_sp sr vm p1) (interp_sp sr vm p2)) ∧
  ∀sr vm p1 p2.
    interp_sp sr vm (SPmult p1 p2) =
    sr.SRM (interp_sp sr vm p1) (interp_sp sr vm p2)

interp_vl_def

⊢ (∀sr vm. interp_vl sr vm [] = sr.SR1) ∧
  ∀sr vm x t. interp_vl sr vm (x::t) = ivl_aux sr vm x t

ivl_aux_def

⊢ (∀sr vm x. ivl_aux sr vm x [] = varmap_find x vm) ∧
  ∀sr vm x x' t'.
    ivl_aux sr vm x (x'::t') = sr.SRM (varmap_find x vm) (ivl_aux sr vm x' t')

spolynom_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('spolynom').
             (∀a0'.
                (∃a. a0' =
                     (λa. ind_type$CONSTR 0 (a,ARB) (λn. ind_type$BOTTOM)) a) ∨
                (∃a. a0' =
                     (λa.
                          ind_type$CONSTR (SUC 0) (ARB,a)
                            (λn. ind_type$BOTTOM)) a) ∨
                (∃a0 a1.
                   (a0' =
                    (λa0 a1.
                         ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB)
                           (ind_type$FCONS a0
                              (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
                      a1) ∧ $var$('spolynom') a0 ∧ $var$('spolynom') a1) ∨
                (∃a0 a1.
                   (a0' =
                    (λa0 a1.
                         ind_type$CONSTR (SUC (SUC (SUC 0))) (ARB,ARB)
                           (ind_type$FCONS a0
                              (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
                      a1) ∧ $var$('spolynom') a0 ∧ $var$('spolynom') a1) ⇒
                $var$('spolynom') a0') ⇒
             $var$('spolynom') a0') rep

spolynom_case_def

⊢ (∀a f f1 f2 f3. spolynom_CASE (SPvar a) f f1 f2 f3 = f a) ∧
  (∀a f f1 f2 f3. spolynom_CASE (SPconst a) f f1 f2 f3 = f1 a) ∧
  (∀a0 a1 f f1 f2 f3. spolynom_CASE (SPplus a0 a1) f f1 f2 f3 = f2 a0 a1) ∧
  ∀a0 a1 f f1 f2 f3. spolynom_CASE (SPmult a0 a1) f f1 f2 f3 = f3 a0 a1

spolynom_normalize_def

⊢ (∀sr i. spolynom_normalize sr (SPvar i) = Cons_varlist [i] Nil_monom) ∧
  (∀sr c. spolynom_normalize sr (SPconst c) = Cons_monom c [] Nil_monom) ∧
  (∀sr l r.
     spolynom_normalize sr (SPplus l r) =
     canonical_sum_merge sr (spolynom_normalize sr l)
       (spolynom_normalize sr r)) ∧
  ∀sr l r.
    spolynom_normalize sr (SPmult l r) =
    canonical_sum_prod sr (spolynom_normalize sr l) (spolynom_normalize sr r)

spolynom_simplify_def

⊢ ∀sr x.
    spolynom_simplify sr x =
    canonical_sum_simplify sr (spolynom_normalize sr x)

spolynom_size_def

⊢ (∀f a. spolynom_size f (SPvar a) = 1 + index_size a) ∧
  (∀f a. spolynom_size f (SPconst a) = 1 + f a) ∧
  (∀f a0 a1.
     spolynom_size f (SPplus a0 a1) =
     1 + (spolynom_size f a0 + spolynom_size f a1)) ∧
  ∀f a0 a1.
    spolynom_size f (SPmult a0 a1) =
    1 + (spolynom_size f a0 + spolynom_size f a1)

Theorems

canonical_sum_11

⊢ (∀a0 a1 a2 a0' a1' a2'.
     (Cons_monom a0 a1 a2 = Cons_monom a0' a1' a2') ⇔
     (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
  ∀a0 a1 a0' a1'.
    (Cons_varlist a0 a1 = Cons_varlist a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')

canonical_sum_Axiom

⊢ ∀f0 f1 f2. ∃fn.
    (fn Nil_monom = f0) ∧
    (∀a0 a1 a2. fn (Cons_monom a0 a1 a2) = f1 a0 a1 a2 (fn a2)) ∧
    ∀a0 a1. fn (Cons_varlist a0 a1) = f2 a0 a1 (fn a1)

canonical_sum_case_cong

⊢ ∀M M' v f f1.
    (M = M') ∧ ((M' = Nil_monom) ⇒ (v = v')) ∧
    (∀a0 a1 a2. (M' = Cons_monom a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ∧
    (∀a0 a1. (M' = Cons_varlist a0 a1) ⇒ (f1 a0 a1 = f1' a0 a1)) ⇒
    (canonical_sum_CASE M v f f1 = canonical_sum_CASE M' v' f' f1')

canonical_sum_case_eq

⊢ (canonical_sum_CASE x v f f1 = v') ⇔
  (x = Nil_monom) ∧ (v = v') ∨
  (∃a l c. (x = Cons_monom a l c) ∧ (f a l c = v')) ∨
  ∃l c. (x = Cons_varlist l c) ∧ (f1 l c = v')

canonical_sum_distinct

⊢ (∀a2 a1 a0. Nil_monom ≠ Cons_monom a0 a1 a2) ∧
  (∀a1 a0. Nil_monom ≠ Cons_varlist a0 a1) ∧
  ∀a2 a1' a1 a0' a0. Cons_monom a0 a1 a2 ≠ Cons_varlist a0' a1'

canonical_sum_induction

⊢ ∀P. P Nil_monom ∧ (∀c. P c ⇒ ∀l a. P (Cons_monom a l c)) ∧
      (∀c. P c ⇒ ∀l. P (Cons_varlist l c)) ⇒
      ∀c. P c

canonical_sum_merge_def

⊢ (∀t2 t1 sr l2 l1 c2 c1.
     canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less =>
         Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2))
     | Equal => Cons_monom (sr.SRP c1 c2) l1 (canonical_sum_merge sr t1 t2)
     | Greater =>
       Cons_monom c2 l2 (canonical_sum_merge sr (Cons_monom c1 l1 t1) t2)) ∧
  (∀t2 t1 sr l2 l1 c1.
     canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less =>
         Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2))
     | Equal =>
       Cons_monom (sr.SRP c1 sr.SR1) l1 (canonical_sum_merge sr t1 t2)
     | Greater =>
       Cons_varlist l2 (canonical_sum_merge sr (Cons_monom c1 l1 t1) t2)) ∧
  (∀t2 t1 sr l2 l1 c2.
     canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less =>
         Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2))
     | Equal =>
       Cons_monom (sr.SRP sr.SR1 c2) l1 (canonical_sum_merge sr t1 t2)
     | Greater =>
       Cons_monom c2 l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2)) ∧
  (∀t2 t1 sr l2 l1.
     canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_varlist l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less =>
         Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2))
     | Equal =>
       Cons_monom (sr.SRP sr.SR1 sr.SR1) l1 (canonical_sum_merge sr t1 t2)
     | Greater =>
       Cons_varlist l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2)) ∧
  (∀sr s1. canonical_sum_merge sr s1 Nil_monom = s1) ∧
  (∀v6 v5 v4 sr.
     canonical_sum_merge sr Nil_monom (Cons_monom v4 v5 v6) =
     Cons_monom v4 v5 v6) ∧
  ∀v8 v7 sr.
    canonical_sum_merge sr Nil_monom (Cons_varlist v7 v8) = Cons_varlist v7 v8

canonical_sum_merge_ind

⊢ ∀P. (∀sr c1 l1 t1 c2 l2 t2.
         ((list_cmp index_compare l1 l2 = Equal) ⇒ P sr t1 t2) ∧
         ((list_cmp index_compare l1 l2 = Greater) ⇒
          P sr (Cons_monom c1 l1 t1) t2) ∧
         ((list_cmp index_compare l1 l2 = Less) ⇒
          P sr t1 (Cons_monom c2 l2 t2)) ⇒
         P sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2)) ∧
      (∀sr c1 l1 t1 l2 t2.
         ((list_cmp index_compare l1 l2 = Equal) ⇒ P sr t1 t2) ∧
         ((list_cmp index_compare l1 l2 = Greater) ⇒
          P sr (Cons_monom c1 l1 t1) t2) ∧
         ((list_cmp index_compare l1 l2 = Less) ⇒ P sr t1 (Cons_varlist l2 t2)) ⇒
         P sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2)) ∧
      (∀sr l1 t1 c2 l2 t2.
         ((list_cmp index_compare l1 l2 = Equal) ⇒ P sr t1 t2) ∧
         ((list_cmp index_compare l1 l2 = Greater) ⇒
          P sr (Cons_varlist l1 t1) t2) ∧
         ((list_cmp index_compare l1 l2 = Less) ⇒
          P sr t1 (Cons_monom c2 l2 t2)) ⇒
         P sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2)) ∧
      (∀sr l1 t1 l2 t2.
         ((list_cmp index_compare l1 l2 = Equal) ⇒ P sr t1 t2) ∧
         ((list_cmp index_compare l1 l2 = Greater) ⇒
          P sr (Cons_varlist l1 t1) t2) ∧
         ((list_cmp index_compare l1 l2 = Less) ⇒ P sr t1 (Cons_varlist l2 t2)) ⇒
         P sr (Cons_varlist l1 t1) (Cons_varlist l2 t2)) ∧
      (∀sr s1. P sr s1 Nil_monom) ∧
      (∀sr v4 v5 v6. P sr Nil_monom (Cons_monom v4 v5 v6)) ∧
      (∀sr v7 v8. P sr Nil_monom (Cons_varlist v7 v8)) ⇒
      ∀v v1 v2. P v v1 v2

canonical_sum_merge_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm x y.
      interp_cs sr vm (canonical_sum_merge sr x y) =
      sr.SRP (interp_cs sr vm x) (interp_cs sr vm y)

canonical_sum_nchotomy

⊢ ∀cc.
    (cc = Nil_monom) ∨ (∃a l c. cc = Cons_monom a l c) ∨
    ∃l c. cc = Cons_varlist l c

canonical_sum_prod_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm x y.
      interp_cs sr vm (canonical_sum_prod sr x y) =
      sr.SRM (interp_cs sr vm x) (interp_cs sr vm y)

canonical_sum_scalar2_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm l s.
      interp_cs sr vm (canonical_sum_scalar2 sr l s) =
      sr.SRM (interp_vl sr vm l) (interp_cs sr vm s)

canonical_sum_scalar3_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm c l s.
      interp_cs sr vm (canonical_sum_scalar3 sr c l s) =
      sr.SRM (sr.SRM c (interp_vl sr vm l)) (interp_cs sr vm s)

canonical_sum_scalar_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm a s.
      interp_cs sr vm (canonical_sum_scalar sr a s) =
      sr.SRM a (interp_cs sr vm s)

canonical_sum_simplify_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm s. interp_cs sr vm (canonical_sum_simplify sr s) = interp_cs sr vm s

datatype_canonical_sum

⊢ DATATYPE (canonical_sum Nil_monom Cons_monom Cons_varlist)

datatype_spolynom

⊢ DATATYPE (spolynom SPvar SPconst SPplus SPmult)

ics_aux_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm x s. ics_aux sr vm x s = sr.SRP x (interp_cs sr vm s)

interp_m_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm x l. interp_m sr vm x l = sr.SRM x (interp_vl sr vm l)

ivl_aux_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm v i. ivl_aux sr vm i v = sr.SRM (varmap_find i vm) (interp_vl sr vm v)

monom_insert_def

⊢ (∀t2 sr l2 l1 c2 c1.
     monom_insert sr c1 l1 (Cons_monom c2 l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less => Cons_monom c1 l1 (Cons_monom c2 l2 t2)
     | Equal => Cons_monom (sr.SRP c1 c2) l1 t2
     | Greater => Cons_monom c2 l2 (monom_insert sr c1 l1 t2)) ∧
  (∀t2 sr l2 l1 c1.
     monom_insert sr c1 l1 (Cons_varlist l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less => Cons_monom c1 l1 (Cons_varlist l2 t2)
     | Equal => Cons_monom (sr.SRP c1 sr.SR1) l1 t2
     | Greater => Cons_varlist l2 (monom_insert sr c1 l1 t2)) ∧
  ∀sr l1 c1. monom_insert sr c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom

monom_insert_ind

⊢ ∀P. (∀sr c1 l1 c2 l2 t2.
         ((list_cmp index_compare l1 l2 = Greater) ⇒ P sr c1 l1 t2) ⇒
         P sr c1 l1 (Cons_monom c2 l2 t2)) ∧
      (∀sr c1 l1 l2 t2.
         ((list_cmp index_compare l1 l2 = Greater) ⇒ P sr c1 l1 t2) ⇒
         P sr c1 l1 (Cons_varlist l2 t2)) ∧ (∀sr c1 l1. P sr c1 l1 Nil_monom) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

monom_insert_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm a l s.
      interp_cs sr vm (monom_insert sr a l s) =
      sr.SRP (sr.SRM a (interp_vl sr vm l)) (interp_cs sr vm s)

spolynom_11

⊢ (∀a a'. (SPvar a = SPvar a') ⇔ (a = a')) ∧
  (∀a a'. (SPconst a = SPconst a') ⇔ (a = a')) ∧
  (∀a0 a1 a0' a1'. (SPplus a0 a1 = SPplus a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
  ∀a0 a1 a0' a1'. (SPmult a0 a1 = SPmult a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')

spolynom_Axiom

⊢ ∀f0 f1 f2 f3. ∃fn.
    (∀a. fn (SPvar a) = f0 a) ∧ (∀a. fn (SPconst a) = f1 a) ∧
    (∀a0 a1. fn (SPplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
    ∀a0 a1. fn (SPmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)

spolynom_case_cong

⊢ ∀M M' f f1 f2 f3.
    (M = M') ∧ (∀a. (M' = SPvar a) ⇒ (f a = f' a)) ∧
    (∀a. (M' = SPconst a) ⇒ (f1 a = f1' a)) ∧
    (∀a0 a1. (M' = SPplus a0 a1) ⇒ (f2 a0 a1 = f2' a0 a1)) ∧
    (∀a0 a1. (M' = SPmult a0 a1) ⇒ (f3 a0 a1 = f3' a0 a1)) ⇒
    (spolynom_CASE M f f1 f2 f3 = spolynom_CASE M' f' f1' f2' f3')

spolynom_case_eq

⊢ (spolynom_CASE x f f1 f2 f3 = v) ⇔
  (∃i. (x = SPvar i) ∧ (f i = v)) ∨ (∃a. (x = SPconst a) ∧ (f1 a = v)) ∨
  (∃s s0. (x = SPplus s s0) ∧ (f2 s s0 = v)) ∨
  ∃s s0. (x = SPmult s s0) ∧ (f3 s s0 = v)

spolynom_distinct

⊢ (∀a' a. SPvar a ≠ SPconst a') ∧ (∀a1 a0 a. SPvar a ≠ SPplus a0 a1) ∧
  (∀a1 a0 a. SPvar a ≠ SPmult a0 a1) ∧ (∀a1 a0 a. SPconst a ≠ SPplus a0 a1) ∧
  (∀a1 a0 a. SPconst a ≠ SPmult a0 a1) ∧
  ∀a1' a1 a0' a0. SPplus a0 a1 ≠ SPmult a0' a1'

spolynom_induction

⊢ ∀P. (∀i. P (SPvar i)) ∧ (∀a. P (SPconst a)) ∧
      (∀s s0. P s ∧ P s0 ⇒ P (SPplus s s0)) ∧
      (∀s s0. P s ∧ P s0 ⇒ P (SPmult s s0)) ⇒
      ∀s. P s

spolynom_nchotomy

⊢ ∀ss.
    (∃i. ss = SPvar i) ∨ (∃a. ss = SPconst a) ∨ (∃s s0. ss = SPplus s s0) ∨
    ∃s s0. ss = SPmult s s0

spolynomial_normalize_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm p. interp_cs sr vm (spolynom_normalize sr p) = interp_sp sr vm p

spolynomial_simplify_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm p. interp_cs sr vm (spolynom_simplify sr p) = interp_sp sr vm p

varlist_insert_def

⊢ (∀t2 sr l2 l1 c2.
     varlist_insert sr l1 (Cons_monom c2 l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less => Cons_varlist l1 (Cons_monom c2 l2 t2)
     | Equal => Cons_monom (sr.SRP sr.SR1 c2) l1 t2
     | Greater => Cons_monom c2 l2 (varlist_insert sr l1 t2)) ∧
  (∀t2 sr l2 l1.
     varlist_insert sr l1 (Cons_varlist l2 t2) =
     case list_cmp index_compare l1 l2 of
       Less => Cons_varlist l1 (Cons_varlist l2 t2)
     | Equal => Cons_monom (sr.SRP sr.SR1 sr.SR1) l1 t2
     | Greater => Cons_varlist l2 (varlist_insert sr l1 t2)) ∧
  ∀sr l1. varlist_insert sr l1 Nil_monom = Cons_varlist l1 Nil_monom

varlist_insert_ind

⊢ ∀P. (∀sr l1 c2 l2 t2.
         ((list_cmp index_compare l1 l2 = Greater) ⇒ P sr l1 t2) ⇒
         P sr l1 (Cons_monom c2 l2 t2)) ∧
      (∀sr l1 l2 t2.
         ((list_cmp index_compare l1 l2 = Greater) ⇒ P sr l1 t2) ⇒
         P sr l1 (Cons_varlist l2 t2)) ∧ (∀sr l1. P sr l1 Nil_monom) ⇒
      ∀v v1 v2. P v v1 v2

varlist_insert_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm l s.
      interp_cs sr vm (varlist_insert sr l s) =
      sr.SRP (interp_vl sr vm l) (interp_cs sr vm s)

varlist_merge_ok

⊢ ∀sr.
    is_semi_ring sr ⇒
    ∀vm x y.
      interp_vl sr vm (list_merge index_lt x y) =
      sr.SRM (interp_vl sr vm x) (interp_vl sr vm y)