Package hol-ring: HOL ring theories

Information

namehol-ring
version1.0
descriptionHOL ring theories
authorHOL developers <hol-developers@lists.sourceforge.net>
licenseMIT
checksum8a4e6846ed0bc1127379258b326f08310f1cf5bc
requiresbase
hol-base
showData.Bool
Data.List
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operators

Defined Constants

Theorems

prelim.LESS = prelim.num2ordering 0

prelim.EQUAL = prelim.num2ordering 1

prelim.GREATER = prelim.num2ordering (arithmetic.BIT2 0)

x. prelim.ordering_size x = 0

a. prelim.num2ordering (prelim.ordering2num a) = a

semi_ring.is_semi_ring (semi_ring.recordtype.semi_ring 0 1 (+) (*))

r.
    ringNorm.r_canonical_sum_simplify r =
    canonical.canonical_sum_simplify (ring.semi_ring_of r)

r.
    ringNorm.r_spolynom_normalize r =
    canonical.spolynom_normalize (ring.semi_ring_of r)

r.
    ringNorm.r_spolynom_simplify r =
    canonical.spolynom_simplify (ring.semi_ring_of r)

r.
    ringNorm.r_canonical_sum_scalar r =
    canonical.canonical_sum_scalar (ring.semi_ring_of r)

r. ringNorm.r_interp_vl r = canonical.interp_vl (ring.semi_ring_of r)

r. ringNorm.r_interp_cs r = canonical.interp_cs (ring.semi_ring_of r)

r. ringNorm.r_interp_sp r = canonical.interp_sp (ring.semi_ring_of r)

r.
    ringNorm.r_canonical_sum_scalar2 r =
    canonical.canonical_sum_scalar2 (ring.semi_ring_of r)

r.
    ringNorm.r_varlist_insert r =
    canonical.varlist_insert (ring.semi_ring_of r)

r.
    ringNorm.r_canonical_sum_merge r =
    canonical.canonical_sum_merge (ring.semi_ring_of r)

r.
    ringNorm.r_canonical_sum_prod r =
    canonical.canonical_sum_prod (ring.semi_ring_of r)

r. ringNorm.r_interp_m r = canonical.interp_m (ring.semi_ring_of r)

r. ringNorm.r_ics_aux r = canonical.ics_aux (ring.semi_ring_of r)

r. ringNorm.r_ivl_aux r = canonical.ivl_aux (ring.semi_ring_of r)

r.
    ringNorm.r_canonical_sum_scalar3 r =
    canonical.canonical_sum_scalar3 (ring.semi_ring_of r)

r.
    ringNorm.r_monom_insert r =
    canonical.monom_insert (ring.semi_ring_of r)

r. ring.is_ring r semi_ring.is_semi_ring (ring.semi_ring_of r)

rep. bool.TYPE_DEFINITION (λn. n < 3) rep

numRing.num_canonical_sum_simplify =
  canonical.canonical_sum_simplify
    (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_spolynom_normalize =
  canonical.spolynom_normalize (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_spolynom_simplify =
  canonical.spolynom_simplify (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_canonical_sum_scalar =
  canonical.canonical_sum_scalar
    (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_interp_vl =
  canonical.interp_vl (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_interp_cs =
  canonical.interp_cs (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_interp_sp =
  canonical.interp_sp (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_canonical_sum_scalar2 =
  canonical.canonical_sum_scalar2
    (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_varlist_insert =
  canonical.varlist_insert (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_canonical_sum_merge =
  canonical.canonical_sum_merge
    (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_canonical_sum_prod =
  canonical.canonical_sum_prod (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_ivl_aux =
  canonical.ivl_aux (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_interp_m =
  canonical.interp_m (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_ics_aux =
  canonical.ics_aux (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_canonical_sum_scalar3 =
  canonical.canonical_sum_scalar3
    (semi_ring.recordtype.semi_ring 0 1 (+) (*))

numRing.num_monom_insert =
  canonical.monom_insert (semi_ring.recordtype.semi_ring 0 1 (+) (*))

x x1. quote.varmap_find x x1 = quote.varmap_find_tupled (x, x1)

a2 a1 a0. ¬(quote.Empty_vm = quote.Node_vm a0 a1 a2)

a a'. a = a' prelim.ordering2num a = prelim.ordering2num a'

a a'. prelim.ordering2num a = prelim.ordering2num a' a = a'

i1 i2. quote.index_lt i1 i2 quote.index_compare i1 i2 = prelim.LESS

i1 i2. quote.index_compare i1 i2 = prelim.EQUAL i1 = i2

r x.
    ringNorm.r_spolynom_simplify r x =
    ringNorm.r_canonical_sum_simplify r (ringNorm.r_spolynom_normalize r x)

r x.
    ringNorm.polynom_simplify r x =
    ringNorm.r_canonical_sum_simplify r (ringNorm.polynom_normalize r x)

sr x.
    canonical.spolynom_simplify sr x =
    canonical.canonical_sum_simplify sr (canonical.spolynom_normalize sr x)

a. a = prelim.LESS a = prelim.EQUAL a = prelim.GREATER

r. r < 3 prelim.ordering2num (prelim.num2ordering r) = r

a. r. a = prelim.num2ordering r r < 3

r. r < 3 a. r = prelim.ordering2num a

l1 l2.
    prelim.list_compare quote.index_compare l1 l2 = prelim.EQUAL l1 = l2

r. ring.is_ring r n. ring.ring_RM r n (ring.ring_R1 r) = n

r. ring.is_ring r n. ring.ring_RP r n (ring.ring_R0 r) = n

r. ring.is_ring r n. ring.ring_RM r (ring.ring_R1 r) n = n

r. ring.is_ring r n. ring.ring_RP r (ring.ring_R0 r) n = n

r.
    semi_ring.is_semi_ring r
    n. semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SR1 r) = n

r.
    semi_ring.is_semi_ring r
    n. semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SR0 r) = n

r.
    semi_ring.is_semi_ring r
    n. semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR1 r) n = n

r.
    semi_ring.is_semi_ring r
    n. semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SR0 r) n = n

r.
    ring.semi_ring_of r =
    semi_ring.recordtype.semi_ring (ring.ring_R0 r) (ring.ring_R1 r)
      (ring.ring_RP r) (ring.ring_RM r)

a a0 f f0.
    semi_ring.semi_ring_SR0 (semi_ring.recordtype.semi_ring a a0 f f0) = a

a a0 f f0.
    semi_ring.semi_ring_SR1 (semi_ring.recordtype.semi_ring a a0 f f0) = a0

a a0 f f0.
    semi_ring.semi_ring_SRM (semi_ring.recordtype.semi_ring a a0 f f0) = f0

a a0 f f0.
    semi_ring.semi_ring_SRP (semi_ring.recordtype.semi_ring a a0 f f0) = f

r.
    ring.is_ring r n. ring.ring_RM r n (ring.ring_R0 r) = ring.ring_R0 r

r.
    ring.is_ring r n. ring.ring_RM r (ring.ring_R0 r) n = ring.ring_R0 r

r.
    semi_ring.is_semi_ring r
    n.
      semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SR0 r) =
      semi_ring.semi_ring_SR0 r

r.
    semi_ring.is_semi_ring r
    n.
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR0 r) n =
      semi_ring.semi_ring_SR0 r

P. P prelim.EQUAL P prelim.GREATER P prelim.LESS a. P a

¬(prelim.LESS = prelim.EQUAL) ¬(prelim.LESS = prelim.GREATER)
  ¬(prelim.EQUAL = prelim.GREATER)

x. a a0 f f0. x = semi_ring.recordtype.semi_ring a a0 f f0

r.
    ring.is_ring r
    n. ring.ring_RP r n (ring.ring_RN r n) = ring.ring_R0 r

x x1 x2.
    prelim.list_merge x x1 x2 = prelim.list_merge_tupled (x, x1, x2)

x x1 x2.
    prelim.list_compare x x1 x2 = prelim.list_compare_tupled (x, x1, x2)

vv. vv = quote.Empty_vm a v v0. vv = quote.Node_vm a v v0

prelim.num2ordering 0 = prelim.LESS
  prelim.num2ordering 1 = prelim.EQUAL
  prelim.num2ordering (arithmetic.BIT2 0) = prelim.GREATER

prelim.ordering2num prelim.LESS = 0
  prelim.ordering2num prelim.EQUAL = 1
  prelim.ordering2num prelim.GREATER = arithmetic.BIT2 0

a a0 f f0 f1. ring.ring_R0 (ring.recordtype.ring a a0 f f0 f1) = a

a a0 f f0 f1. ring.ring_R1 (ring.recordtype.ring a a0 f f0 f1) = a0

a a0 f f0 f1. ring.ring_RN (ring.recordtype.ring a a0 f f0 f1) = f1

a a0 f f0 f1. ring.ring_RM (ring.recordtype.ring a a0 f f0 f1) = f0

a a0 f f0 f1. ring.ring_RP (ring.recordtype.ring a a0 f f0 f1) = f

r. ring.is_ring r n m. ring.ring_RM r n m = ring.ring_RM r m n

r. ring.is_ring r n m. ring.ring_RP r n m = ring.ring_RP r m n

r.
    semi_ring.is_semi_ring r
    n m. semi_ring.semi_ring_SRM r n m = semi_ring.semi_ring_SRM r m n

r.
    semi_ring.is_semi_ring r
    n m. semi_ring.semi_ring_SRP r n m = semi_ring.semi_ring_SRP r m n

x. a a0 f f0 f1. x = ring.recordtype.ring a a0 f f0 f1

ii.
    (i. ii = quote.Left_idx i) (i. ii = quote.Right_idx i)
    ii = quote.End_idx

P.
    (a0 a1 a2 a3. P (semi_ring.recordtype.semi_ring a0 a1 a2 a3))
    x. P x

r.
    ring.is_ring r
    vm p.
      ringNorm.r_interp_cs r vm (ringNorm.polynom_normalize r p) =
      ringNorm.interp_p r vm p

r.
    ring.is_ring r
    vm p.
      ringNorm.r_interp_cs r vm (ringNorm.polynom_simplify r p) =
      ringNorm.interp_p r vm p

sr.
    semi_ring.is_semi_ring sr
    vm s.
      canonical.interp_cs sr vm (canonical.canonical_sum_simplify sr s) =
      canonical.interp_cs sr vm s

sr.
    semi_ring.is_semi_ring sr
    vm p.
      canonical.interp_cs sr vm (canonical.spolynom_normalize sr p) =
      canonical.interp_sp sr vm p

sr.
    semi_ring.is_semi_ring sr
    vm p.
      canonical.interp_cs sr vm (canonical.spolynom_simplify sr p) =
      canonical.interp_sp sr vm p

x0 x1 x2.
    f. f prelim.LESS = x0 f prelim.EQUAL = x1 f prelim.GREATER = x2

a0 a1 a2 a3 f.
    semi_ring.semi_ring_CASE (semi_ring.recordtype.semi_ring a0 a1 a2 a3)
      f = f a0 a1 a2 a3

r.
    ring.is_ring r
    a b.
      ring.ring_RM r (ring.ring_RN r a) b =
      ring.ring_RN r (ring.ring_RM r a b)

P. (a0 a1 a2 a3 a4. P (ring.recordtype.ring a0 a1 a2 a3 a4)) x. P x

f.
    fn.
      a0 a1 a2 a3.
        fn (semi_ring.recordtype.semi_ring a0 a1 a2 a3) = f a0 a1 a2 a3

f1 a a0 f f0.
    semi_ring.semi_ring_SR0_fupd f1
      (semi_ring.recordtype.semi_ring a a0 f f0) =
    semi_ring.recordtype.semi_ring (f1 a) a0 f f0

f1 a a0 f f0.
    semi_ring.semi_ring_SR1_fupd f1
      (semi_ring.recordtype.semi_ring a a0 f f0) =
    semi_ring.recordtype.semi_ring a (f1 a0) f f0

f1 a a0 f f0.
    semi_ring.semi_ring_SRM_fupd f1
      (semi_ring.recordtype.semi_ring a a0 f f0) =
    semi_ring.recordtype.semi_ring a a0 f (f1 f0)

f1 a a0 f f0.
    semi_ring.semi_ring_SRP_fupd f1
      (semi_ring.recordtype.semi_ring a a0 f f0) =
    semi_ring.recordtype.semi_ring a a0 (f1 f) f0

(a. prelim.num2ordering (prelim.ordering2num a) = a)
  r.
    (let n r in n < 3) prelim.ordering2num (prelim.num2ordering r) = r

sr.
    semi_ring.is_semi_ring sr
    vm x l.
      canonical.interp_m sr vm x l =
      semi_ring.semi_ring_SRM sr x (canonical.interp_vl sr vm l)

sr.
    semi_ring.is_semi_ring sr
    vm x s.
      canonical.ics_aux sr vm x s =
      semi_ring.semi_ring_SRP sr x (canonical.interp_cs sr vm s)

s.
    a0 a f0 f.
      s =
      semi_ring.semi_ring_SR0_fupd (const a0)
        (semi_ring.semi_ring_SR1_fupd (const a)
           (semi_ring.semi_ring_SRP_fupd (const f0)
              (semi_ring.semi_ring_SRM_fupd (const f) bool.ARB)))

f a0 a1 a2 a3.
    semi_ring.semi_ring_size f
      (semi_ring.recordtype.semi_ring a0 a1 a2 a3) = 1 + (f a0 + f a1)

a0 a1 a2 a3 a4 f.
    ring.ring_CASE (ring.recordtype.ring a0 a1 a2 a3 a4) f =
    f a0 a1 a2 a3 a4

r r'.
    r < 3 r' < 3
    (prelim.num2ordering r = prelim.num2ordering r' r = r')

r.
    ring.is_ring r
    n m p.
      ring.ring_RM r n (ring.ring_RM r m p) =
      ring.ring_RM r (ring.ring_RM r n m) p

r.
    ring.is_ring r
    n m p.
      ring.ring_RP r n (ring.ring_RP r m p) =
      ring.ring_RP r (ring.ring_RP r n m) p

r.
    semi_ring.is_semi_ring r
    n m p.
      semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SRM r m p) =
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n m) p

r.
    semi_ring.is_semi_ring r
    n m p.
      semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SRP r m p) =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n m) p

r.
    semi_ring.is_semi_ring r
    m n p.
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m n) p =
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m p) n

r.
    semi_ring.is_semi_ring r
    m n p.
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r m n) p =
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n p) m

