int_interp_p : int EVAL_quote$varmap -> int EVAL_ringNorm$polynom -> intint_polynom_normalize : int EVAL_ringNorm$polynom -> int EVAL_canonical$canonical_sumint_polynom_simplify : int EVAL_ringNorm$polynom -> int EVAL_canonical$canonical_sumint_r_canonical_sum_merge : int EVAL_canonical$canonical_sum ->
int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_canonical_sum_prod : int EVAL_canonical$canonical_sum ->
int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_canonical_sum_scalar : int -> int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_canonical_sum_scalar2 : EVAL_quote$index list -> int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_canonical_sum_scalar3 : int ->
EVAL_quote$index list -> int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_canonical_sum_simplify : int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_ics_aux : int EVAL_quote$varmap -> int -> int EVAL_canonical$canonical_sum -> intint_r_interp_cs : int EVAL_quote$varmap -> int EVAL_canonical$canonical_sum -> intint_r_interp_m : int EVAL_quote$varmap -> int -> EVAL_quote$index list -> intint_r_interp_sp : int EVAL_quote$varmap -> int EVAL_canonical$spolynom -> intint_r_interp_vl : int EVAL_quote$varmap -> EVAL_quote$index list -> intint_r_ivl_aux : int EVAL_quote$varmap -> EVAL_quote$index -> EVAL_quote$index list -> intint_r_monom_insert : int ->
EVAL_quote$index list -> int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_r_spolynom_normalize : int EVAL_canonical$spolynom -> int EVAL_canonical$canonical_sumint_r_spolynom_simplify : int EVAL_canonical$spolynom -> int EVAL_canonical$canonical_sumint_r_varlist_insert : EVAL_quote$index list -> int EVAL_canonical$canonical_sum -> int EVAL_canonical$canonical_sumint_interp_p_def⊢ int_interp_p = EVAL_ringNorm$interp_p (ring int_0 int_1 $+ $* numeric_negate)
int_polynom_normalize_def⊢ int_polynom_normalize = EVAL_ringNorm$polynom_normalize (ring int_0 int_1 $+ $* numeric_negate)
int_polynom_simplify_def⊢ int_polynom_simplify = EVAL_ringNorm$polynom_simplify (ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_merge_def⊢ int_r_canonical_sum_merge =
EVAL_ringNorm$r_canonical_sum_merge
(ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_prod_def⊢ int_r_canonical_sum_prod =
EVAL_ringNorm$r_canonical_sum_prod
(ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_scalar2_def⊢ int_r_canonical_sum_scalar2 =
EVAL_ringNorm$r_canonical_sum_scalar2
(ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_scalar3_def⊢ int_r_canonical_sum_scalar3 =
EVAL_ringNorm$r_canonical_sum_scalar3
(ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_scalar_def⊢ int_r_canonical_sum_scalar =
EVAL_ringNorm$r_canonical_sum_scalar
(ring int_0 int_1 $+ $* numeric_negate)
int_r_canonical_sum_simplify_def⊢ int_r_canonical_sum_simplify =
EVAL_ringNorm$r_canonical_sum_simplify
(ring int_0 int_1 $+ $* numeric_negate)
int_r_ics_aux_def⊢ int_r_ics_aux = EVAL_ringNorm$r_ics_aux (ring int_0 int_1 $+ $* numeric_negate)
int_r_interp_cs_def⊢ int_r_interp_cs = EVAL_ringNorm$r_interp_cs (ring int_0 int_1 $+ $* numeric_negate)
int_r_interp_m_def⊢ int_r_interp_m = EVAL_ringNorm$r_interp_m (ring int_0 int_1 $+ $* numeric_negate)
int_r_interp_sp_def⊢ int_r_interp_sp = EVAL_ringNorm$r_interp_sp (ring int_0 int_1 $+ $* numeric_negate)
int_r_interp_vl_def⊢ int_r_interp_vl = EVAL_ringNorm$r_interp_vl (ring int_0 int_1 $+ $* numeric_negate)
int_r_ivl_aux_def⊢ int_r_ivl_aux = EVAL_ringNorm$r_ivl_aux (ring int_0 int_1 $+ $* numeric_negate)
int_r_monom_insert_def⊢ int_r_monom_insert = EVAL_ringNorm$r_monom_insert (ring int_0 int_1 $+ $* numeric_negate)
int_r_spolynom_normalize_def⊢ int_r_spolynom_normalize =
EVAL_ringNorm$r_spolynom_normalize
(ring int_0 int_1 $+ $* numeric_negate)
int_r_spolynom_simplify_def⊢ int_r_spolynom_simplify = EVAL_ringNorm$r_spolynom_simplify (ring int_0 int_1 $+ $* numeric_negate)
int_r_varlist_insert_def⊢ int_r_varlist_insert = EVAL_ringNorm$r_varlist_insert (ring int_0 int_1 $+ $* numeric_negate)
⊢ is_ring (ring int_0 int_1 $+ $* numeric_negate)
int_rewrites⊢ ((&n + &m = &(n + m)) ∧
(-&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
(&n + -&m = if m ≤ n then &(n − m) else -&(m − n)) ∧
(-&n + -&m = -&(n + m)) ∧ (&n * &m = &(n * m)) ∧
(-&n * &m = -&(n * m)) ∧ (&n * -&m = -&(n * m)) ∧
(-&n * -&m = &(n * m)) ∧ ((&n = &m) ⇔ (n = m)) ∧
((&n = -&m) ⇔ (n = 0) ∧ (m = 0)) ∧ ((-&n = &m) ⇔ (n = 0) ∧ (m = 0)) ∧
((-&n = -&m) ⇔ (n = m)) ∧ (--x = x) ∧ (-0 = 0)) ∧ (int_0 = 0) ∧
(int_1 = 1) ∧
(∀n m.
(ZERO < BIT1 n ⇔ T) ∧ (ZERO < BIT2 n ⇔ T) ∧ (n < ZERO ⇔ F) ∧
(BIT1 n < BIT1 m ⇔ n < m) ∧ (BIT2 n < BIT2 m ⇔ n < m) ∧
(BIT1 n < BIT2 m ⇔ ¬(m < n)) ∧ (BIT2 n < BIT1 m ⇔ n < m)) ∧
(∀n m.
(ZERO ≤ n ⇔ T) ∧ (BIT1 n ≤ ZERO ⇔ F) ∧ (BIT2 n ≤ ZERO ⇔ F) ∧
(BIT1 n ≤ BIT1 m ⇔ n ≤ m) ∧ (BIT1 n ≤ BIT2 m ⇔ n ≤ m) ∧
(BIT2 n ≤ BIT1 m ⇔ ¬(m ≤ n)) ∧ (BIT2 n ≤ BIT2 m ⇔ n ≤ m)) ∧
(∀n m.
NUMERAL (n − m) = if m < n then NUMERAL (numeral$iSUB T n m) else 0) ∧
(∀b n m.
(numeral$iSUB b ZERO x = ZERO) ∧ (numeral$iSUB T n ZERO = n) ∧
(numeral$iSUB F (BIT1 n) ZERO = numeral$iDUB n) ∧
(numeral$iSUB T (BIT1 n) (BIT1 m) = numeral$iDUB (numeral$iSUB T n m)) ∧
(numeral$iSUB F (BIT1 n) (BIT1 m) = BIT1 (numeral$iSUB F n m)) ∧
(numeral$iSUB T (BIT1 n) (BIT2 m) = BIT1 (numeral$iSUB F n m)) ∧
(numeral$iSUB F (BIT1 n) (BIT2 m) = numeral$iDUB (numeral$iSUB F n m)) ∧
(numeral$iSUB F (BIT2 n) ZERO = BIT1 n) ∧
(numeral$iSUB T (BIT2 n) (BIT1 m) = BIT1 (numeral$iSUB T n m)) ∧
(numeral$iSUB F (BIT2 n) (BIT1 m) = numeral$iDUB (numeral$iSUB T n m)) ∧
(numeral$iSUB T (BIT2 n) (BIT2 m) = numeral$iDUB (numeral$iSUB T n m)) ∧
(numeral$iSUB F (BIT2 n) (BIT2 m) = BIT1 (numeral$iSUB F n m))) ∧
∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)
int_ring_thms⊢ is_ring (ring int_0 int_1 $+ $* numeric_negate) ∧
(∀vm p. int_interp_p vm p = int_r_interp_cs vm (int_polynom_simplify p)) ∧
(((∀vm c. int_interp_p vm (EVAL_ringNorm$Pconst c) = c) ∧
(∀vm i.
int_interp_p vm (EVAL_ringNorm$Pvar i) = EVAL_quote$varmap_find i vm) ∧
(∀vm p1 p2.
int_interp_p vm (EVAL_ringNorm$Pplus p1 p2) =
int_interp_p vm p1 + int_interp_p vm p2) ∧
(∀vm p1 p2.
int_interp_p vm (EVAL_ringNorm$Pmult p1 p2) =
int_interp_p vm p1 * int_interp_p vm p2) ∧
∀vm p1. int_interp_p vm (EVAL_ringNorm$Popp p1) = -int_interp_p vm p1) ∧
(∀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.
int_r_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
(int_r_canonical_sum_merge t1
(EVAL_canonical$Cons_monom c2 l2 t2)))
(EVAL_canonical$Cons_monom (c1 + c2) l1
(int_r_canonical_sum_merge t1 t2))
(EVAL_canonical$Cons_monom c2 l2
(int_r_canonical_sum_merge (EVAL_canonical$Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 l2 l1 c1.
int_r_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
(int_r_canonical_sum_merge t1
(EVAL_canonical$Cons_varlist l2 t2)))
(EVAL_canonical$Cons_monom (c1 + int_1) l1
(int_r_canonical_sum_merge t1 t2))
(EVAL_canonical$Cons_varlist l2
(int_r_canonical_sum_merge (EVAL_canonical$Cons_monom c1 l1 t1)
t2))) ∧
(∀t2 t1 l2 l1 c2.
int_r_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
(int_r_canonical_sum_merge t1
(EVAL_canonical$Cons_monom c2 l2 t2)))
(EVAL_canonical$Cons_monom (int_1 + c2) l1
(int_r_canonical_sum_merge t1 t2))
(EVAL_canonical$Cons_monom c2 l2
(int_r_canonical_sum_merge (EVAL_canonical$Cons_varlist l1 t1)
t2))) ∧
(∀t2 t1 l2 l1.
int_r_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
(int_r_canonical_sum_merge t1
(EVAL_canonical$Cons_varlist l2 t2)))
(EVAL_canonical$Cons_monom (int_1 + int_1) l1
(int_r_canonical_sum_merge t1 t2))
(EVAL_canonical$Cons_varlist l2
(int_r_canonical_sum_merge (EVAL_canonical$Cons_varlist l1 t1)
t2))) ∧
(∀s1. int_r_canonical_sum_merge s1 EVAL_canonical$Nil_monom = s1) ∧
(∀v6 v5 v4.
int_r_canonical_sum_merge EVAL_canonical$Nil_monom
(EVAL_canonical$Cons_monom v4 v5 v6) =
EVAL_canonical$Cons_monom v4 v5 v6) ∧
∀v8 v7.
int_r_canonical_sum_merge EVAL_canonical$Nil_monom
(EVAL_canonical$Cons_varlist v7 v8) =
EVAL_canonical$Cons_varlist v7 v8) ∧
((∀t2 l2 l1 c2 c1.
int_r_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 (int_r_monom_insert c1 l1 t2))) ∧
(∀t2 l2 l1 c1.
int_r_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 + int_1) l1 t2)
(EVAL_canonical$Cons_varlist l2 (int_r_monom_insert c1 l1 t2))) ∧
∀l1 c1.
int_r_monom_insert c1 l1 EVAL_canonical$Nil_monom =
EVAL_canonical$Cons_monom c1 l1 EVAL_canonical$Nil_monom) ∧
((∀t2 l2 l1 c2.
int_r_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 (int_1 + c2) l1 t2)
(EVAL_canonical$Cons_monom c2 l2 (int_r_varlist_insert l1 t2))) ∧
(∀t2 l2 l1.
int_r_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 (int_1 + int_1) l1 t2)
(EVAL_canonical$Cons_varlist l2 (int_r_varlist_insert l1 t2))) ∧
∀l1.
int_r_varlist_insert l1 EVAL_canonical$Nil_monom =
EVAL_canonical$Cons_varlist l1 EVAL_canonical$Nil_monom) ∧
((∀c0 c l t.
int_r_canonical_sum_scalar c0 (EVAL_canonical$Cons_monom c l t) =
EVAL_canonical$Cons_monom (c0 * c) l
(int_r_canonical_sum_scalar c0 t)) ∧
(∀c0 l t.
int_r_canonical_sum_scalar c0 (EVAL_canonical$Cons_varlist l t) =
EVAL_canonical$Cons_monom c0 l (int_r_canonical_sum_scalar c0 t)) ∧
∀c0.
int_r_canonical_sum_scalar c0 EVAL_canonical$Nil_monom =
EVAL_canonical$Nil_monom) ∧
((∀l0 c l t.
int_r_canonical_sum_scalar2 l0 (EVAL_canonical$Cons_monom c l t) =
int_r_monom_insert c
(ternaryComparisons$list_merge EVAL_quote$index_lt l0 l)
(int_r_canonical_sum_scalar2 l0 t)) ∧
(∀l0 l t.
int_r_canonical_sum_scalar2 l0 (EVAL_canonical$Cons_varlist l t) =
int_r_varlist_insert
(ternaryComparisons$list_merge EVAL_quote$index_lt l0 l)
(int_r_canonical_sum_scalar2 l0 t)) ∧
∀l0.
int_r_canonical_sum_scalar2 l0 EVAL_canonical$Nil_monom =
EVAL_canonical$Nil_monom) ∧
((∀c0 l0 c l t.
int_r_canonical_sum_scalar3 c0 l0 (EVAL_canonical$Cons_monom c l t) =
int_r_monom_insert (c0 * c)
(ternaryComparisons$list_merge EVAL_quote$index_lt l0 l)
(int_r_canonical_sum_scalar3 c0 l0 t)) ∧
(∀c0 l0 l t.
int_r_canonical_sum_scalar3 c0 l0 (EVAL_canonical$Cons_varlist l t) =
int_r_monom_insert c0
(ternaryComparisons$list_merge EVAL_quote$index_lt l0 l)
(int_r_canonical_sum_scalar3 c0 l0 t)) ∧
∀c0 l0.
int_r_canonical_sum_scalar3 c0 l0 EVAL_canonical$Nil_monom =
EVAL_canonical$Nil_monom) ∧
((∀c1 l1 t1 s2.
int_r_canonical_sum_prod (EVAL_canonical$Cons_monom c1 l1 t1) s2 =
int_r_canonical_sum_merge (int_r_canonical_sum_scalar3 c1 l1 s2)
(int_r_canonical_sum_prod t1 s2)) ∧
(∀l1 t1 s2.
int_r_canonical_sum_prod (EVAL_canonical$Cons_varlist l1 t1) s2 =
int_r_canonical_sum_merge (int_r_canonical_sum_scalar2 l1 s2)
(int_r_canonical_sum_prod t1 s2)) ∧
∀s2.
int_r_canonical_sum_prod EVAL_canonical$Nil_monom s2 =
EVAL_canonical$Nil_monom) ∧
((∀c l t.
int_r_canonical_sum_simplify (EVAL_canonical$Cons_monom c l t) =
if c = int_0 then int_r_canonical_sum_simplify t
else if c = int_1 then
EVAL_canonical$Cons_varlist l (int_r_canonical_sum_simplify t)
else EVAL_canonical$Cons_monom c l (int_r_canonical_sum_simplify t)) ∧
(∀l t.
int_r_canonical_sum_simplify (EVAL_canonical$Cons_varlist l t) =
EVAL_canonical$Cons_varlist l (int_r_canonical_sum_simplify t)) ∧
(int_r_canonical_sum_simplify EVAL_canonical$Nil_monom =
EVAL_canonical$Nil_monom)) ∧
((∀vm x. int_r_ivl_aux vm x [] = EVAL_quote$varmap_find x vm) ∧
∀vm x x' t'.
int_r_ivl_aux vm x (x'::t') =
EVAL_quote$varmap_find x vm * int_r_ivl_aux vm x' t') ∧
((∀vm. int_r_interp_vl vm [] = int_1) ∧
∀vm x t. int_r_interp_vl vm (x::t) = int_r_ivl_aux vm x t) ∧
((∀vm c. int_r_interp_m vm c [] = c) ∧
∀vm c x t. int_r_interp_m vm c (x::t) = c * int_r_ivl_aux vm x t) ∧
((∀vm a. int_r_ics_aux vm a EVAL_canonical$Nil_monom = a) ∧
(∀vm a l t.
int_r_ics_aux vm a (EVAL_canonical$Cons_varlist l t) =
a + int_r_ics_aux vm (int_r_interp_vl vm l) t) ∧
∀vm a c l t.
int_r_ics_aux vm a (EVAL_canonical$Cons_monom c l t) =
a + int_r_ics_aux vm (int_r_interp_m vm c l) t) ∧
((∀vm. int_r_interp_cs vm EVAL_canonical$Nil_monom = int_0) ∧
(∀vm l t.
int_r_interp_cs vm (EVAL_canonical$Cons_varlist l t) =
int_r_ics_aux vm (int_r_interp_vl vm l) t) ∧
∀vm c l t.
int_r_interp_cs vm (EVAL_canonical$Cons_monom c l t) =
int_r_ics_aux vm (int_r_interp_m vm c l) t) ∧
((∀i. int_polynom_normalize (EVAL_ringNorm$Pvar i) =
EVAL_canonical$Cons_varlist [i] EVAL_canonical$Nil_monom) ∧
(∀c. int_polynom_normalize (EVAL_ringNorm$Pconst c) =
EVAL_canonical$Cons_monom c [] EVAL_canonical$Nil_monom) ∧
(∀pl pr.
int_polynom_normalize (EVAL_ringNorm$Pplus pl pr) =
int_r_canonical_sum_merge (int_polynom_normalize pl)
(int_polynom_normalize pr)) ∧
(∀pl pr.
int_polynom_normalize (EVAL_ringNorm$Pmult pl pr) =
int_r_canonical_sum_prod (int_polynom_normalize pl)
(int_polynom_normalize pr)) ∧
∀p. int_polynom_normalize (EVAL_ringNorm$Popp p) =
int_r_canonical_sum_scalar3 (-int_1) [] (int_polynom_normalize p)) ∧
∀x. int_polynom_simplify x =
int_r_canonical_sum_simplify (int_polynom_normalize x)