Theory EVAL_numRing

⊢ num_canonical_sum_merge =
  EVAL_canonical$canonical_sum_merge (semi_ring 0 1 $+ $* )

⊢ num_canonical_sum_prod =
  EVAL_canonical$canonical_sum_prod (semi_ring 0 1 $+ $* )

⊢ num_canonical_sum_scalar2 =
  EVAL_canonical$canonical_sum_scalar2 (semi_ring 0 1 $+ $* )

⊢ num_canonical_sum_scalar3 =
  EVAL_canonical$canonical_sum_scalar3 (semi_ring 0 1 $+ $* )

⊢ num_canonical_sum_scalar =
  EVAL_canonical$canonical_sum_scalar (semi_ring 0 1 $+ $* )

⊢ num_canonical_sum_simplify =
  EVAL_canonical$canonical_sum_simplify (semi_ring 0 1 $+ $* )

⊢ num_ics_aux = EVAL_canonical$ics_aux (semi_ring 0 1 $+ $* )

⊢ num_interp_cs = EVAL_canonical$interp_cs (semi_ring 0 1 $+ $* )

⊢ num_interp_m = EVAL_canonical$interp_m (semi_ring 0 1 $+ $* )

⊢ num_interp_sp = EVAL_canonical$interp_sp (semi_ring 0 1 $+ $* )

⊢ num_interp_vl = EVAL_canonical$interp_vl (semi_ring 0 1 $+ $* )

⊢ num_ivl_aux = EVAL_canonical$ivl_aux (semi_ring 0 1 $+ $* )

⊢ num_monom_insert = EVAL_canonical$monom_insert (semi_ring 0 1 $+ $* )

⊢ num_spolynom_normalize =
  EVAL_canonical$spolynom_normalize (semi_ring 0 1 $+ $* )

⊢ num_spolynom_simplify =
  EVAL_canonical$spolynom_simplify (semi_ring 0 1 $+ $* )

⊢ num_varlist_insert = EVAL_canonical$varlist_insert (semi_ring 0 1 $+ $* )