r.
    semi_ring.is_semi_ring r
    m n p.
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m n) p =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m p) n

r.
    semi_ring.is_semi_ring r
    m n p.
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r m n) p =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n p) m

sr.
    semi_ring.is_semi_ring sr
    vm a s.
      canonical.interp_cs sr vm (canonical.canonical_sum_scalar sr a s) =
      semi_ring.semi_ring_SRM sr a (canonical.interp_cs sr vm s)

sr.
    semi_ring.is_semi_ring sr
    vm v i.
      canonical.ivl_aux sr vm i v =
      semi_ring.semi_ring_SRM sr (quote.varmap_find i vm)
        (canonical.interp_vl sr vm v)

(a' a. ¬(quote.Left_idx a = quote.Right_idx a'))
  (a. ¬(quote.Left_idx a = quote.End_idx))
  a. ¬(quote.Right_idx a = quote.End_idx)

P.
    P quote.Empty_vm
    (a1 a2. P a1 P a2 a0. P (quote.Node_vm a0 a1 a2)) v1. P v1

f.
    fn.
      a0 a1 a2 a3 a4.
        fn (ring.recordtype.ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

cc.
    cc = canonical.Nil_monom (a l c. cc = canonical.Cons_monom a l c)
    l c. cc = canonical.Cons_varlist l c

f2 a a0 f f0 f1.
    ring.ring_R0_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring (f2 a) a0 f f0 f1

f2 a a0 f f0 f1.
    ring.ring_R1_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring a (f2 a0) f f0 f1

P.
    (i. P i P (quote.Left_idx i)) (i. P i P (quote.Right_idx i))
    P quote.End_idx i1. P i1

f2 a a0 f f0 f1.
    ring.ring_RN_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring a a0 f f0 (f2 f1)

f2 a a0 f f0 f1.
    ring.ring_RM_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring a a0 f (f2 f0) f1

f2 a a0 f f0 f1.
    ring.ring_RP_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring a a0 (f2 f) f0 f1

(a a'. quote.Left_idx a = quote.Left_idx a' a = a')
  a a'. quote.Right_idx a = quote.Right_idx a' a = a'

f a0 a1 a2 a3 a4.
    ring.ring_size f (ring.recordtype.ring a0 a1 a2 a3 a4) =
    1 + (f a0 + f a1)

P.
    (x. P x)
    a0 a f0 f.
      P
        (semi_ring.semi_ring_SR0_fupd (const a0)
           (semi_ring.semi_ring_SR1_fupd (const a)
              (semi_ring.semi_ring_SRP_fupd (const f0)
                 (semi_ring.semi_ring_SRM_fupd (const f) bool.ARB))))

P.
    (x. P x)
    a0 a f0 f.
      P
        (semi_ring.semi_ring_SR0_fupd (const a0)
           (semi_ring.semi_ring_SR1_fupd (const a)
              (semi_ring.semi_ring_SRP_fupd (const f0)
                 (semi_ring.semi_ring_SRM_fupd (const f) bool.ARB))))

(x y. cmp x y = prelim.EQUAL x = y)
  l1 l2. prelim.list_compare cmp l1 l2 = prelim.EQUAL l1 = l2

r.
    a0 a f1 f0 f.
      r =
      ring.ring_R0_fupd (const a0)
        (ring.ring_R1_fupd (const a)
           (ring.ring_RP_fupd (const f1)
              (ring.ring_RM_fupd (const f0)
                 (ring.ring_RN_fupd (const f) bool.ARB))))

r.
    ring.is_ring r
    n m p.
      ring.ring_RM r (ring.ring_RP r n m) p =
      ring.ring_RP r (ring.ring_RM r n p) (ring.ring_RM r m p)

r.
    semi_ring.is_semi_ring r
    m n p.
      semi_ring.semi_ring_SRM r m (semi_ring.semi_ring_SRP r n p) =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r m n)
        (semi_ring.semi_ring_SRM r m p)

r.
    semi_ring.is_semi_ring r
    n m p.
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRP r n m) p =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r n p)
        (semi_ring.semi_ring_SRM r m p)

sr.
    semi_ring.is_semi_ring sr
    vm x y.
      canonical.interp_vl sr vm (prelim.list_merge quote.index_lt x y) =
      semi_ring.semi_ring_SRM sr (canonical.interp_vl sr vm x)
        (canonical.interp_vl sr vm y)

sr.
    semi_ring.is_semi_ring sr
    vm l s.
      canonical.interp_cs sr vm (canonical.canonical_sum_scalar2 sr l s) =
      semi_ring.semi_ring_SRM sr (canonical.interp_vl sr vm l)
        (canonical.interp_cs sr vm s)

sr.
    semi_ring.is_semi_ring sr
    vm l s.
      canonical.interp_cs sr vm (canonical.varlist_insert sr l s) =
      semi_ring.semi_ring_SRP sr (canonical.interp_vl sr vm l)
        (canonical.interp_cs sr vm s)

sr.
    semi_ring.is_semi_ring sr
    vm x y.
      canonical.interp_cs sr vm (canonical.canonical_sum_merge sr x y) =
      semi_ring.semi_ring_SRP sr (canonical.interp_cs sr vm x)
        (canonical.interp_cs sr vm y)

sr.
    semi_ring.is_semi_ring sr
    vm x y.
      canonical.interp_cs sr vm (canonical.canonical_sum_prod sr x y) =
      semi_ring.semi_ring_SRM sr (canonical.interp_cs sr vm x)
        (canonical.interp_cs sr vm y)

(a. quote.index_size (quote.Left_idx a) = 1 + quote.index_size a)
  (a. quote.index_size (quote.Right_idx a) = 1 + quote.index_size a)
  quote.index_size quote.End_idx = 0

x v0 v1 v2.
    prelim.ordering_CASE x v0 v1 v2 =
    let m prelim.ordering2num x in
    if m < 1 then v0 else if m = 1 then v1 else v2

r.
    (vm. ringNorm.r_interp_vl r vm [] = ring.ring_R1 r)
    vm x t.
      ringNorm.r_interp_vl r vm (x :: t) = ringNorm.r_ivl_aux r vm x t

f0 f1.
    fn.
      fn quote.Empty_vm = f0
      a0 a1 a2. fn (quote.Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)

(sr vm. canonical.interp_vl sr vm [] = semi_ring.semi_ring_SR1 sr)
  sr vm x t.
    canonical.interp_vl sr vm (x :: t) = canonical.ivl_aux sr vm x t

(v f. quote.varmap_CASE quote.Empty_vm v f = v)
  a0 a1 a2 v f.
    quote.varmap_CASE (quote.Node_vm a0 a1 a2) v f = f a0 a1 a2

a0 a1 a2 a0' a1' a2'.
    quote.Node_vm a0 a1 a2 = quote.Node_vm a0' a1' a2'
    a0 = a0' a1 = a1' a2 = a2'

s1 s2.
    s1 = s2
    semi_ring.semi_ring_SR0 s1 = semi_ring.semi_ring_SR0 s2
    semi_ring.semi_ring_SR1 s1 = semi_ring.semi_ring_SR1 s2
    semi_ring.semi_ring_SRP s1 = semi_ring.semi_ring_SRP s2
    semi_ring.semi_ring_SRM s1 = semi_ring.semi_ring_SRM s2

P.
    (x. P x)
    a0 a f1 f0 f.
      P
        (ring.ring_R0_fupd (const a0)
           (ring.ring_R1_fupd (const a)
              (ring.ring_RP_fupd (const f1)
                 (ring.ring_RM_fupd (const f0)
                    (ring.ring_RN_fupd (const f) bool.ARB)))))

P.
    (x. P x)
    a0 a f1 f0 f.
      P
        (ring.ring_R0_fupd (const a0)
           (ring.ring_R1_fupd (const a)
              (ring.ring_RP_fupd (const f1)
                 (ring.ring_RM_fupd (const f0)
                    (ring.ring_RN_fupd (const f) bool.ARB)))))

f0 f1 f2.
    fn.
      (a. fn (quote.Left_idx a) = f0 a (fn a))
      (a. fn (quote.Right_idx a) = f1 a (fn a)) fn quote.End_idx = f2

x.
    (i. x = canonical.SPvar i) (a. x = canonical.SPconst a)
    (s s0. x = canonical.SPplus s s0) s s0. x = canonical.SPmult s s0

sr.
    semi_ring.is_semi_ring sr
    vm c l s.
      canonical.interp_cs sr vm
        (canonical.canonical_sum_scalar3 sr c l s) =
      semi_ring.semi_ring_SRM sr
        (semi_ring.semi_ring_SRM sr c (canonical.interp_vl sr vm l))
        (canonical.interp_cs sr vm s)

sr.
    semi_ring.is_semi_ring sr
    vm a l s.
      canonical.interp_cs sr vm (canonical.monom_insert sr a l s) =
      semi_ring.semi_ring_SRP sr
        (semi_ring.semi_ring_SRM sr a (canonical.interp_vl sr vm l))
        (canonical.interp_cs sr vm s)

P.
    P canonical.Nil_monom
    (c. P c l a. P (canonical.Cons_monom a l c))
    (c. P c l. P (canonical.Cons_varlist l c)) c. P c

(f. quote.varmap_size f quote.Empty_vm = 0)
  f a0 a1 a2.
    quote.varmap_size f (quote.Node_vm a0 a1 a2) =
    1 + (f a0 + (quote.varmap_size f a1 + quote.varmap_size f a2))

r.
    (vm c. ringNorm.r_interp_m r vm c [] = c)
    vm c x t.
      ringNorm.r_interp_m r vm c (x :: t) =
      ring.ring_RM r c (ringNorm.r_ivl_aux r vm x t)

s a0 a f0 f.
    semi_ring.semi_ring_SR0_fupd (const a0)
      (semi_ring.semi_ring_SR1_fupd (const a)
         (semi_ring.semi_ring_SRP_fupd (const f0)
            (semi_ring.semi_ring_SRM_fupd (const f) s))) =
    semi_ring.semi_ring_SR0_fupd (const a0)
      (semi_ring.semi_ring_SR1_fupd (const a)
         (semi_ring.semi_ring_SRP_fupd (const f0)
            (semi_ring.semi_ring_SRM_fupd (const f) bool.ARB)))

r1 r2.
    r1 = r2
    ring.ring_R0 r1 = ring.ring_R0 r2 ring.ring_R1 r1 = ring.ring_R1 r2
    ring.ring_RP r1 = ring.ring_RP r2 ring.ring_RM r1 = ring.ring_RM r2
    ring.ring_RN r1 = ring.ring_RN r2

(sr vm c. canonical.interp_m sr vm c [] = c)
  sr vm c x t.
    canonical.interp_m sr vm c (x :: t) =
    semi_ring.semi_ring_SRM sr c (canonical.ivl_aux sr vm x t)

(lt eq gt. prelim.compare prelim.LESS lt eq gt = lt)
  (lt eq gt. prelim.compare prelim.EQUAL lt eq gt = eq)
  lt eq gt. prelim.compare prelim.GREATER lt eq gt = gt

