|
(expt (doublecaret_TCC1 0
(doublecaret_TCC1-1 nil 3297432002 ("" (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)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal 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))
shostak))
(hathat_sum_TCC1 0
(hathat_sum_TCC1-1 nil 3297443439
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_sum_TCC2 0
(hathat_sum_TCC2-1 nil 3297443439
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_sum 0
(hathat_sum-1 nil 3297442437
("" (skosimp*)
(("" (expand "^^")
(("" (rewrite "exp_sum") (("" (assert) nil nil)) nil)) nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(ln const-decl "real" ln_exp 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields 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_sum formula-decl nil ln_exp nil))
shostak))
(hathat_diff_TCC1 0
(hathat_diff_TCC1-1 nil 3297443439
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_diff_TCC2 0
(hathat_diff_TCC2-1 nil 3297443439
("" (skosimp*)
(("" (assert) (("" (expand "^^") (("" (assert) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt nil))
shostak))
(hathat_diff 0
(hathat_diff-1 nil 3297443002
("" (skosimp*)
(("" (expand "^^")
(("" (rewrite "exp_diff") (("" (assert) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(ln const-decl "real" ln_exp 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields 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_diff formula-decl nil ln_exp nil))
shostak))
(hathat_to_0_TCC1 0
(hathat_to_0_TCC1-1 nil 3302517721 ("" (subtype-tcc) nil nil)
nil shostak))
(hathat_to_0 0
(hathat_to_0-1 nil 3302517403
("" (skosimp*)
(("" (expand "^^") (("" (rewrite "exp_0") nil nil)) nil)) nil)
((^^ const-decl "nnreal" expt nil)
(exp_0 formula-decl nil ln_exp nil))
shostak))
(hathat_to_1_TCC1 0
(hathat_to_1_TCC1-1 nil 3302349197
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_to_1 0
(hathat_to_1-1 nil 3302349243
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "exp_ln")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((^^ const-decl "nnreal" expt 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(exp_ln formula-decl nil ln_exp nil))
shostak))
(hathat_0 0
(hathat_0-1 nil 3302517475
("" (skosimp*) (("" (expand "^^") (("" (propax) nil nil)) nil))
nil)
((^^ const-decl "nnreal" expt nil)) shostak))
(hathat_1 0
(hathat_1-1 nil 3297443317
("" (skosimp*)
(("" (expand "^^")
(("" (rewrite "ln_1") (("" (rewrite "exp_0") nil nil)) nil))
nil))
nil)
((^^ const-decl "nnreal" expt nil)
(exp_0 formula-decl nil ln_exp nil)
(ln_1 formula-decl nil ln_exp nil))
shostak))
(hathat_nat_TCC1 0
(hathat_nat_TCC1-1 nil 3302349197
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_nat 0
(hathat_nat-2 nil 3302349079
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "^")
(("1" (expand "^^")
(("1" (assert)
(("1" (rewrite "exp_0")
(("1" (expand "expt") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "hathat_sum")
(("2" (inst - "a!1" "j!1" "1")
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "hathat_to_1")
(("2" (inst?)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "^")
(("2" (expand "expt" 1 2)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((hathat_to_1 formula-decl nil expt nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(hathat_sum formula-decl nil expt nil)
(expt def-decl "real" exponentiation nil)
(exp_0 formula-decl nil ln_exp nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(nzreal_expt application-judgement "nzreal" exponentiation
nil)
(posreal_expt application-judgement "posreal" exponentiation
nil)
(nat_induction formula-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(^^ const-decl "nnreal" expt nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(pred type-eq-decl nil defined_types 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))
nil)
(hathat_nat-1 nil 3297442087
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "^")
(("1" (expand "^^")
(("1" (assert)
(("1" (rewrite "exp_0")
(("1" (expand "expt") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "hathat_sum")
(("2" (inst - "a!1" "j!1" "1")
(("2" (replace -1)
(("2" (hide -1)
(("2" (rewrite "hathat_1")
(("2" (inst?)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "^")
(("2" (expand "expt" 1 2)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((exp_0 formula-decl nil ln_exp nil)) shostak))
(hathat_lt_cross_TCC1 0
(hathat_lt_cross_TCC1-1 nil 3302017432
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_lt_cross_TCC2 0
(hathat_lt_cross_TCC2-1 nil 3302017432
("" (skosimp*) (("" (assert) nil nil)) nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(hathat_lt_cross 0
(hathat_lt_cross-3 nil 3302350027
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "ln_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "exp((1 / px!1) * ln(a!1))" "b!1")
(("" (assert)
(("" (rewrite "ln_exp")
(("" (mult-by -1 "px!1")
(("" (assert)
(("" (lemma "exp_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "ln(a!1)" "ln(b!1) * px!1")
((""
(assert)
((""
(rewrite "exp_ln")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(^^ const-decl "nnreal" expt nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(exp_strict_increasing formula-decl nil ln_exp nil)
(exp_ln formula-decl nil ln_exp nil)
(ln_exp formula-decl nil ln_exp nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln const-decl "real" ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(>= 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)
(real_times_real_is_real application-judgement "real" reals
nil)
(ln_strict_increasing formula-decl nil ln_exp nil))
nil)
(hathat_lt_cross-2 nil 3302349847
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "ln_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "exp((1 / nzx!1) * ln(a!1))" "b!1")
(("" (assert)
(("" (rewrite "ln_exp")
(("" (mult-by -1 "nzx!1")
(("" (assert)
(("" (lemma "exp_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "ln(a!1)" "ln(b!1) * nzx!1")
((""
(assert)
((""
(rewrite "exp_ln")
((""
(assert)
nil))))))))))))))))))))))))))))
nil)
((ln_strict_increasing formula-decl nil ln_exp nil)
(ln const-decl "real" ln_exp nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln_exp formula-decl nil ln_exp nil)
(exp_ln formula-decl nil ln_exp nil)
(exp_strict_increasing formula-decl nil ln_exp nil)
(strict_increasing? const-decl "bool" real_fun_preds
"reals/"))
nil)
(hathat_lt_cross-1 nil 3301933156
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "ln_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "exp((1 / px!1) * ln(a!1))" "b!1")
(("" (assert)
(("" (rewrite "ln_exp")
(("" (mult-by -1 "px!1")
(("" (assert)
(("" (lemma "exp_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "ln(a!1)" "ln(b!1) * px!1")
((""
(assert)
((""
(rewrite "exp_ln")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((strict_increasing? const-decl "bool" real_fun_preds "reals/")
(exp_strict_increasing formula-decl nil ln_exp nil)
(exp_ln formula-decl nil ln_exp nil)
(ln_exp formula-decl nil ln_exp nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln const-decl "real" ln_exp nil)
(ln_strict_increasing formula-decl nil ln_exp nil))
nil))
(hathat_gt_cross_TCC1 0
(hathat_gt_cross_TCC1-1 nil 3302017433
("" (skosimp*) (("" (assert) nil nil)) nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(hathat_gt_cross 0
(hathat_gt_cross-1 nil 3301932936
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "ln_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "b!1" "exp((1 / px!1) * ln(a!1))")
(("" (assert)
(("" (rewrite "ln_exp")
(("" (mult-by -1 "px!1")
(("" (assert)
(("" (lemma "exp_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "ln(b!1) * px!1" "ln(a!1)")
((""
(assert)
((""
(rewrite "exp_ln")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(^^ const-decl "nnreal" expt nil)
(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)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(exp_strict_increasing formula-decl nil ln_exp nil)
(exp_ln formula-decl nil ln_exp nil)
(ln_exp formula-decl nil ln_exp nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln const-decl "real" ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(>= 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)
(real_times_real_is_real application-judgement "real" reals
nil)
(ln_strict_increasing formula-decl nil ln_exp nil))
shostak))
(hathat_eq_0_TCC1 0
(hathat_eq_0_TCC1-1 nil 3302517721 ("" (subtype-tcc) nil nil)
nil shostak))
(hathat_eq_0 0
(hathat_eq_0-1 nil 3302517739
("" (skosimp*) (("" (expand "^^") (("" (assert) nil nil)) nil))
nil)
((^^ const-decl "nnreal" expt nil)
(real_times_real_is_real application-judgement "real" reals
nil))
shostak))
(hathat_eq_1_TCC1 0
(hathat_eq_1_TCC1-1 nil 3302618459
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(hathat_eq_1 0
(hathat_eq_1-1 nil 3302617949
("" (skosimp*)
(("" (expand "^^")
(("" (prop)
(("1" (lemma "exp_strict_increasing")
(("1" (expand "strict_increasing?")
(("1" (inst-cp - "0" "x!1 * ln(px!1)")
(("1" (inst - "x!1 * ln(px!1)" "0")
(("1" (ground)
(("1" (typepred "ln(px!1)")
(("1" (lemma "ln_eq_0")
(("1" (inst - "px!1")
(("1" (case-replace "ln(px!1) = 0")
(("1"
(assert)
(("1"
(mult-by 1 "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (rewrite "exp_0") nil nil)) nil)
("3" (replace -1)
(("3" (rewrite "ln_1") (("3" (rewrite "exp_0") nil nil))
nil))
nil))
nil))
nil))
nil)
((^^ const-decl "nnreal" expt nil)
(ln_1 formula-decl nil ln_exp nil)
(exp_strict_increasing formula-decl nil ln_exp nil)
(real_times_real_is_real application-judgement "real" reals
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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
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)
(ln const-decl "real" ln_exp nil)
(exp_0 formula-decl nil ln_exp nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ln_eq_0 formula-decl nil ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(both_sides_times1 formula-decl nil real_props nil)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(strict_increasing? const-decl "bool" real_fun_preds
"reals/"))
shostak))
(hathat_cross_TCC1 0
(hathat_cross_TCC1-1 nil 3340380990 ("" (subtype-tcc) nil nil)
((ln const-decl "real" ln_exp nil)
(^^ const-decl "nnreal" expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil))
nil))
(hathat_cross 0
(hathat_cross-1 nil 3340381050
("" (skeep)
(("" (lemma "hathat_lt_cross")
(("" (lemma "hathat_gt_cross")
(("" (inst -1 b a 1/px)
(("" (inst -2 b a 1/px) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((hathat_lt_cross formula-decl nil expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
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)
(hathat_gt_cross formula-decl nil expt nil))
nil))
(hathat_mult_TCC1 0
(hathat_mult_TCC1-1 nil 3340380990 ("" (subtype-tcc) nil nil)
nil nil))
(hathat_mult_TCC2 0
(hathat_mult_TCC2-1 nil 3340380990 ("" (subtype-tcc) nil nil)
((ln const-decl "real" ln_exp nil)
(^^ const-decl "nnreal" expt nil))
nil))
(hathat_mult_TCC3 0
(hathat_mult_TCC3-1 nil 3340380990 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(hathat_mult 0
(hathat_mult-1 nil 3340381085
("" (skeep)
(("" (expand ^^)
(("" (case "exp(px*ln(a))=0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ln const-decl "real" ln_exp nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(hathat_div_TCC1 0
(hathat_div_TCC1-1 nil 3302279507
("" (skosimp*) (("" (assert) nil nil)) nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil))
shostak))
(hathat_div_TCC2 0
(hathat_div_TCC2-1 nil 3302279507
("" (skosimp*)
(("" (lemma "hathat_eq_0")
(("" (inst?)
(("1" (assert) nil nil)
("2" (flatten)
(("2" (replace -1) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((hathat_eq_0 formula-decl nil expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(Integral const-decl "real" integral_def "analysis/")
(ln const-decl "real" ln_exp nil)
(^^ const-decl "nnreal" expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(exp_0 formula-decl nil ln_exp nil)
(nzreal nonempty-type-eq-decl nil 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal 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)
(x!1 skolem-const-decl "real" expt nil))
shostak))
(hathat_div 0
(hathat_div-2 nil 3302350053
("" (skosimp*)
(("" (expand "^^")
(("" (rewrite "ln_div")
(("" (assert)
(("" (rewrite "exp_diff") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((^^ const-decl "nnreal" expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(exp_diff formula-decl nil ln_exp nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(ln const-decl "real" ln_exp nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_times_real_is_real application-judgement "real" 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)
(>= 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)
(ln_div formula-decl nil ln_exp nil))
nil)
(hathat_div-1 nil 3302277568
("" (skosimp*)
(("" (expand "^^")
(("" (rewrite "ln_div")
(("" (assert)
(("" (rewrite "exp_diff") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((ln const-decl "real" ln_exp nil)
(exp_diff formula-decl nil ln_exp nil)
(ln_div formula-decl nil ln_exp nil))
nil))
(hathat_abs_TCC1 0
(hathat_abs_TCC1-1 nil 3302017457
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonzero_abs_is_pos application-judgement
"{y: posreal | y >= x}" real_defs nil))
shostak))
(hathat_abs 0
(hathat_abs-1 nil 3301933515
("" (skosimp*)
(("" (expand "^^")
(("" (lift-if)
(("" (prop)
(("1" (lemma "abs_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "abs")
(("2" (assert)
(("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((^^ const-decl "nnreal" expt 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonzero_abs_is_pos application-judgement
"{y: posreal | y >= x}" real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_eq_0 formula-decl nil abs_lems "reals/")
(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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
shostak))
(hathat_sum_posreal_TCC1 0
(hathat_sum_posreal_TCC1-1 nil 3340381142
("" (subtype-tcc) nil nil) nil nil))
(hathat_sum_posreal 0
(hathat_sum_posreal-1 nil 3340381166
("" (skeep)
(("" (expand ^^)
(("" (rewrite "exp_sum") (("" (assert) nil nil)) nil)) nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(ln const-decl "real" ln_exp 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields 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_sum formula-decl nil ln_exp nil))
nil))
(hathat_diff_posreal_TCC1 0
(hathat_diff_posreal_TCC1-1 nil 3340381142
("" (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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals 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)
(real_times_real_is_real application-judgement "real" reals
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(ln const-decl "real" ln_exp nil)
(^^ const-decl "nnreal" expt nil))
nil))
(hathat_diff_posreal_TCC2 0
(hathat_diff_posreal_TCC2-1 nil 3340381142
("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(hathat_diff_posreal 0
(hathat_diff_posreal-1 nil 3340381209
("" (skeep)
(("" (expand ^^)
(("" (rewrite "exp_diff") (("" (assert) nil nil)) nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals
nil)
(^^ const-decl "nnreal" expt nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(ln const-decl "real" ln_exp 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields 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_diff formula-decl nil ln_exp nil))
nil))
(hathat_cont 0
(hathat_cont-3 nil 3445353939
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "composition_cont_fun[real,real]")
(("" (inst - "(LAMBDA x: x * ln(a!1))" "exp")
(("" (expand "o ")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (lemma "x_to_n_continuous[real]")
(("1" (inst - "1")
(("1" (expand "^")
(("1" (expand "expt")
(("1"
(expand "expt")
(("1"
(lemma "scal_continuous[real]")
(("1"
(inst?)
(("1"
(expand "continuous?" 1)
(("1"
(skosimp*)
(("1"
(inst - "ln(a!1)" "x0!1")
(("1"
(assert)
(("1"
(expand "*")
(("1"
(hide 2)
(("1"
(expand
"continuous?"
-1)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "exp_continuous")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^^ const-decl "nnreal" expt nil)
(real_times_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)
(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)
(ln const-decl "real" ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(expt def-decl "real" exponentiation nil)
(scal_continuous formula-decl nil continuous_functions
"analysis/")
(continuous? const-decl "bool" continuous_functions
"analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(^ const-decl "real" exponentiation nil)
(x_to_n_continuous formula-decl nil continuous_functions
"analysis/")
(exp_continuous formula-decl nil ln_exp nil)
(O const-decl "T3" function_props nil)
(composition_cont_fun formula-decl nil composition_continuous
"analysis/")
(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))
nil)
(hathat_cont-2 nil 3302350539
("" (skosimp*)
(("" (expand "^^")
(("" (lemma "composition_cont_fun[real,real]")
(("" (inst - "(LAMBDA x: x * ln(a!1))" "exp")
(("" (expand "o ")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (lemma "x_to_n_continuous[real]")
(("1" (inst - "1")
(("1" (expand "^")
(("1" (expand "expt")
(("1"
(expand "expt")
(("1"
(lemma "scal_continuous[real]")
(("1"
(inst?)
(("1"
(expand "continuous?" 1)
(("1"
(skosimp*)
(("1"
(inst - "ln(a!1)" "x0!1")
(("1"
(assert)
(("1"
(expand "*")
(("1"
(hide 2)
(("1"
(expand
"continuous"
-1)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "exp_continuous")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ln const-decl "real" ln_exp nil)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(scal_continuous formula-decl nil continuous_functions
"analysis/")
(x_to_n_continuous formula-decl nil continuous_functions
"analysis/")
(exp_continuous formula-decl nil ln_exp nil)
(composition_cont_fun formula-decl nil composition_continuous
"analysis/"))
nil)
(hathat_cont-1 nil 3302350526 ("" (postpone) nil nil) nil
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.54Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
