|- num_canonical_sum_merge = canonical_sum_merge (semi_ring 0 1 $+ $*)
|- num_canonical_sum_prod = canonical_sum_prod (semi_ring 0 1 $+ $*)
|- num_canonical_sum_scalar2 = canonical_sum_scalar2 (semi_ring 0 1 $+ $*)
|- num_canonical_sum_scalar3 = canonical_sum_scalar3 (semi_ring 0 1 $+ $*)
|- num_canonical_sum_scalar = canonical_sum_scalar (semi_ring 0 1 $+ $*)
|- num_canonical_sum_simplify = canonical_sum_simplify (semi_ring 0 1 $+ $*)
|- num_ics_aux = ics_aux (semi_ring 0 1 $+ $*)
|- num_interp_cs = interp_cs (semi_ring 0 1 $+ $*)
|- num_interp_m = interp_m (semi_ring 0 1 $+ $*)
|- num_interp_sp = interp_sp (semi_ring 0 1 $+ $*)
|- num_interp_vl = interp_vl (semi_ring 0 1 $+ $*)
|- num_ivl_aux = ivl_aux (semi_ring 0 1 $+ $*)
|- num_monom_insert = monom_insert (semi_ring 0 1 $+ $*)
|- num_spolynom_normalize = spolynom_normalize (semi_ring 0 1 $+ $*)
|- num_spolynom_simplify = spolynom_simplify (semi_ring 0 1 $+ $*)
|- num_varlist_insert = varlist_insert (semi_ring 0 1 $+ $*)
|- ((!n. 0 + n = n) /\ (!n. n + 0 = n) /\ (!n m. NUMERAL n + NUMERAL m = 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 (NUMERAL_BIT1 n) = 0) /\ (!n. 0 ** NUMERAL (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 = ALT_ZERO)) /\ (!n. (0 = NUMERAL n) = (n = ALT_ZERO)) /\ (!n m. (NUMERAL n = NUMERAL m) = (n = m)) /\ (!n. n < 0 = F) /\ (!n. 0 < NUMERAL n = ALT_ZERO < n) /\ (!n m. NUMERAL n < NUMERAL m = n < m) /\ (!n. 0 > n = F) /\ (!n. NUMERAL n > 0 = ALT_ZERO < n) /\ (!n m. NUMERAL n > NUMERAL m = m < n) /\ (!n. 0 <= n = T) /\ (!n. NUMERAL n <= 0 = n <= ALT_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. ((ALT_ZERO = NUMERAL_BIT1 n) = F) /\ ((NUMERAL_BIT1 n = ALT_ZERO) = F) /\ ((ALT_ZERO = NUMERAL_BIT2 n) = F) /\ ((NUMERAL_BIT2 n = ALT_ZERO) = F) /\ ((NUMERAL_BIT1 n = NUMERAL_BIT2 m) = F) /\ ((NUMERAL_BIT2 n = NUMERAL_BIT1 m) = F) /\ ((NUMERAL_BIT1 n = NUMERAL_BIT1 m) = (n = m)) /\ ((NUMERAL_BIT2 n = NUMERAL_BIT2 m) = (n = m))) /\ ((SUC ALT_ZERO = NUMERAL_BIT1 ALT_ZERO) /\ (!n. SUC (NUMERAL_BIT1 n) = NUMERAL_BIT2 n) /\ !n. SUC (NUMERAL_BIT2 n) = NUMERAL_BIT1 (SUC n)) /\ ((iiSUC ALT_ZERO = NUMERAL_BIT2 ALT_ZERO) /\ (iiSUC (NUMERAL_BIT1 n) = NUMERAL_BIT1 (SUC n)) /\ (iiSUC (NUMERAL_BIT2 n) = NUMERAL_BIT2 (SUC n))) /\ (!n m. (iZ (ALT_ZERO + n) = n) /\ (iZ (n + ALT_ZERO) = n) /\ (iZ (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (iZ (n + m))) /\ (iZ (NUMERAL_BIT1 n + NUMERAL_BIT2 m) = NUMERAL_BIT1 (SUC (n + m))) /\ (iZ (NUMERAL_BIT2 n + NUMERAL_BIT1 m) = NUMERAL_BIT1 (SUC (n + m))) /\ (iZ (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (SUC (n + m))) /\ (SUC (ALT_ZERO + n) = SUC n) /\ (SUC (n + ALT_ZERO) = SUC n) /\ (SUC (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT1 (SUC (n + m))) /\ (SUC (NUMERAL_BIT1 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (SUC (n + m))) /\ (SUC (NUMERAL_BIT2 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (SUC (n + m))) /\ (SUC (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT1 (iiSUC (n + m))) /\ (iiSUC (ALT_ZERO + n) = iiSUC n) /\ (iiSUC (n + ALT_ZERO) = iiSUC n) /\ (iiSUC (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (SUC (n + m))) /\ (iiSUC (NUMERAL_BIT1 n + NUMERAL_BIT2 m) = NUMERAL_BIT1 (iiSUC (n + m))) /\ (iiSUC (NUMERAL_BIT2 n + NUMERAL_BIT1 m) = NUMERAL_BIT1 (iiSUC (n + m))) /\ (iiSUC (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (iiSUC (n + m)))) /\ (!n m. (ALT_ZERO * n = ALT_ZERO) /\ (n * ALT_ZERO = ALT_ZERO) /\ (NUMERAL_BIT1 n * m = iZ (iDUB (n * m) + m)) /\ (NUMERAL_BIT2 n * m = iDUB (iZ (n * m + m)))) /\ (!n. (iDUB (NUMERAL_BIT1 n) = NUMERAL_BIT2 (iDUB n)) /\ (iDUB (NUMERAL_BIT2 n) = NUMERAL_BIT2 (NUMERAL_BIT1 n)) /\ (iDUB ALT_ZERO = ALT_ZERO)) /\ ((ALT_ZERO = ALT_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 (SPconst c) = c) /\ (!vm i. num_interp_sp vm (SPvar i) = varmap_find i vm) /\ (!vm p1 p2. num_interp_sp vm (SPplus p1 p2) = num_interp_sp vm p1 + num_interp_sp vm p2) /\ !vm p1 p2. num_interp_sp vm (SPmult p1 p2) = num_interp_sp vm p1 * num_interp_sp vm p2) /\ (varmap_find End_idx (Node_vm x v1 v2) = x) /\ (varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) /\ (varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) /\ (varmap_find End_idx Empty_vm = @x. T) /\ (varmap_find (Right_idx v5) Empty_vm = @x. T) /\ (varmap_find (Left_idx v4) Empty_vm = @x. T)) /\ ((num_canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) = compare (list_compare index_compare l1 l2) (Cons_monom c1 l1 (num_canonical_sum_merge t1 (Cons_monom c2 l2 t2))) (Cons_monom (c1 + c2) l1 (num_canonical_sum_merge t1 t2)) (Cons_monom c2 l2 (num_canonical_sum_merge (Cons_monom c1 l1 t1) t2))) /\ (num_canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) = compare (list_compare index_compare l1 l2) (Cons_monom c1 l1 (num_canonical_sum_merge t1 (Cons_varlist l2 t2))) (Cons_monom (c1 + 1) l1 (num_canonical_sum_merge t1 t2)) (Cons_varlist l2 (num_canonical_sum_merge (Cons_monom c1 l1 t1) t2))) /\ (num_canonical_sum_merge (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) = compare (list_compare index_compare l1 l2) (Cons_varlist l1 (num_canonical_sum_merge t1 (Cons_monom c2 l2 t2))) (Cons_monom (1 + c2) l1 (num_canonical_sum_merge t1 t2)) (Cons_monom c2 l2 (num_canonical_sum_merge (Cons_varlist l1 t1) t2))) /\ (num_canonical_sum_merge (Cons_varlist l1 t1) (Cons_varlist l2 t2) = compare (list_compare index_compare l1 l2) (Cons_varlist l1 (num_canonical_sum_merge t1 (Cons_varlist l2 t2))) (Cons_monom (1 + 1) l1 (num_canonical_sum_merge t1 t2)) (Cons_varlist l2 (num_canonical_sum_merge (Cons_varlist l1 t1) t2))) /\ (num_canonical_sum_merge (Cons_varlist v7 v8) Nil_monom = Cons_varlist v7 v8) /\ (num_canonical_sum_merge (Cons_monom v4 v5 v6) Nil_monom = Cons_monom v4 v5 v6) /\ (num_canonical_sum_merge Nil_monom Nil_monom = Nil_monom) /\ (num_canonical_sum_merge Nil_monom (Cons_varlist v17 v18) = Cons_varlist v17 v18) /\ (num_canonical_sum_merge Nil_monom (Cons_monom v14 v15 v16) = Cons_monom v14 v15 v16)) /\ ((num_monom_insert c1 l1 (Cons_monom c2 l2 t2) = compare (list_compare index_compare l1 l2) (Cons_monom c1 l1 (Cons_monom c2 l2 t2)) (Cons_monom (c1 + c2) l1 t2) (Cons_monom c2 l2 (num_monom_insert c1 l1 t2))) /\ (num_monom_insert c1 l1 (Cons_varlist l2 t2) = compare (list_compare index_compare l1 l2) (Cons_monom c1 l1 (Cons_varlist l2 t2)) (Cons_monom (c1 + 1) l1 t2) (Cons_varlist l2 (num_monom_insert c1 l1 t2))) /\ (num_monom_insert c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom)) /\ ((num_varlist_insert l1 (Cons_monom c2 l2 t2) = compare (list_compare index_compare l1 l2) (Cons_varlist l1 (Cons_monom c2 l2 t2)) (Cons_monom (1 + c2) l1 t2) (Cons_monom c2 l2 (num_varlist_insert l1 t2))) /\ (num_varlist_insert l1 (Cons_varlist l2 t2) = compare (list_compare index_compare l1 l2) (Cons_varlist l1 (Cons_varlist l2 t2)) (Cons_monom (1 + 1) l1 t2) (Cons_varlist l2 (num_varlist_insert l1 t2))) /\ (num_varlist_insert l1 Nil_monom = Cons_varlist l1 Nil_monom)) /\ ((!c0 c l t. num_canonical_sum_scalar c0 (Cons_monom c l t) = Cons_monom (c0 * c) l (num_canonical_sum_scalar c0 t)) /\ (!c0 l t. num_canonical_sum_scalar c0 (Cons_varlist l t) = Cons_monom c0 l (num_canonical_sum_scalar c0 t)) /\ !c0. num_canonical_sum_scalar c0 Nil_monom = Nil_monom) /\ ((!l0 c l t. num_canonical_sum_scalar2 l0 (Cons_monom c l t) = num_monom_insert c (list_merge index_lt l0 l) (num_canonical_sum_scalar2 l0 t)) /\ (!l0 l t. num_canonical_sum_scalar2 l0 (Cons_varlist l t) = num_varlist_insert (list_merge index_lt l0 l) (num_canonical_sum_scalar2 l0 t)) /\ !l0. num_canonical_sum_scalar2 l0 Nil_monom = Nil_monom) /\ ((!c0 l0 c l t. num_canonical_sum_scalar3 c0 l0 (Cons_monom c l t) = num_monom_insert (c0 * c) (list_merge index_lt l0 l) (num_canonical_sum_scalar3 c0 l0 t)) /\ (!c0 l0 l t. num_canonical_sum_scalar3 c0 l0 (Cons_varlist l t) = num_monom_insert c0 (list_merge index_lt l0 l) (num_canonical_sum_scalar3 c0 l0 t)) /\ !c0 l0. num_canonical_sum_scalar3 c0 l0 Nil_monom = Nil_monom) /\ ((!c1 l1 t1 s2. num_canonical_sum_prod (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 (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 Nil_monom s2 = Nil_monom) /\ ((!c l t. num_canonical_sum_simplify (Cons_monom c l t) = (if c = 0 then num_canonical_sum_simplify t else (if c = 1 then Cons_varlist l (num_canonical_sum_simplify t) else Cons_monom c l (num_canonical_sum_simplify t)))) /\ (!l t. num_canonical_sum_simplify (Cons_varlist l t) = Cons_varlist l (num_canonical_sum_simplify t)) /\ (num_canonical_sum_simplify Nil_monom = Nil_monom)) /\ ((!vm x. num_ivl_aux vm x [] = varmap_find x vm) /\ !vm x x' t'. num_ivl_aux vm x (x'::t') = 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 Nil_monom = a) /\ (!vm a l t. num_ics_aux vm a (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 (Cons_monom c l t) = a + num_ics_aux vm (num_interp_m vm c l) t) /\ ((!vm. num_interp_cs vm Nil_monom = 0) /\ (!vm l t. num_interp_cs vm (Cons_varlist l t) = num_ics_aux vm (num_interp_vl vm l) t) /\ !vm c l t. num_interp_cs vm (Cons_monom c l t) = num_ics_aux vm (num_interp_m vm c l) t) /\ ((!i. num_spolynom_normalize (SPvar i) = Cons_varlist [i] Nil_monom) /\ (!c. num_spolynom_normalize (SPconst c) = Cons_monom c [] Nil_monom) /\ (!l r. num_spolynom_normalize (SPplus l r) = num_canonical_sum_merge (num_spolynom_normalize l) (num_spolynom_normalize r)) /\ !l r. num_spolynom_normalize (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 $+ $*)