(v0 v1 v2. prelim.ordering_CASE prelim.LESS v0 v1 v2 = v0)
  (v0 v1 v2. prelim.ordering_CASE prelim.EQUAL v0 v1 v2 = v1)
  v0 v1 v2. prelim.ordering_CASE prelim.GREATER v0 v1 v2 = v2

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'semi_ring'.
           (a0'.
              (a0 a1 a2 a3.
                 a0' =
                 (let a0 a0 in
                  λa1 a2 a3.
                    ind_type.CONSTR 0 (a0, a1, a2, a3)
                      (λn. ind_type.BOTTOM)) a1 a2 a3) 'semi_ring' a0')
           'semi_ring' a0') rep

x.
    (i. x = ringNorm.Pvar i) (a. x = ringNorm.Pconst a)
    (p p0. x = ringNorm.Pplus p p0) (p p0. x = ringNorm.Pmult p p0)
    p. x = ringNorm.Popp p

r.
    (vm x. ringNorm.r_ivl_aux r vm x [] = quote.varmap_find x vm)
    vm x x' t'.
      ringNorm.r_ivl_aux r vm x (x' :: t') =
      ring.ring_RM r (quote.varmap_find x vm)
        (ringNorm.r_ivl_aux r vm x' t')

a0 a1 a2 a3 a0' a1' a2' a3'.
    semi_ring.recordtype.semi_ring a0 a1 a2 a3 =
    semi_ring.recordtype.semi_ring a0' a1' a2' a3'
    a0 = a0' a1 = a1' a2 = a2' a3 = a3'

(a2 a1 a0. ¬(canonical.Nil_monom = canonical.Cons_monom a0 a1 a2))
  (a1 a0. ¬(canonical.Nil_monom = canonical.Cons_varlist a0 a1))
  a2 a1' a1 a0' a0.
    ¬(canonical.Cons_monom a0 a1 a2 = canonical.Cons_varlist a0' a1')

(sr vm x. canonical.ivl_aux sr vm x [] = quote.varmap_find x vm)
  sr vm x x' t'.
    canonical.ivl_aux sr vm x (x' :: t') =
    semi_ring.semi_ring_SRM sr (quote.varmap_find x vm)
      (canonical.ivl_aux sr vm x' t')

f0 f1 f2.
    fn.
      fn canonical.Nil_monom = f0
      (a0 a1 a2.
         fn (canonical.Cons_monom a0 a1 a2) = f1 a0 a1 a2 (fn a2))
      a0 a1. fn (canonical.Cons_varlist a0 a1) = f2 a0 a1 (fn a1)

M M' f.
    M = M'
    (a0 a1 a2 a3.
       M' = semi_ring.recordtype.semi_ring a0 a1 a2 a3
       f a0 a1 a2 a3 = f' a0 a1 a2 a3)
    semi_ring.semi_ring_CASE M f = semi_ring.semi_ring_CASE M' f'

r a0 a f1 f0 f.
    ring.ring_R0_fupd (const a0)
      (ring.ring_R1_fupd (const a)
         (ring.ring_RP_fupd (const f1)
            (ring.ring_RM_fupd (const f0)
               (ring.ring_RN_fupd (const f) r)))) =
    ring.ring_R0_fupd (const a0)
      (ring.ring_R1_fupd (const a)
         (ring.ring_RP_fupd (const f1)
            (ring.ring_RM_fupd (const f0)
               (ring.ring_RN_fupd (const f) bool.ARB))))

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'ring'.
           (a0'.
              (a0 a1 a2 a3 a4.
                 a0' =
                 (let a0 a0 in
                  λa1 a2 a3 a4.
                    ind_type.CONSTR 0 (a0, a1, a2, a3, a4)
                      (λn. ind_type.BOTTOM)) a1 a2 a3 a4) 'ring' a0')
           'ring' a0') rep

(a f f1 v. quote.index_CASE (quote.Left_idx a) f f1 v = f a)
  (a f f1 v. quote.index_CASE (quote.Right_idx a) f f1 v = f1 a)
  f f1 v. quote.index_CASE quote.End_idx f f1 v = v

P.
    (i. P (canonical.SPvar i)) (a. P (canonical.SPconst a))
    (s s0. P s P s0 P (canonical.SPplus s s0))
    (s s0. P s P s0 P (canonical.SPmult s s0)) s. P s

M M' f.
    M = M'
    (a0 a1 a2 a3 a4.
       M' = ring.recordtype.ring a0 a1 a2 a3 a4
       f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4)
    ring.ring_CASE M f = ring.ring_CASE M' f'

M M' v0 v1 v2.
    M = M' (M' = prelim.LESS v0 = v0')
    (M' = prelim.EQUAL v1 = v1') (M' = prelim.GREATER v2 = v2')
    prelim.ordering_CASE M v0 v1 v2 = prelim.ordering_CASE M' v0' v1' v2'

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'varmap'.
           (a0'.
              a0' = ind_type.CONSTR 0 bool.ARB (λn. ind_type.BOTTOM)
              (a0 a1 a2.
                 a0' =
                 (let a0 a0 in
                  λa1 a2.
                    ind_type.CONSTR (suc 0) a0
                      (ind_type.FCONS a1
                         (ind_type.FCONS a2 (λn. ind_type.BOTTOM)))) a1
                   a2 'varmap' a1 'varmap' a2) 'varmap' a0')
           'varmap' a0') rep

a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
    ring.recordtype.ring a0 a1 a2 a3 a4 =
    ring.recordtype.ring a0' a1' a2' a3' a4'
    a0 = a0' a1 = a1' a2 = a2' a3 = a3' a4 = a4'

M M' v f.
    M = M' (M' = quote.Empty_vm v = v')
    (a0 a1 a2. M' = quote.Node_vm a0 a1 a2 f a0 a1 a2 = f' a0 a1 a2)
    quote.varmap_CASE M v f = quote.varmap_CASE M' v' f'

(a0 a1 a2 a0' a1' a2'.
     canonical.Cons_monom a0 a1 a2 = canonical.Cons_monom a0' a1' a2'
     a0 = a0' a1 = a1' a2 = a2')
  a0 a1 a0' a1'.
    canonical.Cons_varlist a0 a1 = canonical.Cons_varlist a0' a1'
    a0 = a0' a1 = a1'

P.
    (i. P (ringNorm.Pvar i)) (a. P (ringNorm.Pconst a))
    (p p0. P p P p0 P (ringNorm.Pplus p p0))
    (p p0. P p P p0 P (ringNorm.Pmult p p0))
    (p. P p P (ringNorm.Popp p)) p. P p

r.
    (c0 c l t.
       ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_monom c l t) =
       canonical.Cons_monom (ring.ring_RM r c0 c) l
         (ringNorm.r_canonical_sum_scalar r c0 t))
    (c0 l t.
       ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_varlist l t) =
       canonical.Cons_monom c0 l
         (ringNorm.r_canonical_sum_scalar r c0 t))
    c0.
      ringNorm.r_canonical_sum_scalar r c0 canonical.Nil_monom =
      canonical.Nil_monom

rep.
    bool.TYPE_DEFINITION
      (λa0.
         'index'.
           (a0.
              (a.
                 a0 =
                 (let a a in
                  ind_type.CONSTR 0 bool.ARB
                    (ind_type.FCONS a (λn. ind_type.BOTTOM)))
                 'index' a)
              (a.
                 a0 =
                 (let a a in
                  ind_type.CONSTR (suc 0) bool.ARB
                    (ind_type.FCONS a (λn. ind_type.BOTTOM)))
                 'index' a)
              a0 =
              ind_type.CONSTR (suc (suc 0)) bool.ARB
                (λn. ind_type.BOTTOM) 'index' a0) 'index' a0) rep

(v f f1. canonical.canonical_sum_CASE canonical.Nil_monom v f f1 = v)
  (a0 a1 a2 v f f1.
     canonical.canonical_sum_CASE (canonical.Cons_monom a0 a1 a2) v f f1 =
     f a0 a1 a2)
  a0 a1 v f f1.
    canonical.canonical_sum_CASE (canonical.Cons_varlist a0 a1) v f f1 =
    f1 a0 a1

r.
    (vm. ringNorm.r_interp_cs r vm canonical.Nil_monom = ring.ring_R0 r)
    (vm l t.
       ringNorm.r_interp_cs r vm (canonical.Cons_varlist l t) =
       ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t)
    vm c l t.
      ringNorm.r_interp_cs r vm (canonical.Cons_monom c l t) =
      ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t

a01 a1 f01 f1 a02 a2 f02 f2.
    semi_ring.semi_ring_SR0_fupd (const a01)
      (semi_ring.semi_ring_SR1_fupd (const a1)
         (semi_ring.semi_ring_SRP_fupd (const f01)
            (semi_ring.semi_ring_SRM_fupd (const f1) bool.ARB))) =
    semi_ring.semi_ring_SR0_fupd (const a02)
      (semi_ring.semi_ring_SR1_fupd (const a2)
         (semi_ring.semi_ring_SRP_fupd (const f02)
            (semi_ring.semi_ring_SRM_fupd (const f2) bool.ARB)))
    a01 = a02 a1 = a2 f01 = f02 f1 = f2

(f. canonical.canonical_sum_size f canonical.Nil_monom = 0)
  (f a0 a1 a2.
     canonical.canonical_sum_size f (canonical.Cons_monom a0 a1 a2) =
     1 +
     (f a0 +
      (list.list_size quote.index_size a1 +
       canonical.canonical_sum_size f a2)))
  f a0 a1.
    canonical.canonical_sum_size f (canonical.Cons_varlist a0 a1) =
    1 +
    (list.list_size quote.index_size a0 +
     canonical.canonical_sum_size f a1)

M M' f f1 v.
    M = M' (a. M' = quote.Left_idx a f a = f' a)
    (a. M' = quote.Right_idx a f1 a = f1' a)
    (M' = quote.End_idx v = v')
    quote.index_CASE M f f1 v = quote.index_CASE M' f' f1' v'

f0 f1 f2 f3.
    fn.
      (a. fn (canonical.SPvar a) = f0 a)
      (a. fn (canonical.SPconst a) = f1 a)
      (a0 a1. fn (canonical.SPplus a0 a1) = f2 a0 a1 (fn a0) (fn a1))
      a0 a1. fn (canonical.SPmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)

P.
    (sr l1 c2 l2 t2.
       P sr l1 t2 P sr l1 (canonical.Cons_monom c2 l2 t2))
    (sr l1 l2 t2. P sr l1 t2 P sr l1 (canonical.Cons_varlist l2 t2))
    (sr l1. P sr l1 canonical.Nil_monom) v v1 v2. P v v1 v2

(sr c0 c l t.
     canonical.canonical_sum_scalar sr c0 (canonical.Cons_monom c l t) =
     canonical.Cons_monom (semi_ring.semi_ring_SRM sr c0 c) l
       (canonical.canonical_sum_scalar sr c0 t))
  (sr c0 l t.
     canonical.canonical_sum_scalar sr c0 (canonical.Cons_varlist l t) =
     canonical.Cons_monom c0 l (canonical.canonical_sum_scalar sr c0 t))
  sr c0.
    canonical.canonical_sum_scalar sr c0 canonical.Nil_monom =
    canonical.Nil_monom

r.
    (c1 l1 t1 s2.
       ringNorm.r_canonical_sum_prod r (canonical.Cons_monom c1 l1 t1) s2 =
       ringNorm.r_canonical_sum_merge r
         (ringNorm.r_canonical_sum_scalar3 r c1 l1 s2)
         (ringNorm.r_canonical_sum_prod r t1 s2))
    (l1 t1 s2.
       ringNorm.r_canonical_sum_prod r (canonical.Cons_varlist l1 t1) s2 =
       ringNorm.r_canonical_sum_merge r
         (ringNorm.r_canonical_sum_scalar2 r l1 s2)
         (ringNorm.r_canonical_sum_prod r t1 s2))
    s2.
      ringNorm.r_canonical_sum_prod r canonical.Nil_monom s2 =
      canonical.Nil_monom

r.
    (l0 c l t.
       ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_monom c l t) =
       ringNorm.r_monom_insert r c (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar2 r l0 t))
    (l0 l t.
       ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_varlist l t) =
       ringNorm.r_varlist_insert r (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar2 r l0 t))
    l0.
      ringNorm.r_canonical_sum_scalar2 r l0 canonical.Nil_monom =
      canonical.Nil_monom

(sr vm.
     canonical.interp_cs sr vm canonical.Nil_monom =
     semi_ring.semi_ring_SR0 sr)
  (sr vm l t.
     canonical.interp_cs sr vm (canonical.Cons_varlist l t) =
     canonical.ics_aux sr vm (canonical.interp_vl sr vm l) t)
  sr vm c l t.
    canonical.interp_cs sr vm (canonical.Cons_monom c l t) =
    canonical.ics_aux sr vm (canonical.interp_m sr vm c l) t

(x v2 v1. quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x)
  (x v2 v1 i1.
     quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
     quote.varmap_find i1 v2)
  (x v2 v1 i1.
     quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
     quote.varmap_find i1 v1)
  i. quote.varmap_find i quote.Empty_vm = select x.

r.
    (c l t.
       ringNorm.r_canonical_sum_simplify r (canonical.Cons_monom c l t) =
       if c = ring.ring_R0 r then ringNorm.r_canonical_sum_simplify r t
       else if c = ring.ring_R1 r then
         canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t)
       else
         canonical.Cons_monom c l
           (ringNorm.r_canonical_sum_simplify r t))
    (l t.
       ringNorm.r_canonical_sum_simplify r (canonical.Cons_varlist l t) =
       canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t))
    ringNorm.r_canonical_sum_simplify r canonical.Nil_monom =
    canonical.Nil_monom

(a a0 f f0.
     semi_ring.semi_ring_SR0 (semi_ring.recordtype.semi_ring a a0 f f0) =
     a)
  (a a0 f f0.
     semi_ring.semi_ring_SR1 (semi_ring.recordtype.semi_ring a a0 f f0) =
     a0)
  (a a0 f f0.
     semi_ring.semi_ring_SRP (semi_ring.recordtype.semi_ring a a0 f f0) =
     f)
  a a0 f f0.
    semi_ring.semi_ring_SRM (semi_ring.recordtype.semi_ring a a0 f f0) = f0

