(expt (doublecaret_TCC1 0nil 3297432002 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3297443439"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3297443439"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3297442437"" (skosimp*)"" (expand "^^" )"" (rewrite "exp_sum" ) (("" (assert ) nil nil )) nil )) nil ))nil )"real" realsnil )"nnreal" expt nil )"posreal" real_types nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil ln_exp nil ))nil 3297443439"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3297443439"" (skosimp*)"" (assert ) (("" (expand "^^" ) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"nnreal" expt nil ))nil 3297443002"" (skosimp*)"" (expand "^^" )"" (rewrite "exp_diff" ) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"nnreal" expt nil )"posreal" real_types nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil ln_exp nil ))nil 3302517721 ("" (subtype-tcc) nil nil )nil shostak))nil 3302517403"" (skosimp*)"" (expand "^^" ) (("" (rewrite "exp_0" ) nil nil )) nil )) nil )"nnreal" expt nil )nil ln_exp nil ))nil 3302349197"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3302349243"" (skosimp*)"" (expand "^^" )"" (lemma "exp_ln" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"nnreal" expt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" realsnil )nil ln_exp nil ))nil 3302517475"" (skosimp*) (("" (expand "^^" ) (("" (propax) nil nil )) nil ))nil )"nnreal" expt nil )) shostak))nil 3297443317"" (skosimp*)"" (expand "^^" )"" (rewrite "ln_1" ) (("" (rewrite "exp_0" ) nil nil )) nil ))nil ))nil )"nnreal" expt nil )nil ln_exp nil )nil ln_exp nil ))nil 3302349197"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))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 )nil expt nil )"posint" nil )"int" integersnil )nil expt nil )"real" exponentiation nil )nil ln_exp nil )"real" realsnil )"nzreal" exponentiationnil )"posreal" exponentiationnil )nil naturalnumbers nil )"real" exponentiation nil )"nnreal" expt nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil )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 )nil ln_exp nil )) shostak))nil 3302017432"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3302017432"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil ))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" real_types nil )"nnreal" expt nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil ln_exp nil )nil ln_exp nil )nil ln_exp nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil )nil ln_exp nil ))nil )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 )nil ln_exp nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil ln_exp nil )nil ln_exp nil )nil ln_exp nil )"bool" real_fun_preds"reals/" ))nil )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 )"bool" real_fun_preds "reals/" )nil ln_exp nil )nil ln_exp nil )nil ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil ln_exp nil ))nil ))nil 3302017433"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil ))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" real_types nil )"nnreal" expt nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil ln_exp nil )nil ln_exp nil )nil ln_exp nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil )nil ln_exp nil ))nil 3302517721 ("" (subtype-tcc) nil nil )nil shostak))nil 3302517739"" (skosimp*) (("" (expand "^^" ) (("" (assert ) nil nil )) nil ))nil )"nnreal" expt nil )"real" realsnil ))nil 3302618459"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))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" "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 )"nnreal" expt nil )nil ln_exp nil )nil ln_exp nil )"real" realsnil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp nil )nil ln_exp nil )"(strict_total_order?[real])" real_props nil )nil ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"boolean" notequal nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" real_fun_preds"reals/" ))nil 3302279507"" (skosimp*) (("" (assert ) nil nil )) nil )"posreal" real_types nil ))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 )nil expt nil )nil ln_exp nil )"nnreal" expt nil )"real" realsnil )nil reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil numbers nil )nil booleans nil )"boolean" notequal nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" expt nil ))nil 3302350053"" (skosimp*)"" (expand "^^" )"" (rewrite "ln_div" )"" (assert )"" (rewrite "exp_diff" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nnreal" expt nil )"posreal" real_types nil )nil ln_exp nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"real" ln_exp nil )"real" realsnil )"real" realsnil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil ln_exp nil ))nil )nil 3302277568"" (skosimp*)"" (expand "^^" )"" (rewrite "ln_div" )"" (assert )"" (rewrite "exp_diff" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real" ln_exp nil )nil ln_exp nil )nil ln_exp nil ))nil ))nil 3302017457"" (skosimp*) (("" (assert ) nil nil )) nil )"{y: posreal | y >= x}" real_defs nil ))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 )"nnreal" expt nil )"{y: posreal | y >= x}" real_defs nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" nil ))quality 100%
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
