|
(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
--> --------------------
¤ Dauer der Verarbeitung: 0.112 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