r.
    (i.
       ringNorm.r_spolynom_normalize r (canonical.SPvar i) =
       canonical.Cons_varlist (i :: []) canonical.Nil_monom)
    (c.
       ringNorm.r_spolynom_normalize r (canonical.SPconst c) =
       canonical.Cons_monom c [] canonical.Nil_monom)
    (l r'.
       ringNorm.r_spolynom_normalize r (canonical.SPplus l r') =
       ringNorm.r_canonical_sum_merge r (ringNorm.r_spolynom_normalize r l)
         (ringNorm.r_spolynom_normalize r r'))
    l r'.
      ringNorm.r_spolynom_normalize r (canonical.SPmult l r') =
      ringNorm.r_canonical_sum_prod r (ringNorm.r_spolynom_normalize r l)
        (ringNorm.r_spolynom_normalize r r')

P.
    (x v1 v2. P quote.End_idx (quote.Node_vm x v1 v2))
    (i1 x v1 v2.
       P i1 v2 P (quote.Right_idx i1) (quote.Node_vm x v1 v2))
    (i1 x v1 v2.
       P i1 v1 P (quote.Left_idx i1) (quote.Node_vm x v1 v2))
    (i. P i quote.Empty_vm) v v1. P v v1

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

(sr l0 c l t.
     canonical.canonical_sum_scalar2 sr l0 (canonical.Cons_monom c l t) =
     canonical.monom_insert sr c (prelim.list_merge quote.index_lt l0 l)
       (canonical.canonical_sum_scalar2 sr l0 t))
  (sr l0 l t.
     canonical.canonical_sum_scalar2 sr l0 (canonical.Cons_varlist l t) =
     canonical.varlist_insert sr (prelim.list_merge quote.index_lt l0 l)
       (canonical.canonical_sum_scalar2 sr l0 t))
  sr l0.
    canonical.canonical_sum_scalar2 sr l0 canonical.Nil_monom =
    canonical.Nil_monom

P.
    (cmp. P cmp [] []) (cmp v8 v9. P cmp [] (v8 :: v9))
    (cmp v4 v5. P cmp (v4 :: v5) [])
    (cmp x l1 y l2. P cmp l1 l2 P cmp (x :: l1) (y :: l2))
    v v1 v2. P v v1 v2

(sr c l t.
     canonical.canonical_sum_simplify sr (canonical.Cons_monom c l t) =
     if c = semi_ring.semi_ring_SR0 sr then
       canonical.canonical_sum_simplify sr t
     else if c = semi_ring.semi_ring_SR1 sr then
       canonical.Cons_varlist l (canonical.canonical_sum_simplify sr t)
     else
       canonical.Cons_monom c l (canonical.canonical_sum_simplify sr t))
  (sr l t.
     canonical.canonical_sum_simplify sr (canonical.Cons_varlist l t) =
     canonical.Cons_varlist l (canonical.canonical_sum_simplify sr t))
  sr.
    canonical.canonical_sum_simplify sr canonical.Nil_monom =
    canonical.Nil_monom

(cmp. prelim.list_compare cmp [] [] = prelim.EQUAL)
  (v9 v8 cmp. prelim.list_compare cmp [] (v8 :: v9) = prelim.LESS)
  (v5 v4 cmp. prelim.list_compare cmp (v4 :: v5) [] = prelim.GREATER)
  y x l2 l1 cmp.
    prelim.list_compare cmp (x :: l1) (y :: l2) =
    prelim.compare (cmp x y) prelim.LESS (prelim.list_compare cmp l1 l2)
      prelim.GREATER

(l1 a_lt. prelim.list_merge a_lt l1 [] = l1)
  (v5 v4 a_lt. prelim.list_merge a_lt [] (v4 :: v5) = v4 :: v5)
  y x l2 l1 a_lt.
    prelim.list_merge a_lt (x :: l1) (y :: l2) =
    if a_lt x y then x :: prelim.list_merge a_lt l1 (y :: l2)
    else y :: prelim.list_merge a_lt (x :: l1) l2

prelim.list_compare_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       y x l2 l1 cmp. R (cmp, l1, l2) (cmp, x :: l1, y :: l2))
    (λlist_compare_tupled a.
       pair.pair_CASE a
         (λcmp v1.
            pair.pair_CASE v1
              (λv2 v3.
                 list.list_CASE v2
                   (list.list_CASE v3 (id prelim.EQUAL)
                      (λv10 v11. id prelim.LESS))
                   (λx l1.
                      list.list_CASE v3 (id prelim.GREATER)
                        (λy l2.
                           id
                             (prelim.compare (cmp x y) prelim.LESS
                                (list_compare_tupled (cmp, l1, l2))
                                prelim.GREATER))))))

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

(s g f.
     semi_ring.semi_ring_SR0_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
     semi_ring.semi_ring_SR0_fupd (f g) s)
  (s g f.
     semi_ring.semi_ring_SR1_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
     semi_ring.semi_ring_SR1_fupd (f g) s)
  (s g f.
     semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SRP_fupd g s) =
     semi_ring.semi_ring_SRP_fupd (f g) s)
  s g f.
    semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRM_fupd g s) =
    semi_ring.semi_ring_SRM_fupd (f g) s

r.
    (vm a. ringNorm.r_ics_aux r vm a canonical.Nil_monom = a)
    (vm a l t.
       ringNorm.r_ics_aux r vm a (canonical.Cons_varlist l t) =
       ring.ring_RP r a
         (ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t))
    vm a c l t.
      ringNorm.r_ics_aux r vm a (canonical.Cons_monom c l t) =
      ring.ring_RP r a
        (ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t)

f0 f1 f2 f3 f4.
    fn.
      (a. fn (ringNorm.Pvar a) = f0 a)
      (a. fn (ringNorm.Pconst a) = f1 a)
      (a0 a1. fn (ringNorm.Pplus a0 a1) = f2 a0 a1 (fn a0) (fn a1))
      (a0 a1. fn (ringNorm.Pmult a0 a1) = f3 a0 a1 (fn a0) (fn a1))
      a. fn (ringNorm.Popp a) = f4 a (fn a)

a01 a1 f11 f01 f1 a02 a2 f12 f02 f2.
    ring.ring_R0_fupd (const a01)
      (ring.ring_R1_fupd (const a1)
         (ring.ring_RP_fupd (const f11)
            (ring.ring_RM_fupd (const f01)
               (ring.ring_RN_fupd (const f1) bool.ARB)))) =
    ring.ring_R0_fupd (const a02)
      (ring.ring_R1_fupd (const a2)
         (ring.ring_RP_fupd (const f12)
            (ring.ring_RM_fupd (const f02)
               (ring.ring_RN_fupd (const f2) bool.ARB))))
    a01 = a02 a1 = a2 f11 = f12 f01 = f02 f1 = f2

P.
    (sr c1 l1 c2 l2 t2.
       P sr c1 l1 t2 P sr c1 l1 (canonical.Cons_monom c2 l2 t2))
    (sr c1 l1 l2 t2.
       P sr c1 l1 t2 P sr c1 l1 (canonical.Cons_varlist l2 t2))
    (sr c1 l1. P sr c1 l1 canonical.Nil_monom) v v1 v2 v3. P v v1 v2 v3

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'canonical_sum'.
           (a0'.
              a0' =
              ind_type.CONSTR 0 (bool.ARB, bool.ARB)
                (λn. ind_type.BOTTOM)
              (a0 a1 a2.
                 a0' =
                 (let a0 a0 in
                  λa1 a2.
                    ind_type.CONSTR (suc 0) (a0, a1)
                      (ind_type.FCONS a2 (λn. ind_type.BOTTOM))) a1 a2
                 'canonical_sum' a2)
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc (suc 0)) (bool.ARB, a0)
                      (ind_type.FCONS a1 (λn. ind_type.BOTTOM))) a1
                 'canonical_sum' a1) 'canonical_sum' a0')
           'canonical_sum' a0') rep

quote.varmap_find_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (v1 x v2 i1.
          R (i1, v2) (quote.Right_idx i1, quote.Node_vm x v1 v2))
       v2 x v1 i1. R (i1, v1) (quote.Left_idx i1, quote.Node_vm x v1 v2))
    (λvarmap_find_tupled a.
       pair.pair_CASE a
         (λv3 v4.
            quote.varmap_CASE v4 (id (select x. ))
              (λx v1 v2.
                 quote.index_CASE v3
                   (λi1'. id (varmap_find_tupled (i1', v1)))
                   (λi1. id (varmap_find_tupled (i1, v2))) (id x))))

M M' v f f1.
    M = M' (M' = canonical.Nil_monom v = v')
    (a0 a1 a2.
       M' = canonical.Cons_monom a0 a1 a2 f a0 a1 a2 = f' a0 a1 a2)
    (a0 a1. M' = canonical.Cons_varlist a0 a1 f1 a0 a1 = f1' a0 a1)
    canonical.canonical_sum_CASE M v f f1 =
    canonical.canonical_sum_CASE M' v' f' f1'

P.
    (a_lt l1. P a_lt l1 []) (a_lt v4 v5. P a_lt [] (v4 :: v5))
    (a_lt x l1 y l2.
       (¬a_lt x y P a_lt (x :: l1) l2)
       (a_lt x y P a_lt l1 (y :: l2)) P a_lt (x :: l1) (y :: l2))
    v v1 v2. P v v1 v2

