| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 745 kB |
|
Impressum poly_system_strategy.prfSprache: Lisp |
|||||||||||||||
|
(poly_system_strategy (first_eq_TCC1 0 (first_eq_TCC1-1 nil 3621331936 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (first_eq_TCC2 0 (first_eq_TCC2-1 nil 3621331936 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (first_eq_TCC3 0 (first_eq_TCC3-1 nil 3621331936 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (subrange type-eq-decl nil integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil)) (first_eq_TCC4 0 (first_eq_TCC4-1 nil 3621331936 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (subrange type-eq-decl nil integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil)) (first_eq_TCC5 0 (first_eq_TCC5-1 nil 3621331936 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (subrange type-eq-decl nil integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil)) (first_eq_TCC6 0 (first_eq_TCC6-1 nil 3621331936 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (first_eq_TCC7 0 (first_eq_TCC7-1 nil 3621341858 ("" (termination-tcc) nil nil) nil nil)) (greatify_poly_TCC1 0 (greatify_poly_TCC1-1 nil 3622457802 ("" (subtype-tcc) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (* const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (greatify_rel_TCC1 0 (greatify_rel_TCC1-1 nil 3621333990 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil)) nil)) (greatify_def_TCC1 0 (greatify_def_TCC1-1 nil 3621333990 ("" (skeep) (("" (skeep) (("" (expand "greatify_poly_rel") (("" (expand "greatify_poly") (("" (expand "*") (("" (inst - "j") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil)) nil)) (greatify_def 0 (greatify_def-1 nil 3621333996 ("" (skeep) (("" (expand "solvable?") (("" (expand "solvable_at?") (("" (expand "rel5") (("" (ground) (("1" (skeep) (("1" (inst + "x") (("1" (skeep) (("1" (inst - "i") (("1" (assert) (("1" (typepred "greatify_rel(RelF6)(i)") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (expand "greatify_rel" 3 1) (("1" (assert) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_rel" 4) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (expand "greatify_rel" 5) (("1" (assert) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (assert) (("1" (flatten) (("1" (expand "greatify_rel" 7) (("1" (assert) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_rel" 7) (("1" (assert) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "greatify_rel" 8) (("2" (assert) (("2" (expand "greatify_poly_rel" +) (("2" (expand "greatify_poly") (("2" (rewrite "scal_polynomial2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst + "x") (("2" (skeep) (("2" (inst - "i") (("2" (split 1) (("1" (flatten) (("1" (expand "greatify_rel" -) (("1" (assert) (("1" (expand "greatify_poly_rel") (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "greatify_rel" -) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_poly_rel") (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_poly_rel") (("1" (expand "greatify_poly") (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_poly_rel") (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (expand "greatify_poly_rel") (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (expand "greatify_poly_rel") (("2" (expand "greatify_poly") (("2" (rewrite "scal_polynomial2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((solvable? const-decl "bool" poly_system_strategy nil) (rel5 const-decl "bool" poly_system_strategy nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (scal_polynomial2 formula-decl nil polynomials "reals/") (sequence type-eq-decl nil sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (greatify_rel const-decl "{pz: subrange(0, 5) | pz /= 2 AND pz /= 5}" poly_system_strategy nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (solvable_at? const-decl "bool" poly_system_strategy nil)) shostak)) (compute_solvable_single_TCC1 0 (compute_solvable_single_TCC1-1 nil 3621353314 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_single_TCC2 0 (compute_solvable_single_TCC2-1 nil 3621353314 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (base_list const-decl "listn[below(n)](digits)" base_repr "reals/") (sturm_tarski_faster const-decl "{r: real | r = NSol_all(k, a, m, p, n, RelF6) AND rational_pred(r) AND integer_pred(r)}" system_solvers nil) (odd? const-decl "bool" integers nil) (poly_deriv const-decl "real" polynomials "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (compute_solvable_single_TCC3 0 (compute_solvable_single_TCC3-1 nil 3621353314 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rel5 const-decl "bool" poly_system_strategy nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (/= const-decl "boolean" notequal nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (base_list const-decl "listn[below(n)](digits)" base_repr "reals/") (sturm_tarski_faster const-decl "{r: real | r = NSol_all(k, a, m, p, n, RelF6) AND rational_pred(r) AND integer_pred(r)}" system_solvers nil) (odd? const-decl "bool" integers nil) (poly_deriv const-decl "real" polynomials "reals/") (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (compute_solvable_single_TCC4 0 (compute_solvable_single_TCC4-1 nil 3621354679 ("" (skosimp*) (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (replaces -2) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_single_TCC5 0 (compute_solvable_single_TCC5-1 nil 3621354679 ("" (skosimp*) (("" (lift-if) (("" (split -) (("1" (flatten) (("1" (replaces -2) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_single_def 0 (compute_solvable_single_def-1 nil 3621354856 ("" (skeep) (("" (skeep) (("" (expand "compute_solvable_single") (("" (lift-if) (("" (split +) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (replace -1) (("1" (name "x1" "-a(0)/a(1)-1") (("1" (name "x2" "-a(0)/a(1)+1") (("1" (case "(polynomial(a,1)(x1)>0 AND polynomial(a,1)(x2)<0) OR (polynomial(a,1)(x1)<0 AND pol (("1" (inst-cp + "x1") (("1" (inst-cp + "x2") (("1" (inst + "-a(0)/a(1)") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (lemma "system_roots_enum") (("1" (inst - "0" "LAMBDA (k): d" "LAMBDa (k): a") (("1" (assert) (("1" (skeep -) (("1" (case "K = 0") (("1" (inst + "0") (("1" (inst -4 "0" "0") (("1" (assert) (("1" (replace -5 +) (("1" (expand "rel5") (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "enum(K-1)+2") (("1" (replace -4 +) (("1" (expand "rel5") (("1" (inst -3 "2+enum(K-1)" "0") (("1" (assert) (("1" (skosimp*) (("1" (inst - "i!1" "K-1") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "NOT ((sturm_tarski_faster(1, a, d, LAMBDA (k): LAMBDA (j): 1, LAMBDA (k): 0, LAMBDA (j): 1) /= 0) IFF (EXISTS (x:real): polynomial(a,d)(x)=0))") (("1" (hide 3) (("1" (typepred "sturm_tarski_faster(1, a, d, LAMBDA (k): LAMBDA (j): 1, LAMBDA (k): 0, LAMBDA (j): 1)") (("1" (replaces -1) (("1" (hide -) (("1" (expand "NSol_all") (("1" (lemma "empty_card[real]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?") (("1" (expand "member") (("1" (ground) (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "Sol_all" +) (("1" (assert) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1") (("2" (expand "Sol_all" -) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (case "i = 0") (("1" (replaces -1) (("1" (expand "rel5") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (label "izero" 1) (("2" (hide "izero") (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (hide -2) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (expand "rel5") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten +) (("2" (split 2) (("1" (flatten) (("1" (case "NOT (i = 0 OR i = 1 OR i=2 OR i=3 OR i=4 OR i=5)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (expand "rel5") (("1" (assert) (("1" (replace -1) (("1" (case "NOT greatify_rel(LAMBDA (j): 1) = (LAMBDA (j): 1)") (("1" (hide-all-but 1) (("1" (decompose-equality 1) (("1" (expand "greatify_rel") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (split 1) (("1" (flatten) (("1" (lemma "strict_poly_system_solvable") (("1" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): a") (("1" (assert) (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst -1 "0") (("2" (assert) nil nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (expand "sigma") (("3" (expand "sigma") (("3" (assert) (("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): a, LAMBDA (j): d, LAMBDA (j): 1)") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (assert) (("3" (expand "NSol_all" -) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (inst - "x!1") (("3" (expand "member") (("3" (expand "Sol_all" +) (("3" (assert) (("3" (split) (("1" (replace -2 1 :dir rl) (("1" (rewrite "poly_eq_le_degree") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "poly_deriv" +) (("1" (expand "prod_polynomials") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "x!1") (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "strict_poly_system_solvable") (("2" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): a") (("2" (assert) (("2" (flatten) (("2" (hide -1) (("2" (split -1) (("1" (skosimp*) (("1" (inst - "0") (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (skosimp 1) nil nil) ("2" (flatten) (("2" (hide 1) (("2" (skosimp 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): a, LAMBDA (j): d, LAMBDA (j): 1)") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (expand "NSol_all" -1) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp*) (("3" (inst 4 "x!1") (("3" (expand "Sol_all" -1) (("3" (flatten) (("3" (split 4) (("1" (expand "sigma" 1) (("1" (expand "sigma" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "sigma" 1) (("2" (expand "sigma" 1) (("2" (invoke (case "%1 = %2") (! -1 1) (! 1 1)) (("1" (assert) nil nil) ("2" (hide (-1 2)) (("2" (rewrite "poly_eq_le_degree") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "poly_deriv") (("2" (expand "prod_polynomials") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst - "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "rel5") (("2" (propax) nil nil)) nil)) nil) ("3" (replace -1) (("3" (expand "rel5") (("3" (case "NOT greatify_rel(LAMBDA (j): 4) = (LAMBDA (j): 4)") (("1" (decompose-equality 1) (("1" (expand "greatify_rel") (("1" (propax) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (hide -2) (("2" (split +) (("1" (flatten) (("1" (case "NOT EXISTS (x): polynomial(a, d)(x) > 0") (("1" (skeep) (("1" (inst + "x") (("1" (inst + "x") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (replace 3) (("2" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): a, LAMBDA (j): d, LAMBDA (j): 4)") (("2" (hide (-2 -3)) (("2" (replaces -1) (("2" (skosimp*) (("2" (lemma "strict_poly_system_solvable") (("2" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): a") (("2" (assert) (("2" (flatten -1) (("2" (hide -2) (("2" (split -1) (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst -1 "0") (("2" (assert) nil nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (expand "sigma") (("3" (expand "sigma") (("3" (assert) (("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): a, LAMBDA (j): d, LAMBDA (j): 4)") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (expand "NSol_all" -) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (inst - "x!2") (("3" (expand "member") (("3" (expand "Sol_all" +) (("3" (assert) (("3" (split +) (("1" (replace -3 1 :dir rl) (("1" (rewrite "poly_eq_le_degree" 1 :dir rl) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "poly_deriv") (("1" (expand "prod_polynomials") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst + "x!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (lemma "poly_sign_near_infinity") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst - "M!1") (("1" (inst + "M!1") (("1" (assert) (("1" (expand "sign_ext") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -) (("1" (propax) nil nil) ("2" (assert) (("2" (lemma "poly_sign_near_negative_infinity") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (inst - "-M!1") (("2" (assert) (("2" (lemma "even_or_odd") (("2" (inst?) (("2" (assert) (("2" (inst + "-M!1") (("2" (expand "sign_ext") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): a, LAMBDA (j): d, LAMBDA (j): 4)") (("3" (hide (-2 -3)) (("3" (flatten) (("3" (replaces -1) (("3" (expand "NSol_all" +) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?" 1) (("3" (skosimp*) (("3" (inst + "x!1") (("3" (expand "member") (("3" (expand "Sol_all") (("3" (flatten) (("3" (inst - "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (replace -1) (("4" (expand "rel5") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (case "NOT (i=2 OR i=5 )") (("1" (reveal "izero") (("1" (flatten) (("1" (expand "rel5" 4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (split -1) (("1" (assert) (("1" (replace -1) (("1" (expand "rel5") (("1" (case "NOT greatify_rel(LAMBDA (j): 2) = (LAMBDA (j): 1)") (("1" (decompose-equality 1) (("1" (expand "greatify_rel") (("1" (propax) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "*") (("2" (split +) (("1" (flatten) (("1" (assert) (("1" (lemma "strict_poly_system_solvable") (("1" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): (-1)*a") (("1" (assert) (("1" (expand "*") (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst -1 "0") (("2" (assert) nil nil)) nil) ("3" (hide 3) (("3" (skosimp*) (("3" (expand "sigma") (("3" (expand "sigma") (("3" (assert) (("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): LAMBDA (x: nat): (-1) * a(x), LAMBDA (j): d, (LAMBDA (j): 1))") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (assert) (("3" (expand "NSol_all" -) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (inst - "x!1") (("3" (expand "member") (("3" (expand "Sol_all" +) (("3" (assert) (("3" (split) (("1" (case "polynomial(poly_deriv(prod_polynomials(LAMBDA (ii: nat): LAMBDA (x: nat): (-1) * a(x), LAMBDA (ii: nat): d, (LAMBDA (i: nat): 1), 0)), d - 1) (x!1)=(-1)*polynomial(poly_deriv(a), d - 1)(x!1)") (("1" (assert) nil nil) ("2" (rewrite "scal_polynomial2" :dir rl) (("2" (rewrite "poly_eq_le_degree") (("2" (hide 2) (("2" (skosimp*) (("2" (expand "poly_deriv" +) (("2" (expand "prod_polynomials") (("2" (expand "*") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (inst + "x!1") (("4" (skosimp*) (("4" (lemma "scal_polynomial2") (("4" (expand "*" -) (("4" (rewrite -1 +) (("4" (assert) (("4" (lemma "sigma_tolambda") (("4" (expand "polynomial" (-4 1)) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "strict_poly_system_solvable") (("2" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): (-1)*a") (("1" (assert) (("1" (expand "*" -1 1) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (skosimp*) (("1" (inst - "0") (("1" (assert) (("1" (inst + "x!1") (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (skosimp 1) (("1" (expand "*" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (hide 1) (("2" (skosimp 1) (("2" (assert) (("2" (expand "*" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): LAMBDA (zz: nat): (-1) * a(zz), LAMBDA (j): d, (LAMBDA (j): 1))") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (expand "NSol_all" -1) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp*) (("3" (inst 5 "x!1") (("3" (expand "Sol_all" -1) (("3" (flatten) (("3" (inst - "0") (("3" (assert) (("3" (lemma "scal_polynomial2") (("3" (expand "*" -1) (("3" (rewrite -1) (("3" (assert) (("3" (hide-all-but (-3 5)) (("3" (invoke (case "NOT %1 = %2") (! -1 1 2) (! 1 1)) (("1" (rewrite "poly_eq_le_degree") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "rel5") (("2" (assert) (("2" (hide -2) (("2" (split +) (("1" (flatten) (("1" (case "NOT EXISTS (x): polynomial(a, d)(x) < 0") (("1" (skeep) (("1" (inst + "x") (("1" (inst + "x") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (replace 3) (("2" (case "NOT greatify_rel(LAMBDA (j): 5) = (LAMBDA (j): 4)") (("1" (decompose-equality 1) (("1" (expand "greatify_rel" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): (-1) * a, LAMBDA (j): d, (LAMBDA (j): 4))") (("1" (hide (-2 -3)) (("1" (replaces -1) (("1" (skosimp*) (("1" (lemma "strict_poly_system_solvable") (("1" (inst - "0" "LAMBDA (ii:nat): d" "LAMBDA (ii:nat): (-1)*a") (("1" (assert) (("1" (expand "*" -1 1) (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (inst - "0") (("1" (assert) nil nil)) nil) ("2" (inst -1 "0") (("2" (assert) (("2" (expand "*" 1) (("2" (assert) (("2" (expand "*") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (expand "*") (("3" (assert) (("3" (skosimp*) (("3" (expand "sigma") (("3" (expand "sigma") (("3" (assert) (("3" (expand "NSol_all" -) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?") (("3" (inst - "x!2") (("3" (expand "member") (("3" (expand "Sol_all" +) (("3" (assert) (("3" (split +) (("1" (case "polynomial(poly_deriv(prod_polynomials(LAMBDA (ii: nat): LAMBDA (x: nat): (-1) * a(x), LAMBDA (ii: nat): d, (LAMBDA (i: nat): 1), 0)), d - 1) (x!2)=(-1)*polynomial(poly_deriv(a), d - 1)(x!2)") (("1" (assert) nil nil) ("2" (rewrite "scal_polynomial2" :dir rl) (("2" (rewrite "poly_eq_le_degree" 1 :dir rl) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "poly_deriv") (("2" (expand "prod_polynomials") (("2" (expand "*") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst + "x!1") (("4" (skosimp*) (("4" (rewrite "scal_polynomial2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (expand "*" -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "*" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (lemma "poly_sign_near_infinity") (("1" (inst - "(-1)*a" "d") (("1" (assert) (("1" (skosimp*) (("1" (inst - "M!1") (("1" (inst + "M!1") (("1" (assert) (("1" (rewrite "scal_polynomial2") (("1" (expand "*") (("1" (expand "sign_ext") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (lemma "poly_sign_near_negative_infinity") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (inst - "-M!1") (("2" (assert) (("2" (lemma "even_or_odd") (("2" (inst?) (("2" (assert) (("2" (expand "*" -3) (("2" (inst + "-M!1") (("2" (expand "sign_ext") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NOT greatify_rel(LAMBDA (j): 5) = (LAMBDA (j): 4)") (("1" (decompose-equality 1) (("1" (expand "greatify_rel" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (typepred "sturm_tarski_faster(1, poly_deriv(a), d - 1, LAMBDA (j): (-1) * a, LAMBDA (j): d, (LAMBDA (j): 4))") (("1" (hide (-2 -3)) (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (expand "NSol_all" +) (("1" (lemma "empty_card[real]") (("1" (inst?) (("1" (assert) (("1" (expand "empty?" 1) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (expand "member") (("1" (expand "Sol_all") (("1" (flatten) (("1" (inst - "0") (("1" (assert) (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" -1) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "*" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rat nonempty-type-eq-decl nil rationals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (sequence type-eq-decl nil sequences nil) (< const-decl "bool" reals nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (rat_expt application-judgement "rat" exponentiation nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (scal_polynomial2 formula-decl nil polynomials "reals/") (sigma_tolambda formula-decl nil sigma_nat "reals/") (a skolem-const-decl "[nat -> int]" poly_system_strategy nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (poly_sign_near_infinity formula-decl nil more_polynomial_props "reals/") (even_or_odd formula-decl nil naturalnumbers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (poly_sign_near_negative_infinity formula-decl nil more_polynomial_props "reals/") (greatify_rel const-decl "{pz: subrange(0, 5) | pz /= 2 AND pz /= 5}" poly_system_strategy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (poly_deriv const-decl "real" polynomials "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (poly_eq_le_degree formula-decl nil polynomials "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (strict_poly_system_solvable formula-decl nil poly_systems nil) (Sol_all const-decl "finite_set[real]" poly_families nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (empty_card formula-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (subrange type-eq-decl nil integers nil) (NSol_all const-decl "nat" poly_families nil) (sturm_tarski_faster const-decl "{r: real | r = NSol_all(k, a, m, p, n, RelF6) AND rational_pred(r) AND integer_pred(r)}" system_solvers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (K skolem-const-decl "nat" poly_system_strategy nil) (below type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (system_roots_enum formula-decl nil poly_systems nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (rel5 const-decl "bool" poly_system_strategy nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (compute_solvable_single const-decl "bool" poly_system_strategy nil)) shostak)) (poly_deriv_integer 0 (poly_deriv_integer-1 nil 3621599183 ("" (skeep) (("" (expand "poly_deriv") (("" (propax) nil nil)) nil)) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_plus_int_is_int application-judgement "int" integers nil) (poly_deriv const-decl "real" polynomials "reals/")) shostak)) (compute_solvable_TCC1 0 (compute_solvable_TCC1-1 nil 3621339345 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (/= const-decl "boolean" notequal nil)) nil)) (compute_solvable_TCC2 0 (compute_solvable_TCC2-3 nil 3622460405 ("" (skeep) (("" (skeep*) (("" (split) (("1" (typepred "n") (("1" (inst - "fe") (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "fe") (("2" (assert) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (expand "greatify_poly_rel") (("2" (expand "greatify_poly") (("2" (lift-if) (("2" (expand "*") (("2" (typepred "n") (("2" (inst - "fe") (("1" (assert) (("1" (ground) nil nil)) nil) ("2" (typepred "fe") (("2" (assert) (("2" (hide -2) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (k skolem-const-decl "nat" poly_system_strategy nil) (subrange type-eq-decl nil integers nil) (newRel skolem-const-decl "[nat -> {pz: subrange(0, 5) | pz /= 2 AND pz /= 5}]" poly_system_strategy nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (fe skolem-const-decl "{i | (i > k IMPLIES (FORALL (j: upto(k)): newRel(j) > 0)) AND (i <= k IMPLIES newRel(i) = 0 AND (FORALL (j): j < i IMPLIES newRel(j) > 0))}" poly_system_strategy nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (compute_solvable_TCC2-2 nil 3621608685 ("" (skeep*) (("" (typepred "n") (("" (typepred "fe") (("" (assert) (("" (case "fe <=k") (("1" (assert) (("1" (inst - "fe") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (replace -6 +) (("1" (expand "greatify_poly_rel" +) (("1" (expand "*") (("1" (lift-if) (("1" (typepred "n") (("1" (inst - "fe") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ge_realorder name-judgement "RealOrder" real_orders "reals/")) nil) (compute_solvable_TCC2-1 nil 3621339345 ("" (subtype-tcc) nil nil) ((le_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_TCC3 0 (compute_solvable_TCC3-3 nil 3622460555 ("" (skeep*) (("" (lift-if) (("" (assert) (("" (replaces -1) (("" (expand "greatify_poly_rel" -) (("" (expand "greatify_poly") (("" (lift-if) (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst-cp - "1+i_1") (("" (inst - "i_1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (compute_solvable_TCC3-2 nil 3621608859 ("" (skeep) (("" (skeep*) (("" (split) (("1" (typepred "n") (("1" (inst - "fe") (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "fe") (("2" (assert) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (expand "greatify_poly_rel") (("2" (expand "greatify_poly") (("2" (lift-if) (("2" (expand "*") (("2" (typepred "n") (("2" (inst - "fe") (("1" (assert) (("1" (ground) nil nil)) nil) ("2" (typepred "fe") (("2" (assert) (("2" (hide -2) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil) (compute_solvable_TCC3-1 nil 3621339345 ("" (skeep*) (("" (typepred "fe") (("" (assert) (("" (case "fe <=k") (("1" (assert) (("1" (hide -2) (("1" (flatten) (("1" (inst + "fe") (("1" (replace -6 -2) (("1" (expand "greatify_rel" -2) (("1" (lift-if) (("1" (ground) (("1" (replace -5 -1) (("1" (expand "greatify_poly_rel" -1) (("1" (typepred "n") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_TCC4 0 (compute_solvable_TCC4-4 nil 3622460572 ("" (skeep*) (("" (assert) (("" (typepred "Qprodlist") (("" (replace -9 :dir rl) (("" (replace -3 + :dir rl) (("" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("" (assert) (("" (skosimp*) (("" (replace -8 -3) (("" (expand "greatify_poly_rel" -) (("" (expand "greatify_poly") (("" (assert) (("" (expand "*") (("" (lift-if) (("" (assert) (("" (typepred "n") (("" (inst - "i!1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (upto nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (> const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC4-3 nil 3622459343 ("" (skeep*) (("" (lift-if) (("" (assert) (("" (replaces -1) (("" (expand "greatify_poly_rel" -) (("" (expand "greatify_poly") (("" (lift-if) (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst-cp - "1+i_1") (("" (inst - "i_1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/")) nil) (compute_solvable_TCC4-2 nil 3621608892 ("" (skeep*) (("" (assert) (("" (typepred "Qprodlist") (("" (replace -9 :dir rl) (("" (replace -3 + :dir rl) (("" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("" (assert) (("" (skosimp*) (("" (replace -8 -3) (("" (expand "greatify_poly_rel" -) (("" (assert) (("" (expand "*") (("" (lift-if) (("" (assert) (("" (typepred "n") (("" (inst - "i!1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ge_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/") (lt_realorder name-judgement "RealOrder" real_orders "reals/") (list type-decl nil list_adt nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC4-1 nil 3621339345 ("" (skeep*) (("" (lift-if) (("" (assert) (("" (replaces -1) (("" (expand "greatify_poly_rel" -) (("" (lift-if) (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst-cp - "1+i_1") (("" (inst - "i_1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((le_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (lt_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (compute_solvable_TCC5 0 (compute_solvable_TCC5-4 nil 3622460592 ("" (skeep*) (("" (replaces -1) (("" (expand "greatify_poly_rel" -6) (("" (expand "greatify_poly") (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (> const-decl "bool" reals nil) (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC5-3 nil 3622459303 ("" (skeep*) (("" (assert) (("" (typepred "Qprodlist") (("" (replace -9 :dir rl) (("" (replace -3 + :dir rl) (("" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("" (assert) (("" (skosimp*) (("" (replace -8 -3) (("" (expand "greatify_poly_rel" -) (("" (expand "greatify_poly") (("" (assert) (("" (expand "*") (("" (lift-if) (("" (assert) (("" (typepred "n") (("" (inst - "i!1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (list type-decl nil list_adt nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/")) nil) (compute_solvable_TCC5-2 nil 3621608908 ("" (skeep*) (("" (replaces -1) (("" (expand "greatify_poly_rel" -6) (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC5-1 nil 3621339345 ("" (skeep*) (("" (assert) (("" (typepred "Qprodlist") (("" (replace -9 :dir rl) (("" (replace -3 + :dir rl) (("" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("" (assert) (("" (skosimp*) (("" (replace -8 -3) (("" (expand "greatify_poly_rel" -) (("" (assert) (("" (expand "*") (("" (lift-if) (("" (assert) (("" (typepred "n") (("" (inst - "i!1") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ge_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (le_realorder name-judgement "RealOrder" real_orders "reals/") (lt_realorder name-judgement "RealOrder" real_orders "reals/") (list type-decl nil list_adt nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/")) nil)) (compute_solvable_TCC6 0 (compute_solvable_TCC6-4 nil 3622460611 ("" (skeep*) (("" (assert) (("" (rewrite "poly_deriv_integer" +) nil nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (poly_deriv_integer formula-decl nil poly_system_strategy nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC6-3 nil 3622459268 ("" (skeep*) (("" (replaces -1) (("" (expand "greatify_poly_rel" -6) (("" (expand "greatify_poly") (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/")) nil) (compute_solvable_TCC6-2 nil 3621608920 ("" (skeep*) (("" (assert) (("" (rewrite "poly_deriv_integer" +) nil nil)) nil)) nil) ((gt_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC6-1 nil 3621339345 ("" (skeep*) (("" (replaces -1) (("" (expand "greatify_poly_rel" -6) (("" (lift-if) (("" (expand "*") (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/")) nil)) (compute_solvable_TCC7 0 (compute_solvable_TCC7-4 nil 3622460629 ("" (skeep*) (("" (assert) (("" (label "igz" 6) (("" (expand "poly_deriv" +) (("" (copy "igz") (("" (case "NOT Qprod(Qdeg)=0") (("1" (assert) (("1" (mult-by 1 "Qdeg") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -8 -1) (("2" (assert) (("2" (typepred "Qprodlist") (("2" (decompose-equality -3) (("2" (inst - "Qdeg") (("2" (assert) (("2" (replaces -1 :dir rl) (("2" (hide -1) (("2" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("2" (hide -1) (("2" (split -) (("1" (assert) nil nil) ("2" (replaces -5 1) (("2" (hide-all-but 1) (("2" (expand "greatify_poly_rel") (("2" (expand "greatify_poly") (("2" (skosimp*) (("2" (expand "*") (("2" (typepred "n") (("2" (inst - "i!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (poly_deriv const-decl "real" polynomials "reals/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (both_sides_times1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (k skolem-const-decl "nat" poly_system_strategy nil) (i!1 skolem-const-decl "nat" poly_system_strategy nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (length def-decl "nat" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (upto nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC7-3 nil 3622459250 ("" (skeep*) (("" (assert) (("" (rewrite "poly_deriv_integer" +) nil nil)) nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (ge_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/")) nil) (compute_solvable_TCC7-2 nil 3621608951 ("" (skeep*) (("" (assert) (("" (case "NOT Qdeg>=2") (("1" (typepred "Qprodlist") (("1" (replace -7 :dir rl) (("1" (replace -2) (("1" (expand "sigma" 1) (("1" (expand "sigma" 1) (("1" (expand "*" 1 1) (("1" (expand "*" 1 1) (("1" (typepred "n") (("1" (inst-cp - "k-1") (("1" (inst - "k") (("1" (flatten) (("1" (assert) (("1" (case "sigma(0, k - 2, n * (LAMBDA i: 1)) >=0") (("1" (assert) nil nil) ("2" (rewrite "sigma_ge_0") (("2" (skosimp*) (("2" (expand "*" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "Qprod(Qdeg)/=0") (("1" (expand "poly_deriv" +) (("1" (assert) (("1" (flatten) (("1" (mult-by 1 "Qdeg") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "Qprodlist") (("2" (replace -13 :dir rl) (("2" (replace -3 :dir rl) (("2" (replace -9 -4) (("2" (replace -2) (("2" (assert) (("2" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("2" (assert) (("2" (label "hp" 1) (("2" (skosimp*) (("2" (replace -10 -3) (("2" (expand "greatify_poly_rel" -3) (("2" (expand "*") (("2" (typepred "n") (("2" (inst - "i!1") (("2" (flatten) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gt_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/") (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families nil) (product def-decl "real" product "reals/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (list type-decl nil list_adt nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (poly_deriv const-decl "real" polynomials "reals/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC7-1 nil 3621339345 ("" (skeep*) (("" (rewrite "poly_deriv_integer" 5) nil nil)) nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/")) nil)) (compute_solvable_TCC8 0 (compute_solvable_TCC8-2 nil 3622459232 ("" (skeep*) (("" (replaces -1 -7) (("" (copy -6) (("" (expand "greatify_poly_rel" -1) (("" (expand "greatify_poly") (("" (lift-if) (("" (expand "*" -1) (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatify_poly_rel const-decl "[nat -> int]" poly_system_strategy nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (greatify_poly const-decl "[nat -> int]" poly_system_strategy nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil) (compute_solvable_TCC8-1 nil 3621340773 ("" (skeep*) (("" (assert) (("" (copy -7) (("" (replace -2 -1) (("" (expand "greatify_poly_rel" -1) (("" (expand "*") (("" (lift-if) (("" (typepred "n") (("" (inst - "i") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gt_realorder name-judgement "RealOrder" real_orders "reals/") (ge_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")) nil)) (compute_solvable_def 0 (compute_solvable_def-2 nil 3621611318 ("" (skeep) (("" (label "ndef" -1) (("" (case "k = 0") (("1" (replace -1) (("1" (expand "compute_solvable") (("1" (lemma "compute_solvable_single_def") (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (inst - "RelF6(0)") (("1" (replaces -1 :dir rl) (("1" (ground) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (inst - "0") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "compute_solvable" :assert? none) (("2" (name "newp" "greatify_poly_rel(p, RelF6)") (("2" (replace -1) (("2" (name "newRel" "greatify_rel(RelF6)") (("2" (replace -1) (("2" (replace 1) (("2" (case "(EXISTS (i:upto(k)): newRel(i)=0)") (("1" (name "fe" "first_eq(newRel, k)") (("1" (assert) (("1" (replace -2) (("1" (replace -1) (("1" (case "NOT fe<=k") (("1" (typepred "fe") (("1" (assert) (("1" (skosimp*) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "fe") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (typepred "sturm_tarski_faster(k - 1, newp(fe), n(fe), LAMBDA (i): IF i < fe THEN newp(i) ELSE newp(1 + i) ENDIF, LAMBDA (i): IF i < fe THEN n(i) ELSE n(1 + i) ENDIF, LAMBDA (i): IF i < fe THEN newRel(i) ELSE newRel(1 + i) ENDIF)") (("1" (hide (-2 -3)) (("1" (replaces -1) (("1" (expand "NSol_all" +) (("1" (lemma "empty_card[real]") (("1" (inst?) (("1" (replaces -1 :dir rl) (("1" (expand "empty?") (("1" (expand "member") (("1" (ground) (("1" (skosimp*) (("1" (inst -2 "x!1") (("1" (expand "Sol_all") (("1" (split 1) (("1" (inst - "fe") (("1" (expand "newRel" -2) (("1" (expand "greatify_rel" -2) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (expand "rel5" -2) (("1" (expand "newp" +) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!2 < fe") (("1" (assert) (("1" (inst - "i!2") (("1" (expand "rel5" -3) (("1" (expand "newRel" +) (("1" (expand "greatify_rel" +) (("1" (expand "newp" +) (("1" (expand "greatify_poly_rel" +) (("1" (expand "greatify_poly") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil) ("2" (rewrite "scal_polynomial2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "1+i!2") (("2" (assert) (("2" (expand "rel5" -2) (("2" (expand "newRel" +) (("2" (expand "newp" +) (("2" (expand "greatify_rel" +) (("2" (expand "greatify_poly_rel" +) (("2" (expand "greatify_poly") (("2" (lift-if) (("2" (assert) (("2" (rewrite "scal_polynomial2") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1") (("2" (case "NOT RelF6(fe) = 0") (("1" (expand "newRel" -2) (("1" (expand "greatify_rel" -2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (case "j = fe") (("1" (replace -1) (("1" (replace -2) (("1" (expand "rel5" 1) (("1" (expand "Sol_all" -3) (("1" (flatten) (("1" (expand "newp" -3) (("1" (expand "greatify_poly_rel" -3) (("1" (expand "greatify_poly") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j < fe") (("1" (expand "Sol_all") (("1" (flatten) (("1" (inst - "j") (("1" (assert) (("1" (expand "newp" -4) (("1" (expand "newRel" -4) (("1" (expand "greatify_poly_rel" -4) (("1" (expand "greatify_poly") (("1" (expand "greatify_rel" -4) (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (expand "rel5" +) (("1" (rewrite "scal_polynomial2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Sol_all") (("2" (flatten) (("2" (inst - "j-1") (("1" (assert) (("1" (expand "newp" -3) (("1" (expand "newRel" -3) (("1" (expand "greatify_rel" -3) (("1" (expand "greatify_poly_rel" -3) (("1" (expand "greatify_poly") (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (expand "rel5" +) (("1" (rewrite "scal_polynomial2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (inst-cp - "i!1") (("2" (inst - "1+i!1") (("2" (lift-if) (("2" (expand "newp" -1) (("2" (expand "greatify_poly_rel" -1) (("2" (expand "greatify_poly") (("2" (expand "*" -1) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (inst-cp - "i!1") (("2" (flatten) (("2" (inst - "1+i!1") (("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "Qprodlist" "prod_polynomials_list(newp, n, LAMBDA i: 1, k)") (("2" (name "Qdeg" "length(Qprodlist) - 1") (("2" (name "Qprod" "LAMBDA (i): IF i < length(Qprodlist) THEN nth(Qprodlist, i) ELSE 0 ENDIF") (("2" (assert) (("2" (replace -3) (("2" (replace -2) (("2" (replace -1) (("2" (case "NOT length(Qprodlist) - 2 = Qdeg -1") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (lift-if) (("2" (replace 1) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (case "NOT Qdeg>=2") (("1" (assert) (("1" (typepred "Qprodlist") (("1" (replace -2) (("1" (replace -7 1 :dir rl) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "*" 1 1) (("1" (expand "*" 1 1) (("1" (assert) (("1" (copy "ndef") (("1" (inst-cp - "k") (("1" (inst - "k-1") (("1" (flatten) (("1" (assert) (("1" (lemma "sigma_ge_0") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (case "EXISTS (pz:upto(k)): polynomial(p(pz),n(pz))(x) = 0") (("1" (skeep -) (("1" (case "NOT newRel(pz)=4") (("1" (expand "newRel" 1) (("1" (inst - "pz") (("1" (inst + "pz") (("1" (expand "rel5" -3) (("1" (expand "greatify_rel" 1) (("1" (lift-if) (("1" (ground) (("1" (expand "newRel" 6) (("1" (expand "greatify_rel" 6) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sturm_tarski_faster(k, Qprod, Qdeg, newp, n, newRel)") (("2" (hide (-2 -3)) (("2" (replaces -1) (("2" (expand "NSol_all" -) (("2" (lemma "empty_card[real]") (("2" (inst?) (("2" (assert) (("2" (expand "empty?" -1) (("2" (expand "member") (("2" (inst - "x") (("2" (expand "Sol_all" +) (("2" (split 1) (("1" (typepred "Qprodlist") (("1" (replace -11) (("1" (typepred "prod_polynomials(newp, n, LAMBDA i: 1, k)") (("1" (inst - "x") (("1" (replace -6) (("1" (replace -5 :dir rl) (("1" (lemma "Qdeg") (("1" (replaces -1 -2 :dir rl) (("1" (replaces -1 +) (("1" (lemma "product_eq_zero[nat]") (("1" (inst?) (("1" (assert) (("1" (inst + "pz") (("1" (expand "^" 1) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "newp" +) (("1" (expand "greatify_poly_rel" 1) (("1" (expand "greatify_poly") (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!1") (("2" (hide (2 3)) (("2" (expand "rel5") (("2" (expand "newp" +) (("2" (expand "newRel" +) (("2" (expand "greatify_poly_rel" +) (("2" (expand "greatify_poly") (("2" (expand "greatify_rel" +) (("2" (hide 2) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil) ("2" (rewrite "scal_polynomial2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "SS" "LAMBDA (i:nat): IF newRel(i)/=3 OR (newRel(i)=3 AND polynomial(newp(i),n(i))(x)>=0) THEN (("2" (name "NP" "LAMBDA (i:nat): SS(i)*newp(i)") (("2" (lemma "strict_poly_system_solvable") (("2" (inst - "k" "n" "NP") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (hide (1 3)) (("1" (skeep) (("1" (inst - "j") (("1" (assert) (("1" (expand "NP" -1) (("1" (expand "*" -1) (("1" (expand "SS" -1) (("1" (lift-if) (("1" (split -1) (("1" (flatten) (("1" (expand "newRel" 1) (("1" (expand "greatify_rel" 1) (("1" (expand "rel5" 1) (("1" (inst + "j") (("1" (copy 2) (("1" (expand "newRel" 1) (("1" (expand "greatify_rel" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1 2) (("2" (expand "rel5" 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (1 2)) (("2" (skeep) (("2" (inst - "j") (("2" (inst + "j") (("2" (lemma "even_or_odd") (("2" (inst?) (("2" (assert) (("2" (assert) (("2" (lift-if) (("2" (expand "NP" -2) (("2" (expand "SS" -2) (("2" (lift-if) (("2" (lift-if) (("2" (expand "*") (("2" (split -2) (("1" (flatten) (("1" (assert) (("1" (hide -3) (("1" (split -) (("1" (flatten) (("1" (expand "newRel" 2) (("1" (expand "greatify_rel" 2) (("1" (expand "rel5" +) (("1" (ground) (("1" (expand "newRel" +) (("1" (expand "greatify_rel" +) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "newRel" +) (("2" (expand "greatify_rel" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -1 +) (("2" (expand "rel5" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -2) (("2" (split -) (("1" (flatten) (("1" (expand "newRel" +) (("1" (expand "greatify_rel" +) (("1" (lift-if) (("1" (expand "rel5" +) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (expand "rel5" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp -1) (("3" (typepred "sturm_tarski_faster(k, poly_deriv(Qprod), Qdeg - 1, newp, n, newRel)") (("3" (hide (-2 -3)) (("3" (replaces -1) (("3" (expand "NSol_all" -9) (("3" (lemma "empty_card[real]") (("3" (inst?) (("3" (assert) (("3" (expand "empty?" -1) (("3" (expand "member") (("3" (inst - "x!1") (("3" (expand "Sol_all" 1) (("3" (assert) (("3" (split 1) (("1" (case "EXISTS (nzr: nzreal): nzr*prod_polynomials(NP, n, (LAMBDA (i: nat): 1), k) = Qprod") (("1" (skeep -1) (("1" (replace -1 1 :dir rl) (("1" (case "Qdeg-1 = sigma(0, k, n) - 1") (("1" (replace -1 :dir rl) (("1" (rewrite "poly_deriv_scal") (("1" (rewrite "scal_polynomial2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "Qprodlist") (("2" (assert) (("2" (case "n = n*(LAMBDA (i): 1)") (("1" (assert) nil nil) ("2" (decompose-equality 1) (("1" (expand "*" 1) (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "Qprodlist") (("2" (replace -14) (("2" (replace -3 1 :dir rl) (("2" (case "FORALL (dd:nat): dd<=k IMPLIES EXISTS (nzr: nzreal): nzr * prod_polynomials(NP, n, (LAMBDA (i: nat): 1), dd) = prod_polynomials(newp, n, LAMBDA i: 1, dd)") (("1" (inst - "k") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "dd") (("1" (assert) (("1" (inst + "SS(0)") (("1" (decompose-equality 1) (("1" (expand "*" 1) (("1" (expand "prod_polynomials" 1) (("1" (expand "NP" 1) (("1" (expand "*" 1) (("1" (expand "SS" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "d") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (skeep -) (("2" (inst + "SS(1+d)*nzr") (("2" (decompose-equality +) (("2" (expand "prod_polynomials" +) (("2" (expand "*" 1) (("2" (replace -1 + :dir rl) (("2" (expand "polynomial_prod" 1) (("2" (rewrite "sigma_scal" :dir rl) (("1" (rewrite "sigma_scal_right" :dir rl) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "NP" + 2) (("1" (lift-if) (("1" (assert) (("1" (expand "SS" 1) (("1" (lift-if) (("1" (assert) (("1" (expand "*" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (case "FORALL (gg:nat): rational_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x))) AND integer_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x)))") (("1" (inst - "d") nil nil) ("2" (hide 2) (("2" (induct "gg") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (case "FORALL (gg:nat): rational_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x))) AND integer_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x)))") (("1" (inst - "d") nil nil) ("2" (hide 2) (("2" (induct "gg") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "FORALL (gg:nat): rational_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x))) AND integer_pred(sigma[nat](0, gg, LAMBDA (x: nat): n(x)))") (("1" (inst - "d") nil nil) ("2" (hide 2) (("2" (induct "gg") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") (("2" (assert) (("2" (inst 5 "i") (("2" (assert) (("2" (expand "NP" -4) (("2" (rewrite "scal_polynomial2") (("2" (expand "SS" -4) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst + "x") (("4" (skeep) (("4" (expand "NP" 1) (("4" (rewrite "scal_polynomial2") (("4" (expand "SS" 1) (("4" (lift-if) (("4" (split 1) (("1" (flatten) (("1" (case "newRel(i)/=3") (("1" (assert) (("1" (hide -2) (("1" (inst 5 "i") (("1" (inst + "i") (("1" (assert) (("1" (expand "newp" 1) (("1" (expand "newRel" 5) (("1" (expand "greatify_poly_rel" 1) (("1" (expand "greatify_poly") (("1" (expand "greatify_rel" +) (("1" (inst - "i") (("1" (expand "rel5" -6) (("1" (lift-if) (("1" (expand "newRel" -1) (("1" (expand "greatify_rel" -1) (("1" (lift-if) (("1" (rewrite "scal_polynomial2") (("1" (ground) nil --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.689Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26