Theory: ringNorm

Parents

Types

polynom(Arity = 1)

Constants

r_monom_insert :'a ring -> 'a -> index list -> 'a canonical_sum -> 'a canonical_sum
interp_p :'a ring -> 'a varmap -> 'a polynom -> 'a
ii_internal_mk_polynom :(index # 'a) recspace -> 'a polynom
ii_internal_dest_polynom :'a polynom -> (index # 'a) recspace
r_spolynom_simplify :'a ring -> 'a spolynom -> 'a canonical_sum
r_canonical_sum_simplify :'a ring -> 'a canonical_sum -> 'a canonical_sum
r_canonical_sum_scalar2 :'a ring -> index list -> 'a canonical_sum -> 'a canonical_sum
r_canonical_sum_scalar3 :'a ring -> 'a -> index list -> 'a canonical_sum -> 'a canonical_sum
polynom_size :('a -> num) -> 'a polynom -> num
r_interp_m :'a ring -> 'a varmap -> 'a -> index list -> 'a
r_interp_cs :'a ring -> 'a varmap -> 'a canonical_sum -> 'a
r_varlist_insert :'a ring -> index list -> 'a canonical_sum -> 'a canonical_sum
Pconst :'a -> 'a polynom
r_interp_sp :'a ring -> 'a varmap -> 'a spolynom -> 'a
r_interp_vl :'a ring -> 'a varmap -> index list -> 'a
r_spolynom_normalize :'a ring -> 'a spolynom -> 'a canonical_sum
polynom_simplify :'a ring -> 'a polynom -> 'a canonical_sum
r_ivl_aux :'a ring -> 'a varmap -> index -> index list -> 'a
r_canonical_sum_merge :'a ring -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
polynom_case :(index -> 'b) -> ('a -> 'b) -> ('a polynom -> 'a polynom -> 'b) -> ('a polynom -> 'a polynom -> 'b) -> ('a polynom -> 'b) -> 'a polynom -> 'b
Popp :'a polynom -> 'a polynom
r_ics_aux :'a ring -> 'a varmap -> 'a -> 'a canonical_sum -> 'a
Pvar :index -> 'a polynom
r_canonical_sum_scalar :'a ring -> 'a -> 'a canonical_sum -> 'a canonical_sum
r_canonical_sum_prod :'a ring -> 'a canonical_sum -> 'a canonical_sum -> 'a canonical_sum
ii_internalringNorm0 :index -> 'a polynom
ii_internalringNorm1 :'a -> 'a polynom
ii_internalringNorm2 :'a polynom -> 'a polynom -> 'a polynom
ii_internalringNorm3 :'a polynom -> 'a polynom -> 'a polynom
ii_internalringNorm4 :'a polynom -> 'a polynom
Pmult :'a polynom -> 'a polynom -> 'a polynom
polynom_normalize :'a ring -> 'a polynom -> 'a canonical_sum
Pplus :'a polynom -> 'a polynom -> 'a polynom

Definitions

ii_internalringNorm0_def

|- ii_internalringNorm0 =
   (\a. ii_internal_mk_polynom ((\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a))

ii_internalringNorm1_def

|- ii_internalringNorm1 =
   (\a.
      ii_internal_mk_polynom
        ((\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a))

ii_internalringNorm2_def

|- ii_internalringNorm2 =
   (\a0 a1.
      ii_internal_mk_polynom
        ((\a0 a1.
            CONSTR (SUC (SUC 0)) ((@v. T),@v. T)
              (FCONS a0 (FCONS a1 (\n. BOTTOM))))
           (ii_internal_dest_polynom a0) (ii_internal_dest_polynom a1)))

ii_internalringNorm3_def

|- ii_internalringNorm3 =
   (\a0 a1.
      ii_internal_mk_polynom
        ((\a0 a1.
            CONSTR (SUC (SUC (SUC 0))) ((@v. T),@v. T)
              (FCONS a0 (FCONS a1 (\n. BOTTOM))))
           (ii_internal_dest_polynom a0) (ii_internal_dest_polynom a1)))

ii_internalringNorm4_def

|- ii_internalringNorm4 =
   (\a.
      ii_internal_mk_polynom
        ((\a.
            CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),@v. T)
              (FCONS a (\n. BOTTOM))) (ii_internal_dest_polynom a)))

interp_p_def

|- (!r vm c. interp_p r vm (Pconst c) = c) /\
   (!r vm i. interp_p r vm (Pvar i) = varmap_find i vm) /\
   (!r vm p1 p2.
      interp_p r vm (Pplus p1 p2) =
      r.RP (interp_p r vm p1) (interp_p r vm p2)) /\
   (!r vm p1 p2.
      interp_p r vm (Pmult p1 p2) =
      r.RM (interp_p r vm p1) (interp_p r vm p2)) /\
   !r vm p1. interp_p r vm (Popp p1) = r.RN (interp_p r vm p1)

Pconst

|- Pconst = ii_internalringNorm1

Pmult

|- Pmult = ii_internalringNorm3

polynom_case_def

|- (!f f1 f2 f3 f4 a. polynom_case f f1 f2 f3 f4 (Pvar a) = f a) /\
   (!f f1 f2 f3 f4 a. polynom_case f f1 f2 f3 f4 (Pconst a) = f1 a) /\
   (!f f1 f2 f3 f4 a0 a1.
      polynom_case f f1 f2 f3 f4 (Pplus a0 a1) = f2 a0 a1) /\
   (!f f1 f2 f3 f4 a0 a1.
      polynom_case f f1 f2 f3 f4 (Pmult a0 a1) = f3 a0 a1) /\
   !f f1 f2 f3 f4 a. polynom_case f f1 f2 f3 f4 (Popp a) = f4 a

polynom_normalize_def

|- (!r i. polynom_normalize r (Pvar i) = Cons_varlist [i] Nil_monom) /\
   (!r c. polynom_normalize r (Pconst c) = Cons_monom c [] Nil_monom) /\
   (!r pl pr.
      polynom_normalize r (Pplus pl pr) =
      r_canonical_sum_merge r (polynom_normalize r pl)
        (polynom_normalize r pr)) /\
   (!r pl pr.
      polynom_normalize r (Pmult pl pr) =
      r_canonical_sum_prod r (polynom_normalize r pl)
        (polynom_normalize r pr)) /\
   !r p.
     polynom_normalize r (Popp p) =
     r_canonical_sum_scalar3 r (r.RN r.R1) [] (polynom_normalize r p)

polynom_repfns

|- (!a. ii_internal_mk_polynom (ii_internal_dest_polynom a) = a) /\
   !r.
     (\a0'.
        !'polynom'.
          (!a0'.
             (?a. a0' = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/
             (?a. a0' = (\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    CONSTR (SUC (SUC 0)) ((@v. T),@v. T)
                      (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\
                'polynom' a0 /\ 'polynom' a1) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    CONSTR (SUC (SUC (SUC 0))) ((@v. T),@v. T)
                      (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\
                'polynom' a0 /\ 'polynom' a1) \/
             (?a.
                (a0' =
                 (\a.
                    CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),@v. T)
                      (FCONS a (\n. BOTTOM))) a) /\ 'polynom' a) ==>
             'polynom' a0') ==>
          'polynom' a0') r =
     (ii_internal_dest_polynom (ii_internal_mk_polynom r) = r)

polynom_simplify_def

|- !r x.
     polynom_simplify r x = r_canonical_sum_simplify r (polynom_normalize r x)

polynom_size_def

|- (!f a. polynom_size f (Pvar a) = 1 + index_size a) /\
   (!f a. polynom_size f (Pconst a) = 1 + f a) /\
   (!f a0 a1.
      polynom_size f (Pplus a0 a1) =
      1 + (polynom_size f a0 + polynom_size f a1)) /\
   (!f a0 a1.
      polynom_size f (Pmult a0 a1) =
      1 + (polynom_size f a0 + polynom_size f a1)) /\
   !f a. polynom_size f (Popp a) = 1 + polynom_size f a

polynom_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'polynom'.
            (!a0'.
               (?a. a0' = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/
               (?a. a0' = (\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      CONSTR (SUC (SUC 0)) ((@v. T),@v. T)
                        (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\
                  'polynom' a0 /\ 'polynom' a1) \/
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      CONSTR (SUC (SUC (SUC 0))) ((@v. T),@v. T)
                        (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\
                  'polynom' a0 /\ 'polynom' a1) \/
               (?a.
                  (a0' =
                   (\a.
                      CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),@v. T)
                        (FCONS a (\n. BOTTOM))) a) /\ 'polynom' a) ==>
               'polynom' a0') ==>
            'polynom' a0') rep

Popp

|- Popp = ii_internalringNorm4

Pplus

|- Pplus = ii_internalringNorm2

Pvar

|- Pvar = ii_internalringNorm0

r_canonical_sum_merge_def

|- !r. r_canonical_sum_merge r = canonical_sum_merge (semi_ring_of r)

r_canonical_sum_prod_def

|- !r. r_canonical_sum_prod r = canonical_sum_prod (semi_ring_of r)

r_canonical_sum_scalar2_def

|- !r. r_canonical_sum_scalar2 r = canonical_sum_scalar2 (semi_ring_of r)

r_canonical_sum_scalar3_def

|- !r. r_canonical_sum_scalar3 r = canonical_sum_scalar3 (semi_ring_of r)

r_canonical_sum_scalar_def

|- !r. r_canonical_sum_scalar r = canonical_sum_scalar (semi_ring_of r)

r_canonical_sum_simplify_def

|- !r. r_canonical_sum_simplify r = canonical_sum_simplify (semi_ring_of r)

r_ics_aux_def

|- !r. r_ics_aux r = ics_aux (semi_ring_of r)

r_interp_cs_def

|- !r. r_interp_cs r = interp_cs (semi_ring_of r)

r_interp_m_def

|- !r. r_interp_m r = interp_m (semi_ring_of r)

r_interp_sp_def

|- !r. r_interp_sp r = interp_sp (semi_ring_of r)

r_interp_vl_def

|- !r. r_interp_vl r = interp_vl (semi_ring_of r)

r_ivl_aux_def

|- !r. r_ivl_aux r = ivl_aux (semi_ring_of r)

r_monom_insert_def

|- !r. r_monom_insert r = monom_insert (semi_ring_of r)

r_spolynom_normalize_def

|- !r. r_spolynom_normalize r = spolynom_normalize (semi_ring_of r)

r_spolynom_simplify_def

|- !r. r_spolynom_simplify r = spolynom_simplify (semi_ring_of r)

r_varlist_insert_def

|- !r. r_varlist_insert r = varlist_insert (semi_ring_of r)

Theorems

canonical_sum_merge_def

|- !r.
     (r_canonical_sum_merge r (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_monom c1 l1 (r_canonical_sum_merge r t1 (Cons_monom c2 l2 t2)))
        (Cons_monom (r.RP c1 c2) l1 (r_canonical_sum_merge r t1 t2))
        (Cons_monom c2 l2
           (r_canonical_sum_merge r (Cons_monom c1 l1 t1) t2))) /\
     (r_canonical_sum_merge r (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_monom c1 l1 (r_canonical_sum_merge r t1 (Cons_varlist l2 t2)))
        (Cons_monom (r.RP c1 r.R1) l1 (r_canonical_sum_merge r t1 t2))
        (Cons_varlist l2
           (r_canonical_sum_merge r (Cons_monom c1 l1 t1) t2))) /\
     (r_canonical_sum_merge r (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_varlist l1 (r_canonical_sum_merge r t1 (Cons_monom c2 l2 t2)))
        (Cons_monom (r.RP r.R1 c2) l1 (r_canonical_sum_merge r t1 t2))
        (Cons_monom c2 l2
           (r_canonical_sum_merge r (Cons_varlist l1 t1) t2))) /\
     (r_canonical_sum_merge r (Cons_varlist l1 t1) (Cons_varlist l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_varlist l1 (r_canonical_sum_merge r t1 (Cons_varlist l2 t2)))
        (Cons_monom (r.RP r.R1 r.R1) l1 (r_canonical_sum_merge r t1 t2))
        (Cons_varlist l2
           (r_canonical_sum_merge r (Cons_varlist l1 t1) t2))) /\
     (r_canonical_sum_merge r (Cons_varlist v7 v8) Nil_monom =
      Cons_varlist v7 v8) /\
     (r_canonical_sum_merge r (Cons_monom v4 v5 v6) Nil_monom =
      Cons_monom v4 v5 v6) /\
     (r_canonical_sum_merge r Nil_monom Nil_monom = Nil_monom) /\
     (r_canonical_sum_merge r Nil_monom (Cons_varlist v17 v18) =
      Cons_varlist v17 v18) /\
     (r_canonical_sum_merge r Nil_monom (Cons_monom v14 v15 v16) =
      Cons_monom v14 v15 v16)

canonical_sum_prod_def

|- !r.
     (!c1 l1 t1 s2.
        r_canonical_sum_prod r (Cons_monom c1 l1 t1) s2 =
        r_canonical_sum_merge r (r_canonical_sum_scalar3 r c1 l1 s2)
          (r_canonical_sum_prod r t1 s2)) /\
     (!l1 t1 s2.
        r_canonical_sum_prod r (Cons_varlist l1 t1) s2 =
        r_canonical_sum_merge r (r_canonical_sum_scalar2 r l1 s2)
          (r_canonical_sum_prod r t1 s2)) /\
     !s2. r_canonical_sum_prod r Nil_monom s2 = Nil_monom

canonical_sum_scalar2_def

|- !r.
     (!l0 c l t.
        r_canonical_sum_scalar2 r l0 (Cons_monom c l t) =
        r_monom_insert r c (list_merge index_lt l0 l)
          (r_canonical_sum_scalar2 r l0 t)) /\
     (!l0 l t.
        r_canonical_sum_scalar2 r l0 (Cons_varlist l t) =
        r_varlist_insert r (list_merge index_lt l0 l)
          (r_canonical_sum_scalar2 r l0 t)) /\
     !l0. r_canonical_sum_scalar2 r l0 Nil_monom = Nil_monom

canonical_sum_scalar3_def

|- !r.
     (!c0 l0 c l t.
        r_canonical_sum_scalar3 r c0 l0 (Cons_monom c l t) =
        r_monom_insert r (r.RM c0 c) (list_merge index_lt l0 l)
          (r_canonical_sum_scalar3 r c0 l0 t)) /\
     (!c0 l0 l t.
        r_canonical_sum_scalar3 r c0 l0 (Cons_varlist l t) =
        r_monom_insert r c0 (list_merge index_lt l0 l)
          (r_canonical_sum_scalar3 r c0 l0 t)) /\
     !c0 l0. r_canonical_sum_scalar3 r c0 l0 Nil_monom = Nil_monom

canonical_sum_scalar_def

|- !r.
     (!c0 c l t.
        r_canonical_sum_scalar r c0 (Cons_monom c l t) =
        Cons_monom (r.RM c0 c) l (r_canonical_sum_scalar r c0 t)) /\
     (!c0 l t.
        r_canonical_sum_scalar r c0 (Cons_varlist l t) =
        Cons_monom c0 l (r_canonical_sum_scalar r c0 t)) /\
     !c0. r_canonical_sum_scalar r c0 Nil_monom = Nil_monom

canonical_sum_simplify_def

|- !r.
     (!c l t.
        r_canonical_sum_simplify r (Cons_monom c l t) =
        (if c = r.R0 then
           r_canonical_sum_simplify r t
         else
           (if c = r.R1 then
              Cons_varlist l (r_canonical_sum_simplify r t)
            else
              Cons_monom c l (r_canonical_sum_simplify r t)))) /\
     (!l t.
        r_canonical_sum_simplify r (Cons_varlist l t) =
        Cons_varlist l (r_canonical_sum_simplify r t)) /\
     (r_canonical_sum_simplify r Nil_monom = Nil_monom)

ics_aux_def

|- !r.
     (!vm a. r_ics_aux r vm a Nil_monom = a) /\
     (!vm a l t.
        r_ics_aux r vm a (Cons_varlist l t) =
        r.RP a (r_ics_aux r vm (r_interp_vl r vm l) t)) /\
     !vm a c l t.
       r_ics_aux r vm a (Cons_monom c l t) =
       r.RP a (r_ics_aux r vm (r_interp_m r vm c l) t)

interp_cs_def

|- !r.
     (!vm. r_interp_cs r vm Nil_monom = r.R0) /\
     (!vm l t.
        r_interp_cs r vm (Cons_varlist l t) =
        r_ics_aux r vm (r_interp_vl r vm l) t) /\
     !vm c l t.
       r_interp_cs r vm (Cons_monom c l t) =
       r_ics_aux r vm (r_interp_m r vm c l) t

interp_m_def

|- !r.
     (!vm c. r_interp_m r vm c [] = c) /\
     !vm c x t. r_interp_m r vm c (x::t) = r.RM c (r_ivl_aux r vm x t)

interp_sp_def

|- !r.
     (!vm c. r_interp_sp r vm (SPconst c) = c) /\
     (!vm i. r_interp_sp r vm (SPvar i) = varmap_find i vm) /\
     (!vm p1 p2.
        r_interp_sp r vm (SPplus p1 p2) =
        r.RP (r_interp_sp r vm p1) (r_interp_sp r vm p2)) /\
     !vm p1 p2.
       r_interp_sp r vm (SPmult p1 p2) =
       r.RM (r_interp_sp r vm p1) (r_interp_sp r vm p2)

interp_vl_def

|- !r.
     (!vm. r_interp_vl r vm [] = r.R1) /\
     !vm x t. r_interp_vl r vm (x::t) = r_ivl_aux r vm x t

ivl_aux_def

|- !r.
     (!vm x. r_ivl_aux r vm x [] = varmap_find x vm) /\
     !vm x x' t'.
       r_ivl_aux r vm x (x'::t') =
       r.RM (varmap_find x vm) (r_ivl_aux r vm x' t')

monom_insert_def

|- !r.
     (r_monom_insert r c1 l1 (Cons_monom c2 l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_monom c1 l1 (Cons_monom c2 l2 t2))
        (Cons_monom (r.RP c1 c2) l1 t2)
        (Cons_monom c2 l2 (r_monom_insert r c1 l1 t2))) /\
     (r_monom_insert r c1 l1 (Cons_varlist l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_monom c1 l1 (Cons_varlist l2 t2))
        (Cons_monom (r.RP c1 r.R1) l1 t2)
        (Cons_varlist l2 (r_monom_insert r c1 l1 t2))) /\
     (r_monom_insert r c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom)

polynom_11

|- (!a a'. (Pvar a = Pvar a') = (a = a')) /\
   (!a a'. (Pconst a = Pconst a') = (a = a')) /\
   (!a0 a1 a0' a1'.
      (Pplus a0 a1 = Pplus a0' a1') = (a0 = a0') /\ (a1 = a1')) /\
   (!a0 a1 a0' a1'.
      (Pmult a0 a1 = Pmult a0' a1') = (a0 = a0') /\ (a1 = a1')) /\
   !a a'. (Popp a = Popp a') = (a = a')

polynom_Axiom

|- !f0 f1 f2 f3 f4.
     ?fn.
       (!a. fn (Pvar a) = f0 a) /\ (!a. fn (Pconst a) = f1 a) /\
       (!a0 a1. fn (Pplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) /\
       (!a0 a1. fn (Pmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)) /\
       !a. fn (Popp a) = f4 a (fn a)

polynom_case_cong

|- !f4' f4 f3' f3 f2' f2 f1' f1 f' f M' M.
     (M = M') /\ (!a. (M' = Pvar a) ==> (f a = f' a)) /\
     (!a. (M' = Pconst a) ==> (f1 a = f1' a)) /\
     (!a0 a1. (M' = Pplus a0 a1) ==> (f2 a0 a1 = f2' a0 a1)) /\
     (!a0 a1. (M' = Pmult a0 a1) ==> (f3 a0 a1 = f3' a0 a1)) /\
     (!a. (M' = Popp a) ==> (f4 a = f4' a)) ==>
     (polynom_case f f1 f2 f3 f4 M = polynom_case f' f1' f2' f3' f4' M')

polynom_distinct

|- (!a' a. ~(Pvar a = Pconst a')) /\ (!a1 a0 a. ~(Pvar a = Pplus a0 a1)) /\
   (!a1 a0 a. ~(Pvar a = Pmult a0 a1)) /\ (!a' a. ~(Pvar a = Popp a')) /\
   (!a1 a0 a. ~(Pconst a = Pplus a0 a1)) /\
   (!a1 a0 a. ~(Pconst a = Pmult a0 a1)) /\ (!a' a. ~(Pconst a = Popp a')) /\
   (!a1' a0' a1 a0. ~(Pplus a0 a1 = Pmult a0' a1')) /\
   (!a a1 a0. ~(Pplus a0 a1 = Popp a)) /\ !a a1 a0. ~(Pmult a0 a1 = Popp a)

polynom_induction

|- !P.
     (!i. P (Pvar i)) /\ (!a. P (Pconst a)) /\
     (!p p0. P p /\ P p0 ==> P (Pplus p p0)) /\
     (!p p0. P p /\ P p0 ==> P (Pmult p p0)) /\ (!p. P p ==> P (Popp p)) ==>
     !p. P p

polynom_nchotomy

|- !p.
     (?i. p = Pvar i) \/ (?a. p = Pconst a) \/ (?p' p0. p = Pplus p' p0) \/
     (?p' p0. p = Pmult p' p0) \/ ?p'. p = Popp p'

polynom_normalize_ok

|- !r.
     is_ring r ==>
     !vm p. r_interp_cs r vm (polynom_normalize r p) = interp_p r vm p

polynom_simplify_ok

|- !r.
     is_ring r ==>
     !vm p. r_interp_cs r vm (polynom_simplify r p) = interp_p r vm p

spolynom_normalize_def

|- !r.
     (!i. r_spolynom_normalize r (SPvar i) = Cons_varlist [i] Nil_monom) /\
     (!c. r_spolynom_normalize r (SPconst c) = Cons_monom c [] Nil_monom) /\
     (!l r'.
        r_spolynom_normalize r (SPplus l r') =
        r_canonical_sum_merge r (r_spolynom_normalize r l)
          (r_spolynom_normalize r r')) /\
     !l r'.
       r_spolynom_normalize r (SPmult l r') =
       r_canonical_sum_prod r (r_spolynom_normalize r l)
         (r_spolynom_normalize r r')

spolynom_simplify_def

|- !r x.
     r_spolynom_simplify r x =
     r_canonical_sum_simplify r (r_spolynom_normalize r x)

varlist_insert_def

|- !r.
     (r_varlist_insert r l1 (Cons_monom c2 l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_varlist l1 (Cons_monom c2 l2 t2))
        (Cons_monom (r.RP r.R1 c2) l1 t2)
        (Cons_monom c2 l2 (r_varlist_insert r l1 t2))) /\
     (r_varlist_insert r l1 (Cons_varlist l2 t2) =
      compare (list_compare index_compare l1 l2)
        (Cons_varlist l1 (Cons_varlist l2 t2))
        (Cons_monom (r.RP r.R1 r.R1) l1 t2)
        (Cons_varlist l2 (r_varlist_insert r l1 t2))) /\
     (r_varlist_insert r l1 Nil_monom = Cons_varlist l1 Nil_monom)