(a a'. canonical.SPvar a = canonical.SPvar a' a = a')
  (a a'. canonical.SPconst a = canonical.SPconst a' a = a')
  (a0 a1 a0' a1'.
     canonical.SPplus a0 a1 = canonical.SPplus a0' a1'
     a0 = a0' a1 = a1')
  a0 a1 a0' a1'.
    canonical.SPmult a0 a1 = canonical.SPmult a0' a1' a0 = a0' a1 = a1'

r.
    (vm c. ringNorm.r_interp_sp r vm (canonical.SPconst c) = c)
    (vm i.
       ringNorm.r_interp_sp r vm (canonical.SPvar i) =
       quote.varmap_find i vm)
    (vm p1 p2.
       ringNorm.r_interp_sp r vm (canonical.SPplus p1 p2) =
       ring.ring_RP r (ringNorm.r_interp_sp r vm p1)
         (ringNorm.r_interp_sp r vm p2))
    vm p1 p2.
      ringNorm.r_interp_sp r vm (canonical.SPmult p1 p2) =
      ring.ring_RM r (ringNorm.r_interp_sp r vm p1)
        (ringNorm.r_interp_sp r vm p2)

(sr vm a. canonical.ics_aux sr vm a canonical.Nil_monom = a)
  (sr vm a l t.
     canonical.ics_aux sr vm a (canonical.Cons_varlist l t) =
     semi_ring.semi_ring_SRP sr a
       (canonical.ics_aux sr vm (canonical.interp_vl sr vm l) t))
  sr vm a c l t.
    canonical.ics_aux sr vm a (canonical.Cons_monom c l t) =
    semi_ring.semi_ring_SRP sr a
      (canonical.ics_aux sr vm (canonical.interp_m sr vm c l) t)

(f a.
     canonical.spolynom_size f (canonical.SPvar a) =
     1 + quote.index_size a)
  (f a. canonical.spolynom_size f (canonical.SPconst a) = 1 + f a)
  (f a0 a1.
     canonical.spolynom_size f (canonical.SPplus a0 a1) =
     1 + (canonical.spolynom_size f a0 + canonical.spolynom_size f a1))
  f a0 a1.
    canonical.spolynom_size f (canonical.SPmult a0 a1) =
    1 + (canonical.spolynom_size f a0 + canonical.spolynom_size f a1)

r.
    (c0 l0 c l t.
       ringNorm.r_canonical_sum_scalar3 r c0 l0
         (canonical.Cons_monom c l t) =
       ringNorm.r_monom_insert r (ring.ring_RM r c0 c)
         (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar3 r c0 l0 t))
    (c0 l0 l t.
       ringNorm.r_canonical_sum_scalar3 r c0 l0
         (canonical.Cons_varlist l t) =
       ringNorm.r_monom_insert r c0 (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar3 r c0 l0 t))
    c0 l0.
      ringNorm.r_canonical_sum_scalar3 r c0 l0 canonical.Nil_monom =
      canonical.Nil_monom

(a' a. ¬(canonical.SPvar a = canonical.SPconst a'))
  (a1 a0 a. ¬(canonical.SPvar a = canonical.SPplus a0 a1))
  (a1 a0 a. ¬(canonical.SPvar a = canonical.SPmult a0 a1))
  (a1 a0 a. ¬(canonical.SPconst a = canonical.SPplus a0 a1))
  (a1 a0 a. ¬(canonical.SPconst a = canonical.SPmult a0 a1))
  a1' a1 a0' a0. ¬(canonical.SPplus a0 a1 = canonical.SPmult a0' a1')

(sr vm c. canonical.interp_sp sr vm (canonical.SPconst c) = c)
  (sr vm i.
     canonical.interp_sp sr vm (canonical.SPvar i) =
     quote.varmap_find i vm)
  (sr vm p1 p2.
     canonical.interp_sp sr vm (canonical.SPplus p1 p2) =
     semi_ring.semi_ring_SRP sr (canonical.interp_sp sr vm p1)
       (canonical.interp_sp sr vm p2))
  sr vm p1 p2.
    canonical.interp_sp sr vm (canonical.SPmult p1 p2) =
    semi_ring.semi_ring_SRM sr (canonical.interp_sp sr vm p1)
      (canonical.interp_sp sr vm p2)

(sr c0 l0 c l t.
     canonical.canonical_sum_scalar3 sr c0 l0
       (canonical.Cons_monom c l t) =
     canonical.monom_insert sr (semi_ring.semi_ring_SRM sr c0 c)
       (prelim.list_merge quote.index_lt l0 l)
       (canonical.canonical_sum_scalar3 sr c0 l0 t))
  (sr c0 l0 l t.
     canonical.canonical_sum_scalar3 sr c0 l0
       (canonical.Cons_varlist l t) =
     canonical.monom_insert sr c0 (prelim.list_merge quote.index_lt l0 l)
       (canonical.canonical_sum_scalar3 sr c0 l0 t))
  sr c0 l0.
    canonical.canonical_sum_scalar3 sr c0 l0 canonical.Nil_monom =
    canonical.Nil_monom

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

P.
    P quote.End_idx quote.End_idx
    (v10. P quote.End_idx (quote.Left_idx v10))
    (v11. P quote.End_idx (quote.Right_idx v11))
    (v2. P (quote.Left_idx v2) quote.End_idx)
    (v3. P (quote.Right_idx v3) quote.End_idx)
    (n' m'. P n' m' P (quote.Left_idx n') (quote.Left_idx m'))
    (n' m'. P (quote.Left_idx n') (quote.Right_idx m'))
    (n' m'. P n' m' P (quote.Right_idx n') (quote.Right_idx m'))
    (n' m'. P (quote.Right_idx n') (quote.Left_idx m')) v v1. P v v1

(r g f.
     ring.ring_R0_fupd f (ring.ring_R0_fupd g r) =
     ring.ring_R0_fupd (f g) r)
  (r g f.
     ring.ring_R1_fupd f (ring.ring_R1_fupd g r) =
     ring.ring_R1_fupd (f g) r)
  (r g f.
     ring.ring_RP_fupd f (ring.ring_RP_fupd g r) =
     ring.ring_RP_fupd (f g) r)
  (r g f.
     ring.ring_RM_fupd f (ring.ring_RM_fupd g r) =
     ring.ring_RM_fupd (f g) r)
  r g f.
    ring.ring_RN_fupd f (ring.ring_RN_fupd g r) =
    ring.ring_RN_fupd (f g) r

(a a'. ringNorm.Pvar a = ringNorm.Pvar a' a = a')
  (a a'. ringNorm.Pconst a = ringNorm.Pconst a' a = a')
  (a0 a1 a0' a1'.
     ringNorm.Pplus a0 a1 = ringNorm.Pplus a0' a1' a0 = a0' a1 = a1')
  (a0 a1 a0' a1'.
     ringNorm.Pmult a0 a1 = ringNorm.Pmult a0' a1' a0 = a0' a1 = a1')
  a a'. ringNorm.Popp a = ringNorm.Popp a' a = a'

(r i.
     ringNorm.polynom_normalize r (ringNorm.Pvar i) =
     canonical.Cons_varlist (i :: []) canonical.Nil_monom)
  (r c.
     ringNorm.polynom_normalize r (ringNorm.Pconst c) =
     canonical.Cons_monom c [] canonical.Nil_monom)
  (r pl pr.
     ringNorm.polynom_normalize r (ringNorm.Pplus pl pr) =
     ringNorm.r_canonical_sum_merge r (ringNorm.polynom_normalize r pl)
       (ringNorm.polynom_normalize r pr))
  (r pl pr.
     ringNorm.polynom_normalize r (ringNorm.Pmult pl pr) =
     ringNorm.r_canonical_sum_prod r (ringNorm.polynom_normalize r pl)
       (ringNorm.polynom_normalize r pr))
  r p.
    ringNorm.polynom_normalize r (ringNorm.Popp p) =
    ringNorm.r_canonical_sum_scalar3 r (ring.ring_RN r (ring.ring_R1 r)) []
      (ringNorm.polynom_normalize r p)

M M' f f1 f2 f3.
    M = M' (a. M' = canonical.SPvar a f a = f' a)
    (a. M' = canonical.SPconst a f1 a = f1' a)
    (a0 a1. M' = canonical.SPplus a0 a1 f2 a0 a1 = f2' a0 a1)
    (a0 a1. M' = canonical.SPmult a0 a1 f3 a0 a1 = f3' a0 a1)
    canonical.spolynom_CASE M f f1 f2 f3 =
    canonical.spolynom_CASE M' f' f1' f2' f3'

(f a.
     ringNorm.polynom_size f (ringNorm.Pvar a) = 1 + quote.index_size a)
  (f a. ringNorm.polynom_size f (ringNorm.Pconst a) = 1 + f a)
  (f a0 a1.
     ringNorm.polynom_size f (ringNorm.Pplus a0 a1) =
     1 + (ringNorm.polynom_size f a0 + ringNorm.polynom_size f a1))
  (f a0 a1.
     ringNorm.polynom_size f (ringNorm.Pmult a0 a1) =
     1 + (ringNorm.polynom_size f a0 + ringNorm.polynom_size f a1))
  f a.
    ringNorm.polynom_size f (ringNorm.Popp a) =
    1 + ringNorm.polynom_size f a

(a a0 f f0 f1. ring.ring_R0 (ring.recordtype.ring a a0 f f0 f1) = a)
  (a a0 f f0 f1. ring.ring_R1 (ring.recordtype.ring a a0 f f0 f1) = a0)
  (a a0 f f0 f1. ring.ring_RP (ring.recordtype.ring a a0 f f0 f1) = f)
  (a a0 f f0 f1. ring.ring_RM (ring.recordtype.ring a a0 f f0 f1) = f0)
  a a0 f f0 f1. ring.ring_RN (ring.recordtype.ring a a0 f f0 f1) = f1

quote.index_compare quote.End_idx quote.End_idx = prelim.EQUAL
  (v10.
     quote.index_compare quote.End_idx (quote.Left_idx v10) =
     prelim.LESS)
  (v11.
     quote.index_compare quote.End_idx (quote.Right_idx v11) =
     prelim.LESS)
  (v2.
     quote.index_compare (quote.Left_idx v2) quote.End_idx =
     prelim.GREATER)
  (v3.
     quote.index_compare (quote.Right_idx v3) quote.End_idx =
     prelim.GREATER)
  (n' m'.
     quote.index_compare (quote.Left_idx n') (quote.Left_idx m') =
     quote.index_compare n' m')
  (n' m'.
     quote.index_compare (quote.Left_idx n') (quote.Right_idx m') =
     prelim.LESS)
  (n' m'.
     quote.index_compare (quote.Right_idx n') (quote.Right_idx m') =
     quote.index_compare n' m')
  n' m'.
    quote.index_compare (quote.Right_idx n') (quote.Left_idx m') =
    prelim.GREATER

(f1 a a0 f f0.
     semi_ring.semi_ring_SR0_fupd f1
       (semi_ring.recordtype.semi_ring a a0 f f0) =
     semi_ring.recordtype.semi_ring (f1 a) a0 f f0)
  (f1 a a0 f f0.
     semi_ring.semi_ring_SR1_fupd f1
       (semi_ring.recordtype.semi_ring a a0 f f0) =
     semi_ring.recordtype.semi_ring a (f1 a0) f f0)
  (f1 a a0 f f0.
     semi_ring.semi_ring_SRP_fupd f1
       (semi_ring.recordtype.semi_ring a a0 f f0) =
     semi_ring.recordtype.semi_ring a a0 (f1 f) f0)
  f1 a a0 f f0.
    semi_ring.semi_ring_SRM_fupd f1
      (semi_ring.recordtype.semi_ring a a0 f f0) =
    semi_ring.recordtype.semi_ring a a0 f (f1 f0)

r.
    (t2 l2 l1 c2.
       ringNorm.r_varlist_insert r l1 (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
         (canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1 t2)
         (canonical.Cons_monom c2 l2
            (ringNorm.r_varlist_insert r l1 t2)))
    (t2 l2 l1.
       ringNorm.r_varlist_insert r l1 (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
         (canonical.Cons_monom
            (ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1 t2)
         (canonical.Cons_varlist l2 (ringNorm.r_varlist_insert r l1 t2)))
    l1.
      ringNorm.r_varlist_insert r l1 canonical.Nil_monom =
      canonical.Cons_varlist l1 canonical.Nil_monom

(r vm c. ringNorm.interp_p r vm (ringNorm.Pconst c) = c)
  (r vm i.
     ringNorm.interp_p r vm (ringNorm.Pvar i) = quote.varmap_find i vm)
  (r vm p1 p2.
     ringNorm.interp_p r vm (ringNorm.Pplus p1 p2) =
     ring.ring_RP r (ringNorm.interp_p r vm p1)
       (ringNorm.interp_p r vm p2))
  (r vm p1 p2.
     ringNorm.interp_p r vm (ringNorm.Pmult p1 p2) =
     ring.ring_RM r (ringNorm.interp_p r vm p1)
       (ringNorm.interp_p r vm p2))
  r vm p1.
    ringNorm.interp_p r vm (ringNorm.Popp p1) =
    ring.ring_RN r (ringNorm.interp_p r vm p1)

(t2 sr l2 l1 c2.
     canonical.varlist_insert sr l1 (canonical.Cons_monom c2 l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr) c2) l1
          t2)
       (canonical.Cons_monom c2 l2 (canonical.varlist_insert sr l1 t2)))
  (t2 sr l2 l1.
     canonical.varlist_insert sr l1 (canonical.Cons_varlist l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr)
             (semi_ring.semi_ring_SR1 sr)) l1 t2)
       (canonical.Cons_varlist l2 (canonical.varlist_insert sr l1 t2)))
  sr l1.
    canonical.varlist_insert sr l1 canonical.Nil_monom =
    canonical.Cons_varlist l1 canonical.Nil_monom

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'spolynom'.
           (a0'.
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR 0 (a, bool.ARB) (λn. ind_type.BOTTOM))
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc 0) (bool.ARB, a)
                   (λn. ind_type.BOTTOM))
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc (suc 0)) (bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'spolynom' a0 'spolynom' a1)
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc (suc (suc 0)))
                      (bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'spolynom' a0 'spolynom' a1) 'spolynom' a0')
           'spolynom' a0') rep

(x. x = x )
  (prelim.ordering2num prelim.LESS = 0
   prelim.ordering2num prelim.EQUAL = 1
   prelim.ordering2num prelim.GREATER = arithmetic.BIT2 0)
  ((v0 v1 v2. prelim.ordering_CASE prelim.LESS v0 v1 v2 = v0)
   (v0 v1 v2. prelim.ordering_CASE prelim.EQUAL v0 v1 v2 = v1)
   v0 v1 v2. prelim.ordering_CASE prelim.GREATER v0 v1 v2 = v2)
  (prelim.LESS = prelim.EQUAL ) (prelim.LESS = prelim.GREATER )
  (prelim.EQUAL = prelim.GREATER ) (prelim.EQUAL = prelim.LESS )
  (prelim.GREATER = prelim.LESS ) (prelim.GREATER = prelim.EQUAL )

(s g f.
     semi_ring.semi_ring_SR1_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
     semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SR1_fupd f s))
  (s g f.
     semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
     semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SRP_fupd f s))
  (s g f.
     semi_ring.semi_ring_SRP_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
     semi_ring.semi_ring_SR1_fupd g (semi_ring.semi_ring_SRP_fupd f s))
  (s g f.
     semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SR0_fupd g s) =
     semi_ring.semi_ring_SR0_fupd g (semi_ring.semi_ring_SRM_fupd f s))
  (s g f.
     semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SR1_fupd g s) =
     semi_ring.semi_ring_SR1_fupd g (semi_ring.semi_ring_SRM_fupd f s))
  s g f.
    semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRP_fupd g s) =
    semi_ring.semi_ring_SRP_fupd g (semi_ring.semi_ring_SRM_fupd f s)

r.
    (t2 l2 l1 c2 c1.
       ringNorm.r_monom_insert r c1 l1 (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
         (canonical.Cons_monom (ring.ring_RP r c1 c2) l1 t2)
         (canonical.Cons_monom c2 l2
            (ringNorm.r_monom_insert r c1 l1 t2)))
    (t2 l2 l1 c1.
       ringNorm.r_monom_insert r c1 l1 (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
         (canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1 t2)
         (canonical.Cons_varlist l2
            (ringNorm.r_monom_insert r c1 l1 t2)))
    l1 c1.
      ringNorm.r_monom_insert r c1 l1 canonical.Nil_monom =
      canonical.Cons_monom c1 l1 canonical.Nil_monom

M M' f f1 f2 f3 f4.
    M = M' (a. M' = ringNorm.Pvar a f a = f' a)
    (a. M' = ringNorm.Pconst a f1 a = f1' a)
    (a0 a1. M' = ringNorm.Pplus a0 a1 f2 a0 a1 = f2' a0 a1)
    (a0 a1. M' = ringNorm.Pmult a0 a1 f3 a0 a1 = f3' a0 a1)
    (a. M' = ringNorm.Popp a f4 a = f4' a)
    ringNorm.polynom_CASE M f f1 f2 f3 f4 =
    ringNorm.polynom_CASE M' f' f1' f2' f3' f4'

(t2 sr l2 l1 c2 c1.
     canonical.monom_insert sr c1 l1 (canonical.Cons_monom c2 l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
       (canonical.Cons_monom (semi_ring.semi_ring_SRP sr c1 c2) l1 t2)
       (canonical.Cons_monom c2 l2 (canonical.monom_insert sr c1 l1 t2)))
  (t2 sr l2 l1 c1.
     canonical.monom_insert sr c1 l1 (canonical.Cons_varlist l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr c1 (semi_ring.semi_ring_SR1 sr)) l1
          t2)
       (canonical.Cons_varlist l2 (canonical.monom_insert sr c1 l1 t2)))
  sr l1 c1.
    canonical.monom_insert sr c1 l1 canonical.Nil_monom =
    canonical.Cons_monom c1 l1 canonical.Nil_monom

prelim.list_merge_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (l2 l1 y x a_lt.
          ¬a_lt x y R (a_lt, x :: l1, l2) (a_lt, x :: l1, y :: l2))
       l2 l1 y x a_lt.
         a_lt x y R (a_lt, l1, y :: l2) (a_lt, x :: l1, y :: l2))
    (λlist_merge_tupled a.
       pair.pair_CASE a
         (λa_lt v1.
            pair.pair_CASE v1
              (λl1 v3.
                 list.list_CASE v3 (id l1)
                   (λy l2.
                      list.list_CASE l1 (id (y :: l2))
                        (λx l1'.
                           id
                             (if a_lt x y then
                                x :: list_merge_tupled (a_lt, l1', y :: l2)
                              else
                                y ::
                                list_merge_tupled
                                  (a_lt, x :: l1', l2)))))))

(a f f1 f2 f3 f4.
     ringNorm.polynom_CASE (ringNorm.Pvar a) f f1 f2 f3 f4 = f a)
  (a f f1 f2 f3 f4.
     ringNorm.polynom_CASE (ringNorm.Pconst a) f f1 f2 f3 f4 = f1 a)
  (a0 a1 f f1 f2 f3 f4.
     ringNorm.polynom_CASE (ringNorm.Pplus a0 a1) f f1 f2 f3 f4 =
     f2 a0 a1)
  (a0 a1 f f1 f2 f3 f4.
     ringNorm.polynom_CASE (ringNorm.Pmult a0 a1) f f1 f2 f3 f4 =
     f3 a0 a1)
  a f f1 f2 f3 f4.
    ringNorm.polynom_CASE (ringNorm.Popp a) f f1 f2 f3 f4 = f4 a

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'polynom'.
           (a0'.
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR 0 (a, bool.ARB) (λn. ind_type.BOTTOM))
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc 0) (bool.ARB, a)
                   (λn. ind_type.BOTTOM))
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc (suc 0)) (bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'polynom' a0 'polynom' a1)
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc (suc (suc 0)))
                      (bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'polynom' a0 'polynom' a1)
              (a.
                 a0' =
                 (let a a in
                  ind_type.CONSTR (suc (suc (suc (suc 0))))
                    (bool.ARB, bool.ARB)
                    (ind_type.FCONS a (λn. ind_type.BOTTOM)))
                 'polynom' a) 'polynom' a0') 'polynom' a0') rep

(a' a. ¬(ringNorm.Pvar a = ringNorm.Pconst a'))
  (a1 a0 a. ¬(ringNorm.Pvar a = ringNorm.Pplus a0 a1))
  (a1 a0 a. ¬(ringNorm.Pvar a = ringNorm.Pmult a0 a1))
  (a' a. ¬(ringNorm.Pvar a = ringNorm.Popp a'))
  (a1 a0 a. ¬(ringNorm.Pconst a = ringNorm.Pplus a0 a1))
  (a1 a0 a. ¬(ringNorm.Pconst a = ringNorm.Pmult a0 a1))
  (a' a. ¬(ringNorm.Pconst a = ringNorm.Popp a'))
  (a1' a1 a0' a0. ¬(ringNorm.Pplus a0 a1 = ringNorm.Pmult a0' a1'))
  (a1 a0 a. ¬(ringNorm.Pplus a0 a1 = ringNorm.Popp a))
  a1 a0 a. ¬(ringNorm.Pmult a0 a1 = ringNorm.Popp a)

r.
    semi_ring.is_semi_ring r
    (n m. semi_ring.semi_ring_SRP r n m = semi_ring.semi_ring_SRP r m n)
    (n m p.
       semi_ring.semi_ring_SRP r n (semi_ring.semi_ring_SRP r m p) =
       semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRP r n m) p)
    (n m. semi_ring.semi_ring_SRM r n m = semi_ring.semi_ring_SRM r m n)
    (n m p.
       semi_ring.semi_ring_SRM r n (semi_ring.semi_ring_SRM r m p) =
       semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRM r n m) p)
    (n. semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SR0 r) n = n)
    (n. semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR1 r) n = n)
    (n.
       semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SR0 r) n =
       semi_ring.semi_ring_SR0 r)
    n m p.
      semi_ring.semi_ring_SRM r (semi_ring.semi_ring_SRP r n m) p =
      semi_ring.semi_ring_SRP r (semi_ring.semi_ring_SRM r n p)
        (semi_ring.semi_ring_SRM r m p)

