Impressum nnreal_expt.prf
Interaktion und
(nnreal_exptnil 3427171289"" (skosimp)"" (case "y!1>0" )"1" (hide 1 2)"1" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "extend" )"1" (expand "member" )"1" (lemma "density_positive" ("x" "0" "y" "y!1" ))"1" (assert )"1" (skosimp)"1" (inst - "nn_rational_expt(x!1, r!1)" )"1" (typepred "nn_rational_expt(x!1, r!1)" )"1" (assert )"1" "r!1" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_below?" )"2" (inst + "0" )"2" (expand "lower_bound?" )"2" (skosimp)"2" (typepred "s!1" )"2" (expand "extend" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[real -> boolean]" rationals nil )nil rationals nil )"rat" nnreal_expt nil )"nnreal" nn_rational_expt nil )nil rationals nil )nil rationals nil )NOT const-decl "[bool -> bool]" booleans nil )nil rational_props nil )"R" extend nil )"bool" sets nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil ))nil ))nil 3427171289"" (skosimp)"" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "" (expand "greatest_lower_bound?" )"" (flatten)"" (inst - "0" )"" (assert )"" (hide -1 4)"" (expand "lower_bound?" )"" (skosimp)"" (typepred "s!1" )"" (assert )"" (expand "extend" )"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nn_rational_expt nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )"R" extend nil )"bool" booleans nil )nil real_types nil )"bool" reals nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"bool" bounded_real_defs nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3427223359"" (skosimp*)"" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "extend" )"1" (expand "member" )"1" (lemma "density_positive" ("x" "0" "y" "y!1" ))"1" (assert )"1" (skosimp)"1" (inst - "nn_rational_expt(x!1, r!1)" )"1" (typepred "nn_rational_expt(x!1, r!1)" )"1" (assert )"1" (inst + "r!1" ) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_above?" )"2" (expand "extend" )"2" (expand "upper_bound?" )"2" (lemma "density_positive" ("x" "y!1" "y" "y!1+1" ))"2" (assert )"2" (skosimp)"2" (inst + "nn_rational_expt(x!1, r!1)" )"1" (skosimp)"1" (typepred "s!1" )"1" (assert )"1" (skosimp)"1" (replace -2)"1" "nn_rational_expt_increasing" "q" "q!1" "r" "r!1" "x" "x!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[real -> boolean]" rationals nil )nil rationals nil )"rat" nnreal_expt nil )"nnreal" nn_rational_expt nil )nil rationals nil )nil rationals nil )NOT const-decl "[bool -> bool]" booleans nil )nil rational_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"R" extend nil )"bool" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posreal" nil )"posreal" nil )nil nn_rational_expt nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"rat" nnreal_expt nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil ))nil ))nil 3427223359"" (skosimp*)"" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "" (expand "least_upper_bound?" )"" (flatten)"" (hide -2)"" (expand "upper_bound?" )"" (inst - "nn_rational_expt(x!1, 0)" )"1" (typepred "nn_rational_expt(x!1, 0)" )"1" (assert ) nil nil )) nil )"2" (expand "extend" )"2" (typepred "nn_rational_expt(x!1, 0)" )"2" (assert )"2" (inst + "0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nn_rational_expt nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )"R" extend nil )"bool" booleans nil )nil real_types nil )"bool" reals nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nnreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" bounded_real_defs nil ))nil ))nil 3427179456"" (skosimp)"" (case-replace "q!1=0" )"1" (expand "nnreal_expt" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (grind) nil nil )) nil ))nil )"2" (case "q!1>0" )"1" (hide 1)"1" (expand "nnreal_expt" )"1" (case-replace "x!1=1" )"1" (rewrite "nn_rational_expt_1q" ) nil nil )"2" (case-replace "x!1<1" )"1" (assert )"1" (hide 1)"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (expand "greatest_lower_bound?" )"1" (flatten)"1" (inst - "nn_rational_expt(x!1, q!1)" )"1" "1" expand "lower_bound?" )"1" "nn_rational_expt(x!1, q!1)" )"1" (assert ) nil nil )"2" expand "extend" )"2" "q!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "lower_bound?" )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" expand "<=" -2)"2" replace -3)"2" "2" "1" "x!1=0" )"1" assert )"1" "q!2=0" )"1" assert )"1" rewrite "nn_rational_expt_0q" )"1" rewrite "nn_rational_expt_0q" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "nn_rational_expt_0q" )"2" rewrite "nn_rational_expt_0q" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "x!1>0" )"1" "1" "nn_rational_expt_decreasing" "q" "q!2" "r" "q!1" "x" "x!1" ))"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "x!1>1" )"1" (hide 1 2)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (expand "least_upper_bound?" )"1" (flatten)"1" "nn_rational_expt(x!1, q!1)" )"1" "1" expand "upper_bound?" )"1" "nn_rational_expt(x!1, q!1)" )"1" (assert ) nil nil )"2" expand "extend" )"2" "q!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace -3)"2" "2" expand "<=" -1)"2" "1" "nn_rational_expt_increasing" "q" "q!2" "r" "q!1" "x" "x!1" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )nil booleans nil )"bool" reals nil )nil rationals nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil real_types nil )"nnreal" exponentiation nil )"(total_order?[real])" nil )"nnreal" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"nnreal" nnreal_expt nil )nil nn_rational_expt nil )"bool" bounded_real_defs nil )nil nn_rational_expt nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nn_rational_expt nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"R" extend nil )"bool" booleans nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil nn_rational_expt nil )nil nn_rational_expt nil )"bool" bounded_real_defs nil )"(total_order?[real])" nil )"nnreal" nnreal_expt nil )"nnrat" nnreal_expt nil )"bool" reals nil ) (> const-decl "bool" reals nil ))nil 3428161604 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3428161605"" (skosimp)"" (rewrite "nnreal_expt_rat_rew" )"" (rewrite "nn_rational_expt_nat_rew" ) nil nil )) nil ))nil )nil nnreal_expt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )nil booleans nil )"bool" reals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil real_types nil )nil nn_rational_expt nil ))nil 3428161631"" (skosimp)"" (rewrite "nnreal_expt_rat_rew" )"" (rewrite "nn_rational_expt_root_rew" ) nil nil )) nil ))nil )"posrat" nil )nil nnreal_expt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )nil booleans nil )"bool" reals nil )nil rationals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil real_types nil )nil nn_rational_expt nil ))nil 3427304632"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_0q" ) nil nil )) nil )"2" (assert )"2" (case "a!1>0" )"1" (hide 1)"1" (expand "nnreal_expt" )"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(0, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(0, q)}))") "1" (expand "greatest_lower_bound?" )"1" (flatten)"1" (expand "lower_bound?" )"1" (inst - "0" )"1" (inst - "0" )"1" (split -2)"1" (assert ) nil nil )"2" "2" "s!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (hide -1 2)"2" "density_positive" "x" "0" "y" "a!1" ))"2" assert )"2" "2" "r!1" )"1" assert )"1" rewrite "nn_rational_expt_0q" )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nn_rational_expt nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"bool" reals nil )"nnreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil rationals nil )"rat" nnreal_expt nil )nil rational_props nil )"bool" bounded_real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" booleans nil )"R" extend nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nnreal" nn_rational_expt nil ))nil 3427304898"" (skosimp)"" (expand "nnreal_expt" ) (("" (propax) nil nil )) nil )) nil )"nnreal" nnreal_expt nil )) shostak))nil 3427304910"" (skosimp)"" (rewrite "nnreal_expt_rat_rew" )"" (rewrite "nn_rational_expt_nat_rew" )"" (ground) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil nnreal_expt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )nil booleans nil )"bool" reals nil )nil rationals nil )nil real_types nil )"(total_order?[real])" nil )"nnreal" exponentiation nil )"nnreal" nil )"real" exponentiation nil )"real" exponentiation nil )"nnreal" exponentiation nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil nn_rational_expt nil ))nil 3427306409"" (skosimp)"" (expand "nnreal_expt" )"" (case-replace "a!1=0" )"1" (assert ) nil nil )"2" (assert )"2" (case-replace "px!1=1" )"1" (assert ) nil nil )"2" (assert )"2" (case "px!1<1" )"1" (assert )"1" (case "a!1>0" )"1" (hide 1 2)"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" (expand "extend" )"1" (expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "density_positive" "x" "a!1" "y" "a!1+1" ))"1" assert )"1" "1" "nn_rational_expt(px!1, r!1)" )"1" "1" "nn_rational_expt_pos" "px" "px!1" "q" "r!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "2" "s!1" )"2" assert )"2" "2" "nn_rational_expt_decreasing" "q" "q!1" "r" "r!1" "x" "px!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (case "a!1>0&px!1>1" )"1" (flatten)"1" (hide 1 2 3)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" (expand "least_upper_bound?" )"1" "1" expand "extend" )"1" expand "upper_bound?" )"1" "density_positive" "x" "0" "y" "a!1" ))"1" assert )"1" "1" "nn_rational_expt(px!1, r!1)" )"1" "nn_rational_expt_pos" "px" "px!1" "q" "r!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "nn_rational_expt(px!1, r!1)" )"1" assert )"1" "r!1" )"1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"nnreal" nnreal_expt nil )"posreal" nnreal_expt nil )"rat" nnreal_expt nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil rationals nil )"rat" nnreal_expt nil )"posreal" nil )nil nn_rational_expt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )nil nn_rational_expt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil rational_props nil )"posreal" nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" booleans nil )"R" extend nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nnreal" nn_rational_expt nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props 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]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3427304987"" (skosimp)"" (case-replace "a!1=0" )"1" (assert )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_is_0" ) nil nil )) nil ))nil )"2" (assert )"2" (case "a!1>0" )"1" (hide 1)"1" (split)"1" (flatten)"1" (case "x!1>0" )"1" (hide 1)"1" (assert )"1" "nnreal_expt_pos" "px" "x!1" "a" "a!1" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" (replace -1)"2" (rewrite "nnreal_expt_0a" ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nnreal_expt nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )nil nn_rational_expt nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil nnreal_expt nil )nil real_types nil )nil real_types nil )nil nnreal_expt nil ))nil 3427306444"" (skosimp)"" (split)"1" (flatten)"1" (case "x!1<=1" )"1" (hide 1)"1" (expand "<=" )"1" (split)"1" (assert )"1" (case-replace "x!1=0" )"1" (rewrite "nnreal_expt_0a" )"1" (assert ) nil nil )) nil )"2" (case "x!1>0" )"1" (hide 1)"1" (expand "nnreal_expt" )"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" expand "extend" )"1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "nn_rational_expt(x!1, 0)" )"1" rewrite "nn_rational_expt_nat_rew" )"1" rewrite "expt_x0" )"1" (assert ) nil nil ))nil ))nil )"2" "nn_rational_expt(x!1, 0)" )"2" assert )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "nnreal_expt_1a" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (expand "nnreal_expt" )"2" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "2" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "2" (expand "extend" )"2" (expand "least_upper_bound?" )"2" (flatten)"2" "density_positive" ("x" "0" "y" "pa!1" ))"2" (assert )"2" (skosimp)"2" (expand "upper_bound?" )"2" "nn_rational_expt(x!1, r!1)" )"1" "nn_rational_expt_gt1" "x" "x!1" "pq" "r!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "nn_rational_expt(x!1, r!1)" )"1" assert )"1" "r!1" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nnreal_expt nil )"bool" bounded_real_defs nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil nn_rational_expt nil )"nnreal" exponentiation nil )"(total_order?[real])" nil )nil exponentiation nil )"posreal" nnreal_expt nil )"nnreal" nnreal_expt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" booleans nil )"R" extend nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nnreal" nn_rational_expt nil )nil nnreal_expt nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )nil nn_rational_expt nil )nil rationals nil )nil rationals nil )"rat" nnreal_expt nil )nil rationals nil )nil rational_props nil ))nil 3427306586"" (skosimp)"" (split)"1" (flatten)"1" (case "1<=x!1" )"1" (hide 1)"1" (expand "<=" )"1" (split -1)"1" (assert )"1" (expand "nnreal_expt" )"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (expand "extend" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" expand "upper_bound?" )"1" "nn_rational_expt(x!1, 0)" )"1" rewrite "nn_rational_expt_nat_rew" )"1" rewrite "expt_x0" )"1" (assert ) nil nil ))nil ))nil )"2" "nn_rational_expt(x!1, 0)" )"2" assert )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (rewrite "nnreal_expt_1a" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (expand "nnreal_expt" )"2" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "2" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "2" (expand "extend" )"2" (expand "greatest_lower_bound?" )"2" (flatten)"2" (expand "lower_bound?" )"2" "density_positive" "x" "0" "y" "pa!1" ))"2" (assert )"2" (skosimp)"2" "nn_rational_expt(x!1, r!1)" )"1" "nn_rational_expt_lt1" "x" "x!1" "pq" "r!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "nn_rational_expt(x!1, r!1)" )"1" assert )"1" "r!1" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"nnreal" nn_rational_expt nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )"R" extend nil )"bool" booleans nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nnreal" nnreal_expt nil )"posreal" nnreal_expt nil )nil exponentiation nil )"(total_order?[real])" nil )"nnreal" exponentiation nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" bounded_real_defs nil )"nnreal" nnreal_expt nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )nil rational_props nil )nil nn_rational_expt nil )nil rationals nil )nil rationals nil )"(strict_total_order?[real])" real_props nil )"rat" nnreal_expt nil )nil rationals nil )"bool" bounded_real_defs nil ))nil 3427304524"" (skosimp) (("" (rewrite "nnreal_expt_is_0" ) nil nil )) nil )nil nnreal_expt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil ))nil 3427343585"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "inv_nn_rational_expt" ) nil nil )) nil ))nil )"2" (case "a!1>0" )"1" (hide 1)"1" (lemma "nnreal_expt_pos" ("px" "px!1" "a" "a!1" ))"1" (expand "nnreal_expt" )"1" (case-replace "px!1=1" )"1" (replace 1)"1" (case-replace "px!1 < 1" )"1" "both_sides_div_pos_lt2" "pz" "1" "py" "px!1" "px" "1" ))"1" (rewrite "div_simp" )"1" (assert )"1" (hide 1)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(1 / px!1, q)}))") "1" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(1 / px!1, q)}))") "1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" expand "greatest_lower_bound?" )"1" expand "least_upper_bound?" )"1" expand "upper_bound?" )"1" expand "lower_bound?" )"1" "1" "1/GLB" )"1" "1" "div_mult_pos_le1" "z" "1" ))"1" case "LUB>0" )"1" "GLB" "LUB" )"1" "LUB" "GLB" )"1" "1/LUB" )"1" "1" assert )nil nil )"2" "2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace "2" "nn_rational_expt_pos" "px" "px!1" "q" "q!1" ))"2" "2" "inv_nn_rational_expt" "px" "px!1" "q" "q!1" ))"2" "both_sides_div_pos_le2" "pz" "1" "px" "LUB" "py" "1 / nn_rational_expt(px!1, q!1)" ))"1" "1 / (1 / nn_rational_expt(px!1, q!1))=nn_rational_expt(px!1, q!1)" )"1" replace "1" replace "1" "1" "1" "nn_rational_expt(1 / px!1, q!1)" )"1" expand "extend" )"1" assert )"1" "q!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" "2" "nn_rational_expt(1 / px!1, 0)" )"1" "nn_rational_expt_pos" "px" "1/px!1" "q" "0" ))"1" assert )nil nil ))nil )"2" expand "extend" )"2" "nn_rational_expt(1 / px!1, 0)" )"2" assert )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace "2" "2" rewrite "inv_nn_rational_expt" )"2" "nn_rational_expt_pos" "px" "px!1" "q" "q!1" ))"2" "both_sides_div_pos_le2" "pz" "1" "px" "nn_rational_expt(px!1, q!1)" "py" "GLB" ))"1" replace "1" "1" "nn_rational_expt(px!1, q!1)" )"1" expand "extend" )"1" "q!1" )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_div_pos_lt2" "pz" "1" "px" "px!1" "py" "1" ))"2" (assert )"2" (case "px!1>1" )"1" (hide 1 2)"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(1 / px!1, q)}))") "1" "GLB" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(1 / px!1, q)}))") "1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" "LUB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(px!1, q)}))") "1" expand "greatest_lower_bound?" )"1" expand "lower_bound?" )"1" expand "least_upper_bound?" )"1" expand "upper_bound?" )"1" "1" "1/LUB" )"1" "1" case "GLB>0" )"1" "both_sides_div_pos_le2" "pz" "1" ))"1" "1/LUB" "GLB" )"1" "1" "1" "1" assert )nil nil )"2" "2" assert )"2" "1 / (1 / LUB)=LUB" )"1" "1" "1/GLB" )"1" "1" nil nil )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace "2" "2" "nn_rational_expt_pos" "px" "px!1" "q" "q!1" ))"2" rewrite "div_mult_pos_le2" )"2" "div_mult_pos_le2" "py" "nn_rational_expt(px!1, q!1)" "x" "GLB" "z" "1" ))"1" replace "1" "1" rewrite "inv_nn_rational_expt" "1" "nn_rational_expt(1 / px!1, q!1)" )"1" expand "extend" )"1" "q!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "div_div1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "posreal_div_posreal_is_posreal" "px" "1" "py" "LUB" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "LUB" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "s!1" )"2" expand "extend" "2" "2" "2" replace "2" "2" rewrite "inv_nn_rational_expt" "2" "2" "nn_rational_expt_pos" "px" "px!1" "q" "q!1" ))"2" "both_sides_div_pos_le2" "pz" "1" "px" "LUB" "py" "nn_rational_expt(px!1, q!1)" ))"1" replace "1" "1" "nn_rational_expt(px!1, q!1)" )"1" expand "extend" )"1" "q!1" )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nn_rational_expt nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"posreal" nil )"nnreal" nnreal_expt nil )nil real_types nil )"real" reals nil )nil real_props nil )"nnrat" nnreal_expt nil )nil real_props nil )"{x | AND " nil )"{x | AND " nil )"nnrat" nnreal_expt nil )"posrat" nil )nil real_props nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nn_rational_expt nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"R" extend nil )"bool" booleans nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"{x | AND " nil )"(total_order?[real])" nil )"real" reals nil )nil nn_rational_expt nil )"nnrat" nnreal_expt nil )nil real_props nil )"{x | AND " nil )"posreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"(total_order?[real])" nil )nil real_props nil )"nnrat" nnreal_expt nil )"bool" bounded_real_defs nil )nil real_props nil )nil reals nil )"bool" reals nil )nil nnreal_expt nil ))nil 3427347035"" case "FORALL (a, x, y: nnreal): a>0=> ") "1" (skosimp)"1" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (hide -2) (("1" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "a!1" "x!1" "y!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (x, y: nnreal, a:posreal): ") "1" (skosimp)"1" (inst - "_" "_" "a!1" )"1" (case "x!1>1" )"1" (inst - "x!1" "y!1" ) (("1" (assert ) nil nil )) nil )"2" (case-replace "x!1=1" )"1" (hide -2 -1 1)"1" (rewrite "nnreal_expt_1a" )"1" (assert ) nil nil )) nil ))nil )"2" (case "x!1<1" )"1" (hide 1 2)"1" (case "0<x!1" )"1" (case-replace "y!1=0" )"1" "nnreal_expt_is_0" "x" "0" "a" "a!1" ))"1" (assert ) nil nil )) nil )"2" (case "y!1>0" )"1" (hide 1)"1" (inst - "1/x!1" "1/y!1" )"1" assert )"1" rewrite "inv_nnreal_expt" )"1" rewrite "inv_nnreal_expt" )"1" rewrite "div_times" )"1" rewrite "inv_nnreal_expt" )"1" "nnreal_expt_pos" "px" "x!1" "a" "a!1" ))"1" "nnreal_expt_pos" "px" "y!1" "a" "a!1" ))"1" "nnreal_expt_pos" "px" "x!1*y!1" "a" "a!1" ))"1" rewrite "div_times" )"1" rewrite "both_sides_div2" )"1" rewrite "div_mult_pos_gt1" )nil nil )"2" expand "/=" )"2" rewrite "zero_times3" )nil nil ))nil ))nil ))nil )"2" rewrite "posreal_times_posreal_is_posreal" )nil nil ))nil ))nil ))nil )"2" rewrite "posreal_times_posreal_is_posreal" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "div_mult_pos_ge1" )nil nil ))nil )"3" (assert ) nil nil )"4" assert )"4" rewrite "div_mult_pos_ge1" )nil nil ))nil )"5" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (case-replace "x!1=0" )"1" "nnreal_expt_is_0" "x" "0" "a" "a!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (x, y: nnreal, a: posreal): ") "1" (skosimp)"1" (lemma "trich_lt" ("x" "y!1" "y" "1" ))"1" (split -1)"1" (case-replace "y!1=0" )"1" "nnreal_expt_is_0" ("x" "0" "a" "a!1" ))"1" (assert ) nil nil )) nil )"2" (case "y!1>0" )"1" (hide 1)"1" (case "1/y!1>1" )"1" "trich_lt" ("x" "x!1*y!1" "y" "1" ))"1" (split -1)"1" "both_sides_div_pos_lt2" "pz" "1" "px" "1" "py" "x!1*y!1" ))"1" assert )"1" rewrite "div_simp" )"1" "_" "1 / (x!1 * y!1)" "a!1" )"1" rewrite "inv_nnreal_expt" -6)"1" "x!1" )"1" assert )"1" "x!1 * (1 / (x!1 * y!1))=1/y!1" )"1" rewrite "inv_nnreal_expt" )"1" assert )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "posreal_times_posreal_is_posreal" )nil nil ))nil )"2" "div_cancel3" "x" "1" "y" "x!1" "n0z" "y!1" ))"2" assert )"2" replace -1 * rl)"2" "2" rewrite "div_cancel2" )"2" rewrite "nnreal_expt_1a" )"2" rewrite "inv_nnreal_expt" )"2" rewrite "div_cancel2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "1/y!1" "x!1 * y!1" "a!1" )"1" assert )"1" rewrite "inv_nnreal_expt" )"1" "1 / y!1 * (x!1 * y!1)=x!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "div_mult_pos_gt1" ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (replace -1)"2" (rewrite "nnreal_expt_1a" )"2" (assert ) nil nil )) nil ))nil )"3" (inst - "x!1" "y!1" "a!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" "lt_times_lt_pos1" "px" "1" "y" "x!1" "nnz" "1" "w" "y!1" ))"2" (assert )"2" (typepred "a!1" )"2" "nnreal_expt_pos" "px" "x!1" "a" "a!1" ))"2" "nnreal_expt_pos" "px" "y!1" "a" "a!1" ))"2" "nnreal_expt_pos" "px" "x!1*y!1" "a" "a!1" ))"2" (name "X" "nnreal_expt(x!1, a!1)" )"2" "Y" "nnreal_expt(y!1, a!1)" )"2" "XY" "nnreal_expt(x!1*y!1, a!1)" )"2" expand "nnreal_expt" )"2" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1 * y!1, q)}))") "2" replace -2)"2" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(y!1, q)}))") "2" replace -4)"2" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "2" replace -6)"2" "2" expand "least_upper_bound?" )"2" "2" "X*Y" )"2" "1" "XY/Y" )"1" "1" rewrite "div_mult_pos_le2" "1" assert )nil nil ))nil )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace "2" rewrite "div_mult_pos_le2" "2" "2" "XY/nn_rational_expt(x!1, q!1)" )"1" "1" rewrite "div_mult_pos_le2" "1" assert )nil nil ))nil )"2" "2" rewrite "div_mult_pos_le2" "2" "s!2" )"2" expand "extend" )"2" "2" "2" replace "2" "2" "Q" "max(q!1,q!2)" )"2" case "Q>=q!1 & Q>=q!2 & a!1>=Q" )"1" "1" case "nn_rational_expt(y!1, q!2)<=nn_rational_expt(y!1, Q)" )"1" case "nn_rational_expt(x!1, q!1)<=nn_rational_expt(x!1, Q)" )"1" "1" "nn_rational_expt(x!1*y!1, Q)" )"1" rewrite "mult_nn_rational_expt" "1" "le_times_le_pos" "nnx" "nn_rational_expt(x!1, q!1)" "y" "nn_rational_expt(x!1, Q)" "nnz" "nn_rational_expt(y!1, q!2)" "w" "nn_rational_expt(y!1, Q)" ))"1" assert )nil nil ))nil ))nil )"2" expand "extend" )"2" "nn_rational_expt(x!1 * y!1, Q)" )"2" assert )"2" "Q" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand ">=" "2" expand "<=" "2" "2" "1" "nn_rational_expt_increasing" "q" "q!1" "r" "Q" "x" "x!1" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn_rational_expt_increasing" "q" "q!2" "r" "Q" "x" "y!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "upper_bound?" )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace "2" "nn_rational_expt(x!1, q!1)" )"1" "nn_rational_expt(y!1, q!1)" )"1" rewrite "mult_nn_rational_expt" "1" "le_times_le_pos" "nnx" "nn_rational_expt(x!1, q!1)" "y" "X" "nnz" "nn_rational_expt(y!1, q!1)" "w" "Y" ))"1" assert )nil nil ))nil ))nil )"2" expand "extend" )"2" assert )"2" "nn_rational_expt(y!1, q!1)" )"2" assert )"2" "q!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "nn_rational_expt(x!1, q!1)" )"2" assert )"2" "q!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"nnreal" nn_rational_expt nil )"bool" reals nil ) (extend const-decl "R" extend nil )"bool" booleans nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )nil real_props nil )"nnreal" nnreal_expt nil )"nnrat" nnreal_expt nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil rationals nil )"posreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"nnrat" nnreal_expt nil )"{s: nonneg_rat | s >= q!1 AND s >= q!2}" nil )nil real_props nil )nil nn_rational_expt nil )nil nn_rational_expt nil )"bool" bounded_real_defs nil )"nnreal" nnreal_expt nil )"real" reals nil )"nnrat" nnreal_expt nil )"(total_order?[real])" nil )"posrat" nil )"real" reals nil )nil real_props nil )nil real_props nil )nil real_props nil )"nnreal" nnreal_expt nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nzreal" nil )"boolean" notequal nil )"nnreal" nnreal_expt nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nnreal" nnreal_expt nil )nil nnreal_expt nil )nil reals nil )nil real_props nil )"(divides(n))" divides nil )"odd_int" integers nil )"posint" nil )nil nnreal_expt nil )nil real_props nil )nil extra_real_props nil )nil real_props nil )nil real_types nil )nil real_props nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )nil nnreal_expt nil )"nnreal" nnreal_expt nil )nil real_types nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"(total_order?[real])" nil )"nnreal" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"nnreal" exponentiation nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nnreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nnreal" nnreal_expt nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3427307311"" (skosimp)"" (lemma "inv_nnreal_expt" ("a" "a!1" "px" "py!1" ))"" "mult_nnreal_expt" ("a" "a!1" "x" "x!1" "y" "1/py!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nnreal_expt nil )"real" reals nil )"nnreal" nil )"nzreal" nil )"nnreal" nil )"posreal" nil )nil nnreal_expt nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))nil 3427444865"" (skosimp)"" (lemma "density_positive" ("x" "a!1" "y" "b!1" ))"" (assert )"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" +)"1" (rewrite "nn_rational_expt_nat_rew" +)"1" (rewrite "expt_x0" )"1" "nnreal_expt_lt1" ("x" "x!1" "pa" "b!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case "a!1>0" )"1" (hide 1)"1" (expand "nnreal_expt" )"1" (assert )"1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "A" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "B" "glb(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "nn_rational_expt(x!1, r!1)" )"1" "density_positive" "x" "a!1" "y" "r!1" ))"1" assert )"1" "1" "nn_rational_expt(x!1, r!2)" )"1" "1" "nn_rational_expt_decreasing" "q" "r!2" "r" "r!1" "x" "x!1" ))"1" (assert ) nil nil )"2" assert )nil nil ))nil )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace -3)"2" "nn_rational_expt_decreasing" "q" "q!1" "r" "r!2" "x" "x!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "nn_rational_expt(x!1, r!1)" )"2" assert )"2" "r!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil rational_props nil )"nnreal" nnreal_expt nil )"nnreal" nn_rational_expt nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"R" extend nil )"bool" booleans nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )nil nn_rational_expt nil )"rat" nnreal_expt nil )"rat" nnreal_expt nil )nil rationals nil )"nnreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"(total_order?[real])" nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )nil exponentiation nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil nnreal_expt nil )"nnreal" exponentiation nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3427445921"" (skosimp)"" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" )"1" (lemma "nnreal_expt_gt1" ("x" "x!1" "pa" "b!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case "a!1>0" )"1" (hide 1)"1" (expand "nnreal_expt" )"1" (assert )"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "A" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" "B" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (expand "least_upper_bound?" )"1" (expand "upper_bound?" )"1" (flatten)"1" "density_positive" "x" "a!1" "y" "b!1" ))"1" assert )"1" "1" "density_positive" "x" "r!1" "y" "b!1" ))"1" assert )"1" "1" "nn_rational_expt(x!1, r!2)" )"1" "nn_rational_expt(x!1, r!1)" )"1" "1" "nn_rational_expt_increasing" "q" "r!1" "r" "r!2" "x" "x!1" ))"1" (assert ) nil nil )"2" assert )nil nil ))nil )"2" "2" "s!1" )"2" expand "extend" )"2" "2" "2" replace -3)"2" "nn_rational_expt_increasing" "q" "q!1" "r" "r!1" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "nn_rational_expt(x!1, r!2)" )"1" assert )"1" "r!2" )"1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nnreal" exponentiation nil )nil nnreal_expt nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"bool" bounded_real_defs nil )nil rational_props nil )"(total_order?[real])" nil )"rat" nnreal_expt nil )"nnreal" nnreal_expt nil )"nnreal" nnreal_expt nil )nil nn_rational_expt nil )nil rationals nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" booleans nil )"R" extend nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"nnreal" nn_rational_expt nil )"nnreal" nnreal_expt nil ))nil 3427305418"" (skosimp)"" (case-replace "x!1=0" )"1" (rewrite "nnreal_expt_0a" )"1" (lemma "nnreal_expt_pos" ("px" "y!1" "a" "pa!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (case "x!1>0" )"1" (hide 1)"1" (lemma "nnreal_expt_pos" ("px" "x!1" "a" "pa!1" ))"1" "div_nnreal_expt" "x" "y!1" "py" "x!1" "a" "pa!1" ))"1" "posreal_div_posreal_is_posreal" "px" "y!1" "py" "x!1" ))"1" "nnreal_expt_gt1" ("x" "y!1/x!1" "pa" "pa!1" ))"1" (assert )"1" (replace -3)"1" (hide -3)"1" (rewrite "div_mult_pos_gt1" )"1" (rewrite "div_mult_pos_gt1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil nnreal_expt nil )nil nnreal_expt nil )"real" reals nil )nil nnreal_expt nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(total_order?[real])" nil )"nnreal" nnreal_expt nil )nil extra_real_props nil )"nnreal" nil )nil real_types nil ))nil 3427562805"" case "FORALL (epsilon, pa, x: posreal): ") "1" (skosimp)"1" (case-replace "x!1=0" )"1" (rewrite "nnreal_expt_0a" )"1" (inst + "1" )"1" (skosimp)"1" (rewrite "nnreal_expt_0a" )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "epsilon!1" "pa!1" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (lemma "trich_lt" ("x" "x!1" "y" "1" ))"2" (split -1)"1" case "forall (y,epsilon:posreal): ") "1" case "forall (y,epsilon:posreal): y < 1 => EXISTS q: nn_rational_expt(x!1,q)<y & y-nn_rational_expt(x!1,q) < epsilon" )"1" case "forall (y,epsilon:posreal): y < 1 => EXISTS q: y<nn_rational_expt(x!1,q) & nn_rational_expt(x!1,q)-y < epsilon" )"1" "nnreal_expt_pos" ("px" "x!1" "a" "pa!1" ))"1" "nnreal_expt_lt1" ("x" "x!1" "pa" "pa!1" ))"1" (assert )"1" "nnreal_expt(x!1, pa!1)" "epsilon!1/2" )"1" "nnreal_expt(x!1, pa!1)" "epsilon!1/2" )"1" (replace -1)"1" "1" case "q!1<pa!1" )"1" case "pa!1<q!2" )"1" "1" rewrite "nnreal_expt_rat_rew" "1" rewrite "nnreal_expt_rat_rew" "1" "min(q!2-pa!1,pa!1-q!1)" )"1" "1" case "q!1<pb!1&pb!1<q!2" )"1" "1" "nnreal_expt_decreasing" "a" "q!1" "b" "pb!1" "x" "x!1" ))"1" "nnreal_expt_decreasing" "b" "q!2" "a" "pb!1" "x" "x!1" ))"1" assert )"1" "XA" "nnreal_expt(x!1, pa!1)" )"1" "XB" "nnreal_expt(x!1, pb!1)" )"1" "LOW" "nnreal_expt(x!1, q!2)" )"1" "HIGH" "nnreal_expt(x!1, q!1)" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "nnreal_expt_rat_rew" "2" rewrite "nnreal_expt_rat_rew" "2" "2" "pa!1=q!2" )"1" (assert ) nil nil )"2" "nnreal_expt_decreasing" "a" "q!2" "b" "pa!1" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1=pa!1" )"1" assert )"1" rewrite "nnreal_expt_rat_rew" "1" (assert ) nil nil ))nil ))nil )"2" "nnreal_expt_decreasing" "a" "pa!1" "b" "q!1" "x" "x!1" ))"2" rewrite "nnreal_expt_rat_rew" "2" rewrite "nnreal_expt_rat_rew" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (skosimp)"2" (name "EPS" "min(epsilon!2/2,1-y!1)" )"2" case "EPS>0&1-y!1>=EPS&epsilon!2/2>=EPS" )"1" (flatten)"1" (inst - "y!1+EPS/2" "EPS/2" )"1" assert )"1" "1" "q!1" )"1" "DRL" "nn_rational_expt(x!1, q!1)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" (hide -3 2) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (name "EPS" "min(epsilon!2/2,y!1)" )"2" (case "EPS>0&y!1>=EPS&epsilon!2/2>=EPS" )"1" (flatten)"1" (inst - "y!1-EPS/2" "EPS/2" )"1" (assert )"1" "1" "q!1" )"1" "DRL" "nn_rational_expt(x!1, q!1)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" "nn_rational_expt_approx_gt1" "x" "1/x!1" "y" "1/y!1" ))"2" (case-replace "1 / x!1 > 1 AND 1 / y!1 > 1" )"1" (flatten)"1" (inst - "epsilon!2" )"1" (skosimp)"1" (inst + "q!1" )"1" rewrite "inv_nn_rational_expt" )"1" rewrite "minus_div1" -3)"1" rewrite "abs_div" -3)"1" "q!1=0" )"1" rewrite "nn_rational_expt_nat_rew" )"1" rewrite "expt_x0" )"1" expand "abs" -4 2)"1" rewrite "div_mult_pos_lt1" "1" "both_sides_times_pos_lt1" "pz" "epsilon!2" "x" "y!1" "y" "1" ))"1" assert )"1" "abs(y!1 - 1)=abs(1 - y!1)" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "q!1>0" )"1" "1" "nnreal_expt_pos" "px" "x!1" "a" "q!1" ))"1" "nnreal_expt_lt1" "x" "x!1" "pa" "q!1" ))"1" replace -8 -1)"1" "1" "div_mult_pos_lt1" "z" "abs(y!1 - nn_rational_expt(x!1, q!1))" "py" "abs(nn_rational_expt(x!1, q!1) * y!1)" "x" "epsilon!2" ))"1" replace -1 -7)"1" "1" rewrite "abs_mult" "1" expand "abs" "1" expand "abs" "1" "posreal_times_posreal_is_posreal" "px" "nn_rational_expt(x!1, q!1)" "py" "y!1" ))"1" "lt_times_lt_pos1" "px" "nnreal_expt(x!1, q!1)" "y" "1" "nnz" "y!1" "w" "1" ))"1" "1" "abs(y!1 - nn_rational_expt(x!1, q!1))=abs(nn_rational_expt(x!1, q!1) - y!1)" )"1" "1" "LHS" "abs(nn_rational_expt(x!1, q!1) - y!1)" )"1" "both_sides_times_pos_lt1" "pz" "epsilon!2" "x" "nn_rational_expt(x!1, q!1) * y!1" "y" "1" ))"1" assert )"1" rewrite "nnreal_expt_rat_rew" nil nil ))nil ))nil ))nil ))nil )"2" "2" "DRL" "nn_rational_expt(x!1, q!1)" )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil )"2" nil nil ))nil )"2" rewrite "nnreal_expt_rat_rew" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "abs_mult" "2" expand "abs" "2" rewrite "posreal_times_posreal_is_posreal" )"2" rewrite "nnreal_expt_rat_rew" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (split)"1" (assert )"1" (rewrite "div_mult_pos_gt1" ) nil nil ))nil )"2" "div_mult_pos_gt2" "x" "1" "z" "1" "py" "y!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (inst + "1" )"2" (skosimp)"2" (rewrite "nnreal_expt_1a" )"2" (rewrite "nnreal_expt_1a" )"2" (expand "abs" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" case "forall (y,epsilon:posreal): y > 1 => EXISTS q: nn_rational_expt(x!1,q)<y & y-nn_rational_expt(x!1,q) < epsilon" )"1" case "forall (y,epsilon:posreal): y > 1 => EXISTS q: y<nn_rational_expt(x!1,q) & nn_rational_expt(x!1,q)-y < epsilon" )"1" (inst - "nnreal_expt(x!1, pa!1)" "epsilon!1/2" )"1" (inst - "nnreal_expt(x!1, pa!1)" "epsilon!1/2" )"1" (rewrite "nnreal_expt_gt1" )"1" (assert )"1" (skosimp*)"1" (case "q!2<pa!1&pa!1<q!1" )"1" (flatten)"1" "min(q!1-pa!1,pa!1-q!2)" )"1" "1" case "q!2<pb!1&pb!1<q!1" )"1" "1" "nnreal_expt_increasing" "a" "q!2" "b" "pb!1" "x" "x!1" ))"1" "nnreal_expt_increasing" "b" "q!1" "a" "pb!1" "x" "x!1" ))"1" assert )"1" rewrite "nnreal_expt_rat_rew" "1" rewrite "nnreal_expt_rat_rew" "1" "LOW" "nnreal_expt(x!1, q!2)" )"1" "HIGH" "nnreal_expt(x!1, q!1)" )"1" "XA" "nnreal_expt(x!1, pa!1)" )"1" "XB" "nnreal_expt(x!1, pb!1)" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" rewrite "nnreal_expt_rat_rew" "2" rewrite "nnreal_expt_rat_rew" "2" case "q!2=pa!1" )"1" replace -1)"1" (assert ) nil nil ))nil )"2" case "q!2>pa!1" )"1" "nnreal_expt_increasing" "a" "pa!1" "b" "q!2" "x" "x!1" ))"1" (assert ) nil nil ))nil )"2" assert )"2" "2" "pa!1=q!1" )"1" (assert ) nil nil )"2" "nnreal_expt_increasing" "a" "q!1" "b" "pa!1" "x" "x!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "nnreal_expt_pos" ) nil nil ))nil )"2" (rewrite "nnreal_expt_pos" ) nil nil ))nil )"2" (hide -1 2)"2" (skosimp)"2" (name "EPS" "min(epsilon!2/2,y!1-1)" )"2" (case "EPS>0&epsilon!2/2>=EPS&y!1-1>=EPS" )"1" (flatten)"1" "nn_rational_expt_approx_gt1" "x" "x!1" "y" "y!1+EPS/2" "epsilon" "EPS/2" ))"1" (assert )"1" "1" "q!1" )"1" "DRL" "nn_rational_expt(x!1, q!1)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (name "EPS" "min(epsilon!2/2,y!1-1)" )"2" (case "EPS>0&epsilon!2/2>=EPS&y!1-1>=EPS" )"1" (flatten)"1" "nn_rational_expt_approx_gt1" "x" "x!1" "y" "y!1-EPS/2" "epsilon" "EPS/2" ))"1" (assert )"1" (skosimp)"1" "q!1" )"1" "DRL" "nn_rational_expt(x!1, q!1)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )"posreal" nnreal_expt nil )nil nnreal_expt nil )nil nnreal_expt nil )"nnrat" nnreal_expt nil )"nnrat" nnreal_expt nil )nil nnreal_expt nil )"nnreal" nn_rational_expt nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )"posreal" nil )"{z: posreal | z <= epsilon!2 / 2 AND z <= y!1}" nnreal_expt nil )"posreal" nnreal_expt nil )"posreal" nnreal_expt nil )"posreal" nil )nil nnreal_expt nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )nil nnreal_expt nil )"nnrat" nnreal_expt nil )"posreal" nnreal_expt nil )"nnrat" nnreal_expt nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"(total_order?[real])" nil )nil nnreal_expt nil )nil nnreal_expt nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nnreal_expt nil )"posreal" nnreal_expt nil )"{p: real | p <= epsilon!2 / 2 AND p <= 1 - y!1}" nnreal_expt nil )nil reals nil )nil real_props nil )"nnreal" nil )"posreal" nil )nil exponentiation nil )"{y: posreal | y >= x}" nil )nil real_props nil )nil real_props nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"odd_int" integers nil )"posint" nil )nil real_types nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" nil )nil nn_rational_expt nil )nil extra_real_props nil )nil extra_real_props nil )nil nn_rational_expt nil )"(strict_total_order?[real])" real_props nil )"nnreal" nnreal_expt nil )nil nnreal_expt nil )"odd_int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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 )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nnreal" nnreal_expt nil ))nil 3427605142"" (skosimp)"" (case-replace "y!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "nnreal_expt_gt1" ("x" "gt1x!1" "pa" "y!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )nil nnreal_expt nil ))nil ))nil 3427608443"" (expand "bijective?" )"" (skosimp)"" (split)"1" (expand "injective?" )"1" (skosimp)"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1)"1" "nnreal_expt_increasing" "x" "gt1x!1" "a" "x1!1" "b" "x2!1" ))"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" "nnreal_expt_increasing" "x" "gt1x!1" "b" "x1!1" "a" "x2!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp)"2" (typepred "y!1" )"2" (expand ">=" -3)"2" (expand "<=" -3)"2" (split -3)"1" case "nonempty?({x:real| x>=0 & nnreal_expt(gt1x!1, x) < y!1})" )"1" case "bounded_above?({x:real| x>=0 & nnreal_expt(gt1x!1, x) < y!1})" )"1" "lub({x: real | x >= 0 & nnreal_expt(gt1x!1, x) < y!1})" )"1" "LUB" "lub({x: real | ") "1" (expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" case "LUB>=0" )"1" "LUB" )"1" "trich_lt" "x" "nnreal_expt(gt1x!1, LUB)" "y" "y!1" ))"1" "1" "EPS" "min(y!1-nnreal_expt(gt1x!1, LUB),y!1-1)" )"1" case "EPS>0&y!1 - nnreal_expt(gt1x!1, LUB)>=EPS& y!1 - 1 >= EPS" )"1" "1" "nn_rational_expt_approx_gt1" "x" "gt1x!1" "y" "y!1-EPS/2" "epsilon" "EPS/2" ))"1" assert )"1" "1" "1" case "nnreal_expt(gt1x!1, LUB)<nn_rational_expt(gt1x!1, q!1)&nn_rational_expt(gt1x!1, q!1)<y!1" )"1" rewrite "nnreal_expt_rat_rew" "1" "1" case "LUB<q!1" )"1" "q!1" )"1" assert )nil nil ))nil )"2" "LUB=q!1" )"1" assert )nil nil )"2" "nnreal_expt_increasing" "a" "q!1" "b" "LUB" "x" "gt1x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "XL" "nnreal_expt(gt1x!1, LUB)" )"2" "XQ" "nn_rational_expt(gt1x!1, q!1)" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil )"2" "2" "DRL" "nnreal_expt(gt1x!1, LUB)" )"2" nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil )"3" "3" "EPS" "nnreal_expt(gt1x!1, LUB)-y!1" )"3" case "EPS>0" )"1" "nn_rational_expt_approx_gt1" "x" "gt1x!1" "y" "y!1+EPS/2" "epsilon" "EPS/2" ))"1" assert )"1" "1" rewrite "nnreal_expt_rat_rew" "1" case "y!1<nnreal_expt(gt1x!1, q!1)& nnreal_expt(gt1x!1, q!1)<nnreal_expt(gt1x!1, LUB)" )"1" "1" "1" case "q!1<LUB" )"1" "q!1" )"1" assert )"1" "1" "s!1" )"1" "nnreal_expt_increasing" "a" "q!1" "b" "s!1" "x" "gt1x!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "q!1=LUB" )"1" assert )nil nil )"2" "nnreal_expt_increasing" "a" "LUB" "b" "q!1" "x" "gt1x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "XL" "nnreal_expt(gt1x!1, LUB)" )"2" "XQ" "nnreal_expt(gt1x!1, q!1)" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" "0" )"1" (assert ) nil nil )"2" rewrite "nnreal_expt_rat_rew" )"2" rewrite "nn_rational_expt_nat_rew" )"2" rewrite "expt_x0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (expand "bounded_above?" )"2" (expand "upper_bound?" )"2" "nn_rational_expt_approx_gt1" "x" "gt1x!1" "y" "y!1+1" "epsilon" "1" ))"2" assert )"2" "2" "q!1" )"2" "2" "s!1" )"2" case "y!1<nn_rational_expt(gt1x!1, q!1)" )"1" "nnreal_expt_increasing" "x" "gt1x!1" "a" "q!1" "b" "s!1" ))"1" rewrite "nnreal_expt_rat_rew" "1" assert )nil nil ))nil ))nil )"2" expand "abs" )"2" "nn_rational_expt(gt1x!1, q!1) - 1 - y!1 < 0" )"1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "0" )"2" expand "member" )"2" rewrite "nnreal_expt_rat_rew" )"2" rewrite "nn_rational_expt_nat_rew" )"2" (rewrite "expt_x0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (inst + "0" )"2" (rewrite "nnreal_expt_rat_rew" )"2" (rewrite "nn_rational_expt_nat_rew" )"2" (rewrite "expt_x0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"nnreal" nnreal_expt nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )"posreal" nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil nn_rational_expt nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )nil exponentiation nil )"(total_order?[real])" nil )"{r | r > 1}" nnreal_expt nil )"{r | r >= 1}" nnreal_expt nil )"{x_1 | " nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil nn_rational_expt nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )"nnreal" nn_rational_expt nil )"nnrat" nnreal_expt nil )"(total_order?[real])" nil )"odd_int" integers nil )nil nnreal_expt nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"bool" bounded_real_defs nil )"bool" sets nil )"bool" sets nil )"bool" functions 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil ))nil 3427605142"" (skosimp)"" (case-replace "y!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "nnreal_expt_lt1" ("x" "lt1x!1" "pa" "y!1" ))"1" (assert )"1" (lemma "nnreal_expt_pos" ("px" "lt1x!1" "a" "y!1" ))"1" (propax) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"(strict_total_order?[real])" real_props nil )nil nnreal_expt nil )nil nnreal_expt nil ))nil ))nil 3427690611"" (skosimp)"" "both_sides_div_pos_lt2" "pz" "1" "py" "lt1x!1" "px" "1" ))"" (rewrite "div_simp" )"" (assert )"" (lemma "nnreal_bijective1" ("gt1x" "1/lt1x!1" ))"" (expand "bijective?" )"" (flatten)"" (split)"1" (expand "injective?" )"1" (skosimp*)"1" (inst - "x1!1" "x2!1" )"1" (rewrite "inv_nnreal_expt" )"1" (rewrite "inv_nnreal_expt" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp)"2" (typepred "y!1" )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "y!1" ))"2" "both_sides_div_pos_lt2" "pz" "1" "py" "y!1" "px" "1" ))"2" (rewrite "div_simp" )"2" assert )"2" "1/y!1" )"1" "1" rewrite "inv_nnreal_expt" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )nil nnreal_expt nil )"nzreal" nil )nil real_types nil )"bool" functions nil )nil real_types nil )"{r | r <= 1}" nnreal_expt nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil nnreal_expt nil )nil real_props nil )"boolean" notequal nil )nil reals nil ))nil 3428142252"" (skosimp)"" (split)"1" (expand "extend" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "nn_rational_expt(gt1x!1, 0)" )"1" (typepred "nn_rational_expt(gt1x!1, 0)" )"1" (assert )"1" (inst + "0" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (expand "bounded_above?" )"2" (expand "upper_bound?" )"2" (lemma "density_positive" ("x" "py!1" "y" "py!1+1" ))"2" (assert )"2" (skosimp)"2" (inst + "nn_rational_expt(gt1x!1, r!1)" )"1" (skosimp)"1" (typepred "s!1" )"1" (assert )"1" (skosimp)"1" "nn_rational_expt_increasing" "q" "q!1" "r" "r!1" "x" "gt1x!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nnreal" nn_rational_expt nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals 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]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" sets nil )"R" extend nil )"bool" bounded_real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil rational_props nil )"posreal" nil )nil nn_rational_expt nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"rat" nnreal_expt nil )nil rationals nil )"(total_order?[real])" nil )"bool" bounded_real_defs nil ))nil ))nil 3428142943"" (skosimp)"" (expand "nnreal_expt" )"" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(gt1x!1, q)}))") "" "LE" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(gt1x!1, q)}))") "" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(gt1x!1, q)}))") "" "LT" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(gt1x!1, q)}))") "" (expand "extend" )"" (expand "least_upper_bound?" )"" (expand "upper_bound?" )"" (flatten)"" (inst-cp -2 "LE" )"" (split -3)"1" (expand "<=" -1)"1" (split -1)"1" "1" "LT" )"1" "1" (assert ) nil nil )"2" "2" "s!1" )"2" replace -2 -1)"2" "2" expand "<=" -1)"2" "1" "s!1" )"1" "q!1" )"1" assert )nil nil ))nil ))nil )"2" case "s!1=LE" )"1" replace -1)"1" assert )"1" "EPS" "(LE-LT)/2" )"1" case "LT>1" )"1" "nn_rational_expt_approx_gt1" "x" "gt1x!1" "y" "LT+EPS" "epsilon" "EPS" ))"1" assert )"1" "1" case "LT<nn_rational_expt(gt1x!1, q!2)& nn_rational_expt(gt1x!1, q!2)<LE" )"1" "1" "1" case "q!2<q!1" )"1" "nn_rational_expt(gt1x!1, q!2)" )"1" assert )nil nil )"2" "nn_rational_expt(gt1x!1, q!2)" )"2" assert )"2" "q!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "q!2=q!1" )"1" assert )nil nil )"2" "nn_rational_expt_increasing" "q" "q!1" "r" "q!2" "x" "gt1x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "DRL" "nn_rational_expt(gt1x!1, q!2)" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" "density_positive" "x" "0" "y" "py!1" ))"2" assert )"2" "2" "nn_rational_expt(gt1x!1, r!1)" )"1" "nn_rational_expt_gt1" "x" "gt1x!1" "pq" "r!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "nn_rational_expt(gt1x!1, r!1)" )"1" assert )"1" "r!1" )nil nil ))nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "s!1" )"2" "s!1" )"2" "1" assert )nil nil )"2" "2" "s!2" )"2" assert )"2" "2" "nn_rational_expt_increasing" "q" "q!2" "r" "q!1" "x" "gt1x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp)"2" (typepred "s!1" )"2" assert )"2" "2" "s!1" )"2" "q!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nnreal_expt nil )"odd_int" integers nil )nil nn_rational_expt nil )"nnrat" nnreal_expt nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil nn_rational_expt nil )"real" reals nil )"real" reals nil )nil rationals nil )"rat" nnreal_expt nil )nil rationals nil )nil rationals nil )nil nn_rational_expt nil )nil rational_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"(total_order?[real])" nil )"posreal" nnreal_expt nil )"{r | r > 1}" nnreal_expt nil )"(LAMBDA (t: real): IF t >= 0 THEN EXISTS q: q <= py!1 AND t = nn_rational_expt(gt1x!1, q)" nnreal_expt nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(LAMBDA (t: real): IF t >= 0 THEN EXISTS q: q < py!1 AND t = nn_rational_expt(gt1x!1, q)" nnreal_expt nil) "bool" bounded_real_defs nil )"bool" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" reals nil )nil real_types nil )"bool" booleans nil )"R" extend nil )"[real -> boolean]" rationals nil )nil rationals nil )nil rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"nnreal" nn_rational_expt nil ))nil 3427462388"" case "FORALL (a, b:nnreal, x: posreal): x>1 => ") "1" (skosimp)"1" (case-replace "x!1=0" )"1" (hide -2 -1)"1" (rewrite "nnreal_expt_0a" )"1" (rewrite "nnreal_expt_0a" )"1" (rewrite "nnreal_expt_0a" ) (("1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (case-replace "x!1=1" )"1" (rewrite "nnreal_expt_1a" )"1" (rewrite "nnreal_expt_1a" )"1" (rewrite "nnreal_expt_1a" ) nil nil )) nil ))nil )"2" (case "0<x!1&x!1<1" )"1" (flatten)"1" (inst - "a!1" "b!1" "1/x!1" )"1" (assert )"1" (rewrite "inv_nnreal_expt" )"1" (rewrite "inv_nnreal_expt" )"1" (rewrite "inv_nnreal_expt" )"1" (rewrite "div_times" )"1" (rewrite "cross_mult" )"1" (rewrite "div_mult_pos_gt1" ) nil nil )"2" (expand "/=" )"2" rewrite "zero_times3" )"2" "1" rewrite "nnreal_expt_is_0" )nil nil )"2" rewrite "nnreal_expt_is_0" )nil nil ))nil ))nil ))nil )"3" (expand "/=" )"3" rewrite "nnreal_expt_is_0" )nil nil ))nil ))nil )"2" (expand "/=" )"2" (rewrite "nnreal_expt_is_0" ) nil nil ))nil )"3" (expand "/=" )"3" (rewrite "nnreal_expt_is_0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "x!1" ))"2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (inst - "a!1" "b!1" "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (lemma "nnreal_expt_def_gt1" ("gt1x" "x!1" ))"1" (case-replace "a!1=0" )"1" (assert )"1" (lemma "nnreal_expt_rat_rew" ("x" "x!1" "q" "0" ))"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case-replace "b!1=0" )"1" (lemma "nnreal_expt_rat_rew" ("x" "x!1" "q" "0" ))"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (case "a!1>0" )"1" (case "b!1>0" )"1" (hide 1 2)"1" (inst-cp - "a!1" )"1" (inst-cp - "b!1" )"1" (inst - "a!1+b!1" )"1" "XAB" "nnreal_expt(x!1, a!1 + b!1)" )"1" "XA" "nnreal_expt(x!1, a!1)" )"1" "XB" "nnreal_expt(x!1, b!1)" )"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" replace -4)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" replace -5 * rl)"1" replace -6 * rl)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" replace -8 * rl)"1" "1" expand "least_upper_bound?" )"1" expand "extend" )"1" expand "upper_bound?" )"1" "1" "XA*XB" )"1" "1" case "XAB>1" )"1" case "XA>1" )"1" "XAB/XB" )"1" "1" rewrite "div_mult_pos_le2" "1" assert )nil nil ))nil )"2" expand "<=" "2" "1" "1" "1" "s!1" )"1" replace "1" "1" replace "1" rewrite "div_mult_pos_le2" "1" "1" expand ">=" "1" expand "<=" "1" "1" "XAB/nn_rational_expt(x!1, q!1)" )"1" "1" rewrite "div_mult_pos_le2" "1" assert )nil nil ))nil )"2" "2" "s!2" )"2" replace "2" "2" replace "2" "2" rewrite "div_mult_pos_le2" "2" rewrite "nn_rational_expt_plus" "2" "nn_rational_expt(x!1, q!1 + q!2)" )"2" "q!1+q!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "nn_rational_expt_is_0" "x" "x!1" "q" "q!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" "density_positive" "x" "0" "y" "a!1" ))"2" assert )"2" "2" "nn_rational_expt(x!1, r!1)" )"1" "nn_rational_expt_gt1" "x" "x!1" "pq" "r!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "nn_rational_expt(x!1, r!1)" )"1" assert )"1" "r!1" )nil nil ))nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "density_positive" "x" "0" "y" "a!1+b!1" ))"2" assert )"2" "2" "nn_rational_expt(x!1,r!1)" )"1" "nn_rational_expt_gt1" "x" "x!1" "pq" "r!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "nn_rational_expt(x!1, r!1)" )"1" assert )"1" "r!1" )nil nil ))nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "s!1" )"2" assert )"2" "2" replace "2" "2" "2" "EPS" "min((a!1+b!1-q!1)/2,min(a!1,b!1))" )"2" case "EPS>0&a!1>=EPS&b!1>=EPS&(a!1 + b!1 - q!1) / 2>=EPS" )"1" "1" "density_positive" "x" "a!1-EPS" "y" "a!1" ))"1" assert )"1" "1" "density_positive" "x" "b!1-EPS" "y" "b!1" ))"1" assert )"1" "1" "nn_rational_expt(x!1, r!1)" )"1" "nn_rational_expt(x!1, r!2)" )"1" "nn_rational_expt_gt1" "x" "x!1" "pq" "r!1" ))"1" "nn_rational_expt_gt1" "x" "x!1" "pq" "r!2" ))"1" assert )"1" "le_times_le_pos" "nnx" "nn_rational_expt(x!1, r!1)" "y" "XA" "nnz" "nn_rational_expt(x!1, r!2)" "w" "XB" ))"1" assert )"1" "nn_rational_expt_plus" "x" "x!1" "q" "r!1" "r" "r!2" ))"1" case "q!1<=r!1+r!2" )"1" replace "1" case "nn_rational_expt(x!1, q!1) <= nn_rational_expt(x!1, r!1 + r!2)" )"1" assert )nil nil )"2" "2" "q!1=r!1+r!2" )"1" assert )nil nil )"2" "nn_rational_expt_increasing" "q" "q!1" "r" "r!1+r!2" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "nn_rational_expt(x!1, r!2)" )"1" assert )"1" "r!2" )nil nil ))nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" "nn_rational_expt(x!1, r!1)" )"2" assert )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )nil nnreal_expt nil )"nnreal" nnreal_expt nil )"nnreal" nn_rational_expt nil )"R" extend nil )"bool" booleans nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"real" reals nil )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"{z: nonneg_real | z <= x AND z <= y}" real_defs nil )"rat" nnreal_expt nil )nil real_props nil )nil nn_rational_expt nil )"rat" rationals nil )"rat" nnreal_expt nil )nil rationals nil )"rat" nnreal_expt nil )nil rationals nil )nil rationals nil )nil nn_rational_expt nil )nil rational_props nil )"real" reals nil )"nnreal" nnreal_expt nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil nn_rational_expt nil )"nonneg_rat" nil )"nnrat" nnreal_expt nil )"nnrat" nnreal_expt nil )"posreal" nnreal_expt nil )nil nn_rational_expt nil )nil real_props nil )"(total_order?[real])" nil )"rat" nnreal_expt nil )"nnreal" nnreal_expt nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil nn_rational_expt nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )nil exponentiation nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )nil nnreal_expt nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil reals nil )nil real_props nil )"odd_int" integers nil )"posint" nil )nil nnreal_expt nil )nil real_props nil )nil extra_real_props nil )nil real_props nil )nil nnreal_expt nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nnreal" nnreal_expt nil )"boolean" notequal nil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil nnreal_expt nil )"nnreal" nil )"nnreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"nnreal" nnreal_expt nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3428096947"" case "FORALL (a, b, x: posreal): x>1 => ") "1" (skosimp)"1" (case-replace "a!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" )"1" (rewrite "nnreal_expt_1a" ) nil nil )) nil ))nil ))nil )"2" (case-replace "b!1=0" )"1" (rewrite "nnreal_expt_rat_rew" )"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" )"1" "nnreal_expt_rat_rew" "x" "nnreal_expt(x!1, a!1)" "q" "0" ))"1" (replace -1)"1" (hide -1)"1" (rewrite "nn_rational_expt_nat_rew" )"1" (rewrite "expt_x0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "a!1>0" )"1" (case "b!1>0" )"1" (case-replace "x!1=1" )"1" (rewrite "nnreal_expt_1a" )"1" (rewrite "nnreal_expt_1a" )"1" (rewrite "nnreal_expt_1a" ) nil nil )) nil ))nil )"2" (case-replace "x!1=0" )"1" (rewrite "nnreal_expt_0a" )"1" "posreal_times_posreal_is_posreal" "px" "a!1" "py" "b!1" ))"1" (assert )"1" (rewrite "nnreal_expt_0a" )"1" (rewrite "nnreal_expt_0a" ) nil nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil )"2" (case "0<x!1&x!1<1" )"1" (flatten)"1" (inst - "a!1" "b!1" "1/x!1" )"1" (assert )"1" (rewrite "inv_nnreal_expt" )"1" (rewrite "inv_nnreal_expt" )"1" rewrite "inv_nnreal_expt" )"1" rewrite "cross_mult" )"1" rewrite "div_mult_pos_gt1" )nil nil )"2" expand "/=" )"2" rewrite "nnreal_expt_is_0" )"2" rewrite "nnreal_expt_is_0" )nil nil ))nil ))nil )"3" expand "/=" )"3" rewrite "nnreal_expt_is_0" )nil nil ))nil ))nil )"2" "nnreal_expt_pos" "px" "x!1" "a" "a!1" ))"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "x!1" ))"2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (inst - "a!1" "b!1" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (lemma "nnreal_expt_def_gt1" ("gt1x" "x!1" ))"1" (inst-cp - "a!1*b!1" )"1" (inst - "a!1" )"1" (lemma "nnreal_expt_gt1" ("x" "x!1" "pa" "a!1" ))"1" "nnreal_expt_def_gt1" "gt1x" "nnreal_expt(x!1, a!1)" "py" "b!1" ))"1" (name-replace "XA" "nnreal_expt(x!1, a!1)" )"1" (assert )"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" (replace -4 * rl)"1" (hide -4)"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(XA, q)}))") "1" "XB" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(XA, q)}))") "1" replace -3)"1" "1" "XAB" "nnreal_expt(x!1, a!1 * b!1)" )"1" "lub(extend[real, nnreal, bool, FALSE] AND z = nn_rational_expt(x!1, q)}))") "1" replace -5 * rl)"1" "1" expand "extend" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "XB" )"1" "1" expand "<=" "1" "1" "1" "XAB" )"1" assert )"1" "1" "s!1" )"1" replace "1" "1" replace "1" "1" "q!1=0" )"1" rewrite "nn_rational_expt_nat_rew" )"1" rewrite "expt_x0" )"1" "1" "nn_rational_expt(x!1,0)" )"1" rewrite "nn_rational_expt_nat_rew" )"1" rewrite "expt_x0" )nil nil ))nil )"2" "nn_rational_expt(x!1, 0)" )"2" assert )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "q!1>0" )"1" "1" case "exists (r:posrat): a!1 < r & r*q!1<a!1*b!1" )"1" "1" "nn_rational_expt(x!1, r!1)" )"1" "1" expand "<=" "1" "1" "nn_rational_expt_strict_increasing" "x" "XA" "y" "nn_rational_expt(x!1, r!1)" "pq" "q!1" ))"1" assert )"1" rewrite "nn_rational_expt_times" "1" "nn_rational_expt(x!1, r!1 * q!1)" )"1" assert )nil nil )"2" "r!1*q!1" )nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" replace "2" rewrite "nn_rational_expt_times" "2" "nn_rational_expt(x!1, r!1 * q!1)" )"2" "r!1*q!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "s!2" )"2" assert )"2" "2" replace "2" expand "<=" "2" "2" "nn_rational_expt_increasing" "q" "q!2" "r" "r!1" "x" "x!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "posreal_times_posreal_is_posreal" "px" "a!1" "py" "b!1" ))"2" "density_positive" "x" "a!1" "y" "a!1*b!1/q!1" ))"1" assert )"1" rewrite "div_mult_pos_lt2" "1" "both_sides_times_pos_lt1" "pz" "a!1" "x" "q!1" "y" "b!1" ))"1" assert )"1" "1" "r!1" )"1" assert )"1" rewrite "div_mult_pos_lt2" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "2" assert )"2" "s!1" )"2" replace "2" "2" replace "2" "2" "density_positive" "x" "q!1/a!1" "y" "b!1" ))"2" assert )"2" rewrite "div_mult_pos_le2" "2" rewrite "div_mult_pos_lt1" "2" "2" "div_mult_pos_lt1" "py" "a!1" "z" "q!1" "x" "r!1" ))"2" assert )"2" "2" "nn_rational_expt(XA, r!1)" )"1" case "nn_rational_expt(x!1, q!1)<=nn_rational_expt(XA, r!1)" )"1" assert )nil nil )"2" "2" "nn_rational_expt(x!1, q!1/r!1)" )"1" expand "<=" "1" "1" "nn_rational_expt_strict_increasing" "x" "nn_rational_expt(x!1, q!1 / r!1)" "y" "XA" "pq" "r!1" ))"1" assert )"1" rewrite "nn_rational_expt_times" "1" assert )nil nil ))nil ))nil )"2" rewrite "div_mult_pos_ge1" nil nil ))nil )"2" replace "2" rewrite "nn_rational_expt_times" "1" assert )nil nil )"2" rewrite "div_mult_pos_ge1" nil nil ))nil ))nil ))nil ))nil )"2" "nn_rational_expt(x!1, q!1 / r!1)" )"1" assert )"1" "q!1/r!1" )"1" assert )"1" rewrite "div_mult_pos_lt1" nil nil ))nil )"2" rewrite "div_mult_pos_ge1" nil nil ))nil ))nil )"2" assert )"2" rewrite "div_mult_pos_ge1" nil nil ))nil ))nil )"3" rewrite "div_mult_pos_ge1" nil nil ))nil ))nil ))nil )"2" "nn_rational_expt(XA, r!1)" )"2" assert )"2" "r!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )nil nnreal_expt nil )"nnreal" nil )nil real_props nil )"real" reals nil )"nnreal" nnreal_expt nil )"rat" nnreal_expt nil )nil real_props nil )"nnrat" nnreal_expt nil )"rat" rationals nil )nil real_props nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nonneg_rat" nil )nil rationals nil )nil rationals nil )nil nn_rational_expt nil )nil nil )nil nn_rational_expt nil )"nnrat" nnreal_expt nil )"posrat" nnreal_expt nil )nil real_props nil )"rat" rationals nil )"rat" nnreal_expt nil )nil rationals nil )nil real_props nil )nil rational_props nil )"(total_order?[real])" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"posreal" nnreal_expt nil )"posreal" nnreal_expt nil )"posreal" nnreal_expt nil )"bool" bounded_real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" booleans nil )"R" extend nil )"nnreal" nn_rational_expt nil )nil nnreal_expt nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil nnreal_expt nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil nnreal_expt nil )nil reals nil )nil real_props nil )nil extra_real_props nil )nil nnreal_expt nil )nil nnreal_expt nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nnreal" nnreal_expt nil )"boolean" notequal nil )"nnreal" nnreal_expt nil )"nnreal" nnreal_expt nil )"nzreal" nil )"bool" reals nil )"(total_order?[real])" nil )nil rationals nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nnreal_expt nil )"nnreal" nil )nil exponentiation nil )nil nnreal_expt nil )"nnreal" exponentiation nil )nil nn_rational_expt nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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 )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"nnreal" nnreal_expt nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.774Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
