| products/Sources/formale Sprachen/PVS/lnexp/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: expt.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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_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) (exp_0 formula-decl nil ln_exp nil) (^^ const-decl "nnreal" expt nil) (real_times_real_is_real application-judgement "real" reals 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) ((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) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak))) ¤ Dauer der Verarbeitung: 0.12 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 |