r.
    ring.is_ring r
    (n m. ring.ring_RP r n m = ring.ring_RP r m n)
    (n m p.
       ring.ring_RP r n (ring.ring_RP r m p) =
       ring.ring_RP r (ring.ring_RP r n m) p)
    (n m. ring.ring_RM r n m = ring.ring_RM r m n)
    (n m p.
       ring.ring_RM r n (ring.ring_RM r m p) =
       ring.ring_RM r (ring.ring_RM r n m) p)
    (n. ring.ring_RP r (ring.ring_R0 r) n = n)
    (n. ring.ring_RM r (ring.ring_R1 r) n = n)
    (n. ring.ring_RP r n (ring.ring_RN r n) = ring.ring_R0 r)
    n m p.
      ring.ring_RM r (ring.ring_RP r n m) p =
      ring.ring_RP r (ring.ring_RM r n p) (ring.ring_RM r m p)

(f2 a a0 f f0 f1.
     ring.ring_R0_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
     ring.recordtype.ring (f2 a) a0 f f0 f1)
  (f2 a a0 f f0 f1.
     ring.ring_R1_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
     ring.recordtype.ring a (f2 a0) f f0 f1)
  (f2 a a0 f f0 f1.
     ring.ring_RP_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
     ring.recordtype.ring a a0 (f2 f) f0 f1)
  (f2 a a0 f f0 f1.
     ring.ring_RM_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
     ring.recordtype.ring a a0 f (f2 f0) f1)
  f2 a a0 f f0 f1.
    ring.ring_RN_fupd f2 (ring.recordtype.ring a a0 f f0 f1) =
    ring.recordtype.ring a a0 f f0 (f2 f1)

((g f.
      semi_ring.semi_ring_SR0_fupd f semi_ring.semi_ring_SR0_fupd g =
      semi_ring.semi_ring_SR0_fupd (f g))
   h g f.
     semi_ring.semi_ring_SR0_fupd f
     (semi_ring.semi_ring_SR0_fupd g h) =
     semi_ring.semi_ring_SR0_fupd (f g) h)
  ((g f.
      semi_ring.semi_ring_SR1_fupd f semi_ring.semi_ring_SR1_fupd g =
      semi_ring.semi_ring_SR1_fupd (f g))
   h g f.
     semi_ring.semi_ring_SR1_fupd f
     (semi_ring.semi_ring_SR1_fupd g h) =
     semi_ring.semi_ring_SR1_fupd (f g) h)
  ((g f.
      semi_ring.semi_ring_SRP_fupd f semi_ring.semi_ring_SRP_fupd g =
      semi_ring.semi_ring_SRP_fupd (f g))
   h g f.
     semi_ring.semi_ring_SRP_fupd f
     (semi_ring.semi_ring_SRP_fupd g h) =
     semi_ring.semi_ring_SRP_fupd (f g) h)
  (g f.
     semi_ring.semi_ring_SRM_fupd f semi_ring.semi_ring_SRM_fupd g =
     semi_ring.semi_ring_SRM_fupd (f g))
  h g f.
    semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRM_fupd g h) =
    semi_ring.semi_ring_SRM_fupd (f g) h

(r g f.
     ring.ring_R1_fupd f (ring.ring_R0_fupd g r) =
     ring.ring_R0_fupd g (ring.ring_R1_fupd f r))
  (r g f.
     ring.ring_RP_fupd f (ring.ring_R0_fupd g r) =
     ring.ring_R0_fupd g (ring.ring_RP_fupd f r))
  (r g f.
     ring.ring_RP_fupd f (ring.ring_R1_fupd g r) =
     ring.ring_R1_fupd g (ring.ring_RP_fupd f r))
  (r g f.
     ring.ring_RM_fupd f (ring.ring_R0_fupd g r) =
     ring.ring_R0_fupd g (ring.ring_RM_fupd f r))
  (r g f.
     ring.ring_RM_fupd f (ring.ring_R1_fupd g r) =
     ring.ring_R1_fupd g (ring.ring_RM_fupd f r))
  (r g f.
     ring.ring_RM_fupd f (ring.ring_RP_fupd g r) =
     ring.ring_RP_fupd g (ring.ring_RM_fupd f r))
  (r g f.
     ring.ring_RN_fupd f (ring.ring_R0_fupd g r) =
     ring.ring_R0_fupd g (ring.ring_RN_fupd f r))
  (r g f.
     ring.ring_RN_fupd f (ring.ring_R1_fupd g r) =
     ring.ring_R1_fupd g (ring.ring_RN_fupd f r))
  (r g f.
     ring.ring_RN_fupd f (ring.ring_RP_fupd g r) =
     ring.ring_RP_fupd g (ring.ring_RN_fupd f r))
  r g f.
    ring.ring_RN_fupd f (ring.ring_RM_fupd g r) =
    ring.ring_RM_fupd g (ring.ring_RN_fupd f r)

((g f.
      ring.ring_R0_fupd f ring.ring_R0_fupd g =
      ring.ring_R0_fupd (f g))
   h g f.
     ring.ring_R0_fupd f (ring.ring_R0_fupd g h) =
     ring.ring_R0_fupd (f g) h)
  ((g f.
      ring.ring_R1_fupd f ring.ring_R1_fupd g =
      ring.ring_R1_fupd (f g))
   h g f.
     ring.ring_R1_fupd f (ring.ring_R1_fupd g h) =
     ring.ring_R1_fupd (f g) h)
  ((g f.
      ring.ring_RP_fupd f ring.ring_RP_fupd g =
      ring.ring_RP_fupd (f g))
   h g f.
     ring.ring_RP_fupd f (ring.ring_RP_fupd g h) =
     ring.ring_RP_fupd (f g) h)
  ((g f.
      ring.ring_RM_fupd f ring.ring_RM_fupd g =
      ring.ring_RM_fupd (f g))
   h g f.
     ring.ring_RM_fupd f (ring.ring_RM_fupd g h) =
     ring.ring_RM_fupd (f g) h)
  (g f.
     ring.ring_RN_fupd f ring.ring_RN_fupd g =
     ring.ring_RN_fupd (f g))
  h g f.
    ring.ring_RN_fupd f (ring.ring_RN_fupd g h) =
    ring.ring_RN_fupd (f g) h

(s f.
     semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SR1_fupd f s) =
     semi_ring.semi_ring_SR0 s)
  (s f.
     semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SRP_fupd f s) =
     semi_ring.semi_ring_SR0 s)
  (s f.
     semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SRM_fupd f s) =
     semi_ring.semi_ring_SR0 s)
  (s f.
     semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SR0_fupd f s) =
     semi_ring.semi_ring_SR1 s)
  (s f.
     semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SRP_fupd f s) =
     semi_ring.semi_ring_SR1 s)
  (s f.
     semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SRM_fupd f s) =
     semi_ring.semi_ring_SR1 s)
  (s f.
     semi_ring.semi_ring_SRP (semi_ring.semi_ring_SR0_fupd f s) =
     semi_ring.semi_ring_SRP s)
  (s f.
     semi_ring.semi_ring_SRP (semi_ring.semi_ring_SR1_fupd f s) =
     semi_ring.semi_ring_SRP s)
  (s f.
     semi_ring.semi_ring_SRP (semi_ring.semi_ring_SRM_fupd f s) =
     semi_ring.semi_ring_SRP s)
  (s f.
     semi_ring.semi_ring_SRM (semi_ring.semi_ring_SR0_fupd f s) =
     semi_ring.semi_ring_SRM s)
  (s f.
     semi_ring.semi_ring_SRM (semi_ring.semi_ring_SR1_fupd f s) =
     semi_ring.semi_ring_SRM s)
  (s f.
     semi_ring.semi_ring_SRM (semi_ring.semi_ring_SRP_fupd f s) =
     semi_ring.semi_ring_SRM s)
  (s f.
     semi_ring.semi_ring_SR0 (semi_ring.semi_ring_SR0_fupd f s) =
     f (semi_ring.semi_ring_SR0 s))
  (s f.
     semi_ring.semi_ring_SR1 (semi_ring.semi_ring_SR1_fupd f s) =
     f (semi_ring.semi_ring_SR1 s))
  (s f.
     semi_ring.semi_ring_SRP (semi_ring.semi_ring_SRP_fupd f s) =
     f (semi_ring.semi_ring_SRP s))
  s f.
    semi_ring.semi_ring_SRM (semi_ring.semi_ring_SRM_fupd f s) =
    f (semi_ring.semi_ring_SRM s)

P.
    (sr c1 l1 t1 c2 l2 t2.
       P sr t1 t2 P sr t1 (canonical.Cons_monom c2 l2 t2)
       P sr (canonical.Cons_monom c1 l1 t1) t2
       P sr (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_monom c2 l2 t2))
    (sr c1 l1 t1 l2 t2.
       P sr t1 t2 P sr t1 (canonical.Cons_varlist l2 t2)
       P sr (canonical.Cons_monom c1 l1 t1) t2
       P sr (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_varlist l2 t2))
    (sr l1 t1 c2 l2 t2.
       P sr t1 t2 P sr t1 (canonical.Cons_monom c2 l2 t2)
       P sr (canonical.Cons_varlist l1 t1) t2
       P sr (canonical.Cons_varlist l1 t1)
         (canonical.Cons_monom c2 l2 t2))
    (sr l1 t1 l2 t2.
       P sr t1 t2 P sr t1 (canonical.Cons_varlist l2 t2)
       P sr (canonical.Cons_varlist l1 t1) t2
       P sr (canonical.Cons_varlist l1 t1)
         (canonical.Cons_varlist l2 t2))
    (sr s1. P sr s1 canonical.Nil_monom)
    (sr v4 v5 v6.
       P sr canonical.Nil_monom (canonical.Cons_monom v4 v5 v6))
    (sr v7 v8. P sr canonical.Nil_monom (canonical.Cons_varlist v7 v8))
    v v1 v2. P v v1 v2

((g f.
      semi_ring.semi_ring_SR1_fupd f semi_ring.semi_ring_SR0_fupd g =
      semi_ring.semi_ring_SR0_fupd g semi_ring.semi_ring_SR1_fupd f)
   h g f.
     semi_ring.semi_ring_SR1_fupd f
     (semi_ring.semi_ring_SR0_fupd g h) =
     semi_ring.semi_ring_SR0_fupd g
     (semi_ring.semi_ring_SR1_fupd f h))
  ((g f.
      semi_ring.semi_ring_SRP_fupd f semi_ring.semi_ring_SR0_fupd g =
      semi_ring.semi_ring_SR0_fupd g semi_ring.semi_ring_SRP_fupd f)
   h g f.
     semi_ring.semi_ring_SRP_fupd f
     (semi_ring.semi_ring_SR0_fupd g h) =
     semi_ring.semi_ring_SR0_fupd g
     (semi_ring.semi_ring_SRP_fupd f h))
  ((g f.
      semi_ring.semi_ring_SRP_fupd f semi_ring.semi_ring_SR1_fupd g =
      semi_ring.semi_ring_SR1_fupd g semi_ring.semi_ring_SRP_fupd f)
   h g f.
     semi_ring.semi_ring_SRP_fupd f
     (semi_ring.semi_ring_SR1_fupd g h) =
     semi_ring.semi_ring_SR1_fupd g
     (semi_ring.semi_ring_SRP_fupd f h))
  ((g f.
      semi_ring.semi_ring_SRM_fupd f semi_ring.semi_ring_SR0_fupd g =
      semi_ring.semi_ring_SR0_fupd g semi_ring.semi_ring_SRM_fupd f)
   h g f.
     semi_ring.semi_ring_SRM_fupd f
     (semi_ring.semi_ring_SR0_fupd g h) =
     semi_ring.semi_ring_SR0_fupd g
     (semi_ring.semi_ring_SRM_fupd f h))
  ((g f.
      semi_ring.semi_ring_SRM_fupd f semi_ring.semi_ring_SR1_fupd g =
      semi_ring.semi_ring_SR1_fupd g semi_ring.semi_ring_SRM_fupd f)
   h g f.
     semi_ring.semi_ring_SRM_fupd f
     (semi_ring.semi_ring_SR1_fupd g h) =
     semi_ring.semi_ring_SR1_fupd g
     (semi_ring.semi_ring_SRM_fupd f h))
  (g f.
     semi_ring.semi_ring_SRM_fupd f semi_ring.semi_ring_SRP_fupd g =
     semi_ring.semi_ring_SRP_fupd g semi_ring.semi_ring_SRM_fupd f)
  h g f.
    semi_ring.semi_ring_SRM_fupd f (semi_ring.semi_ring_SRP_fupd g h) =
    semi_ring.semi_ring_SRP_fupd g (semi_ring.semi_ring_SRM_fupd f h)

