| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 6.10.2014 mit Größe 1 MB |
|
Quelle poly_system_strategy.prf Sprache: 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 polynomial(a,1)(x2)>0)") (("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" --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.33Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28