| products/Sources/formale Sprachen/Coq/tools/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: root.prf Sprache: Unknown
|
(root
(root_0n 0 (root_0n-1 nil 3427758277 ("" (skosimp) (("" (expand "root") (("" (expand "sign") (("" (expand "abs") (("" (rewrite "nn_root_0n") nil nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_0n formula-decl nil nn_root nil) (sign const-decl "Sign" sign "reals/")) shostak)) (root_1n 0 (root_1n-1 nil 3427758449 ("" (skosimp) (("" (expand "root") (("" (expand "sign") (("" (expand "abs") (("" (assert) (("" (rewrite "nn_root_1n") nil nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nn_root_1n formula-decl nil nn_root 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (sign const-decl "Sign" sign "reals/")) shostak)) (root_x1 0 (root_x1-1 nil 3427758482 ("" (skosimp) (("" (expand "root") (("" (expand "sign") (("" (expand "abs") (("" (case-replace "x!1=0") (("1" (assert) (("1" (rewrite "nn_root_0n") nil nil)) nil) ("2" (case "x!1<0") (("1" (assert) (("1" (rewrite "nn_root_x1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "nn_root_x1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (< const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (nn_root_x1 formula-decl nil nn_root nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_0n formula-decl nil nn_root 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sign const-decl "Sign" sign "reals/")) shostak)) (root_nn_root_rew_TCC1 0 (root_nn_root_rew_TCC1-1 nil 3427764460 ("" (subtype-tcc) nil 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) (odd? const-decl "bool" integers nil)) nil)) (root_nn_root_rew 0 (root_nn_root_rew-1 nil 3427764461 ("" (skosimp) (("" (expand "root") (("" (expand "abs") (("" (case-replace "nx!1=0") (("1" (rewrite "nn_root_0n") (("1" (assert) nil nil)) nil) ("2" (expand "sign") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sign_nat formula-decl nil sign "reals/") (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) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_0n formula-decl nil nn_root nil) (sign const-decl "Sign" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (root_expt_TCC1 0 (root_expt_TCC1-1 nil 3427758158 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (root_expt_TCC2 0 (root_expt_TCC2-1 nil 3427758158 ("" (skosimp) (("" (typepred "pn!1") (("" (split -2) (("1" (expand ">=") (("1" (expand "<=") (("1" (flatten) (("1" (split) (("1" (lemma "expt_pos" ("px" "x!1" "i" "pn!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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) (expt def-decl "real" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers 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) (nat_expt application-judgement "nat" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "real" exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (expt_pos formula-decl nil exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (<= const-decl "bool" reals nil)) nil)) (root_expt 0 (root_expt-1 nil 3427759297 ("" (skosimp) (("" (expand "root") (("" (rewrite "abs_hat_nat" 1 :dir rl) (("" (rewrite "nn_root_expt") (("" (expand "sign") (("" (expand "abs") (("" (case-replace "x!1<0") (("1" (typepred "pn!1") (("1" (assert) (("1" (expand "odd?") (("1" (skosimp) (("1" (replace -2) (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x1") (("1" (rewrite "expt_times") (("1" (rewrite "expt_x2") (("1" (lemma "negreal_times_negreal_is_posreal" ("nx" "x!1" "ny" "x!1")) (("1" (lemma "expt_pos" ("px" "x!1*x!1" "i" "j!1")) (("1" (lemma "both_sides_times_pos_lt1" ("pz" "(x!1 * x!1) ^ j!1" "x" "x!1" "y" "0")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (case-replace "x!1=0") (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_pos" ("px" "x!1" "i" "pn!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (nn_root_expt formula-decl nil nn_root nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nat_exp application-judgement "nat" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans 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) (expt_x1 formula-decl nil exponentiation nil) (expt_x2 formula-decl nil exponentiation nil) (expt_pos formula-decl nil exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (^ const-decl "real" exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (expt_times formula-decl nil exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (< const-decl "bool" reals nil) (sign const-decl "Sign" sign "reals/") (nnreal_exp application-judgement "nnreal" exponentiation nil) (odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (abs_hat_nat formula-decl nil exponentiation nil)) shostak)) (expt_root_TCC1 0 (expt_root_TCC1-1 nil 3427758158 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (expt_root 0 (expt_root-1 nil 3427759817 ("" (skosimp) (("" (expand "root") (("" (case-replace "x!1=0") (("1" (expand "sign") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) (("1" (expand "abs") (("1" (rewrite "nn_root_0n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x!1>0") (("1" (expand "abs") (("1" (expand "sign") (("1" (assert) (("1" (rewrite "expt_nn_root") nil nil)) nil)) nil)) nil) ("2" (expand "sign") (("2" (expand "abs") (("2" (assert) (("2" (typepred "pn!1") (("2" (split -2) (("1" (assert) nil nil) ("2" (expand "odd?") (("2" (skosimp) (("2" (replace -1) (("2" (lemma "nn_root_pos" ("px" "-x!1" "pn" "1+2*j!1")) (("1" (rewrite "mult_expt") (("1" (rewrite "expt_nn_root") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_times") (("1" (rewrite "expt_x1") (("1" (rewrite "expt_x2") (("1" (rewrite "expt_1i") (("1" (assert) 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) ((root const-decl "real" root nil) (expt_nn_root formula-decl nil nn_root nil) (nnreal type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nn_root const-decl "nnreal" nn_root nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (mult_expt formula-decl nil exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (expt_x1 formula-decl nil exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (expt_x2 formula-decl nil exponentiation nil) (expt_times formula-decl nil exponentiation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nn_root_pos formula-decl nil nn_root nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (sign const-decl "Sign" sign "reals/") (expt def-decl "real" exponentiation nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nat_expt application-judgement "nat" exponentiation 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_0n formula-decl nil nn_root nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nnreal_expt application-judgement "nnreal" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "real" exponentiation 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (root_is_0 0 (root_is_0-1 nil 3427760275 ("" (skosimp) (("" (expand "root") (("" (rewrite "zero_times3") (("" (rewrite "nn_root_is_0") (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (nn_root_is_0 formula-decl nil nn_root nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign const-decl "Sign" sign "reals/") (Sign type-eq-decl nil sign "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nn_root const-decl "nnreal" nn_root nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (zero_times3 formula-decl nil real_props nil)) shostak)) (root_pos 0 (root_pos-1 nil 3427760361 ("" (skosimp) (("" (expand "root") (("" (typepred "nn_root(abs(x!1), pn!1)") (("" (split) (("1" (flatten) (("1" (expand "sign") (("1" (assert) (("1" (case-replace "x!1=0") (("1" (assert) (("1" (expand "abs") (("1" (rewrite "nn_root_0n") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "sign") (("2" (assert) (("2" (rewrite "nn_root_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (sign const-decl "Sign" sign "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (nn_root_0n formula-decl nil nn_root nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal nonempty-type-eq-decl nil real_types nil) (nn_root_pos formula-decl nil nn_root 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) (nnreal type-eq-decl nil real_types 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nn_root const-decl "nnreal" nn_root nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (odd? const-decl "bool" integers nil)) shostak)) (root_neg 0 (root_neg-1 nil 3427760534 ("" (skosimp) (("" (expand "root") (("" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("" (split -1) (("1" (expand "sign") (("1" (expand "abs") (("1" (assert) (("1" (lemma "nn_root_pos" ("px" "-x!1" "pn" "pn!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (expand "sign") (("2" (assert) (("2" (replace -1) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sign") (("3" (expand "abs") (("3" (assert) (("3" (typepred "nn_root(x!1, pn!1)") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_pos formula-decl nil nn_root nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign const-decl "Sign" sign "reals/") (nn_root_0n formula-decl nil nn_root nil) (nn_root const-decl "nnreal" nn_root nil) (nnreal type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (trich_lt formula-decl nil real_props 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)) shostak)) (root_gt1 0 (root_gt1-1 nil 3427760682 ("" (skosimp) (("" (expand "root") (("" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("" (split) (("1" (expand "sign") (("1" (expand "abs") (("1" (assert) (("1" (typepred "nn_root(-x!1, pn!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "abs") (("2" (expand "sign") (("2" (assert) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sign") (("3" (assert) (("3" (rewrite "nn_root_gt1") (("3" (expand "abs") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nn_root const-decl "nnreal" nn_root nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign const-decl "Sign" sign "reals/") (nn_root_0n formula-decl nil nn_root nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nn_root_gt1 formula-decl nil nn_root nil) (trich_lt formula-decl nil real_props 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)) shostak)) (root_lt1 0 (root_lt1-1 nil 3427763570 ("" (skosimp) (("" (typepred "pn!1") (("" (case-replace "x!1>=0") (("1" (expand "root") (("1" (expand ">=") (("1" (expand "<=") (("1" (split -1) (("1" (expand "sign") (("1" (assert) (("1" (rewrite "nn_root_lt1") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "sign") (("2" (expand "abs") (("2" (assert) (("2" (replace -1 * rl) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -2) (("2" (expand "root") (("2" (expand "sign") (("2" (expand "abs") (("2" (assert) (("2" (lemma "nn_root_pos" ("px" "-x!1" "pn" "pn!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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) (minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nn_root_pos formula-decl nil nn_root nil) (root const-decl "real" root nil) (<= const-decl "bool" reals nil) (nn_root_0n formula-decl nil nn_root nil) (sign const-decl "Sign" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (nn_root_lt1 formula-decl nil nn_root nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (neg_root_TCC1 0 (neg_root_TCC1-1 nil 3427775104 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers 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)) nil)) (neg_root_TCC2 0 (neg_root_TCC2-1 nil 3427775104 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers 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)) nil)) (neg_root 0 (neg_root-1 nil 3427775105 ("" (skosimp) (("" (expand "root") (("" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("" (expand "abs") (("" (expand "sign") (("" (split) (("1" (assert) nil nil) ("2" (assert) (("2" (replace -1) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_even_is_even application-judgement "even_int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nn_root_0n formula-decl nil nn_root nil) (sign const-decl "Sign" sign "reals/") (trich_lt formula-decl nil real_props 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)) shostak)) (mult_root_TCC1 0 (mult_root_TCC1-1 nil 3427758158 ("" (skosimp) (("" (typepred "pn!1") (("" (assert) (("" (flatten) (("" (lemma "le_times_le_pos" ("nnx" "0" "y" "x!1" "nnz" "0" "w" "y!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (le_times_le_pos formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (mult_root_TCC2 0 (mult_root_TCC2-1 nil 3427759296 ("" (skosimp) (("" (typepred "pn!1") (("" (assert) nil nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (mult_root_TCC3 0 (mult_root_TCC3-1 nil 3427760995 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd? const-decl "bool" integers 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)) nil)) (mult_root 0 (mult_root-1 nil 3427762524 ("" (skosimp) (("" (expand "root") (("" (expand "sign") (("" (expand "abs") (("" (lemma "trichotomy" ("x" "x!1")) (("" (split -1) (("1" (lemma "trichotomy" ("x" "y!1")) (("1" (split) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "x!1" "py" "y!1")) (("1" (assert) (("1" (rewrite "mult_nn_root") nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "both_sides_times_pos_lt1" ("pz" "x!1" "x" "y!1" "y" "0")) (("3" (assert) (("3" (lemma "mult_nn_root" ("x" "-y!1" "y" "x!1" "pn" "pn!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "trichotomy" ("x" "y!1")) (("3" (split) (("1" (lemma "both_sides_times_pos_lt1" ("pz" "y!1" "x" "x!1" "y" "0")) (("1" (assert) (("1" (lemma "mult_nn_root" ("x" "-x!1" "y" "y!1" "pn" "pn!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (rewrite "nn_root_0n") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "negreal_times_negreal_is_posreal" ("nx" "x!1" "ny" "y!1")) (("1" (assert) (("1" (rewrite "mult_nn_root" + :dir rl) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_nn_root formula-decl nil nn_root 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (odd? const-decl "bool" integers nil) (nnreal type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (minus_even_is_even application-judgement "even_int" integers nil) (nn_root_0n formula-decl nil nn_root nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (trichotomy formula-decl nil real_axioms 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) (sign const-decl "Sign" sign "reals/")) shostak)) (inv_root_TCC1 0 (inv_root_TCC1-1 nil 3427758158 ("" (skosimp) (("" (typepred "pn!1") (("" (replace 2 -2) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "n0x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil)) (inv_root_TCC2 0 (inv_root_TCC2-1 nil 3427758158 ("" (skosimp) (("" (rewrite "root_is_0") nil nil)) nil) ((root_is_0 formula-decl nil root 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) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (odd? const-decl "bool" integers nil)) nil)) (inv_root 0 (inv_root-1 nil 3427764733 ("" (skosimp) (("" (expand "root") (("" (rewrite "abs_div") (("" (expand "abs" 1 1) (("" (case-replace "sign(1 / n0x!1) =sign(n0x!1)") (("1" (rewrite "inv_nn_root") (("1" (assert) (("1" (hide -1) (("1" (expand "sign") (("1" (case-replace "n0x!1 > 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "trichotomy" ("x" "n0x!1")) (("2" (split -1) (("1" (expand "sign") (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "n0x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (expand "sign") (("3" (rewrite "div_mult_neg_ge1" +) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (root const-decl "real" root nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (div_mult_neg_ge1 formula-decl nil real_props nil) (trichotomy formula-decl nil real_axioms nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (odd? const-decl "bool" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (inv_nn_root formula-decl nil nn_root nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (sign const-decl "Sign" sign "reals/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nzint nonempty-type-eq-decl nil integers 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) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (abs_div formula-decl nil real_props nil)) shostak)) (div_root_TCC1 0 (div_root_TCC1-1 nil 3427758158 ("" (skosimp) (("" (typepred "pn!1") (("" (replace 2 -2) (("" (flatten) (("" (lemma "both_sides_div_pos_ge1" ("pz" "n0y!1" "x" "x!1" "y" "0")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((odd? const-decl "bool" integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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_div_nzreal_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil)) nil)) (div_root_TCC2 0 (div_root_TCC2-1 nil 3427761736 ("" (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 "boolean" notequal nil) (nzreal nonempty-type-eq-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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd? const-decl "bool" integers 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)) nil)) (div_root_TCC3 0 (div_root_TCC3-1 nil 3427761736 ("" (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 "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) --> -------------------- --> maximum size reached --> -------------------- [ Dauer der Verarbeitung: 0.40 Sekunden (vorverarbeitet) ] |