r.
    (t2 t1 l2 l1 c2 c1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_monom c2 l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r c1 c2) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_monom c2 l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_monom c1 l1 t1) t2)))
    (t2 t1 l2 l1 c1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_varlist l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_varlist l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_monom c1 l1 t1) t2)))
    (t2 t1 l2 l1 c2.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
         (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_monom c2 l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_monom c2 l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_varlist l1 t1) t2)))
    (t2 t1 l2 l1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
         (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_varlist l2 t2)))
         (canonical.Cons_monom
            (ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_varlist l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_varlist l1 t1) t2)))
    (s1. ringNorm.r_canonical_sum_merge r s1 canonical.Nil_monom = s1)
    (v6 v5 v4.
       ringNorm.r_canonical_sum_merge r canonical.Nil_monom
         (canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6)
    v8 v7.
      ringNorm.r_canonical_sum_merge r canonical.Nil_monom
        (canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8

(t2 t1 sr l2 l1 c2 c1.
     canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
       (canonical.Cons_monom c2 l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_monom c1 l1
          (canonical.canonical_sum_merge sr t1
             (canonical.Cons_monom c2 l2 t2)))
       (canonical.Cons_monom (semi_ring.semi_ring_SRP sr c1 c2) l1
          (canonical.canonical_sum_merge sr t1 t2))
       (canonical.Cons_monom c2 l2
          (canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
             t2)))
  (t2 t1 sr l2 l1 c1.
     canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
       (canonical.Cons_varlist l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_monom c1 l1
          (canonical.canonical_sum_merge sr t1
             (canonical.Cons_varlist l2 t2)))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr c1 (semi_ring.semi_ring_SR1 sr)) l1
          (canonical.canonical_sum_merge sr t1 t2))
       (canonical.Cons_varlist l2
          (canonical.canonical_sum_merge sr (canonical.Cons_monom c1 l1 t1)
             t2)))
  (t2 t1 sr l2 l1 c2.
     canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
       (canonical.Cons_monom c2 l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_varlist l1
          (canonical.canonical_sum_merge sr t1
             (canonical.Cons_monom c2 l2 t2)))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr) c2) l1
          (canonical.canonical_sum_merge sr t1 t2))
       (canonical.Cons_monom c2 l2
          (canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
             t2)))
  (t2 t1 sr l2 l1.
     canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
       (canonical.Cons_varlist l2 t2) =
     prelim.compare (prelim.list_compare quote.index_compare l1 l2)
       (canonical.Cons_varlist l1
          (canonical.canonical_sum_merge sr t1
             (canonical.Cons_varlist l2 t2)))
       (canonical.Cons_monom
          (semi_ring.semi_ring_SRP sr (semi_ring.semi_ring_SR1 sr)
             (semi_ring.semi_ring_SR1 sr)) l1
          (canonical.canonical_sum_merge sr t1 t2))
       (canonical.Cons_varlist l2
          (canonical.canonical_sum_merge sr (canonical.Cons_varlist l1 t1)
             t2)))
  (sr s1. canonical.canonical_sum_merge sr s1 canonical.Nil_monom = s1)
  (v6 v5 v4 sr.
     canonical.canonical_sum_merge sr canonical.Nil_monom
       (canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6)
  v8 v7 sr.
    canonical.canonical_sum_merge sr canonical.Nil_monom
      (canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8

(r f. ring.ring_R0 (ring.ring_R1_fupd f r) = ring.ring_R0 r)
  (r f. ring.ring_R0 (ring.ring_RP_fupd f r) = ring.ring_R0 r)
  (r f. ring.ring_R0 (ring.ring_RM_fupd f r) = ring.ring_R0 r)
  (r f. ring.ring_R0 (ring.ring_RN_fupd f r) = ring.ring_R0 r)
  (r f. ring.ring_R1 (ring.ring_R0_fupd f r) = ring.ring_R1 r)
  (r f. ring.ring_R1 (ring.ring_RP_fupd f r) = ring.ring_R1 r)
  (r f. ring.ring_R1 (ring.ring_RM_fupd f r) = ring.ring_R1 r)
  (r f. ring.ring_R1 (ring.ring_RN_fupd f r) = ring.ring_R1 r)
  (r f. ring.ring_RP (ring.ring_R0_fupd f r) = ring.ring_RP r)
  (r f. ring.ring_RP (ring.ring_R1_fupd f r) = ring.ring_RP r)
  (r f. ring.ring_RP (ring.ring_RM_fupd f r) = ring.ring_RP r)
  (r f. ring.ring_RP (ring.ring_RN_fupd f r) = ring.ring_RP r)
  (r f. ring.ring_RM (ring.ring_R0_fupd f r) = ring.ring_RM r)
  (r f. ring.ring_RM (ring.ring_R1_fupd f r) = ring.ring_RM r)
  (r f. ring.ring_RM (ring.ring_RP_fupd f r) = ring.ring_RM r)
  (r f. ring.ring_RM (ring.ring_RN_fupd f r) = ring.ring_RM r)
  (r f. ring.ring_RN (ring.ring_R0_fupd f r) = ring.ring_RN r)
  (r f. ring.ring_RN (ring.ring_R1_fupd f r) = ring.ring_RN r)
  (r f. ring.ring_RN (ring.ring_RP_fupd f r) = ring.ring_RN r)
  (r f. ring.ring_RN (ring.ring_RM_fupd f r) = ring.ring_RN r)
  (r f. ring.ring_R0 (ring.ring_R0_fupd f r) = f (ring.ring_R0 r))
  (r f. ring.ring_R1 (ring.ring_R1_fupd f r) = f (ring.ring_R1 r))
  (r f. ring.ring_RP (ring.ring_RP_fupd f r) = f (ring.ring_RP r))
  (r f. ring.ring_RM (ring.ring_RM_fupd f r) = f (ring.ring_RM r))
  r f. ring.ring_RN (ring.ring_RN_fupd f r) = f (ring.ring_RN r)

((g f.
      ring.ring_R1_fupd f ring.ring_R0_fupd g =
      ring.ring_R0_fupd g ring.ring_R1_fupd f)
   h g f.
     ring.ring_R1_fupd f (ring.ring_R0_fupd g h) =
     ring.ring_R0_fupd g (ring.ring_R1_fupd f h))
  ((g f.
      ring.ring_RP_fupd f ring.ring_R0_fupd g =
      ring.ring_R0_fupd g ring.ring_RP_fupd f)
   h g f.
     ring.ring_RP_fupd f (ring.ring_R0_fupd g h) =
     ring.ring_R0_fupd g (ring.ring_RP_fupd f h))
  ((g f.
      ring.ring_RP_fupd f ring.ring_R1_fupd g =
      ring.ring_R1_fupd g ring.ring_RP_fupd f)
   h g f.
     ring.ring_RP_fupd f (ring.ring_R1_fupd g h) =
     ring.ring_R1_fupd g (ring.ring_RP_fupd f h))
  ((g f.
      ring.ring_RM_fupd f ring.ring_R0_fupd g =
      ring.ring_R0_fupd g ring.ring_RM_fupd f)
   h g f.
     ring.ring_RM_fupd f (ring.ring_R0_fupd g h) =
     ring.ring_R0_fupd g (ring.ring_RM_fupd f h))
  ((g f.
      ring.ring_RM_fupd f ring.ring_R1_fupd g =
      ring.ring_R1_fupd g ring.ring_RM_fupd f)
   h g f.
     ring.ring_RM_fupd f (ring.ring_R1_fupd g h) =
     ring.ring_R1_fupd g (ring.ring_RM_fupd f h))
  ((g f.
      ring.ring_RM_fupd f ring.ring_RP_fupd g =
      ring.ring_RP_fupd g ring.ring_RM_fupd f)
   h g f.
     ring.ring_RM_fupd f (ring.ring_RP_fupd g h) =
     ring.ring_RP_fupd g (ring.ring_RM_fupd f h))
  ((g f.
      ring.ring_RN_fupd f ring.ring_R0_fupd g =
      ring.ring_R0_fupd g ring.ring_RN_fupd f)
   h g f.
     ring.ring_RN_fupd f (ring.ring_R0_fupd g h) =
     ring.ring_R0_fupd g (ring.ring_RN_fupd f h))
  ((g f.
      ring.ring_RN_fupd f ring.ring_R1_fupd g =
      ring.ring_R1_fupd g ring.ring_RN_fupd f)
   h g f.
     ring.ring_RN_fupd f (ring.ring_R1_fupd g h) =
     ring.ring_R1_fupd g (ring.ring_RN_fupd f h))
  ((g f.
      ring.ring_RN_fupd f ring.ring_RP_fupd g =
      ring.ring_RP_fupd g ring.ring_RN_fupd f)
   h g f.
     ring.ring_RN_fupd f (ring.ring_RP_fupd g h) =
     ring.ring_RP_fupd g (ring.ring_RN_fupd f h))
  (g f.
     ring.ring_RN_fupd f ring.ring_RM_fupd g =
     ring.ring_RM_fupd g ring.ring_RN_fupd f)
  h g f.
    ring.ring_RN_fupd f (ring.ring_RM_fupd g h) =
    ring.ring_RM_fupd g (ring.ring_RN_fupd f h)

((n. 0 + n = n) (n. n + 0 = n) (n m. n + m = numeral.iZ (n + m))
   (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
   (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
   (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
   (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
   (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
   prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
   (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
   (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
   (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
   (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
   (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
   (n. odd n odd n) (n. even n even n) ¬odd 0 even 0)
  (n m.
     (0 = bit1 n ) (bit1 n = 0 ) (0 = arithmetic.BIT2 n )
     (arithmetic.BIT2 n = 0 ) (bit1 n = arithmetic.BIT2 m )
     (arithmetic.BIT2 n = bit1 m ) (bit1 n = bit1 m n = m)
     (arithmetic.BIT2 n = arithmetic.BIT2 m n = m))
  (suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
   n. suc (arithmetic.BIT2 n) = bit1 (suc n))
  (numeral.iiSUC 0 = arithmetic.BIT2 0
   numeral.iiSUC (bit1 n) = bit1 (suc n)
   numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n))
  (n m.
     numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
     numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
     numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
     numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
     numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
     arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
     suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
     suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
     suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
     suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
     bit1 (numeral.iiSUC (n + m))
     numeral.iiSUC (0 + n) = numeral.iiSUC n
     numeral.iiSUC (n + 0) = numeral.iiSUC n
     numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
     numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
     bit1 (numeral.iiSUC (n + m))
     numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
     bit1 (numeral.iiSUC (n + m))
     numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
     arithmetic.BIT2 (numeral.iiSUC (n + m)))
  (n m.
     0 * n = 0 n * 0 = 0
     bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m)
     arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m)))
  (n.
     numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
     numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
     numeral.iDUB 0 = 0) (0 = 0 ) (0 = 0 )

semi_ring.is_semi_ring (semi_ring.recordtype.semi_ring 0 1 (+) (*))
  (vm p.
     numRing.num_interp_sp vm p =
     numRing.num_interp_cs vm (numRing.num_spolynom_simplify p))
  (((vm c. numRing.num_interp_sp vm (canonical.SPconst c) = c)
    (vm i.
       numRing.num_interp_sp vm (canonical.SPvar i) =
       quote.varmap_find i vm)
    (vm p1 p2.
       numRing.num_interp_sp vm (canonical.SPplus p1 p2) =
       numRing.num_interp_sp vm p1 + numRing.num_interp_sp vm p2)
    vm p1 p2.
      numRing.num_interp_sp vm (canonical.SPmult p1 p2) =
      numRing.num_interp_sp vm p1 * numRing.num_interp_sp vm p2)
   (x v2 v1.
      quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x)
   (x v2 v1 i1.
      quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
      quote.varmap_find i1 v2)
   (x v2 v1 i1.
      quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
      quote.varmap_find i1 v1)
   i. quote.varmap_find i quote.Empty_vm = select x. )
  ((t2 t1 l2 l1 c2 c1.
      numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
        (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1
           (numRing.num_canonical_sum_merge t1
              (canonical.Cons_monom c2 l2 t2)))
        (canonical.Cons_monom (c1 + c2) l1
           (numRing.num_canonical_sum_merge t1 t2))
        (canonical.Cons_monom c2 l2
           (numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
              t2)))
   (t2 t1 l2 l1 c1.
      numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
        (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1
           (numRing.num_canonical_sum_merge t1
              (canonical.Cons_varlist l2 t2)))
        (canonical.Cons_monom (c1 + 1) l1
           (numRing.num_canonical_sum_merge t1 t2))
        (canonical.Cons_varlist l2
           (numRing.num_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
              t2)))
   (t2 t1 l2 l1 c2.
      numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
        (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1
           (numRing.num_canonical_sum_merge t1
              (canonical.Cons_monom c2 l2 t2)))
        (canonical.Cons_monom (1 + c2) l1
           (numRing.num_canonical_sum_merge t1 t2))
        (canonical.Cons_monom c2 l2
           (numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
              t2)))
   (t2 t1 l2 l1.
      numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
        (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1
           (numRing.num_canonical_sum_merge t1
              (canonical.Cons_varlist l2 t2)))
        (canonical.Cons_monom (1 + 1) l1
           (numRing.num_canonical_sum_merge t1 t2))
        (canonical.Cons_varlist l2
           (numRing.num_canonical_sum_merge (canonical.Cons_varlist l1 t1)
              t2)))
   (s1. numRing.num_canonical_sum_merge s1 canonical.Nil_monom = s1)
   (v6 v5 v4.
      numRing.num_canonical_sum_merge canonical.Nil_monom
        (canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6)
   v8 v7.
     numRing.num_canonical_sum_merge canonical.Nil_monom
       (canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8)
  ((t2 l2 l1 c2 c1.
      numRing.num_monom_insert c1 l1 (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
        (canonical.Cons_monom (c1 + c2) l1 t2)
        (canonical.Cons_monom c2 l2 (numRing.num_monom_insert c1 l1 t2)))
   (t2 l2 l1 c1.
      numRing.num_monom_insert c1 l1 (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
        (canonical.Cons_monom (c1 + 1) l1 t2)
        (canonical.Cons_varlist l2 (numRing.num_monom_insert c1 l1 t2)))
   l1 c1.
     numRing.num_monom_insert c1 l1 canonical.Nil_monom =
     canonical.Cons_monom c1 l1 canonical.Nil_monom)
  ((t2 l2 l1 c2.
      numRing.num_varlist_insert l1 (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
        (canonical.Cons_monom (1 + c2) l1 t2)
        (canonical.Cons_monom c2 l2 (numRing.num_varlist_insert l1 t2)))
   (t2 l2 l1.
      numRing.num_varlist_insert l1 (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
        (canonical.Cons_monom (1 + 1) l1 t2)
        (canonical.Cons_varlist l2 (numRing.num_varlist_insert l1 t2)))
   l1.
     numRing.num_varlist_insert l1 canonical.Nil_monom =
     canonical.Cons_varlist l1 canonical.Nil_monom)
  ((c0 c l t.
      numRing.num_canonical_sum_scalar c0 (canonical.Cons_monom c l t) =
      canonical.Cons_monom (c0 * c) l
        (numRing.num_canonical_sum_scalar c0 t))
   (c0 l t.
      numRing.num_canonical_sum_scalar c0 (canonical.Cons_varlist l t) =
      canonical.Cons_monom c0 l (numRing.num_canonical_sum_scalar c0 t))
   c0.
     numRing.num_canonical_sum_scalar c0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((l0 c l t.
      numRing.num_canonical_sum_scalar2 l0 (canonical.Cons_monom c l t) =
      numRing.num_monom_insert c (prelim.list_merge quote.index_lt l0 l)
        (numRing.num_canonical_sum_scalar2 l0 t))
   (l0 l t.
      numRing.num_canonical_sum_scalar2 l0 (canonical.Cons_varlist l t) =
      numRing.num_varlist_insert (prelim.list_merge quote.index_lt l0 l)
        (numRing.num_canonical_sum_scalar2 l0 t))
   l0.
     numRing.num_canonical_sum_scalar2 l0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((c0 l0 c l t.
      numRing.num_canonical_sum_scalar3 c0 l0
        (canonical.Cons_monom c l t) =
      numRing.num_monom_insert (c0 * c)
        (prelim.list_merge quote.index_lt l0 l)
        (numRing.num_canonical_sum_scalar3 c0 l0 t))
   (c0 l0 l t.
      numRing.num_canonical_sum_scalar3 c0 l0
        (canonical.Cons_varlist l t) =
      numRing.num_monom_insert c0 (prelim.list_merge quote.index_lt l0 l)
        (numRing.num_canonical_sum_scalar3 c0 l0 t))
   c0 l0.
     numRing.num_canonical_sum_scalar3 c0 l0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((c1 l1 t1 s2.
      numRing.num_canonical_sum_prod (canonical.Cons_monom c1 l1 t1) s2 =
      numRing.num_canonical_sum_merge
        (numRing.num_canonical_sum_scalar3 c1 l1 s2)
        (numRing.num_canonical_sum_prod t1 s2))
   (l1 t1 s2.
      numRing.num_canonical_sum_prod (canonical.Cons_varlist l1 t1) s2 =
      numRing.num_canonical_sum_merge
        (numRing.num_canonical_sum_scalar2 l1 s2)
        (numRing.num_canonical_sum_prod t1 s2))
   s2.
     numRing.num_canonical_sum_prod canonical.Nil_monom s2 =
     canonical.Nil_monom)
  ((c l t.
      numRing.num_canonical_sum_simplify (canonical.Cons_monom c l t) =
      if c = 0 then numRing.num_canonical_sum_simplify t
      else if c = 1 then
        canonical.Cons_varlist l (numRing.num_canonical_sum_simplify t)
      else
        canonical.Cons_monom c l (numRing.num_canonical_sum_simplify t))
   (l t.
      numRing.num_canonical_sum_simplify (canonical.Cons_varlist l t) =
      canonical.Cons_varlist l (numRing.num_canonical_sum_simplify t))
   numRing.num_canonical_sum_simplify canonical.Nil_monom =
   canonical.Nil_monom)
  ((vm x. numRing.num_ivl_aux vm x [] = quote.varmap_find x vm)
   vm x x' t'.
     numRing.num_ivl_aux vm x (x' :: t') =
     quote.varmap_find x vm * numRing.num_ivl_aux vm x' t')
  ((vm. numRing.num_interp_vl vm [] = 1)
   vm x t.
     numRing.num_interp_vl vm (x :: t) = numRing.num_ivl_aux vm x t)
  ((vm c. numRing.num_interp_m vm c [] = c)
   vm c x t.
     numRing.num_interp_m vm c (x :: t) = c * numRing.num_ivl_aux vm x t)
  ((vm a. numRing.num_ics_aux vm a canonical.Nil_monom = a)
   (vm a l t.
      numRing.num_ics_aux vm a (canonical.Cons_varlist l t) =
      a + numRing.num_ics_aux vm (numRing.num_interp_vl vm l) t)
   vm a c l t.
     numRing.num_ics_aux vm a (canonical.Cons_monom c l t) =
     a + numRing.num_ics_aux vm (numRing.num_interp_m vm c l) t)
  ((vm. numRing.num_interp_cs vm canonical.Nil_monom = 0)
   (vm l t.
      numRing.num_interp_cs vm (canonical.Cons_varlist l t) =
      numRing.num_ics_aux vm (numRing.num_interp_vl vm l) t)
   vm c l t.
     numRing.num_interp_cs vm (canonical.Cons_monom c l t) =
     numRing.num_ics_aux vm (numRing.num_interp_m vm c l) t)
  ((i.
      numRing.num_spolynom_normalize (canonical.SPvar i) =
      canonical.Cons_varlist (i :: []) canonical.Nil_monom)
   (c.
      numRing.num_spolynom_normalize (canonical.SPconst c) =
      canonical.Cons_monom c [] canonical.Nil_monom)
   (l r.
      numRing.num_spolynom_normalize (canonical.SPplus l r) =
      numRing.num_canonical_sum_merge (numRing.num_spolynom_normalize l)
        (numRing.num_spolynom_normalize r))
   l r.
     numRing.num_spolynom_normalize (canonical.SPmult l r) =
     numRing.num_canonical_sum_prod (numRing.num_spolynom_normalize l)
       (numRing.num_spolynom_normalize r))
  x.
    numRing.num_spolynom_simplify x =
    numRing.num_canonical_sum_simplify (numRing.num_spolynom_normalize x)

External Type Operators

External Constants

Assumptions

wellFounded (<)

t. t

n. 0 n

bool.LET = λf x. f x

x. id x = x

t. t ¬t

(¬) = λt. t

() = λP. P ((select) P)

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

x. x = x

t. ¬¬t t

n. n * 0 = 0

n. n + 0 = n

A. A ¬A

t. ¬t t

t. (t ) ¬t

x y. const x y = x

() = λp q. p q p

t. t t

n. suc n = 1 + n

x. (fst x, snd x) = x

x y. fst (x, y) = x

x y. snd (x, y) = y

a1 a0. ¬([] = a0 :: a1)

P x. P x P ((select) P)

pair.pair_CASE (x, y) f = f x y

x. q r. x = (q, r)

x y. x = y y = x

A B. A B B A

m n. m * n = n * m

m n. m + n = n + m

R f. wellFounded R wellFounded (relation.inv_image R f)

(¬A ) (A )

m n. m < n suc m n

m n. ¬(m < n) n m

() = λp q. (λf. f p q) = λf. f

P. ¬(m. P m) m. ¬P m

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

f g x. (f g) x = f (g x)

R f. relation.inv_image R f = λx y. R (f x) (f y)

l. l = [] h t. l = h :: t

P a. (a0''. a0'' = a P a0'') P a

P t. (x. x = t P x) () P

f x y. pair.UNCURRY f (x, y) = f x y

() = λt1 t2. t. (t1 t) (t2 t) t

t1 t2. (t1 t2) (t2 t1) (t1 t2)

m n. m = n m n n m

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

P Q. P (x. Q x) x. P Q x

P Q. (x. P x Q) (x. P x) Q

P Q. (x. P x) Q x. P x Q

¬(A B) (A ) ¬B

(x y) (z w) x z y w

(x y) (z w) x z y w

x y z. x = y y = z x = z

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. m + p = n + p m = n

m n p. m + p < n + p m < n

m n p. m + n m + p n p

m n p. m n n p m p

f g h. f (g h) = f g h

(x. P x Q x) (x. P x) x. Q x

t1 t2. (if then t1 else t2) = t1 (if then t1 else t2) = t2

t1 t2. (t1 t2) t1 t2 ¬t1 ¬t2

n m. arithmetic.- n m = if m < n then numeral.iSUB n m else 0

(t. ¬¬t t) (¬ ) (¬ )

m n. ¬(m = n) suc m n suc n m

m n p. (m + n) * p = m * p + n * p

f R y z. R y z relation.RESTRICT f R z y = f y

P Q. (x. P x Q x) (x. P x) x. Q x

P. P [] (t. P t h. P (h :: t)) l1. P l1

a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' a0 = a0' a1 = a1'

Fn. f. c i r. f (ind_type.CONSTR c i r) = Fn c i r (λn. f (r n))

numeral.iiSUC 0 = arithmetic.BIT2 0
  numeral.iiSUC (bit1 n) = bit1 (suc n)
  numeral.iiSUC (arithmetic.BIT2 n) = arithmetic.BIT2 (suc n)

n.
    numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
    numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
    numeral.iDUB 0 = 0

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

f0 f1. fn. fn [] = f0 a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)

R. wellFounded R P. (x. (y. R y x P y) P x) x. P x

(a f. ind_type.FCONS a f 0 = a)
  a f n. ind_type.FCONS a f (suc n) = f n

x x' y y'. (x x') (x' (y y')) (x y x' y')

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
  n. suc (arithmetic.BIT2 n) = bit1 (suc n)

P (arithmetic.- a b) d. (b = a + d P 0) (a = b + d P d)

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

M R f.
    f = relation.WFREC R M wellFounded R
    x. f x = M (relation.RESTRICT f R x) x

bool.TYPE_DEFINITION =
  λP rep.
    (x' x''. rep x' = rep x'' x' = x'') x. P x x'. x = rep x'

(v f. list.list_CASE [] v f = v)
  a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

P.
    (rep. bool.TYPE_DEFINITION P rep)
    rep abs. (a. abs (rep a) = a) r. P r rep (abs r) = r

(f. list.list_size f [] = 0)
  f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

P Q x x' y y'.
    (P Q) (Q x = x') (¬Q y = y')
    (if P then x else y) = if Q then x' else y'

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

n m.
    0 * n = 0 n * 0 = 0
    bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m)
    arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))

m n.
    0 * m = 0 m * 0 = 0 1 * m = m m * 1 = m suc m * n = m * n + n
    m * suc n = m + m * n

n m.
    (0 n ) (bit1 n 0 ) (arithmetic.BIT2 n 0 )
    (bit1 n bit1 m n m) (bit1 n arithmetic.BIT2 m n m)
    (arithmetic.BIT2 n bit1 m ¬(m n))
    (arithmetic.BIT2 n arithmetic.BIT2 m n m)

n m.
    (0 < bit1 n ) (0 < arithmetic.BIT2 n ) (n < 0 )
    (bit1 n < bit1 m n < m)
    (arithmetic.BIT2 n < arithmetic.BIT2 m n < m)
    (bit1 n < arithmetic.BIT2 m ¬(m < n))
    (arithmetic.BIT2 n < bit1 m n < m)

n m.
    (0 = bit1 n ) (bit1 n = 0 ) (0 = arithmetic.BIT2 n )
    (arithmetic.BIT2 n = 0 ) (bit1 n = arithmetic.BIT2 m )
    (arithmetic.BIT2 n = bit1 m ) (bit1 n = bit1 m n = m)
    (arithmetic.BIT2 n = arithmetic.BIT2 m n = m)

b n m.
    numeral.iSUB b 0 x = 0 numeral.iSUB n 0 = n
    numeral.iSUB (bit1 n) 0 = numeral.iDUB n
    numeral.iSUB (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (bit1 m) = bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) 0 = bit1 n
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)

n m.
    numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
    numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
    numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
    suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
    suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (0 + n) = numeral.iiSUC n
    numeral.iiSUC (n + 0) = numeral.iiSUC n
    numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (numeral.iiSUC (n + m))

(n. 0 + n = n) (n. n + 0 = n) (n m. n + m = numeral.iZ (n + m))
  (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
  (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
  (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
  (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
  (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
  prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
  (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
  (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
  (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
  (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
  (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
  (n. odd n odd n) (n. even n even n) ¬odd 0 even 0