| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: double_index.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(hyperbolicx
(sinh_lemma 0 (sinh_lemma-1 nil 3394197876 ("" (skosimp) (("" (expand "sinh") (("" (expand "cauchy_sinh") (("" (lemma "exp_lemma" ("x" "x!1" "cx" "cx!1")) (("" (lemma "neg_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (lemma "exp_lemma" ("x" "-x!1" "cx" "cauchy_neg(cx!1)")) (("" (assert) (("" (lemma "sub_lemma" ("x" "exp(x!1)" "cx" "cauchy_exp(cx!1)" "y" "exp(-x!1)" "cy" "cauchy_exp(cauchy_neg(cx!1))")) (("" (assert) (("" (lemma "lemma_div2n" ("x" "exp(x!1) - exp(-x!1)" "cx" "cauchy_sub(cauchy_exp(cx!1),cauchy_exp(cauchy_neg(cx!1)))" "n" "1")) (("" (assert) (("" (expand "div2n") (("" (rewrite "expt_x1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sinh const-decl "real" hyperbolic "lnexp_fnd/") (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (exp_lemma formula-decl nil exp nil) (cauchy_exp_is_posreal application-judgement "cauchy_posreal" exp nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posint_exp application-judgement "posint" exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (div2n const-decl "real" shift nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cauchy_sub const-decl "cauchy_real" sub nil) (lemma_div2n formula-decl nil shift nil) (sub_lemma formula-decl nil sub nil) (cauchy_exp const-decl "[nat -> int]" exp 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) (= const-decl "[T, T -> boolean]" equalities nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cauchy_neg const-decl "cauchy_real" neg nil) (neg_lemma formula-decl nil neg nil) (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil)) shostak)) (cosh_lemma 0 (cosh_lemma-1 nil 3394198044 ("" (skosimp) (("" (expand "cauchy_cosh") (("" (expand "cosh") (("" (lemma "neg_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (lemma "exp_lemma" ("x" "x!1" "cx" "cx!1")) (("" (lemma "exp_lemma" ("x" "-x!1" "cx" "cauchy_neg(cx!1)")) (("" (assert) (("" (lemma "add_lemma" ("x" "exp(x!1)" "cx" "cauchy_exp(cx!1)" "y" "exp(-x!1)" "cy" "cauchy_exp(cauchy_neg(cx!1))")) (("" (assert) (("" (lemma "lemma_div2n" ("x" "exp(-x!1) + exp(x!1)" "cx" "cauchy_add(cauchy_exp(cx!1),cauchy_exp(cauchy_neg(cx!1)))" "n" "1")) (("" (assert) (("" (expand "div2n") (("" (rewrite "expt_x1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (neg_lemma formula-decl nil neg nil) (exp_lemma formula-decl nil exp nil) (posint_exp application-judgement "posint" exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (div2n const-decl "real" shift nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cauchy_add const-decl "cauchy_real" add nil) (lemma_div2n formula-decl nil shift nil) (add_lemma formula-decl nil add nil) (cauchy_exp const-decl "[nat -> int]" exp 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) (= const-decl "[T, T -> boolean]" equalities nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cauchy_neg const-decl "cauchy_real" neg nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (cauchy_exp_is_posreal application-judgement "cauchy_posreal" exp nil) (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/")) shostak)) (cauchy_sinh_type 0 (cauchy_sinh_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skosimp) (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (inst + "sinh(x!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sinh const-decl "real" hyperbolic "lnexp_fnd/") (sinh_lemma formula-decl nil hyperbolicx nil)) nil)) (cauchy_cosh_type 0 (cauchy_cosh_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skosimp) (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (expand "cauchy_posreal?") (("" (inst + "cosh(x!1)") (("1" (assert) nil nil) ("2" (typepred "cosh(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cauchy_posreal? const-decl "bool" cauchy nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (x!1 skolem-const-decl "real" hyperbolicx nil) (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/") (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (AND const-decl "[bool, bool -> bool]" booleans 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) (cosh_lemma formula-decl nil hyperbolicx nil)) nil)) (cauchy_coth_TCC1 0 (cauchy_coth_TCC1-1 nil 3394195229 ("" (skosimp) (("" (typepred "cnzx!1") (("" (expand "cauchy_nzreal?") (("" (skosimp) (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cnzx!1")) (("" (assert) (("" (inst + "sinh(x!1)") (("" (hide -1 -2) (("" (typepred "x!1") (("" (lemma "sinh_strict_increasing") (("" (expand "strict_increasing?") (("" (lemma "trichotomy" ("x" "x!1")) (("" (split -1) (("1" (inst - "0" "x!1") (("1" (rewrite "sinh_0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (inst - "x!1" "0") (("3" (rewrite "sinh_0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/") (trichotomy formula-decl nil real_axioms 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) (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (x!1 skolem-const-decl "nzreal" hyperbolicx nil) (sinh const-decl "real" hyperbolic "lnexp_fnd/") (sinh_lemma formula-decl nil hyperbolicx nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (tanh_lemma 0 (tanh_lemma-1 nil 3394198250 ("" (skosimp) (("" (expand "tanh") (("" (expand "cauchy_tanh") (("" (lemma "sinh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (lemma "div_lemma" ("x" "sinh(x!1)" "cx" "cauchy_sinh(cx!1)" "nzy" "cosh(x!1)" "nzcy" "cauchy_cosh(cx!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/") (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (sinh_lemma formula-decl nil hyperbolicx nil) (cauchy_cosh_type application-judgement "cauchy_posreal" hyperbolicx nil) (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_lemma formula-decl nil div nil) (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/") (sinh const-decl "real" hyperbolic "lnexp_fnd/") (cosh_lemma formula-decl nil hyperbolicx nil) (cauchy_tanh const-decl "[nat -> int]" hyperbolicx nil)) shostak)) (sech_lemma 0 (sech_lemma-1 nil 3394198358 ("" (skosimp) (("" (expand "sech") (("" (expand "cauchy_sech") (("" (lemma "cosh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (lemma "inv_lemma" ("nzx" "cosh(x!1)" "nzcx" "cauchy_cosh(cx!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sech const-decl "posreal_le1" hyperbolic "lnexp_fnd/") (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (cosh_lemma formula-decl nil hyperbolicx nil) (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/") (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (inv_lemma formula-decl nil inv nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cauchy_cosh_type application-judgement "cauchy_posreal" hyperbolicx nil) (cauchy_sech const-decl "[nat -> int]" hyperbolicx nil)) shostak)) (coth_lemma 0 (coth_lemma-1 nil 3394198526 ("" (skosimp) (("" (expand "cauchy_coth") (("" (expand "coth") (("" (lemma "sinh_lemma" ("x" "nzx!1" "cx" "cnzx!1")) (("" (lemma "cosh_lemma" ("x" "nzx!1" "cx" "cnzx!1")) (("" (assert) (("" (expand "tanh") (("" (rewrite "div_div1") (("1" (assert) (("1" (lemma "div_lemma" ("x" "cosh(nzx!1)" "cx" "cauchy_cosh(cnzx!1)" "nzy" "sinh(nzx!1)" "nzcy" "cauchy_sinh(cnzx!1)")) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "sinh_0") (("2" (lemma "sinh_strict_increasing") (("2" (expand "strict_increasing?") (("2" (lemma "trichotomy" ("x" "nzx!1")) (("2" (split -1) (("1" (inst - "0" "nzx!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (inst - "nzx!1" "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_coth const-decl "[nat -> int]" hyperbolicx nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (sinh_lemma formula-decl nil hyperbolicx nil) (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx nil) (cauchy_cosh_type application-judgement "cauchy_posreal" hyperbolicx nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cosh const-decl "posreal_ge1" hyperbolic "lnexp_fnd/") (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (sinh const-decl "real" hyperbolic "lnexp_fnd/") (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div1 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (div_lemma formula-decl nil div nil) (cauchy_cosh const-decl "[nat -> int]" hyperbolicx nil) (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil) (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (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) (trichotomy formula-decl nil real_axioms nil) (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/") (tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/") (cosh_lemma formula-decl nil hyperbolicx nil) (coth const-decl "real_abs_gt1" hyperbolic "lnexp_fnd/")) shostak)) (csch_lemma 0 (csch_lemma-1 nil 3394198422 ("" (skosimp) (("" (lemma "sinh_lemma" ("x" "nzx!1" "cx" "cnzx!1")) (("" (assert) (("" (expand "cauchy_csch") (("" (expand "csch") (("" (lemma "inv_lemma" ("nzx" "sinh(nzx!1)" "nzcx" "cauchy_sinh(cnzx!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (sinh_lemma formula-decl nil hyperbolicx nil) (cauchy_csch const-decl "[nat -> int]" hyperbolicx nil) (cauchy_sinh_type application-judgement "cauchy_real" hyperbolicx nil) (inv_lemma formula-decl nil inv nil) (cauchy_sinh const-decl "[nat -> int]" hyperbolicx nil) (sinh const-decl "real" hyperbolic "lnexp_fnd/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (csch const-decl "real" hyperbolic "lnexp_fnd/")) shostak)) (cauchy_tanh_type 0 (cauchy_tanh_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skosimp) (("" (lemma "tanh_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (typepred "tanh(x!1)") (("" (expand "cauchy_smallreal?") (("" (inst + "tanh(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cauchy_smallreal? const-decl "bool" cauchy nil) (smallreal nonempty-type-eq-decl nil prelude_aux nil) (tanh const-decl "real_abs_lt1" hyperbolic "lnexp_fnd/") (real_abs_lt1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (tanh_lemma formula-decl nil hyperbolicx nil)) nil)) (cauchy_coth_type 0 (cauchy_coth_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cnzx!1") (("" (expand "cauchy_nzreal?") (("" (skosimp) (("" (lemma "coth_lemma" ("nzx" "x!1" "cnzx" "cnzx!1")) (("" (assert) (("" (typepred "coth(x!1)") (("" (inst + "coth(x!1)") (("" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (x!1 skolem-const-decl "nzreal" hyperbolicx 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) (coth const-decl "real_abs_gt1" hyperbolic "lnexp_fnd/") (real_abs_gt1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (coth_lemma formula-decl nil hyperbolicx nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (cauchy_csch_type 0 (cauchy_csch_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cnzx!1") (("" (expand "cauchy_nzreal?") (("" (skosimp) (("" (lemma "csch_lemma" ("nzx" "x!1" "cnzx" "cnzx!1")) (("" (assert) (("" (inst + "csch(x!1)") (("" (hide -1 -2) (("" (expand "csch") (("" (lemma "sinh_strict_increasing") (("" (expand "strict_increasing?") (("" (lemma "trichotomy" ("x" "x!1")) (("" (split -1) (("1" (inst - "0" "x!1") (("1" (rewrite "sinh_0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (inst - "x!1" "0") (("3" (rewrite "sinh_0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sinh_strict_increasing formula-decl nil hyperbolic "lnexp_fnd/") (trichotomy formula-decl nil real_axioms nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sinh_0 formula-decl nil hyperbolic "lnexp_fnd/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (x!1 skolem-const-decl "nzreal" hyperbolicx nil) (csch const-decl "real" hyperbolic "lnexp_fnd/") (csch_lemma formula-decl nil hyperbolicx nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) nil)) (cauchy_sech_type 0 (cauchy_sech_type-1 nil 3394196253 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skosimp) (("" (lemma "sech_lemma" ("x" "x!1" "cx" "cx!1")) (("" (assert) (("" (expand "cauchy_posreal?") (("" (inst + "sech(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sech const-decl "posreal_le1" hyperbolic "lnexp_fnd/") (posreal_le1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (<= const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_posreal? const-decl "bool" cauchy nil) (sech_lemma formula-decl nil hyperbolicx nil)) nil)) (cauchy_ge1_TCC1 0 (cauchy_ge1_TCC1-1 nil 3394200357 ("" (expand "cauchy_ge1?") (("" (inst + "1") (("" (rewrite "int_lemma") nil nil)) nil)) 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (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) (int_lemma formula-decl nil int nil) (cauchy_ge1? const-decl "bool" hyperbolicx nil)) nil)) (subtype_TCC1 0 (subtype_TCC1-1 nil 3394200357 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_ge1?") (("" (skosimp) (("" (expand "cauchy_posreal?") (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil) (cauchy_ge1? const-decl "bool" hyperbolicx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_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) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_posreal? const-decl "bool" cauchy nil)) nil)) (cauchy_asinh_TCC1 0 (cauchy_asinh_TCC1-1 nil 3394199209 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real?") (("" (skosimp) (("" (expand "cauchy_nnreal?") (("" (lemma "mul_lemma" ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1")) (("" (assert) (("" (rewrite "sq_rew") (("" (lemma "add_lemma" ("x" "sq(x!1)" "y" "1" "cx" "cauchy_mul(cx!1, cx!1)" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (inst + "1+sq(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mul_lemma formula-decl nil mul nil) (sq_rew formula-decl nil sq "reals/") (int_lemma formula-decl nil int nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (add_lemma formula-decl nil add nil) (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_int const-decl "cauchy_real" int nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (cauchy_nnreal? const-decl "bool" cauchy nil)) nil)) (cauchy_asinh_TCC2 0 (cauchy_asinh_TCC2-1 nil 3508998299 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_posreal?") (("" (expand "cauchy_real?") (("" (skosimp) (("" (lemma "mul_lemma" ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1")) (("" (rewrite "sq_rew") (("" (assert) (("" (lemma "add_lemma" ("x" "sq(x!1)" "y" "1" "cx" "cauchy_mul(cx!1, cx!1)" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (case "1+sq(x!1)>=1") (("1" (lemma "sqrt_lemma" ("nnx" "1 + sq(x!1)" "nncx" "cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1))")) (("1" (assert) (("1" (lemma "add_lemma" ("x" "x!1" "y" "sqrt(1 + sq(x!1))" "cx" "cx!1" "cy" "cauchy_sqrt(cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1)))")) (("1" (assert) (("1" (inst + "sqrt(1 + sq(x!1)) + x!1") (("1" (hide-all-but (-3 1)) (("1" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "sqrt(1 + sq(x!1))")) (("1" (rewrite "sq_abs") (("1" (rewrite "sq_sqrt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cauchy_nnreal?") (("2" (inst + "1+sq(x!1)") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mul_lemma formula-decl nil mul nil) (int_lemma formula-decl nil int nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sq_abs formula-decl nil sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sq_lt formula-decl nil sq "reals/") (x!1 skolem-const-decl "real" hyperbolicx nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil) (nnreal type-eq-decl nil real_types nil) (cauchy_add const-decl "cauchy_real" add nil) (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (sqrt_lemma formula-decl nil sqrtx nil) (add_lemma formula-decl nil add nil) (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_int const-decl "cauchy_real" int nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (sq_rew formula-decl nil sq "reals/") (cauchy_posreal? const-decl "bool" cauchy nil)) nil)) (cauchy_acosh_TCC1 0 (cauchy_acosh_TCC1-2 nil 3508599835 ("" (skosimp) (("" (typepred "cge1x!1") (("" (expand "cauchy_ge1?") (("" (skosimp) (("" (typepred "x!1") (("" (lemma "sub_lemma" ("x" "sq(x!1)" "y" "1" "cx" "cauchy_mul(cge1x!1, cge1x!1)" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (expand "sq" -1 1) (("" (rewrite "mul_lemma") (("" (expand "cauchy_nnreal?") (("" (inst + "sq(x!1)-1") (("" (lemma "sq_le" ("nna" "1" "nnb" "x!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil) (cauchy_ge1? const-decl "bool" hyperbolicx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (sub_lemma formula-decl nil sub nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (sq_le formula-decl nil sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (x!1 skolem-const-decl "posreal_ge1" hyperbolicx nil) (nnreal type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mul_lemma formula-decl nil mul nil) (int_lemma formula-decl nil int nil) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")) nil) (cauchy_acosh_TCC1-1 nil 3394200357 ("" (skosimp) (("" (typepred "cge1x!1") (("" (expand "cauchy_ge1?") (("" (skosimp) (("" (lemma "mul_lemma" ("x" "x!1" "cx" "cge1x!1" "y" "x!1" "cy" "cge1x!1")) (("" (rewrite "sq_rew") (("" (assert) (("" (lemma "sub_lemma" ("x" "sq(x!1)" "cx" "cauchy_mul(cge1x!1, cge1x!1)" "y" "1" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (expand "cauchy_nnreal?") (("" (inst + "sq(x!1)-1") (("" (hide-all-but 1) (("" (typepred "x!1") (("" (lemma "sq_le" ("nna" "1" "nnb" "x!1")) (("" (rewrite "sq_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_rew formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (cauchy_int const-decl "cauchy_real" int nil) (cauchy_mul const-decl "cauchy_real" mul nil) (sub_lemma formula-decl nil sub nil) (sq_1 formula-decl nil sq "reals/") (sq_le formula-decl nil sq "reals/") (cauchy_nnreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (mul_lemma formula-decl nil mul nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")) nil)) (cauchy_acosh_TCC2 0 (cauchy_acosh_TCC2-1 nil 3508998299 ("" (skosimp) (("" (typepred "cge1x!1") (("" (expand "cauchy_ge1?") (("" (skosimp) (("" (typepred "x!1") (("" (lemma "sub_lemma" ("x" "sq(x!1)" "y" "1" "cx" "cauchy_mul(cge1x!1, cge1x!1)" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (expand "sq" -1 1) (("" (rewrite "mul_lemma") (("" (case "sq(x!1)-1>=0") (("1" (lemma "sqrt_lemma" ("nnx" "sq(x!1)-1" "nncx" "cauchy_sub(cauchy_mul(cge1x!1, cge1x!1), cauchy_int(1))")) (("1" (assert) (("1" (lemma "add_lemma" ("x" "x!1" "cx" "cge1x!1" "y" "sqrt(sq(x!1) - 1)" "cy" "cauchy_sqrt(cauchy_sub(cauchy_mul(cge1x!1, cge1x!1), cauchy_int(1)))")) (("1" (assert) (("1" (expand "cauchy_posreal?") (("1" (inst + "sqrt(sq(x!1) - 1) + x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (lemma "sq_le" ("nna" "1" "nnb" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ge1 nonempty-type-eq-decl nil hyperbolicx nil) (cauchy_ge1? const-decl "bool" hyperbolicx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (sub_lemma formula-decl nil sub nil) (real_minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (cauchy_posreal? const-decl "bool" cauchy nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil) (add_lemma formula-decl nil add nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_lemma formula-decl nil sqrtx nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil) (cauchy_sub const-decl "cauchy_real" sub nil) (nnreal type-eq-decl nil real_types nil) (sq_1 formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_le formula-decl nil sq "reals/") (mul_lemma formula-decl nil mul nil) (int_lemma formula-decl nil int nil) (posreal_ge1 nonempty-type-eq-decl nil hyperbolic "lnexp_fnd/")) nil)) (cauchy_atanh_TCC1 0 (cauchy_atanh_TCC1-1 nil 3394199209 ("" (skosimp) (("" (typepred "csx!1") (("" (expand "cauchy_smallreal?") (("" (skosimp) (("" (typepred "sx!1") (("" (lemma "sub_lemma" ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy" "csx!1")) (("" (rewrite "int_lemma") (("" (assert) (("" (expand "cauchy_nzreal?") (("" (inst + "1-sx!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_smallreal nonempty-type-eq-decl nil cauchy nil) (cauchy_smallreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (sub_lemma formula-decl nil sub nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_lemma formula-decl nil int nil) (smallreal nonempty-type-eq-decl nil prelude_aux nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil)) nil)) (cauchy_atanh_TCC2 0 (cauchy_atanh_TCC2-1 nil 3394199209 ("" (skosimp) (("" (typepred "csx!1") (("" (expand "cauchy_smallreal?") (("" (skosimp) (("" (typepred "sx!1") (("" (lemma "add_lemma" ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy" "csx!1")) (("" (lemma "sub_lemma" ("x" "1" "cx" "cauchy_int(1)" "y" "sx!1" "cy" "csx!1")) (("" (rewrite "int_lemma") (("" (assert) (("" (lemma "div_lemma" ("x" "1+sx!1" "cx" "cauchy_add(cauchy_int(1), csx!1)" "nzy" "1 - sx!1" "nzcy" "cauchy_sub(cauchy_int(1), csx!1)")) (("" (assert) (("" (expand "cauchy_posreal?") (("" (inst + "(1 + sx!1) / (1 - sx!1)") (("" (assert) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1 + sx!1" "py" "1 - sx!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_smallreal nonempty-type-eq-decl nil cauchy nil) (cauchy_smallreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (add_lemma formula-decl nil add nil) (int_lemma formula-decl nil int nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_sub const-decl "cauchy_real" sub nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_add const-decl "cauchy_real" add nil) (div_lemma formula-decl nil div nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cauchy_posreal? const-decl "bool" cauchy nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (sx!1 skolem-const-decl "smallreal" hyperbolicx 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) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sub_lemma formula-decl nil sub nil) (smallreal nonempty-type-eq-decl nil prelude_aux nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil)) nil)) (asinh_lemma 0 (asinh_lemma-1 nil 3394201044 ("" (skosimp) (("" (expand "cauchy_asinh") (("" (expand "asinh") (("" (lemma "mul_lemma" ("x" "x!1" "cx" "cx!1" "y" "x!1" "cy" "cx!1")) (("" (assert) (("" (rewrite "sq_rew") (("" (lemma "add_lemma" ("x" "sq(x!1)" "cx" "cauchy_mul(cx!1, cx!1)" "y" "1" "cy" "cauchy_int(1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (lemma "sqrt_lemma" ("nnx" "1 + sq(x!1)" "nncx" "cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1))")) (("1" (assert) (("1" (lemma "add_lemma" ("x" "x!1" "cx" "cx!1" "y" "sqrt(1 + sq(x!1))" "cy" "cauchy_sqrt(cauchy_add(cauchy_mul(cx!1, cx!1), cauchy_int(1)))")) (("1" (assert) (("1" (lemma "ln_lemma" ("px" "sqrt(1 + sq(x!1)) + x!1" "pcx" "cauchy_add(cx!1, cauchy_sqrt(cauchy_add (cauchy_mul(cx!1, cx!1), cauchy_int(1))))")) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "sqrt_lt" ("nny" "sq(x!1)" "nnz" "1+sq(x!1)")) (("2" (case "x!1>=0") (("1" (rewrite "sqrt_sq") (("1" (assert) nil nil)) nil) ("2" (rewrite "sqrt_sq_neg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cauchy_nnreal?") (("2" (inst + "1+sq(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_asinh const-decl "[nat -> int]" hyperbolicx nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.87 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.Bot Zugriff |
