Quelle power.prf
Sprache: Lisp
(powernil 3250077324 ("" (grind) nil 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 )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"(strict_total_order?[real])" real_props nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3250077324 ("" (grind) nil 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 )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"real" reals nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "floor_def" ("x" "x!1+1/2" )) (("" (grind) nil nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"real" reals nil )"rat" rationals nil )"int" prelude_aux nil )"rat" rationals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"(total_order?[real])" nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_odd" ("n" "pn!1" ))"" (replace -2 -1)"" (assert )"" (hide -2)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" (replace -5 -1 rl)"" (simplify -1)"" (flatten)"" (hide -6)"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" (assert )"" (flatten)"" (inst-cp - "sx!1" )"" "e1!1 + sx!1" )"" "sx!1 - e1!1" )"" "rx!1 * e1!1" )"1" replace -7)"1" replace -8)"1" replace -9)"1" replace -10)"1" "1" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"1" "1" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"1" "1" "1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" "both_sides_times_neg_lt1" "nz" "-1" "y" "sx!1 - e1!1" "x" "rx!1 * e1!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "py" "-(rx!1 * e1!1)" "px" "-(sx!1 + e1!1)" ))"1" "both_sides_times_neg_lt1" "nz" "-1" "x" "sx!1 + e1!1" "y" "rx!1 * e1!1" ))"1" "1" "both_sides_times_pos_lt1" "x" "-((-sx!1) ^ pn!1) - 2 ^ -(1 + p!1)" "y" "-((-(e1!1 + sx!1)) ^ pn!1)" "pz" "2^p!1" ))"1" "1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "1" expand "^" "1" expand "expt" )"1" expand "expt" )"1" "both_sides_times_pos_lt1" "x" "-((-(sx!1 - e1!1)) ^ pn!1)" "y" "2 ^ -(1 + p!1) + -((-sx!1) ^ pn!1)" "pz" "2^p!1" ))"1" "1" replace "1" assert )"1" "1" "both_sides_times_neg_lt1" "nz" "-1" "y" "(-(e1!1 + sx!1)) ^ pn!1" "x" "(-(rx!1 * e1!1)) ^ pn!1" ))"1" "both_sides_times_neg_lt1" "nz" "-1" "y" "(-(rx!1 * e1!1)) ^ pn!1" "x" "(-(sx!1 - e1!1)) ^ pn!1" ))"1" "AA" "(-sx!1) ^ pn!1" )"1" "B" "(-(rx!1 * e1!1)) ^ pn!1" )"1" "C" "(-(sx!1 - e1!1)) ^ pn!1" )"1" "D" "(-(e1!1 + sx!1)) ^ pn!1" )"1" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "-C" "y" "-B" ))"1" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "-B" "y" "-D" ))"1" assert )"1" "1" "1" replace "1" replace "1" "1" replace "1" "1" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "-AA - 2 ^ -(1 + p!1)" "y" "-C" ))"1" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "-D" "y" "2 ^ -(1 + p!1) -AA" ))"1" 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 ))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" "2" "div_mult_pos_lt2" "py" "e1!1" "z" "sx!1" "x" "rx!1 - 1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )"int" integers nil )"nzreal" exponentiation nil )"rat" rationals nil )"real" reals nil )"rat" rationals nil )"posint" exponentiation nil )"real" reals nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil power nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil rationals nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"odd_int" integers nil )"posint" nil )nil real_types nil )nil real_types nil )"bool" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"real" exponentiation nil )"[T, T -> boolean]" equalities nil )"nzreal" nil )nil reals nil )nil exponentiation nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"real" reals nil )"posreal" power nil )"rat" power nil )nil prelude_aux nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil appendix nil )"posint" nil )"nzint" integers nil )"posrat" nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_even" ("n" "pn!1" ))"" (replace -2 -1)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" (assert )"" (flatten)"" (hide (-10 -13 -14 -15 -12))"" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"" (expand "^" -1 1)"" (expand "expt" )"" (expand "expt" )"" "rx!1 * e1!1" )"" "sx!1 - e1!1" )"" "e1!1 + sx!1" )"" replace -10)"" replace -11)"" replace -12)"" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(e1!1 * rx!1)" "py" "-(sx!1 - e1!1)" ))"" "both_sides_expt_pos_lt" "pm" "pn!1" "py" "-(e1!1 * rx!1)" "px" "-(sx!1 + e1!1)" ))"" assert )"" "both_sides_times_pos_lt1" "x" "(-(rx!1 * e1!1)) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"" "both_sides_times_pos_lt1" "y" "(-(rx!1 * e1!1)) ^ pn!1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "pz" "2^p!1" ))"" 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 ))nil ))nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )nil real_types nil )nil real_types nil )nil rationals nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil power nil )"real" reals nil )"rat" rationals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"odd_int" integers nil )"posint" nil )"real" reals nil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_props nil )"posrat" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil exponentiation nil )"real" reals nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"real" exponentiation nil )nil reals nil )nil exponentiation nil )nil real_props nil )"rat" rationals nil )nil prelude_aux nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil appendix nil )"posint" nil )"nzint" integers nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_odd" ("n" "pn!1" ))"" (replace -2 -1)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" (assert )"" (flatten)"" (replace -15)"" (rewrite "expt_0pn" )"" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"" (split -1)"1" (inst-cp - "rx!1*e1!1" )"1" replace -14)"1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "0" "pz" "2^p!1" ))"1" assert )"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" expand "^" -1 1)"1" expand "expt" )"1" expand "expt" )"1" replace -1 -2 rl)"1" "both_sides_times_pos_lt1" "x" "-((-(rx!1 * e1!1)) ^ pn!1)" "y" "0" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" assert )"1" "sx!1" )"1" "sx!1-e1!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "-(sx!1 - e1!1)" ))"1" "AA" "(-sx!1)^pn!1" )"1" "B" "(-(rx!1*e1!1))^pn!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-e1!1 * rx!1" "py" "-(sx!1 - e1!1)" ))"1" assert )"1" "1" "1" replace "1" "both_sides_times_pos_lt1" "x" "-AA - 2 ^ -(1 + p!1)" "y" "-B" "pz" "2^p!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "negreal_times_negreal_is_posreal" "nx" "-e1!1" "ny" "rx!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_times_neg_gt2" "nz" "-1" "x" "rx!1*e1!1" "y" "0" ))"2" "neg_times_lt" "x" "rx!1" "y" "e1!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "neg_times_lt" "x" "rx!1" "y" "e1!1" ))"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 )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )nil real_types nil )nil real_types nil )nil rationals nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil power nil )"real" reals nil )"int" integers nil )"odd_int" integers nil )"posint" nil )"nzreal" exponentiation nil )"real" reals nil )"rat" rationals nil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )"bool" reals nil )"rat" power nil )"posreal" power nil )nil real_types nil )nil real_types nil )"real" reals nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posrat" nil )"[T, T -> boolean]" equalities nil )"nzreal" real_typesnil )nil real_types nil )nil exponentiation nil )"real" exponentiation nil )nil reals nil )nil exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" reals nil )nil real_props nil )"even_int" integersnil )nil real_props nil )nil prelude_A4 nil )nil real_props nil )"rat" rationals nil )nil prelude_aux nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil appendix nil )"posint" nil )"nzint" integers nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_even" ("n" "pn!1" ))"" (replace -2 -1)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" (assert )"" (flatten)"" (hide (-10 -13 -14 -15 -16))"" (replace -11)"" (rewrite "expt_0pn" )"" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"" (split -1)"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" assert )"1" "rx!1 * e1!1" )"1" "sx!1 - e1!1" )"1" replace -13)"1" "both_sides_times_pos_lt1" "x" "0" "y" "(-(rx!1 * e1!1)) ^ pn!1" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "x" "(-(rx!1 * e1!1)) ^ pn!1" "pz" "2^p!1" ))"1" assert )"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" expand "^" -1 1)"1" expand "expt" )"1" expand "expt" )"1" replace "1" assert )"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 ))nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )nil real_types nil )nil real_types nil )nil rationals nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil power nil )"real" reals nil )"rat" rationals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"odd_int" integers nil )"posint" nil )"real" reals nil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil prelude_A4 nil )nil exponentiation nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil exponentiation nil )nil reals nil )"real" exponentiation nil )"posrat" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )nil exponentiation nil )"real" reals nil )nil real_props nil )nil real_props nil )"rat" rationals nil )nil prelude_aux nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil appendix nil )"posint" nil )"nzint" integers nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_odd" ("n" "pn!1" ))"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" (assert )"" (flatten)"" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1 + p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1 + p!1)" ))"" (case "floor(log2(pn!1)) >= 0" )"1" assert )"1" assert )"1" "1" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"1" "rx!1 * e1!1" )"1" "sx!1 - e1!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "-((-(rx!1 * e1!1)) ^ pn!1)" "pz" "2^p!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "e1!1" ))"1" "sx!1" )"1" "posreal_exp" "x" "-(e1!1 * rx!1)" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "-((-(rx!1 * e1!1)) ^ pn!1)" "y" "2 ^ -(1 + p!1) + -((-sx!1) ^ pn!1)" "pz" "2^p!1" ))"1" replace "1" assert )"1" replace "1" "1" "2 ^ (-(1 + p!1) + p!1) = 1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "expt_pos" "px" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" ))"2" "posreal_times_posreal_is_posreal" "px" "-rx!1" "py" "e1!1" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" rewrite "expt_0pn" )"2" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "e1!1" ))"2" "sx!1" )"2" "posreal_exp" "x" "-sx!1" "i" "pn!1" ))"2" "both_sides_times_pos_lt1" "x" "(-sx!1) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"2" "both_sides_times_neg_lt1" "nz" "-1" "y" "(-sx!1) ^ pn!1 * 2 ^ p!1" "x" "1/2" ))"2" "both_sides_times_neg_lt1" "nz" "-(2 ^ p!1)" "x" "(-sx!1) ^ pn!1" "y" "0" ))"2" assert )"2" replace "2" replace -10)"2" "2 ^ (-(1 + p!1) + p!1)=1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "both_sides_times_pos_lt1" "x" "0" "y" "rx!1" "pz" "e1!1" ))"3" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "rx!1 * e1!1" "py" "e1!1 + sx!1" ))"1" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" "sx!1" )"1" "posreal_exp" "x" "-sx!1" "i" "pn!1" ))"1" "posreal_exp" "x" "rx!1 * e1!1" "i" "pn!1" ))"1" "both_sides_times_neg_lt1" "nz" "-(2 ^ p!1)" "y" "0" "x" "(-sx!1) ^ pn!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "(rx!1 * e1!1) ^ pn!1" "pz" "2^p!1" ))"1" assert )"1" "2 ^ (-(1 + p!1) + p!1) = 1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "log2_strict_increasing" )"2" expand "strict_increasing?" )"2" "pn!1=1" )"1" expand "log2" )"1" rewrite "ln_1" )"1" rewrite "floor_int" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "pn!1=2" )"1" expand "log2" 2)"1" rewrite "div_simp" )"1" rewrite "floor_int" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "pn!1" )"2" expand "log2" -1 1)"2" rewrite "div_simp" )"2" (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 integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )"nzint" integers nil )"posint" nil )nil appendix nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil prelude_aux nil )"rat" rationals nil )nil real_props nil )nil exponentiation nil )nil reals nil )nil real_props nil )nil real_props nil )"nzrat" rationalsnil )"odd_int" integers nil )"odd_int" integersnil )"posreal" nil )"nzreal" nil )"nnreal" exponentiation nil )nil prelude_A4 nil )nil real_props nil )"rat" rationals nil )nil real_types nil )nil exponentiation nil )"nnreal" nil )"posreal" exponentiation nil )"posnat" exponentiation nil )"even_int" integersnil )"real" exponentiation nil )"posrat" nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"even_int" integersnil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"real" reals nil )nil real_types nil )nil real_types nil )"posreal" power nil )"rat" power nil )"(total_order?[real])" nil )"posrat" nil )"real" reals nil )"(total_order?[real])" nil )"nonneg_int" nil )"posint" nil )nil prelude_aux nil )nil ln_exp "lnexp_fnd/" )nil floor_ceil nil )"real" ln_exp "lnexp_fnd/" )nil real_props nil )nil reals nil )"bool" real_fun_preds "reals/" )nil exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"real" prelude_aux nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )nil integers nil )nil exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"int" integers nil )"posint" exponentiation nil )"real" reals nil )"nzreal" exponentiation nil )"posint" nil )"odd_int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"rat" rationals nil )"real" reals nil )nil power nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil rationals nil )nil real_types nil )nil real_types nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"bool" integers nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_even" ("n" "pn!1" ))"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" (assert )"" (flatten)"" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"" (split -1)"1" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"1" (inst-cp - "rx!1 * e1!1" )"1" (inst-cp - "sx!1 - e1!1" )"1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" "posreal_exp" "x" "-(sx!1)" "i" "pn!1" ))"1" "sx!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" "both_sides_times_pos_lt1" "x" "(-(rx!1 * e1!1)) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "2 ^ (-(1 + p!1) + p!1) = 1/2" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "e1!1" ))"1" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1+p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1 + p!1)" ))"1" "both_sides_times_pos_lt1" "x" "(-sx!1) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "(-(rx!1 * e1!1)) ^ pn!1" "pz" "2^p!1" ))"1" assert )"1" assert )"1" assert )"1" case "floor(log2(pn!1))>=0" )"1" assert )nil nil )"2" "2" "pn!1=1" )"1" expand "log2" )"1" rewrite "ln_1" )"1" rewrite "floor_int" )"1" assert )nil nil ))nil ))nil ))nil )"2" "pn!1=2" )"1" expand "log2" )"1" rewrite "div_simp" )"1" rewrite "floor_int" )"1" assert )nil nil ))nil ))nil ))nil )"2" "log2_strict_increasing" )"2" expand "strict_increasing?" )"2" "2" "pn!1" )"2" expand "log2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1 -2))"2" (assert ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (rewrite "expt_0pn" )"2" "posreal_exp" "x" "e1!1 + sx!1" "i" "pn!1" ))"2" "both_sides_times_pos_lt1" "x" "0" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"2" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"2" "sx!1" )"2" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "e1!1" ))"2" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"2" "2 ^ (-(1 + p!1) + p!1) = 1/2" )"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1+p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1 + p!1)" ))"1" "both_sides_times_pos_lt1" "x" "(-sx!1) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" assert )"1" assert )"1" replace -21 * rl)"1" case "floor(log2(pn!1))>=0" )"1" assert )nil nil )"2" "2" "pn!1=1" )"1" expand "log2" )"1" rewrite "ln_1" )"1" rewrite "floor_int" )"1" assert )nil nil ))nil ))nil ))nil )"2" "pn!1=2" )"1" expand "log2" )"1" rewrite "div_simp" )"1" rewrite "floor_int" )"1" assert )nil nil ))nil ))nil ))nil )"2" "log2_strict_increasing" )"2" expand "strict_increasing?" )"2" "2" "pn!1" )"2" expand "log2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (case "2 ^ (-(1 + p!1) + p!1) = 1 / 2" )"1" (case "floor(log2(pn!1))>=0" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "e1!1 * rx!1" "py" "e1!1 + sx!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" "sx!1" )"1" "posreal_exp" "x" "rx!1 * e1!1" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "(rx!1 * e1!1) ^ pn!1" "pz" "2 ^ p!1" ))"1" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1+p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1 + p!1)" ))"1" "both_sides_times_pos_lt1" "x" "(-sx!1) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-sx!1" "py" "e1!1" ))"1" assert )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "both_sides_times_pos_lt1" "x" "0" "y" "rx!1" "pz" "e1!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_times_pos_lt1" "x" "0" "y" "rx!1" "pz" "e1!1" ))"2" (assert ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (case-replace "pn!1=1" )"1" expand "log2" )"1" rewrite "ln_1" )"1" rewrite "floor_int" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "pn!1=2" )"1" expand "log2" )"1" rewrite "div_simp" )"1" rewrite "floor_int" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "log2_strict_increasing" )"2" expand "strict_increasing?" )"2" "2" "pn!1" )"2" expand "log2" -1 1)"2" rewrite "div_simp" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )"nzint" integers nil )"posint" nil )nil appendix nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil prelude_aux nil )"rat" rationals nil )nil real_props nil )"(total_order?[real])" nil )"bool" reals nil )"rat" power nil )"posreal" power nil )nil real_types nil )nil real_types nil )"real" reals nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"posrat" nil )nil exponentiation nil )nil integers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"real" prelude_aux nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )nil ln_exp "lnexp_fnd/" )nil floor_ceil nil )"real" ln_exp "lnexp_fnd/" )nil prelude_aux nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil reals nil )"posrat" nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"nnreal" nil )nil real_props nil )"real" exponentiation nil )"posnat" exponentiation nil )nil reals nil )nil exponentiation nil )nil exponentiation nil )"real" reals nil )nil real_props nil )nil prelude_A4 nil )"nnreal" exponentiation nil )"nzreal" nil )"even_int" integersnil )"posreal" nil )"odd_int" integersnil )"odd_int" integers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"int" integers nil )"posint" exponentiation nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"rat" rationals nil )"real" reals nil )nil power nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil rationals nil )nil real_types nil )nil real_types nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"int" prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"real" reals nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" (assert )"" (flatten)"" (hide -9)"" (replace -7)"" (rewrite "expt_0pn" )"" "div_mult_pos_lt1" "py" "e1!1" "z" "0" "x" "rx!1+1" ))"" "div_mult_pos_lt2" "py" "e1!1" "z" "0" "x" "rx!1-1" ))"" (assert )"" (hide (-11 -12 -9))"" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"" expand "^" -1 1)"" expand "expt" )"" expand "expt" )"" "1" "both_sides_times_pos_lt1" "y" "0" "x" "rx!1" "pz" "e1!1" ))"1" case "even?(pn!1)" )"1" "expt_neg_even" "n" "pn!1" ))"1" replace -2 -1)"1" assert )"1" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"1" "rx!1 * e1!1" )"1" replace -2)"1" "1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "e1!1" ))"1" "both_sides_times_pos_lt1" "x" "(-(rx!1 * e1!1)) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "y" "(-(rx!1 * e1!1)) ^ pn!1" "x" "0" "pz" "2^p!1" ))"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "odd_even" 1)"2" "expt_neg_odd" "n" "pn!1" ))"2" replace -2 -1)"2" assert )"2" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"2" "-e1!1" )"2" "rx!1 * e1!1" )"2" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"2" replace "2" "AA" "(-(rx!1 * e1!1)) ^ pn!1" )"2" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(e1!1 * rx!1)" "py" "e1!1" ))"2" "2" replace "2" assert )"2" "both_sides_times_neg_lt1" "y" "AA" "x" "e1!1 ^ pn!1" "nz" "-1*2^p!1" ))"2" "both_sides_times_neg_lt1" "x" "AA" "y" "0" "nz" "-1*2^p!1" ))"2" assert )"2" "both_sides_times_neg_lt1" "x" "2 ^ -(1 + p!1)" "y" "e1!1 ^ pn!1" "nz" "2 ^ p!1 * -1" ))"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 )"2" replace -1)"2" rewrite "expt_0pn" )"2" (assert ) nil nil ))nil ))nil )"3" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "e1!1 * rx!1" "py" "e1!1" ))"1" assert )"1" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "y" "(rx!1 * e1!1) ^ pn!1" "x" "-1 * 2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "1" replace "1" assert )"1" "posreal_exp" "x" "rx!1 * e1!1" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "y" "(rx!1 * e1!1) ^ pn!1" "x" "0" "pz" "2^p!1" ))"1" assert )nil nil ))nil )"2" "both_sides_times_pos_lt1" "x" "0" "y" "rx!1" "pz" "e1!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_times_pos_lt1" "x" "0" "y" "rx!1" "pz" "e1!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )nil integers nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil rationals nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power nil )"real" reals nil )"int" integers nil )"odd_int" integers nil )"posint" nil )"rat" rationals nil )"real" reals nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )nil prelude_A4 nil )"nat" exponentiation nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )nil reals nil )"real" exponentiation nil )"bool" integers nil )"real" reals nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"bool" reals nil )nil real_types nil )nil real_types nil )"posrat" nil )"real" reals nil )"nzrat" rationalsnil )"nzreal" nil )"nnreal" nil )nil prelude_A4 nil )nil prelude_A4 nil )"nzreal" real_typesnil )"[T, T -> boolean]" equalities nil )nil real_props nil )"nzint" integersnil )nil prelude_aux nil )nil real_props nil )"nnreal" exponentiation nil )"posreal" nil )nil real_props nil )"real" reals nil )"nzreal" exponentiation nil )"posreal" exponentiation nil )"posreal" nil )"posrat" nil )"(total_order?[real])" nil )"nnreal" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )"nzint" integers nil )"posint" nil )nil appendix nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil prelude_aux nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_odd" ("n" "pn!1" ))"" (replace -2 -1)"" (hide -2)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" (assert )"" (flatten)"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" (assert )"" (flatten)"" (hide (-11))"" (inst - "sx!1 - e1!1" )"" (replace -7)"" "div_mult_pos_lt1" "py" "e1!1" "z" "sx!1" "x" "rx!1+1" ))"" "div_mult_pos_lt2" "py" "e1!1" "z" "sx!1" "x" "rx!1-1" ))"" assert )"" "" "" "trich_lt" "x" "rx!1" "y" "0" ))"" "1" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"1" assert )"1" "rx!1 * e1!1" )"1" replace -3)"1" "expt_plus" "i" "-(1 + p!1)" "j" "p!1" "n0x" "2" ))"1" expand "^" -1 1)"1" expand "expt" )"1" expand "expt" )"1" "1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" assert )"1" "both_sides_times_pos_lt1" "x" "-((-(rx!1 * e1!1)) ^ pn!1)" "pz" "2^p!1" "y" "0" ))"1" "posreal_exp" "x" "-(sx!1 - e1!1)" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "0" "pz" "2^p!1" ))"1" "both_sides_times_pos_lt1" "y" "sx!1 ^ pn!1 + 2 ^ -(1 + p!1)" "x" "0" "pz" "2^p!1" ))"1" "1" replace "1" "posreal_exp" "x" "e1!1 + sx!1" "i" "pn!1" ))"1" assert )"1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" assert )"1" assert )"1" "AA" "(-(rx!1 * e1!1)) ^ pn!1" )"1" "B" "sx!1 ^ pn!1" )"1" "both_sides_times_neg_lt1" "nz" "2^p!1 * -1" "y" "AA" "x" "(-(sx!1 - e1!1)) ^ pn!1" ))"1" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "B - 2 ^ -(1 + p!1)" "y" "-AA" ))"1" "1" replace "1" 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 ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" rewrite "expt_0pn" )"2" "posreal_exp" "x" "-(sx!1 - e1!1)" "i" "pn!1" ))"2" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "0" "pz" "2^p!1" ))"2" "posreal_exp" "x" "sx!1" "i" "pn!1" ))"2" "both_sides_times_pos_lt1" "x" "0" "y" "sx!1 ^ pn!1" "pz" "2^p!1" ))"2" assert )"2" "both_sides_times_neg_lt1" "y" "0" "x" "(-(sx!1 - e1!1)) ^ pn!1" "nz" "-1" ))"2" assert )"2" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"2" expand "^" "2" expand "expt" )"2" expand "expt" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "e1!1 * rx!1" "py" "e1!1 + sx!1" ))"1" "posreal_exp" "x" "e1!1 * rx!1" "i" "pn!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" expand "^" -1 1)"1" expand "expt" )"1" expand "expt" )"1" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "pz" "2 ^ p!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "0" "pz" "2^p!1" ))"1" "1" replace "1" "posreal_exp" "x" "-(sx!1 - e1!1)" "i" "pn!1" ))"1" assert )"1" assert )"1" assert )"1" "both_sides_times_pos_lt1" "y" "(rx!1 * e1!1) ^ pn!1" "x" "0" "pz" "2^p!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_times_pos_lt1" "y" "rx!1" "x" "0" "pz" "e1!1" ))"2" (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 integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )"int" integers nil )"nzreal" exponentiation nil )"rat" rationals nil )"real" reals nil )"rat" rationals nil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nzint" integers nil )"posint" nil )nil appendix nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil prelude_aux nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )"real" reals nil )"real" reals nil )"nnreal" nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )"nzint" integersnil )"[T, T -> boolean]" equalities nil )nil exponentiation nil )"posrat" nil )"real" exponentiation nil )nil reals nil )nil exponentiation nil )nil real_props nil )nil prelude_A4 nil )"nnreal" exponentiation nil )"nzreal" nil )"posreal" nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integers nil )"real" reals nil )nil power nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil rationals nil )nil real_types nil )nil real_types nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"bool" integers nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "expt_neg_even" ("n" "pn!1" ))"" (replace -2 -1)"" (hide -2)"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" "div_mult_pos_lt1" "py" "e1!1" "z" "sx!1" "x" "rx!1+1" ))"" "div_mult_pos_lt2" "py" "e1!1" "z" "sx!1" "x" "rx!1-1" ))"" (case "floor(log2(pn!1))>=0" )"1" (case-replace "2 ^ (-(1 + p!1) + p!1) = 1/2" )"1" (lemma "trich_lt" ("x" "rx!1" "y" "0" ))"1" (split -1)"1" "both_sides_times_pos_lt1" "x" "rx!1" "y" "0" "pz" "e1!1" ))"1" (inst-cp - "rx!1 * e1!1" )"1" "sx!1 -e1!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "-(rx!1 * e1!1)" "py" "-(sx!1 - e1!1)" ))"1" "both_sides_times_pos_lt1" "x" "(-(rx!1 * e1!1)) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "sx!1" "py" "e1!1" ))"1" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1+p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1+p!1)" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "posreal_exp" "x" "-(rx!1 * e1!1)" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "(-(rx!1 * e1!1)) ^ pn!1" "pz" "2^p!1" ))"1" assert )"1" "1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" assert )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "posreal_exp" "x" "e1!1 + sx!1" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "0" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "sx!1" "py" "e1!1" ))"1" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1+p!1)" ))"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1 + p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2 ^ p!1" ))"1" assert )"1" "1" replace -10)"1" replace -6 * rl)"1" replace -22 * rl)"1" replace -4)"1" "expt_pos" "px" "sx!1" "i" "pn!1" ))"1" "expt_pos" "px" "2" "i" "p!1" ))"1" "posreal_times_posreal_is_posreal" "px" "sx!1 ^ pn!1" "py" "2 ^ p!1" ))"1" assert )"1" "sx!1 - e1!1" )"1" assert )"1" replace "1" case "Y!1=0" )"1" assert )nil nil )"2" "2" expand "^" )"2" expand "expt" "2" expand "round" )"2" "floor_def" "x" "1/2" ))"2" "2" assert )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 ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (inst-cp - "sx!1 - e1!1" )"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "e1!1 * rx!1" "py" "e1!1 + sx!1" ))"1" "posreal_exp" "x" "e1!1 * rx!1" "i" "pn!1" ))"1" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "pz" "2 ^ p!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" ))"1" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "sx!1" "py" "e1!1" ))"1" "expt_times" "n0x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1)" "j" "pn!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-(3 + floor(log2(pn!1)) + p!1) * pn!1" "j" "-(1 + p!1)" ))"1" "lt_times_lt_pos1" "px" "1" "y" "pn!1" "nnz" "1 + p!1" "w" "3 + floor(log2(pn!1)) + p!1" ))"1" "both_sides_times_pos_lt1" "x" "sx!1 ^ pn!1" "y" "2 ^ -(1 + p!1)" "pz" "2^p!1" ))"1" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"1" "posreal_times_posreal_is_posreal" "px" "(e1!1 * rx!1) ^ pn!1" "py" "2 ^ p!1" ))"1" assert )"1" "1" assert )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "expt_pos" "px" "e1!1*rx!1" "i" "pn!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )"3" "posreal_times_posreal_is_posreal" "px" "e1!1" "py" "rx!1" ))"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (case-replace "pn!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "pn!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" rewrite "floor_int" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" "2" "pn!1" )"2" expand "log2" -1 1)"2" rewrite "div_simp" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil prelude_A4 nil )"nzint" integers nil )"posint" nil )nil appendix nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil prelude_aux nil )"rat" rationals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil real_props nil )"bool" real_fun_preds "reals/" )nil prelude_aux nil )"real" ln_exp "lnexp_fnd/" )nil floor_ceil nil )nil ln_exp "lnexp_fnd/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"posrat" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"posint" exponentiation nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"rat" power nil )"posreal" power nil )nil real_types nil )nil real_types nil )"real" reals nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil reals nil )"int" integers nil )nil exponentiation nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )nil exponentiation nil )"int" integers nil )"odd_int" integers nil )"nnreal" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"posint" nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"posrat" nil )nil real_props nil )"real" reals nil )"smallreal" power nil )"real" reals nil )nil real_props nil )"nnreal" exponentiation nil )"odd_int" integersnil )"odd_int" integers nil )"int" prelude_aux nil )"nat" floor_ceil nil )nil floor_ceil nil )"real" exponentiation nil )nil real_types nil )nil exponentiation nil )"even_int" integersnil )nil real_props nil )"posnat" exponentiation nil )"real" prelude_aux nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )nil integers nil )nil real_props nil )"rat" rationals nil )"real" reals nil )nil power nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil rationals nil )nil real_types nil )nil real_types nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (skosimp*)"" "div_mult_pos_lt1" "py" "e1!1" "x" "rx!1 + 1" "z" "sx!1" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1 - 1" "z" "sx!1" ))"" "lemma_A2_generalized" "r" "Y!1" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" ))"" (replace -6 -1 rl)"" (simplify -1)"" (assert )"" (hide (-7 -8 -6))"" (flatten)"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" (assert )"" (flatten)"" (name-replace "AA" "sx!1 - e1!1" )"" (replace -9)"" rewrite "expt_0pn" )"" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"" expand "^" -1 1)"" expand "expt" )"" expand "expt" )"" "both_sides_times_pos_lt1" "pz" "2 ^ p!1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "0" ))"" "posreal_exp" "x" "rx!1 * e1!1" "i" "pn!1" ))"" "both_sides_times_pos_lt1" "x" "0" "y" "(rx!1 * e1!1) ^ pn!1" "pz" "2^p!1" ))"" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "rx!1 * e1!1" "py" "e1!1 + sx!1" ))"" "both_sides_times_pos_lt1" "x" "(rx!1 * e1!1) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" "pz" "2^p!1" ))"" "" replace "" "" replace "" assert )"" 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 ))nil ))nil ))nil ))nil ))nil ))nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"rat" rationals nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )nil power nil )"real" reals nil )"(total_order?[real])" nil )"nzint" integers nil )"posint" nil )nil appendix nil )nil exponentiation nil )nil reals nil )"real" exponentiation nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posrat" nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil exponentiation nil )nil prelude_A4 nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"posrat" nil )"posint" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"rat" rationals nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"real" prelude_aux nil )"boolean" notequal nil )"int" integers nil )"posint" nil ))nil ))nil 3250077324"" (skosimp*)"" "div_mult_pos_lt1" ("py" "e1!1" "x" "rx!1+1" "z" "sx!1" ))"" "div_mult_pos_lt2" "py" "e1!1" "x" "rx!1-1" "z" "sx!1" ))"" (assert )"" (hide (-6 -7))"" "lemma_A4" "pn" "pn!1" "e1" "e1!1" "n" "p!1+1" "x" "sx!1" "e2" "2^-(p!1+1)" ))"" (assert )"" (flatten)"" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "sx!1 - e1!1" "py" "e1!1 * rx!1" ))"" "both_sides_expt_pos_lt" "pm" "pn!1" "py" "sx!1 + e1!1" "px" "e1!1 * rx!1" ))"" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" "y" "(e1!1 + sx!1) ^ pn!1" ))"" "both_sides_times_pos_lt1" "pz" "2^p!1" "y" "sx!1 ^ pn!1 + 2 ^ -(1 + p!1)" "x" "( sx!1-e1!1) ^ pn!1" ))"" "expt_plus" "n0x" "2" "i" "-(1 + p!1)" "j" "p!1" ))"" (expand "^" -1 1)"" expand "expt" )"" expand "expt" )"" "" replace -1 (-2 -3) rl)"" assert )"" "lemma_A2_generalized" "x" "(rx!1 * e1!1) ^ pn!1 * 2 ^ p!1" "r" "Y!1" ))"" assert )"" "" assert )"" "both_sides_expt_pos_lt" "pm" "pn!1" "px" "e1!1 * rx!1" "py" "sx!1+e1!1" ))"" "both_sides_expt_pos_lt" "pm" "pn!1" "py" "e1!1 * rx!1" "px" "sx!1-e1!1" ))"" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "(sx!1 - e1!1) ^ pn!1" "y" "(e1!1 * rx!1) ^ pn!1" ))"" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "(e1!1 * rx!1) ^ pn!1" "y" "(sx!1 + e1!1) ^ pn!1" ))"" assert )"" "both_sides_times_pos_lt1" "pz" "2^p!1" "x" "(e1!1 + sx!1) ^ pn!1" "y" "2 ^ -(1 + p!1) + sx!1 ^ pn!1" ))"" "both_sides_times_pos_lt1" "pz" "2^p!1" "y" "(sx!1-e1!1) ^ pn!1" "x" "sx!1 ^ pn!1 - 2 ^ -(1 + p!1)" ))"" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"rat" rationals nil )"int" integers nil )"real" reals nil )"posint" exponentiation nil )"real" reals nil )"int" integers nil )"int" integers nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nzint" integers nil )"posint" nil )nil appendix nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil naturalnumbers nil )nil integers nil )nil integers nil )nil power nil )"(total_order?[real])" nil )"posrat" nil )"real" exponentiation nil )nil reals nil )nil exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"rat" rationals nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"posint" nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"posint" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"rat" exponentiation nil )"posnat" exponentiation nil )"rat" rationals nil )"boolean" notequal nil )"int" prelude_aux nil )"real" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324"" (skosimp*)"" (lemma "trich_lt" ("x" "sx!1" "y" "0" ))"" (name "e1!1" "2^-(p!1+floor(log2(pn!1))+3)" )"" (replace -1)"" "expt_inverse" "i" "-(p!1 + floor(log2(pn!1)) + 3)" "n0x" "2" ))"" (replace -2 -1)"" (replace -1 (-5 -6))"" (hide -1)"" (split -2)"1" (lemma "trich_lt" ("x" "sx!1+e1!1" "y" "0" ))"1" (split -1)"1" (case "even?(pn!1)" )"1" "cauchy_power_lt1_n_even" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"1" (assert ) nil nil )) nil )"2" "cauchy_power_lt1_n_odd" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (rewrite "odd_even" 1)"2" (assert ) nil nil )) nil ))nil ))nil )"2" (case "even?(pn!1)" )"1" "cauchy_power_lt1_snz_even" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"1" (assert ) nil nil )) nil )"2" "cauchy_power_lt1_snz_odd" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (rewrite "odd_even" 1)"2" (assert ) nil nil )) nil ))nil ))nil )"3" (case "even?(pn!1)" )"1" "cauchy_power_lt1_sn_even" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"1" (assert ) nil nil )) nil )"2" (rewrite "odd_even" 1)"2" "cauchy_power_lt1_sn_odd" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" "cauchy_power_lt1_z" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (assert ) nil nil )) nil )"3" (lemma "trich_lt" ("x" "sx!1-e1!1" "y" "0" ))"3" (split -1)"1" (case "even?(pn!1)" )"1" "cauchy_power_lt1_sp_even" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"1" (assert ) nil nil )) nil )"2" (rewrite "odd_even" 1)"2" "cauchy_power_lt1_sp_odd" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"2" "cauchy_power_lt1_pz" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"2" (assert ) nil nil )) nil )"3" "cauchy_power_lt1_p" "pn" "pn!1" "sx" "sx!1" "e1" "e1!1" "p" "p!1" "Y" "Y!1" "rx" "rx!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"int" integers nil )"rat" exponentiation nil )"posint" exponentiation nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil power nil )nil power nil )nil power nil )nil power nil )nil power nil )"real" reals nil )nil power nil )nil power nil )nil power nil )nil power nil )"bool" integers nil )"int" integers nil )"real" reals nil )"rat" rationals nil )"posrat" nil )"real" reals nil )"rat" rationals nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )nil rationals nil )nil power nil )nil prelude_aux nil )nil power nil )nil reals nil )nil exponentiation nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" prelude_aux nil )nil integers nil )nil integers nil )nil rationals nil )nil rationals nil ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"posint" nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324"" (subtype-tcc) nil nil )"posint" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )"rat" exponentiation nil )"posnat" exponentiation nil )"rat" rationals nil )"boolean" notequal nil )"int" prelude_aux nil )"real" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324"" (skosimp*)"" "cauchy_power_lt1_main_generalized" "pn" "pn!1" "sx" "sx!1" "p" "p!1" "Y" "Y!1" "rx" "X!1" ))"" (assert ) nil nil )) nil ))nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil rationals nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"rat" rationals nil )"rat" exponentiation nil )"int" integers nil )"posint" exponentiation nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil ))nil ))nil 3250077324"" (skosimp*)"" (case-replace "pn!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "pn!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "pn!1" )"2" (expand "log2" -1 1)"2" (rewrite "div_simp" ) (("2" (assert ) nil nil ))nil ))nil ))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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"int" integers nil )nil ln_exp "lnexp_fnd/" )"real" reals nil )"(total_order?[real])" nil )"real" ln_exp "lnexp_fnd/" )nil real_types nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil integers nil )nil floor_ceil nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" prelude_aux nil )nil prelude_aux nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"nat" floor_ceil nil )"posint" nil )"even_int" integersnil )nil real_props nil )nil reals nil ))nil ))nil 3287579065"" (lemma "cauchy_power_lt1_isreal_TCC1" ) (("" (assert ) nil nil ))nil )"posint" nil )nil power nil ))nil 3563629402"" (subtype-tcc) nil nil )"posint" nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324"" (skosimp*)"" (case "floor(log2(pn!1))>=0" )"1" (typepred "scx!1" )"1" (expand "cauchy_real?" )"1" (expand "cauchy_smallreal?" )"1" (expand "cauchy_prop" )"1" (skosimp*)"1" (inst + "sx!1^pn!1" )"1" (skosimp*)"1" (inst - "3 + p!1 + floor(log2(pn!1))" )"1" (flatten)"1" "cauchy_power_lt1_main" "Y" "round((scx!1(3 + p!1 + floor(log2(pn!1))) * " " p" " p!1" " pn" " pn!1" " sx" " sx!1" " X" "scx!1(3 + p!1 + floor(log2(pn!1)))" ))"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (case-replace "pn!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (case-replace "pn!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "pn!1" )"2" (expand "log2" -1 1)"2" (rewrite "div_simp" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil integers nil )nil integers nil )"real" prelude_aux nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"posint" nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"rat" exponentiation nil )"posint" exponentiation nil )"bool" cauchy nil )"bool" cauchy nil )"(total_order?[real])" nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"posnat" power nil )"nat" power nil )"int" integers nil )"rat" rationals nil )nil power nil )"int" prelude_aux nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil ln_exp "lnexp_fnd/" )"real" reals nil )nil floor_ceil nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" ln_exp "lnexp_fnd/" )nil prelude_aux nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil reals nil ))nil ))nil 3250077324"" (skosimp)"" (lemma "cauchy_power_lt1_isreal" ("scx" "scx!1" "pn" "pn!1" ))"" (propax) nil nil )) nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" cauchy nil )"boolean" notequal nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (expand "cauchy_prop" )"" (skosimp*)"" (case "p!1+floor(log2(pn!1))+3>=0" )"1" (inst - "p!1+floor(log2(pn!1))+3" )"1" (flatten)"1" (expand "cauchy_power_lt1" )"1" "cauchy_power_lt1_main" "Y" "round((scx!1(3 + p!1 + floor(log2(pn!1))) * " " p" " p!1" " pn" " pn!1" " sx" " sx!1" " X" "scx!1(3 + p!1 + floor(log2(pn!1)))" ))"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (case-replace "pn!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "pn!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "pn!1" )"2" expand "log2" -1 1)"2" rewrite "div_simp" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert )"2" (hide-all-but 1)"2" (case-replace "pn!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "pn!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "pn!1" )"2" (expand "log2" -1 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" exponentiation nil )"bool" cauchy nil )nil integers nil )nil integers nil )"real" prelude_aux nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"int" integers nil )"int" integers nil )"rat" rationals nil )nil power nil )"bool" cauchy nil )nil cauchy nil )"int" prelude_aux nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil prelude_aux nil )"posint" nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )nil ln_exp "lnexp_fnd/" )"real" reals nil )"real" reals nil )nil floor_ceil nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" ln_exp "lnexp_fnd/" )nil prelude_aux nil )"bool" real_fun_preds "reals/" )"nat" floor_ceil nil )"even_int" integersnil )nil real_props nil )nil reals nil )"cauchy_real" power nil )"rat" exponentiation nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"nat" power nil )"posnat" power nil )"(total_order?[real])" nil ))nil ))nil 3250077324"" (skosimp*)"" (case "floor(log2(abs(X0!1) + 1))>=0" )"1" (case "p!1>=1" )"1" (lemma "lemma_A3" ("i" "p!1-1" "px" "abs(X0!1) + 1" ))"1" (assert )"1" (flatten)"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "p!1 - 1" "j" "p!1" ))"1" (simplify -1)"1" (lemma "posreal_exp" ("x" "2" "i" "p!1" ))"1" (expand "abs" )"1" (case "X0!1 < 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but 1)"2" (case "FORALL (n:posnat): floor(log2(n)) >= 0" )"1" (inst - "abs(X0!1) + 1" ) nil nil )"2" (hide 2)"2" (skosimp*)"2" (case-replace "n!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "n!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "n!1" )"2" (expand "log2" -1 1)"2" (rewrite "div_simp" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"real" prelude_aux nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"posint" nil )"int" integers nil )nil appendix nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"nzint" integers nil )"posint" exponentiation nil )nil naturalnumbers nil )nil integers nil )nil integers nil )nil reals nil )nil real_props nil )"bool" real_fun_preds "reals/" )nil prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil floor_ceil nil )"real" reals nil )nil ln_exp "lnexp_fnd/" )"[T, T -> boolean]" equalities nil )"{j: nonneg_int | j >= i}" nil ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"{j: nonneg_int | j >= i}" nil )"posint" nil )"int" integers nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posnat" exponentiation nil )"real" exponentiation nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"posnat" exponentiation nil )"rat" exponentiation nil )"rat" rationals nil )"posint" nil )"int" integers nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"{j: nonneg_int | j >= i}" nil )"boolean" notequal nil )"real" prelude_aux nil )"real" integral_def "analysis/" )"real" ln_exp "lnexp_fnd/" )"int" prelude_aux nil )"real" exponentiation nil ))nil ))nil 3250077324"" (skosimp*)"" (lemma "cauchy_power_div1" ("X0" "X0!1" "x" "x!1" "p" "q!1" ))"" (assert )"" (flatten)"" (case "FORALL (n:posnat): floor(log2(n)) >= 0" )"1" (inst-cp - "1+abs(X0!1)" )"1" (inst - "pn!1" )"1" "cauchy_power_lt1_main_generalized" "pn" "pn!1" "sx" "x!1*2^-q!1" "rx" "X!1*2^-q!1" "p" "p!1+pn!1*q!1" "Y" "Y!1" ))"1" "expt_product_n0i" "x" "x!1" "y" "2 ^ -q!1" "pn" "pn!1" ))"1" "expt_times" "n0x" "2" "i" "-q!1" "j" "pn!1" ))"1" "expt_plus" "n0x" "2" "i" "-q!1 * pn!1" "j" "p!1 + pn!1 * q!1" ))"1" "expt_plus" "n0x" "2" "i" "-1 *q!1 * pn!1" "j" "q!1* pn!1 +p!1 " ))"1" "expt_inverse" "n0x" "2" "i" "p1!1" ))"1" "expt_product_n0i" "x" "X!1/2 ^ p1!1" "y" "2 ^ -q!1" "pn" "pn!1" ))"1" "expt_plus" "n0x" "2" "i" "pn!1 * q!1" "j" "p!1" ))"1" "expt_plus" "n0x" "2" "i" "-q!1 * pn!1" "j" "pn!1 * q!1" ))"1" rewrite "expt_x0" )"1" "both_sides_times_pos_lt1" "x" "X!1 - 1" "y" "x!1 * 2 ^ p1!1" "pz" "2 ^ -q!1" ))"1" "both_sides_times_pos_lt1" "y" "X!1 + 1" "x" "x!1 * 2 ^ p1!1" "pz" "2 ^ -q!1" ))"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "-q!1" "j" "0" ))"1" rewrite "expt_x0" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "expt_inverse" ("n0x" "2" "i" "q!1" ))"2" "div_mult_pos_lt1" "py" "2 ^ q!1" "x" "1" "z" "x!1" ))"2" "div_mult_pos_lt2" "py" "2 ^ q!1" "x" "-1" "z" "x!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (case-replace "n!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (case-replace "n!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "n!1" )"2" (expand "log2" -1 1)"2" (rewrite "div_simp" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power nil )"[T, T -> boolean]" equalities nil )nil ln_exp "lnexp_fnd/" )nil floor_ceil nil )"real" ln_exp "lnexp_fnd/" )nil prelude_aux nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil reals nil )"posint" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"nonneg_int" nil )"int" integers nil )nil power nil )"[numfield, numfield -> numfield]" number_fields nil )nil rationals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil prelude_aux nil )"nnrat" exponentiation nil )nil exponentiation nil )nil reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"rat" rationals nil )"rat" rationals nil )"nzint" integers nil )"posrat" nil )"posint" nil )"posrat" nil )"odd_int" integers nil )"posrat" exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil prelude_A4 nil )nil real_props nil )"nzint" integersnil )"real" reals nil )nil real_props nil )"real" prelude_aux nil )nil real_types nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil )"posint" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"rat" rationals nil )"rat" exponentiation nil )"rat" rationals nil )"real" reals nil )"{j: nonneg_int | j >= i}" nil ))nil ))nil 3250077324"" (skosimp*)"" (case "FORALL (n:posnat): floor(log2(n)) >= 0" )"1" (inst-cp - "pn!1" )"1" (inst - "abs(cx!1(0))+1" )"1" "posreal_times_posreal_is_posreal" "px" "pn!1" "py" "1 + floor(log2(abs(cx!1(0)) + 1))" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (case-replace "n!1=1" )"1" (expand "log2" )"1" (rewrite "ln_1" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (case-replace "n!1=2" )"1" (expand "log2" )"1" (rewrite "div_simp" )"1" (rewrite "floor_int" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "log2_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "2" "n!1" )"2" (expand "log2" -1 1)"2" (rewrite "div_simp" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" prelude_aux nil )nil real_types nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers 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]" number_fieldsnil )nil booleans nil )nil numbers nil )"{j: nonneg_int | j >= i}" nil )"posint" nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"nzint" integers nil )"nnrat" exponentiation nil )"rat" rationals nil )"nonneg_int" nil )"posint" nil )"nonneg_int" nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"int" integers nil )nil reals nil )nil real_props nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )nil prelude_aux nil )"real" ln_exp "lnexp_fnd/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil floor_ceil nil )"real" reals nil )nil ln_exp "lnexp_fnd/" )"[T, T -> boolean]" equalities nil ))nil ))nil 3250077324"" (skosimp)"" (typepred "cx!1" )"" (expand "cauchy_real?" )"" (skosimp)"" (inst + "x!1^pn!1" )"" (expand "cauchy_prop" )"" (skosimp)"" (inst-cp - "0" )"" (name-replace "X0!1" "cx!1(0)" )"" (rewrite "expt_x0" )"" (typepred "floor_log2(1 + abs(X0!1))" )"" (typepred "floor_log2(pn!1)" )"" (rewrite "floor_log2_def" )"" (rewrite "floor_log2_def" )"" "QF" "floor(log2(1+abs(X0!1)))" )"" "posreal_times_posreal_is_posreal" "px" "QF+1" "py" "pn!1" ))"1" "P1" "3 + p!1 + floor(log2(pn!1))+(QF+1)*pn!1" )"1" replace -1)"1" "cauchy_power_main" "X0" "X0!1" "x" "x!1" "q" "QF+1" "p1" "P1" "p" "p!1" "X" "cx!1(P1)" "Y" "round((cx!1(P1) * 2 ^ -P1) ^ pn!1 * 2 ^ p!1)" "pn" "pn!1" ))"1" "1" rewrite "expt_inverse" )"1" assert )"1" "P1" )"1" replace -6)"1" expand "QF" -1)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (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 )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals 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]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cauchy nil )nil exponentiation nil )"int" integers nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{i | i <= log2(1 + abs(X0!1)) & log2(1 + abs(X0!1)) < 1 + i}" nil )"posrat" nil )nil exponentiation nil )nil reals nil )"int" prelude_aux nil )nil power nil )"rat" rationals nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_types nil )"real" prelude_aux nil )nil appendix nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" appendix nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"posint" exponentiation nil )"rat" exponentiation nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"posint" nil )"{j: nonneg_int | j >= i}" nil ))nil ))nil 3250077324"" (lemma "cauchy_power_isreal" ) (("" (propax) nil nil )) nil )nil power nil )) nil ))nil 3250077324 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" cauchy nil )"boolean" notequal nil )"posnat" exponentiation nil ))nil ))nil 3250077324"" (skosimp)"" (expand "cauchy_prop" )"" (skosimp)"" (expand "cauchy_power" )"" "cauchy_power_main" "x" "x!1" "X0" "cx!1(0)" "q" "1+floor_log2(abs(cx!1(0))+1)" "p1" "3 + floor_log2(pn!1) + " " p" " p!1" " Y" "round((cx!1(3 + floor_log2(pn!1) + " " X" " cx!1(3 + floor_log2(pn!1) +" " pn" " pn!1")) "" (rewrite "floor_log2_def" )"" (rewrite "floor_log2_def" )"" "P1" "3 + floor(log2(pn!1)) + ") "" (inst-cp - "P1" )"1" (replace -3 -1)"1" (inst - "0" )"1" (rewrite "expt_x0" )"1" (flatten)"1" (assert )"1" rewrite "expt_inverse" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "P1" )"2" (hide-all-but 1)"2" (assert )"2" (lemma "floor_log2_def" )"2" (inst-cp - "pn!1" )"2" "floor_log2(pn!1)" )"2" "1 + abs(cx!1(0))" )"2" "floor_log2(1 + abs(cx!1(0)))" )"2" assert )"2" "both_sides_times_pos_le1" "pz" "pn!1" "x" "0" "y" "floor_log2(1 + abs(cx!1(0)))" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" exponentiation nil )"bool" cauchy nil )"{j: nonneg_int | j >= i}" nil )"posint" nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"rat" exponentiation nil )"cauchy_real" power nil )nil appendix nil )"int" integers nil )"int" integers nil )"posint" nil )"real" prelude_aux nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil integers nil )"[T, T -> boolean]" equalities nil )"even_int" integersnil )"(total_order?[real])" nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil exponentiation nil )"rat" rationals nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )nil exponentiation nil )nil reals nil )"int" power nil )"(total_order?[real])" nil )"nzint" integers nil )"rat" rationals nil )"posint" nil )nil power 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 )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" appendix nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"int" prelude_aux nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.642 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