⊢ ((∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧
   (∀n m. NUMERAL n + NUMERAL m = NUMERAL (numeral$iZ (n + m))) ∧
   (∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧
   (∀n m. NUMERAL n * NUMERAL m = NUMERAL (n * m)) ∧ (∀n. 0 − n = 0) ∧
   (∀n. n − 0 = n) ∧ (∀n m. NUMERAL n − NUMERAL m = NUMERAL (n − m)) ∧
   (∀n. 0 ** NUMERAL (BIT1 n) = 0) ∧ (∀n. 0 ** NUMERAL (BIT2 n) = 0) ∧
   (∀n. n ** 0 = 1) ∧ (∀n m. NUMERAL n ** NUMERAL m = NUMERAL (n ** m)) ∧
   SUC 0 = 1 ∧ (∀n. SUC (NUMERAL n) = NUMERAL (SUC n)) ∧ PRE 0 = 0 ∧
   (∀n. PRE (NUMERAL n) = NUMERAL (PRE n)) ∧
   (∀n. NUMERAL n = 0 ⇔ n = ZERO) ∧ (∀n. 0 = NUMERAL n ⇔ n = ZERO) ∧
   (∀n m. NUMERAL n = NUMERAL m ⇔ n = m) ∧ (∀n. n < 0 ⇔ F) ∧
   (∀n. 0 < NUMERAL n ⇔ ZERO < n) ∧ (∀n m. NUMERAL n < NUMERAL m ⇔ n < m) ∧
   (∀n. 0 > n ⇔ F) ∧ (∀n. NUMERAL n > 0 ⇔ ZERO < n) ∧
   (∀n m. NUMERAL n > NUMERAL m ⇔ m < n) ∧ (∀n. 0 ≤ n ⇔ T) ∧
   (∀n. NUMERAL n ≤ 0 ⇔ n ≤ ZERO) ∧ (∀n m. NUMERAL n ≤ NUMERAL m ⇔ n ≤ m) ∧
   (∀n. n ≥ 0 ⇔ T) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧
   (∀n m. NUMERAL n ≥ NUMERAL m ⇔ m ≤ n) ∧ (∀n. ODD (NUMERAL n) ⇔ ODD n) ∧
   (∀n. EVEN (NUMERAL n) ⇔ EVEN n) ∧ ¬ODD 0 ∧ EVEN 0) ∧
  (∀n m.
     (ZERO = BIT1 n ⇔ F) ∧ (BIT1 n = ZERO ⇔ F) ∧ (ZERO = BIT2 n ⇔ F) ∧
     (BIT2 n = ZERO ⇔ F) ∧ (BIT1 n = BIT2 m ⇔ F) ∧ (BIT2 n = BIT1 m ⇔ F) ∧
     (BIT1 n = BIT1 m ⇔ n = m) ∧ (BIT2 n = BIT2 m ⇔ n = m)) ∧
  (SUC ZERO = BIT1 ZERO ∧ (∀n. SUC (BIT1 n) = BIT2 n) ∧
   ∀n. SUC (BIT2 n) = BIT1 (SUC n)) ∧
  (numeral$iiSUC ZERO = BIT2 ZERO ∧ numeral$iiSUC (BIT1 n) = BIT1 (SUC n) ∧
   numeral$iiSUC (BIT2 n) = BIT2 (SUC n)) ∧
  (∀n m.
     numeral$iZ (ZERO + n) = n ∧ numeral$iZ (n + ZERO) = n ∧
     numeral$iZ (BIT1 n + BIT1 m) = BIT2 (numeral$iZ (n + m)) ∧
     numeral$iZ (BIT1 n + BIT2 m) = BIT1 (SUC (n + m)) ∧
     numeral$iZ (BIT2 n + BIT1 m) = BIT1 (SUC (n + m)) ∧
     numeral$iZ (BIT2 n + BIT2 m) = BIT2 (SUC (n + m)) ∧
     SUC (ZERO + n) = SUC n ∧ SUC (n + ZERO) = SUC n ∧
     SUC (BIT1 n + BIT1 m) = BIT1 (SUC (n + m)) ∧
     SUC (BIT1 n + BIT2 m) = BIT2 (SUC (n + m)) ∧
     SUC (BIT2 n + BIT1 m) = BIT2 (SUC (n + m)) ∧
     SUC (BIT2 n + BIT2 m) = BIT1 (numeral$iiSUC (n + m)) ∧
     numeral$iiSUC (ZERO + n) = numeral$iiSUC n ∧
     numeral$iiSUC (n + ZERO) = numeral$iiSUC n ∧
     numeral$iiSUC (BIT1 n + BIT1 m) = BIT2 (SUC (n + m)) ∧
     numeral$iiSUC (BIT1 n + BIT2 m) = BIT1 (numeral$iiSUC (n + m)) ∧
     numeral$iiSUC (BIT2 n + BIT1 m) = BIT1 (numeral$iiSUC (n + m)) ∧
     numeral$iiSUC (BIT2 n + BIT2 m) = BIT2 (numeral$iiSUC (n + m))) ∧
  (∀n m.
     ZERO * n = ZERO ∧ n * ZERO = ZERO ∧
     BIT1 n * m = numeral$iZ (numeral$iDUB (n * m) + m) ∧
     BIT2 n * m = numeral$iDUB (numeral$iZ (n * m + m))) ∧
  (∀n. numeral$iDUB (BIT1 n) = BIT2 (numeral$iDUB n) ∧
       numeral$iDUB (BIT2 n) = BIT2 (BIT1 n) ∧ numeral$iDUB ZERO = ZERO) ∧
  (ZERO = ZERO ⇔ T) ∧ (0 = 0 ⇔ T)

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

⊢ is_semi_ring (semi_ring 0 1 $+ $* )