Quelle inv.prf
Sprache: Lisp
(invnil 3250067368 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3250067368 ("" (grind) nil nil )"real" exponentiation nil )"real" exponentiation nil ))nil ))nil 3250067368 ("" (subtype-tcc) nil nil ) nil nil ))nil 3250067368 ("" (subtype-tcc) nil nil ) nil nil ))nil 3250067368"" (skosimp*)"" (lemma "expt_plus" ("n0x" "nzx!1" "i" "s!1" "j" "s!1" ))"" (assert ) nil nil )) nil ))nil )nil reals nil )"boolean" notequal 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 exponentiation nil )"nzreal" exponentiation nil )"nonneg_int" nil )"nzreal" nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil ))nil ))nil 3250067368"" (skolem!)"" (typepred "nzcx!1" )"" (lemma "cauchy_dich5" ("nzcx" "nzcx!1" ))"" (split)"1" (lemma "cauchy_neg_characteristic" ("ncx" "nzcx!1" ))"1" (expand "cauchy_negreal?" )"1" (skolem!)"1" (typepred "x!1" )"1" (expand "cauchy_prop" )"1" (lemma "epsilon_log2" ("px" "-x!1" ))"1" (skolem!)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst -7 "p!1+4" )"1" "p!1+4" )"1" expand "member" )"1" "p!1+4" )"1" rewrite "abs_nonpos" )"1" "expt_plus" "n0x" "2" "i" "4" "j" "p!1" ))"1" expand "^" -1 2)"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" replace -1)"1" "1" "both_sides_times_pos_lt1" "x" "1" "y" "-x!1 * 2 ^ p!1" "pz" "2^p!1" ))"1" "div_mult_pos_lt1" "z" "1" "py" "2^p!1" "x" "-x!1" ))"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 )"2" (propax) nil nil ))nil )"2" (lemma "cauchy_pos_characteristic" ("pcx" "nzcx!1" ))"1" (expand "cauchy_posreal?" )"1" (skolem!)"1" (typepred "x!1" )"1" (expand "cauchy_prop" )"1" (lemma "epsilon_log2" ("px" "x!1" ))"1" (skolem!)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst - "p!1+4" )"1" "p!1+4" )"1" "p!1+4" )"1" expand "member" )"1" rewrite "abs_nonneg" )"1" "div_mult_pos_lt1" "z" "1" "py" "2^p!1" "x" "x!1" ))"1" "both_sides_times_pos_lt1" "x" "1" "y" "x!1 * 2 ^ p!1" "pz" "2^p!1" ))"1" "expt_plus" "n0x" "2" "i" "4" "j" "p!1" ))"1" expand "^" -1 2)"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" replace -1)"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 )"2" (propax) 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" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nzreal" real_typesnil )nil appendix nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" sets nil )"(total_order?[real])" nil )nil real_types nil )nil prelude_aux nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"int" integers nil )"real" exponentiation nil )"int" integers nil )"nzreal" nil )nil real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"int" integers nil )nil real_props nil )"real" exponentiation nil )"posnat" exponentiation nil )nil reals nil )"boolean" notequal nil )nil exponentiation nil )"bool" sets nil )"bool" cauchy nil )"posint" exponentiation nil )nil unique nil )"bool" cauchy nil )nil cauchy nil )nil real_types nil )nil prelude_aux nil )"posreal" nil )nil unique nil )"bool" cauchy nil )nil cauchy nil )nil unique nil ))nil ))nil 3250067368"" (lemma "minimum_inv_exists" ) (("" (propax) nil nil )) nil )nil inv nil )) nil ))nil 3250067368"" (skosimp*)"" (expand "minimum_inv" )"" (lemma "minimum_inv_exists" ("nzcx" "nzcx!1" ))"" "min_def" ("a" "s!1" "S" "{s | 3 <= abs(nzcx!1(s))}" ))"1" (grind) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"nat" inv nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )nil min_nat nil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"bool" min_nat nil )"bool" sets nil )"bool" sets nil )nil inv 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 ))nil 3250067368"" (skosimp*)"" (copy -2)"" (expand "cauchy_prop" -1)"" (inst - "s!1" )"" (lemma "minimum_inv_prop0" ("s" "s!1" "nzcx" "nzcx!1" ))"" (typepred "nzcx!1" )"" (lemma "cauchy_dich5" ("nzcx" "nzcx!1" ))"" (split -1)"1" (copy -1)"1" (expand "cauchy_negreal?" -1)"1" (skolem!)"1" (typepred "x!2" )"1" "unique_cauchy" "x" "x!1" "y" "x!2" "cx" "nzcx!1" ))"1" (replace -4 -1)"1" replace -10 -1)"1" "1" replace -1)"1" rewrite "abs_nonpos" 1)"1" "cauchy_neg_characteristic" "ncx" "nzcx!1" "p" "s!1" ))"1" rewrite "abs_nonpos" -8)"1" "1" "both_sides_plus_le1" "x" "3" "y" "-nzcx!1(s!1)" "z" "-1" ))"1" "both_sides_times_neg_lt1" "y" "x!2 * 2 ^ s!1" "x" "1 + nzcx!1(s!1)" "nz" "-1" ))"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cauchy_pos_characteristic" "pcx" "nzcx!1" "p" "s!1" ))"1" (rewrite "abs_nonneg" -4)"1" (expand "cauchy_posreal?" )"1" (skolem!)"1" "unique_cauchy" "x" "x!1" "y" "x!2" "cx" "nzcx!1" ))"1" (replace -3 -1)"1" replace -8 -1)"1" "1" replace -1)"1" "x!2" )"1" rewrite "abs_nonneg" 1)"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )NOT const-decl "[bool -> bool]" booleans nil )"bool" cauchy nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil unique nil )nil cauchy nil )"int" integers nil )"nzreal" nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nat" inv nil )"int" integers nil )"even_int" integersnil )"(total_order?[real])" nil )"posrat" nil )"posnat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"odd_int" integers nil )"int" integers nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"{y: posreal | y >= x}" nil )nil prelude_aux nil )nil real_types nil )nil cauchy nil )"bool" cauchy nil )nil unique nil )nil real_types nil )nil prelude_aux nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil cauchy nil )"bool" cauchy nil )nil unique nil )nil unique nil )nil inv nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )"posint" exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "trich_lt" ("x" "nzx!1" "y" "0" ))"" (lemma "expt_ge1" ("b" "2" ))"" (lemma "expt_plus" ("n0x" "2" ))"" (inst-cp -2 "p!1 + s!1 + 2" )"" (inst-cp -1 "p!1 + s!1 + 2" "s!1" )"" (replace -2)"" "both_sides_times_pos_le1" "x" "2" "y" "abs(nzx!1) * 2 ^ s!1" "pz" "2 ^ (p!1 + s!1 + 2)" ))"" (replace -7 -1)"" (flatten -1)"" (name "AA" "2 ^ (p!1 + s!1 + 2)" )"" (replace -1)"" (inst -5 "s!1" )"" (name "B" "2 ^ s!1" )"" replace -1)"" "" "1" rewrite "abs_nonpos" )"1" "both_sides_times_neg_le1" "y" "2*AA" "x" "-nzx!1 * B * AA" "nz" "-1" ))"1" (grind) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" rewrite "abs_nonneg" )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal 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 exponentiation nil )"posreal" nil )nil real_props nil )nil real_types nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields 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" integers nil )"posint" nil )nil real_types nil )nil prelude_aux nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil prelude_aux nil )"(strict_total_order?[real])" real_props nil )"nzreal" real_typesnil )"nzint" integersnil )"(total_order?[real])" nil )"int" integers nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"nzreal" nil )"odd_int" integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"even_int" integersnil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil )"posint" nil )"posint" exponentiation nil )"{y: posreal | y >= x}" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"nonneg_int" nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil exponentiation nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil ))nil ))nil 3392691345"" (skosimp*) (("" (typepred "s!1" ) (("" (assert ) nil nil )) nil ))nil )"nat" inv 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 )"bool" reals 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 )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3392691345"" (skosimp)"" (assert )"" (typepred "s!1" )"" (expand "minimum_inv" )"" (typepred "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" (inst - "s!1" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "minimum_inv_exists" ) nil nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )nil inv nil )"posint" nil )nil real_types 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 )set type-eq-decl nil sets nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"nat" inv nil ))nil ))nil 3392691816"" (skosimp*)"" (replace 1)"" (lift-if)"" (simplify 2)"" (prop)"" (typepred "nzcx!1" )"" (expand "cauchy_nzreal?" )"" (skosimp)"" (expand "cauchy_prop" )"" (inst-cp - "s!1" )"" (case "s!1>=minimum_inv(nzcx!1)" )"1" (hide 1 -4)"1" (expand "minimum_inv" )"1" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" "s!1" )"1" expand "minimum_inv" )"1" "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "minimum_inv_exists" "nzcx" "nzcx!1" ))"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"posint" nil )"int" integers 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 )"nat" inv nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )nil inv nil )"bool" cauchy nil )"posint" exponentiation nil ))nil ))nil 3392691816"" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3392693652"" (skosimp)"" (expand "minimum_inv_impl" )"" case "forall (s:{n:nat | n <= minimum_inv(nzcx!1)}): minimum_inv_aux(nzcx!1, minimum_inv(nzcx!1)-s) = minimum_inv(nzcx!1)" )"1" (inst - "minimum_inv(nzcx!1)" ) (("1" (assert ) nil nil ))nil )"2" (hide 2)"2" case "forall (n:nat): n <= minimum_inv(nzcx!1) => minimum_inv_aux(nzcx!1, minimum_inv(nzcx!1) - n) = ") "1" (skosimp)"1" (inst - "s!1" ) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (induct "n" )"1" (flatten)"1" (expand "minimum_inv_aux" )"1" (expand "minimum_inv" )"1" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" (assert ) nil nil )"2" (rewrite "minimum_inv_exists" ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "minimum_inv_aux" 1)"2" (expand "<=" -2)"2" (split -2)"1" (assert )"1" (replace -2)"1" (lift-if)"1" "1" assert )"1" "1" expand "minimum_inv" )"1" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" "MIN - 1 - j!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" rewrite "minimum_inv_exists" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (assert )"2" (replace -2)"2" "2" "2" "2" expand "minimum_inv" )"2" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" "0" )"1" (assert ) nil nil ))nil ))nil )"2" rewrite "minimum_inv_exists" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp) (("3" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 2)"3" (skosimp) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"nat" inv nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nat" inv nil )MIN skolem-const-decl "{a | AND " inv nil )nil inv nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"bool" sets nil )set type-eq-decl nil sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )nil defined_types nil )"cauchy_nzreal" inv nil )"[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" integers 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" reals nil )"bool" cauchy nil )nil cauchy nil )"nat" inv nil )"[T, T -> boolean]" equalities nil )"nat" inv nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3250067368"" (skosimp*)"" (lemma "expt_plus" ("n0x" "2" "i" "p!1 + s!1" "j" "3" ))"" (lemma "expt_ge1" ("b" "2" "n" "p!1 + s!1" ))"" (expand "^" -2 3)"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (replace -2 -3) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil naturalnumbers nil )"bool" reals 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 exponentiation nil )"nonneg_int" nil )"real" exponentiation nil )"(total_order?[real])" nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"real" exponentiation nil )"posnat" exponentiation nil )"posint" exponentiation nil )nil integers nil )"bool" reals nil )nil exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" "both_sides_minus_lt1" "x" "2 ^ (p!1 + s!1 + 3) - 1" "y" "pn!1" "z" "1" ))"" (replace -2 -1)"" (rewrite "lt_equiv_le_plus_one" -1)"" (lemma "expt_ge1" ("b" "2" "n" "2+p!1+s!1" ))"" (expand ">=" )"" "both_sides_minus_le1" "z" "1" "x" "1" "y" "2 ^ (2+ ")) "" (replace -2 -1)"" "both_sides_plus_le1" "x" "0" "y" "2 ^ (2+p!1 + s!1) - 1" "z" "2 ^ (2+p!1 + s!1)" ))"" (replace -2 -1)"" (simplify)"" "expt_plus" "n0x" "2" "i" "1" "j" "2 + p!1 + s!1" ))"" (expand "^" -1 2)"" (expand "expt" )"" expand "expt" )"" replace -1 -2 rl)"" "lt_le_transitivity" "x" "2 ^ (2 + p!1 + s!1)" "y" "2 ^ (3 + p!1 + s!1) - 1" "z" "pn!1" ))"" "total_le" )"" expand "total_order?" )"" expand "partial_order?" )"" expand "preorder?" )"" expand "transitive?" )"" "" "2 ^ (2 + p!1 + s!1)" "2 ^ (3 + p!1 + s!1) - 1" "pn!1 - 1" )"" replace -7)"" replace -10)"" replace -11)"" "" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "3 + 2 * p!1 + 2 * s!1" "j" "4 + 2 * p!1 + 2 * s!1" ))"" "" "lt_times_lt_pos1" "px" "2 ^ (2 + p!1 + s!1)" "y" "pn!1 - 1" "nnz" "2 ^ (2 + p!1 + s!1)" "w" "pn!1" ))"" replace "" replace "" "" "expt_times2" "nzx" "2" "s" "2 + p!1 + s!1" ))"" replace "" "" 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 ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans 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 )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 )"posint" nil )nil prelude_aux nil )"even_int" integersnil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"posint" nil )"int" integers nil )"(total_order?[real])" nil )nil exponentiation nil )nil reals nil )"posnat" exponentiation nil )"real" exponentiation nil )nil real_props nil )"bool" orders nil )"bool" relations nil )nil inv nil )"odd_int" integersnil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil exponentiation nil )"odd_int" integers nil )"bool" orders nil )"bool" orders nil )nil prelude_aux nil )"posint" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil integers nil )nil exponentiation nil )"even_int" integersnil )"posint" exponentiation nil )"nonneg_int" nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p1" ("p" "p!1" "s" "s!1" "pn" "pn!1" ))"" (name "t!1" "2 ^ (p!1 + s!1 + 3) - 1" )"" (replace -1)"" (name "t!2" "2 ^ (2 * p!1 + 2 * s!1 + 3)" )"" (replace -1)"" (hide (-1 -2)) (("" (grind) 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 inv nil )"nonneg_int" nil )"posint" exponentiation nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"int" integers nil )"[T, T -> boolean]" equalities 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 )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p1" ("p" "p!1" "s" "s!1" "pn" "pn!1" ))"" "both_sides_times_pos_lt2" "x" "2 ^ (2 * p!1 + 2 * s!1 + 2) / pn!1 - (pn!1 - 1) / 2" "y" "0" "pz" "2" ))"" (replace -1 1 rl)"" (simplify 1)"" (rewrite "div_cancel1" )"" (rewrite "times_div1" )"" (hide -1)"" "both_sides_times_pos_lt2" "x" "(2 * 2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1 - (pn!1 - 1)" "y" "0" "pz" "pn!1" ))"" (replace -1 1 rl)"" (hide -1)"" (simplify 1)"" (rewrite "div_cancel2" )"" "both_sides_plus_lt1" "x" "(2 * 2 ^ (2 + 2 * p!1 + 2 * s!1)) - pn!1 * pn!1 + pn!1" "y" "0" "z" "pn!1 * pn!1 + pn!1" ))"" replace -1 1 rl)"" "" "" (grind) 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 inv nil )nil reals nil )nil real_props nil )"posrat" nil )"even_int" integersnil )"int" integers nil )nil real_props nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"odd_int" integers nil )"odd_int" integers nil )"even_int" integersnil )"odd_int" integersnil )"real" exponentiation nil )nil real_props nil )"posint" nil )"odd_int" integers nil )nil real_props nil )"(divides(m))" divides nil )"posint" nil )"int" integers nil )"rat" rationals nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil )"nonneg_int" nil )"posint" exponentiation nil )"posrat" nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans 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 real_types nil )nil real_types nil )nil real_props nil )"rat" rationals nil )"even_int" integersnil )"posint" nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p2" ("p" "p!1" "s" "s!1" "pn" "pn!1" ))"" "both_sides_times_pos_lt2" "x" "2 ^ (2 * p!1 + 2 * s!1 + 2) / pn!1 - (pn!1 + 1) / 2" "y" "0" "pz" "2" ))"" (replace -1 1 rl)"" (simplify 1)"" (rewrite "div_cancel1" )"" (rewrite "times_div1" )"" "both_sides_times_pos_lt2" "x" "(2 * 2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1 - (1+pn!1)" "y" "0" "pz" "pn!1" ))"" (replace -1 1 rl)"" (simplify 1)"" (rewrite "div_cancel2" )"" "both_sides_plus_lt1" "x" "(2 * 2 ^ (2 + 2 * p!1 + 2 * s!1)) - pn!1 * pn!1 - " " y" " 0" " z" " pn!1 * pn!1 - pn!1")) "" (replace -1 1 rl)"" (hide (-1 -2 -3))"" (grind) 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 inv nil )nil reals nil )nil real_props nil )"posrat" nil )"int" integers nil )"even_int" integersnil )nil real_props nil )"real" exponentiation nil )"int" integers nil )"odd_int" integersnil )"even_int" integersnil )"odd_int" integers nil )"odd_int" integers nil )"(total_order?[real])" nil )"posnat" exponentiation nil )"nzint" integersnil )nil real_props nil )"posint" nil )"odd_int" integers nil )nil real_props nil )"(divides(m))" divides nil )"posint" nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil )"nonneg_int" nil )"posint" exponentiation nil )"posrat" nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"rat" rationals nil )nil real_props nil )nil real_types nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3250067368"" (skosimp*)"" "lemma_A2" "p" "2 ^ (2 * p!1 + 2 * s!1 + 2)" "r" "r!1" "q" "pn!1" ))"" (replace -1)"" (flatten)"" (hide (-1 -2 -4))"" "div_mult_pos_le2" "x" "r!1 - 1 / 2" "z" "2 ^ (2 * p!1 + 2 * s!1 + 2)" "py" "pn!1" ))"" (replace -1 -2 rl)"" "both_sides_minus_le1" "x" "r!1 - 1 / 2" "y" "2 ^ (2 * p!1 + 2 * s!1 + 2) / pn!1" "z" "1/2" ))"" (replace -1 -3 rl)"" (simplify -3)"" (rewrite "div_cancel1" -3)"" (hide (-1 -2))"" "both_sides_times_pos_le1" "x" "r!1 - 1" "y" "(2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1 - 1 / 2" "pz" "pn!1+1" ))"" (replace -1 -2 rl)"" "" "" "inv_p4" "p" "p!1" "s" "s!1" "pn" "pn!1" ))"" replace -3 -1)"" "" "both_sides_plus_lt1" "x" "(2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1 - (1 + pn!1) / 2" "y" "0" "z" "2 ^ (2 + 2 * p!1 + 2 * s!1)" ))"" (grind) 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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans 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 appendix nil )"posint" exponentiation nil )"even_int" integersnil )"posint" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_props nil )"rat" rationals nil )"posrat" nil )nil real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"posint" nil )"int" integers nil )nil real_props nil )nil inv nil )"int" integers nil )"rat" rationals nil )"posrat" nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integersnil )"odd_int" integers nil )"even_int" integersnil )"real" exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"rat" rationals nil )"(divides(m))" divides nil ))nil ))nil 3250067368"" (skosimp*)"" "lemma_A2" "p" "2 ^ (2 * p!1 + 2 * s!1 + 2)" "r" "r!1" "q" "pn!1" ))"" (replace -1)"" (flatten)"" (lemma "inv_p3" ("p" "p!1" "s" "s!1" "pn" "pn!1" ))"" (replace -6 -1)"" (hide (-2 -3 -4 -6))"" (simplify -1)"" "div_mult_pos_lt1" "z" "2 ^ (2 * p!1 + 2 * s!1 + 2)" "x" "(r!1 + 1 / 2)" "py" "pn!1" ))"" (replace -1 -3 rl)"" "both_sides_plus_lt1" "x" "2 ^ (2 * p!1 + 2 * s!1 + 2)/pn!1" "y" "r!1 + 1 / 2" "z" "1/2" ))"" (replace -1 -4 rl)"" (hide (-1 -2))"" (simplify -2)"" rewrite "div_cancel1" -2)"" "" "expt_plus" "n0x" "2" "i" "3" "j" "p!1 + s!1" ))"" expand "^" -1 2)"" expand "expt" )"" expand "expt" )"" expand "expt" )"" expand "expt" )"" "expt_ge1" "b" "2" "n" "p!1 + s!1" ))"" "both_sides_times_pos_ge1" "x" "2 ^ (p!1 + s!1)" "y" "1" "pz" "8" ))"" replace -1 -2 rl)"" "both_sides_minus_ge1" "x" "2 ^ (p!1 + s!1) * 8" "y" "8" "z" "1" ))"" expand ">=" )"" replace "" replace "" "" "lt_le_transitivity" "x" "7" "y" "2 ^ (3 + p!1 + s!1) - 1" "z" "pn!1" ))"" replace "" replace "" "" "both_sides_minus_lt1" "x" "7" "y" "pn!1" "z" "1" ))"" replace "" "" "both_sides_times_pos_lt1" "x" "1 / 2 + (2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1" "y" "1 + r!1" "pz" "pn!1-1" ))"1" replace "1" "1" rewrite "div_cancel2" "1" "both_sides_times_neg_lt1" "y" "(2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1 - (pn!1 - 1) / 2" "x" "0" "nz" "-1" ))"1" replace "1" "1" "both_sides_plus_lt1" "x" "0" "y" "(pn!1 - 1) / 2 - (2 ^ (2 + 2 * p!1 + 2 * s!1)) / pn!1" "z" "2 ^ (2 + 2 * p!1 + 2 * s!1)" ))"1" replace "1" assert )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 ))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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans 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 appendix nil )"posint" exponentiation nil )"even_int" integersnil )"posint" nil )"nonneg_int" nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"int" integers nil )"posrat" nil )"rat" rationals nil )"rat" rationals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posrat" nil )nil exponentiation nil )nil reals nil )"posnat" exponentiation nil )"real" exponentiation nil )nil exponentiation nil )nil integers nil )nil prelude_aux nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"rat" rationals nil )"posrat" nil )nil real_props nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"nzrat" rationals nil )"odd_int" integers nil )nil real_props nil )nil reals nil )"even_int" integersnil )nil real_props nil )"int" integers nil )"(total_order?[real])" nil )nil real_props nil )"(divides(m))" divides nil )"even_int" integersnil )"posint" nil )nil real_props nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )nil real_types nil )nil real_props nil )"rat" rationals nil )nil inv nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "expt_plus" ("n0x" "2" "i" "p!1 + s!1" "j" "3" ))"" (replace -1 -2)"" (hide -1)"" (expand "^" -1 2)"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (lemma "expt_ge1" ("b" "2" "n" "p!1+s!1" ))"" (name "t" "2^(p!1+s!1)" )"" (replace -1)"" (hide -1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil naturalnumbers nil )"bool" reals 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 exponentiation nil )"nonneg_int" nil )"int" integers nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )nil exponentiation nil )"bool" reals nil )nil integers nil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"int" integers nil )"posint" nil )"int" prelude_aux nil )"rat" rationals nil )"posrat" nil )"nat" floor_ceil nil )"even_int" integersnil )"odd_int" integers nil )"posint" nil )"posrat" nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" exponentiation nil )"posnat" exponentiation nil )"posint" exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p5" ("p" "p!1" "s" "s!1" "pn" "pn!1" "r" "r!1" ))"" (lemma "inv_p6" ("p" "p!1" "s" "s!1" "pn" "pn!1" "r" "r!1" ))"" (replace -3 -1 rl)"" (replace -3 -2 rl)"" (replace -4)"" (simplify -1)"" (simplify -2)"" (hide (-3 -4))"" "both_sides_times_pos_lt1" "x" "(r!1 - 1) / 2 ^ p!1" "y" "2 ^ (p!1 + 2 * s!1 + 2) / (pn!1 + 1)" "pz" "2 ^ p!1" ))"" (replace -1 1 rl)"" "both_sides_times_pos_lt1" "y" "(r!1 + 1) / 2 ^ p!1" "x" "2 ^ (p!1 + 2 * s!1 + 2) / (pn!1 - 1)" "pz" "2 ^ p!1" ))"1" (replace -1 1 rl)"1" (hide (-1 -2))"1" rewrite "div_cancel2" )"1" rewrite "div_cancel2" )"1" rewrite "times_div2" )"1" rewrite "times_div2" )"1" "1" "expt_plus" "n0x" "2" "i" "p!1+s!1" "j" "3" ))"1" expand "^" -1 3)"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" "expt_ge1" "b" "2" "n" "p!1 + s!1" ))"1" replace -2 -3)"1" "1" "both_sides_times_pos_ge1" "x" "2 ^ (p!1 + s!1)" "y" "1" "pz" "8" ))"1" replace "1" "1" expand ">=" )"1" "both_sides_minus_le1" "x" "8" "y" "8 * 2 ^ (p!1 + s!1)" "z" "1" ))"1" replace "1" "1" "lt_le_transitivity" "x" "7" "y" "8 * 2 ^ (p!1 + s!1) - 1" "z" "pn!1" ))"1" "1" replace "1" replace "1" "1" "1" "both_sides_times_pos_lt1" "x" "r!1 - 1" "y" "((2 ^ (2 + p!1 + 2 * s!1)) * 2 ^ p!1) / (1 + pn!1)" "pz" "1 + pn!1" ))"1" replace "1" "both_sides_times_pos_lt1" "y" "1+r!1" "x" "((2 ^ (2 + p!1 + 2 * s!1)) * 2 ^ p!1) / (pn!1-1)" "pz" "pn!1-1" ))"1" replace "1" "1" "expt_plus" "n0x" "2" "i" "2 + p!1 + 2 * s!1" "j" "p!1" ))"1" replace "1" "1" "times_div2" )"1" "1+p!1" "2 ^ (2 + p!1 + 2 * s!1 + p!1)" "1+p!1" )"1" rewrite "div_cancel2" )"1" rewrite "div_cancel2" )"1" rewrite "div_cancel2" )"1" "1" nil 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 ))nil ))nil ))nil ))nil ))nil )"2" (reveal -2)"2" (hide-all-but (-1 1))"2" "expt_plus" "i" "p!1 + s!1" "j" "3" ))"2" "2" )"2" replace -1)"2" "2" expand "^" -1 2)"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" "expt_ge1" "b" "2" "n" "p!1+s!1" ))"2" "t" "2 ^ (p!1 + s!1)" )"2" replace -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 ))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 inv nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"even_int" integersnil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )"posrat" nil )nil real_props nil )nil real_types nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )nil reals nil )"posnat" exponentiation nil )"real" exponentiation nil )nil exponentiation nil )nil integers nil )"odd_int" integersnil )nil prelude_aux nil )"even_int" integersnil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )"posint" nil )nil real_props nil )nil real_props nil )nil reals nil )nil integers nil )"[T, T -> boolean]" equalities nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil inv nil ))nil ))nil 3250067368"" (skosimp*)"" "both_sides_times_pos_le1" "x" "2" "y" "px!1 * 2 ^ s!1" "pz" "2 ^ (p!1 + s!1 + 2)" ))"" (replace -1 -2 rl)"" "expt_plus" ("n0x" "2" "i" "1" "j" "p!1 + s!1 + 2" ))"" "expt_plus" "n0x" "2" "i" "s!1" "j" "p!1 + s!1 + 2" ))"" (simplify -1)"" (replace -1)"" (expand "^" -2 2)"" (expand "expt" )"" (expand "expt" )"" (replace -2 -4 rl)"" "lt_le_transitivity" "x" "2 ^ (3 + p!1 + s!1)" "y" "px!1 * 2 ^ s!1 * 2 ^ (p!1 + s!1 + 2)" "z" "pn!1 + 1" ))"" (replace -5 -1)"" (replace -7 -1)"" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"posint" exponentiation nil )"posint" nil )nil exponentiation nil )nil reals nil )"nonneg_int" nil )"int" integers nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )nil prelude_aux nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"posnat" exponentiation nil )"int" integers nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integersnil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p8" ("px" "px!1" "s" "s!1" "pn" "pn!1" "p" "p!1" ))"" (lemma "inv_p7" ("r" "r!1" "p" "p!1" "s" "s!1" "pn" "pn!1" ))"" (replace -4 -1 rl)"" (replace -3)"" (replace -5)"" (replace -6)"" (simplify -2)"" (replace -2 -1)"" (simplify -1)"" "expt_plus" "n0x" "2" "i" "3" "j" "p!1+s!1" ))"" (expand "^" -1 2)"" (expand "expt" )"" (expand "expt" )"" expand "expt" )"" expand "expt" )"" "expt_ge1" "b" "2" "n" "p!1+s!1" ))"" "both_sides_times_pos_le1" "x" "1" "y" "2 ^ (p!1 + s!1)" "pz" "8" ))"" expand ">=" )"" replace -1 -2 rl)"" replace -3 -2 rl)"" "both_sides_minus_le1" "x" "8" "y" "2 ^ (3 + p!1 + s!1)" "z" "1" ))"" replace -3 -1)"" "" "lt_le_transitivity" "x" "7" "y" "2 ^ (3 + p!1 + s!1) - 1" "z" "pn!1" ))"" replace -2 -1)"" replace -7 -1)"" "" "" "" "1" case "1<=r!1" )"1" "lt_times_lt_pos1" "px" "px!1 * 2 ^ (p!1 + 2 * s!1 + 2)" "y" "pn!1 + 1" "nnz" "(r!1 - 1) / 2 ^ p!1" "w" "(2 ^ (2 + p!1 + 2 * s!1)) / (1 + pn!1)" ))"1" replace "1" expand "<=" "1" replace "1" "both_sides_times_pos_lt1" "x" "((r!1 - 1) / 2 ^ p!1) * px!1" "y" "(1+pn!1)/(1+pn!1)" "pz" "2 ^ (2 + p!1 + 2 * s!1)" ))"1" "1" "1" "both_sides_times_pos_lt1" "x" "((r!1 - 1) / 2 ^ p!1) * px!1" "y" "1" "pz" "2 ^ (2 + p!1 + 2 * s!1)" ))"1" "1" "div_cancel1" "x" "2 ^ (2 + p!1 + 2 * s!1)" "n0z" "1+pn!1" ))"1" "1" replace "1" replace "1" "1" "div_mult_pos_lt1" "x" "1" "py" "2^p!1" "z" "(r!1 - 1) * px!1" ))"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "expt_ge1" "b" "2" "n" "p!1" ))"2" "a!1" "2 ^ p!1" )"2" replace "2" "2" "2" expand ">=" )"2" "both_sides_minus_le1" "x" "1" "y" "r!1" "z" "1" ))"2" replace "2" assert )"2" "div_mult_pos_le2" "x" "0" "z" "r!1 - 1" "py" "a!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "px!1" )"2" rewrite "le_equiv_not_lt" "2" "expt_ge1" "b" "2" "n" "p!1" ))"2" "both_sides_minus_lt1" "x" "r!1" "y" "1" "z" "1" ))"2" replace "2" "2" "both_sides_times_pos_lt1" "x" "r!1 - 1" "y" "0" "pz" "px!1" ))"2" replace "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_minus_lt1" "x" "7" "y" "pn!1" "z" "1" ))"2" replace "2" "2" "expt_ge1" "b" "2" "n" "p!1" ))"2" "expt_ge1" "b" "2" "n" "p!1 + 2 * s!1 + 2" ))"2" "div_mult_pos_lt1" "z" "2 ^ (2 + p!1 + 2 * s!1)" "py" "pn!1 - 1" "x" "(1 + r!1) / 2 ^ p!1" ))"1" replace "1" "lt_times_lt_pos1" "px" "2 ^ (2 + p!1 + 2 * s!1)" "y" "(1 + r!1) / 2 ^ p!1 * (pn!1 - 1)" "nnz" "pn!1 - 1" "w" "px!1 * 2 ^ (p!1 + 2 * s!1 + 2)" ))"1" expand "<=" "1" replace "1" replace "1" "1" "div_mult_pos_lt2" "z" "(r!1 + 1) * px!1" "x" "1" "py" "2 ^ p!1" ))"1" replace "1" "both_sides_times_pos_lt1" "x" "1" "y" "(r!1 + 1) * px!1 / 2 ^ p!1" "pz" "2 ^ (2 + p!1 + 2 * s!1) * (pn!1-1)" ))"1" replace "1" assert )nil nil ))nil )"2" "lt_times_lt_pos1" "nnz" "6" "w" "pn!1 - 1" "px" "1" "y" "2 ^ (2 + p!1 + 2 * s!1)" ))"2" replace "2" "expt_ge1" "b" "2" "n" "2 + p!1 + 2 * s!1" ))"2" expand ">=" )"2" replace "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 ))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_types nil )nil real_types 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 inv nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"even_int" integersnil )"posint" exponentiation nil )"int" integers nil )"posint" nil )"int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )"posreal" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posrat" nil )"real" exponentiation nil )nil real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"(total_order?[real])" nil )"odd_int" integersnil )"even_int" integersnil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"posint" nil )"bool" reals nil )"even_int" integersnil )nil real_props nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil real_props nil )nil reals nil )"real" reals nil )"real" reals nil )nil real_props nil )"posrat" nil )nil real_props nil )"posrat" nil )"rat" rationals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )nil prelude_aux nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil prelude_aux nil )nil integers nil )nil exponentiation nil )"real" exponentiation nil )"posnat" exponentiation nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil exponentiation nil )nil inv nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p0" ("p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (assert ) nil nil )) nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 inv nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" exponentiation nil )"posint" nil )"nonneg_int" nil )"posint" nil )"odd_int" integers nil )"nzrat" rationalsnil )"nprat" rationalsnil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"int" integers nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p0" ("p" "p!1" "s" "s!1" "pn" "-1 * nn!1" ))"" (replace -3 -1)"" (lemma "inv_p3" ("p" "p!1" "s" "s!1" "pn" "-1 * nn!1" ))"" (replace -4 -1)"" "lemma_A2" "r" "r!1" "p" "-1*2 ^ (2 * p!1 + 2 * s!1 + 2)" "q" "-1*nn!1" ))"" (replace -4 -1 rl)"" (simplify)"" (flatten)"" (hide (-2 -5 -6))"" "div_mult_neg_lt2" "x" "r!1 - 1" "ny" "1 + nn!1" "z" "2 ^ (2 + 2 * p!1 + 2 * s!1)" ))"1" (replace -1 1)"1" (hide -1)"1" "AA" "2 ^ (2 + 2 * p!1 + 2 * s!1)" )"1" replace -1)"1" "1" "both_sides_times_neg_lt1" "y" "AA / (-1 * nn!1) - (-1 - nn!1) / 2" "x" "0" "nz" "-1" ))"1" "both_sides_times_neg_le1" "y" "1 / 2 * nn!1 - nn!1 * r!1" "x" "-1 * AA" "nz" "-1" ))"1" replace -1 -3 rl)"1" replace -2 -4 rl)"1" "1" "1" "1" "expt_ge1" "b" "2" "n" "2 + 2 * p!1 + 2 * s!1" ))"1" replace -2)"1" "1" "div_mult_neg_le2" "z" "AA" "x" "r!1-1/2" "ny" "nn!1" ))"1" "both_sides_minus_le1" "x" "r!1 - 1 / 2" "y" "AA / nn!1" "z" "1/2" ))"1" "1" rewrite "div_cancel1" "1" "both_sides_times_neg_le1" "y" "r!1 - 1" "x" "AA / nn!1 - 1 / 2" "nz" "nn!1+1" ))"1" replace "1" replace "1" replace "1" "1" "1" "lt_minus_lt1" "x" "-1 * (1 / 2) - 1 / 2 * nn!1 + AA / nn!1 +AA" "y" "-1 - nn!1 + (nn!1 * r!1 + r!1)" "w" "0" "z" "(-1 - nn!1) / 2 - AA / (-1 * nn!1)" ))"1" replace "1" replace "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 2)) (("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 )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 inv nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil inv nil )"posint" nil )nil appendix nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"nprat" rationalsnil )"int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )"[T, T -> boolean]" equalities nil )nil integers nil )nil real_props nil )nil exponentiation nil )nil integers nil )nil real_props nil )nil real_props nil )"nnrat" rationalsnil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil real_props nil )"rat" rationals nil )"posrat" nil )"rat" rationals nil )"rat" rationals nil )"nzrat" rationalsnil )"int" integers nil )"posint" exponentiation nil )"odd_int" integers nil )"even_int" integersnil )"even_int" integersnil )"nonneg_int" nil )"nonneg_int" nil ))nil ))nil 3250067368 ("" (subtype-tcc) nil nil )"posint" nil )"posnat" exponentiation nil )"odd_int" integers nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"nzrat" rationalsnil )"nprat" rationalsnil )"int" prelude_aux nil )"real" exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p0" ("p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (lemma "inv_p4" ("p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (replace -4)"" (simplify (-1 -2))"" "lemma_A2" "r" "r!1" "p" "-1*2 ^ (2 * p!1 + 2 * s!1 + 2)" "q" "-1*nn!1" ))"" (replace -4 -1 rl)"" (simplify -1)"" (flatten)"" (hide (-1 -5 -6))"" (lemma "expt_ge1" ("b" "2" ))"" (inst - "2 * p!1 + 2 * s!1 + 2" )"" "AA" "2 ^ (2 * p!1 + 2 * s!1 + 2)" )"" (replace -1)"" "" "div_mult_neg_lt1" "z" "AA" "ny" "nn!1 - 1" "x" "r!1 + 1" ))"" replace -1)"" "" "div_mult_neg_lt2" "z" "-1*AA" "ny" "nn!1" "x" "-1*r!1 - 1/2" ))"" replace -1 -3 rl)"" "both_sides_times_neg_lt1" "x" "r!1 + 1 / 2" "y" "AA / nn!1" "nz" "-1" ))"" replace -1)"" "" "both_sides_plus_lt1" "x" "AA / nn!1" "y" "r!1 + 1 / 2" "z" "1 / 2" ))"" replace -3 -1)"" "" rewrite "div_cancel1" "" "both_sides_times_neg_lt1" "y" "1 / 2 + AA / nn!1" "x" "1 + r!1" "nz" "nn!1 - 1" ))"" replace "" "" "both_sides_times_neg_lt1" "y" "AA / (-1 * nn!1) - (1 - nn!1) / 2" "x" "0" "nz" "-1" ))"" replace "" "" "lt_minus_lt1" "x" "nn!1 * r!1 - r!1 + (nn!1 - 1)" "y" "1 / 2 * nn!1 - 1 / 2 + (AA / nn!1 * nn!1 - AA / nn!1)" "w" "AA / (-1 * nn!1) - (1 - nn!1) / 2" "z" "0" ))"" replace "" "" 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 integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 inv nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nonneg_int" nil )"nonneg_int" nil )"even_int" integersnil )"even_int" integersnil )"odd_int" integers nil )"posint" exponentiation nil )"int" integers nil )"nzrat" rationalsnil )"rat" rationals nil )"rat" rationals nil )"int" integers nil )nil appendix nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"rat" rationals nil )"nzrat" rationalsnil )nil real_props nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil real_props nil )"nnrat" rationalsnil )nil real_props nil )"nprat" rationalsnil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil exponentiation nil )"rat" rationals nil )"posrat" nil )"(total_order?[real])" nil )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil inv nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p0" ("p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (assert ) nil nil )) nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 inv nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" exponentiation nil )"posint" nil )"nonneg_int" nil )"posint" nil )"nzint" integers nil )"nzrat" rationalsnil )"nprat" rationalsnil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"int" integers nil )"odd_int" integers nil ))nil ))nil 3250067368 ("" (subtype-tcc) nil nil )"posint" nil )"posnat" exponentiation nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"nzrat" rationalsnil )"nprat" rationalsnil )"int" integers nil )"int" integers nil )"int" prelude_aux nil )"real" exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_p0" ("p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (replace -3 -1)"" (simplify -1)"" "inv_n5" "p" "p!1" "s" "s!1" "nn" "nn!1" "r" "r!1" ))"" "inv_n6" "p" "p!1" "s" "s!1" "nn" "nn!1" "r" "r!1" ))"" (replace -4 (-1 -2) rl)"" (replace -5 (-1 -2))"" (simplify (-1 -2))"" (lemma "expt_ge1" ("b" "2" "n" "p!1" ))"" "expt_plus" "n0x" "2" "i" "p!1" "j" "p!1 + 2 * s!1 + 2" ))"" (replace -1)"" "div_mult_pos_lt1" "z" "r!1 - 1" "py" "2 ^ p!1" "x" "2 ^ (p!1 + 2 * s!1 + 2) / (nn!1 + 1)" ))"1" "div_mult_pos_lt2" "z" "r!1 + 1" "py" "2 ^ p!1" "x" "2 ^ (p!1 + 2 * s!1 + 2) / (nn!1 - 1)" ))"1" replace -5)"1" replace -6)"1" "1" replace -1 1)"1" replace -2 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -6))"2" (grind) 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 )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 inv nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil inv nil )"nzrat" rationalsnil )nil exponentiation nil )nil integers nil )"posint" nil )"odd_int" integersnil )nil real_props nil )"rat" rationals nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_types nil )nil real_props nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil )"posint" exponentiation nil )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"nonneg_int" nil )nil inv nil )"odd_int" integers nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "expt_ge1" ("b" "2" ))"" (inst-cp - "s!1" )"" (inst - "p!1 + s!1 + 2" )"" "expt_plus" "n0x" "2" "i" "p!1 + s!1 + 2" "j" "s!1" ))"" "both_sides_plus_lt1" "x" "nn!1 - 1" "y" "nx!1 * 2 ^ (p!1 + 2 * s!1 + 2)" "z" "1" ))"" "both_sides_times_neg_lt1" "y" "nn!1" "x" "nx!1 * 2 ^ (p!1 + 2 * s!1 + 2) + 1" "nz" "-1" ))"" (simplify -1)"" "both_sides_times_pos_le1" "x" "2" "y" "-1 *nx!1 * 2 ^ s!1" "pz" "2 ^ (2 + p!1 + s!1)" ))"" "expt_plus" "n0x" "2" "i" "2 + p!1 + s!1" "j" "1" ))"" (expand "^" -1 3)"" (expand "expt" )"" (expand "expt" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 exponentiation nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"nzreal" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" exponentiation nil )"nonneg_int" nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"posint" nil )"nzint" integersnil )"(divides(m))" divides nil )"posnat" exponentiation nil )"real" exponentiation nil )"nzint" integers nil )"int" integers nil )"nzreal" real_typesnil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )nil real_types nil )nil real_types nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )nil real_props nil )"real" reals nil )"odd_int" integers nil )nil reals nil )"boolean" notequal nil )nil exponentiation nil )"bool" reals nil )nil naturalnumbers nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "inv_n8" ("nx" "nx!1" "nn" "nn!1" "p" "p!1" "s" "s!1" ))"" (lemma "inv_n7" ("nn" "nn!1" "p" "p!1" "s" "s!1" "r" "r!1" ))"" (replace -4 -1 rl)"" (replace -3)"" (replace -5)"" (replace -6)"" (simplify -2)"" (replace -2)"" (simplify -1)"" (flatten)"" "inv_p0" "p" "p!1" "s" "s!1" "pn" "-1*nn!1" ))"" (replace -4)"" (simplify -1)"" "expt_ge1" ("b" "2" ))"" "expt_plus" ("n0x" "2" ))"" "div_mult_neg_lt1" "z" "2 ^ p!1" "ny" "nx!1" "x" "r!1 + 1" ))"" replace -1)"" "div_mult_neg_lt2" "z" "2 ^ p!1" "ny" "nx!1" "x" "r!1 - 1" ))"" replace -1)"" "" "p!1" )"" "div_mult_pos_lt1" "z" "r!1 - 1" "py" "2 ^ p!1" "x" "(2 ^ (2 + p!1 + 2 * s!1)) / (1 + nn!1)" ))"1" replace -1)"1" "div_mult_pos_lt2" "z" "r!1 + 1" "py" "2 ^ p!1" "x" "(2 ^ (2 + p!1 + 2 * s!1)) / (nn!1 -1)" ))"1" replace -1)"1" "1" "2 + p!1 + 2 * s!1" )"1" "B" "2 ^ p!1" )"1" replace "1" "AA" "2 ^ (2 + p!1 + 2 * s!1)" )"1" replace "1" "1" "1" "div_mult_pos_lt2" "x" "nx!1" "z" "nn!1 + 1" "py" "AA" ))"1" replace "1" "lt_times_lt_neg1" "x" "r!1 - 1" "ny" "AA / (1 + nn!1) * B" "z" "nx!1" "npw" "(nn!1 + 1) / AA" ))"1" "1" "div_times" "x" "AA" "n0x" "nn!1 + 1" "y" "nn!1 + 1" "n0y" "AA" ))"1" "1" "1" rewrite "div_simp" "1" "both_sides_times1" "x" "(AA / (1 + nn!1)) * ((1 + nn!1) / AA)" "y" "1" "n0z" "B" ))"1" replace "1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "both_sides_times_neg_le1" "y" "6" "x" "-1*nn!1" "nz" "-1" ))"2" "both_sides_plus_le1" "x" "nn!1" "y" "-6" "z" "1" ))"2" "both_sides_times_pos_le1" "x" "nn!1 + 1" "y" "-5" "pz" "AA" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "both_sides_times_neg_le1" "y" "6" "x" "-1*nn!1" "nz" "-1" ))"2" "both_sides_plus_le1" "y" "-6" "x" "nn!1" "z" "1" ))"2" "2" "div_mult_neg_le1" "x" "0" "ny" "1+nn!1" "z" "AA*B" ))"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "div_mult_pos_le1" "py" "AA" "z" "1 + nn!1" "x" "0" ))"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "trich_lt" "x" "r!1 + 1" "y" "0" ))"2" "1" "lt_times_lt_neg1" "x" "AA / (nn!1 - 1) * B" "ny" "r!1 + 1" "z" "nn!1 - 1" "npw" "nx!1 * AA" ))"1" "both_sides_times_pos_lt1" "x" "(r!1 + 1) * nx!1" "y" "B" "pz" "AA" ))"1" "1" replace "1" rewrite "times_div2" "1" rewrite "div_cancel2" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil )"3" "both_sides_times_neg_lt1" "y" "0" "x" "r!1 + 1" "nz" "nx!1" ))"3" nil nil ))nil ))nil ))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 naturalnumbers nil )"bool" reals nil )nil real_types nil )nil real_types 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 inv nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"even_int" integersnil )"posint" exponentiation nil )"int" integers nil )"int" integers nil )"rat" rationals nil )"nzrat" rationalsnil )"nzreal" nil )"nzreal" nil )"npreal" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"nzint" integers nil )"nzint" integersnil )nil inv nil )nil integers nil )"bool" reals nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil exponentiation nil )"boolean" notequal nil )nil reals nil )"real" reals nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"nzreal" real_typesnil )nil real_props nil )"even_int" integers nil )nil real_props nil )nil real_props nil )"odd_int" integers nil )nil real_props nil )"rat" rationals nil )nil real_props nil )"real" reals nil )"posint" nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil real_props nil )nil real_props nil )"nzrat" rationalsnil )nil real_props nil )nil real_props nil )nil real_props nil )"rat" rationals nil )"even_int" integersnil )nil real_props nil )nil real_props nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )nil real_types nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil integers nil )nil exponentiation nil )"odd_int" integers nil )nil inv nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "trich_lt" ("x" "nzx!1" "y" "0" ))"" (split -1)"1" (rewrite "abs_nonpos" )"1" (lemma "expt_ge1" ("b" "2" ))"1" (lemma "expt_plus" ("n0x" "2" ))"1" "both_sides_times_neg_le1" "y" "2" "x" "-1 * nzx!1 * 2 ^ s!1" "nz" "-1" ))"1" (replace -5 -1)"1" (flatten)"1" (simplify -1)"1" (inst-cp -3 "p!1 + s!1 + 2" )"1" "both_sides_times_pos_le1" "x" "2 ^ s!1 * nzx!1" "y" "2 * -1" "pz" "2 ^ (p!1 + s!1 + 2)" ))"1" (replace -2 -1)"1" (simplify -1)"1" "2 + p!1 + s!1" "s!1" )"1" replace -3)"1" "AA" "2 ^ (2 + p!1 + s!1)" )"1" replace -1)"1" "B" "2 ^ s!1" )"1" replace -1)"1" expand ">=" )"1" "inv_n9" "nx" "nzx!1" "nn" "nzn!1" "s" "s!1" "p" "p!1" "r" "r!1" ))"1" replace -2)"1" replace -10)"1" replace -11 -1 rl)"1" replace -6)"1" replace -12)"1" replace -13)"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "3" (grind) 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 )"3" (rewrite "abs_nonneg" )"3" (lemma "expt_ge1" ("b" "2" ))"3" (lemma "expt_plus" ("n0x" "2" ))"3" (inst-cp -2 "s!1" )"3" (inst -2 "p!1 + s!1 + 2" )"3" (inst-cp - "p!1 + s!1 + 2" "s!1" )"3" (replace -2)"3" "both_sides_times_pos_le1" "x" "2" "y" "nzx!1 * 2 ^ s!1" "pz" "2 ^ (p!1 + s!1 + 2)" ))"3" (replace -7 -1)"3" (flatten)"3" "inv_p9" "px" "nzx!1" "s" "s!1" "r" "r!1" "p" "p!1" "pn" "nzn!1" ))"1" replace -8 -1)"1" replace -9 -1 rl)"1" replace -4)"1" replace -10)"1" replace -11)"1" "1" "1" "1" "1" "div_mult_pos_lt2" "x" "r!1 - 1" "py" "nzx!1" "z" "2 ^ p!1" ))"1" replace -1)"1" assert )nil nil ))nil ))nil )"2" "div_mult_pos_lt1" "x" "r!1 + 1" "py" "nzx!1" "z" "2 ^ p!1" ))"2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "AA" "2 ^ (p!1 + s!1 + 2)" )"3" replace -1)"3" "B" "2 ^ s!1" )"3" replace -1)"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal 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 )"(total_order?[real])" nil )nil prelude_aux nil )nil real_types nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil inv nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_props nil )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(total_order?[real])" nil )nil prelude_aux nil )nil booleans nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"{y: posreal | y >= x}" nil )"posint" exponentiation nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"even_int" integersnil )"nzreal" real_typesnil )nil exponentiation nil )"nzint" integersnil )nil real_props nil )nil real_types nil )nil real_types nil )"posint" nil )"posint" nil )"even_int" integersnil )"int" integers nil )nil inv nil )nil integers nil )nil integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzreal" nil )"nzrat" rationalsnil )"int" integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil naturalnumbers nil )"real" exponentiation nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"nzreal" nil )"odd_int" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil exponentiation nil ))nil ))nil 3250067368"" (skosimp*)"" (lemma "minimum_inv_prop0" ("s" "s!1" "nzcx" "nzcx!1" ))"" "cauchy_monotonic" "s" "s!1" "nzcx" "nzcx!1" "p" "p!1 + s!1 + 2" ))"" (lemma "cauchy_dich5" ("nzcx" "nzcx!1" ))"" (split -1)"1" "cauchy_neg_characteristic" "p" "2 + p!1 + 2 * s!1" "ncx" "nzcx!1" ))"1" (rewrite "abs_nonpos" )"1" (assert )"1" (assert )"1" (assert ) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (grind) nil nil ))nil )"2" (propax) nil nil ))nil )"2" "cauchy_pos_characteristic" "pcx" "nzcx!1" "p" "2 + p!1 + 2 * s!1" ))"1" (rewrite "abs_nonneg" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy 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 inv nil )nil unique nil )nil unique nil )"bool" cauchy nil )nil cauchy nil )"posnat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nat" inv nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" cauchy nil )"real" exponentiation nil )nil prelude_aux nil )nil real_types nil )nil unique nil )"bool" cauchy nil )nil cauchy nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )nil abs_lems "reals/" )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"nonneg_int" nil )nil prelude_aux nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil unique nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil )"posint" nil )"posint" nil ))nil ))nil 3250067368"" (skosimp*)"" "minimum_inv_prop1" "s" "s!1" "nzcx" "nzcx!1" "x" "nzx!1" ))"" (replace -3 -1)"" (expand "cauchy_prop" )"" (skosimp*)"" (inst - "2 + p!1 + 2 * s!1" )"" (name "nzn!1" "nzcx!1(2 + p!1 + 2 * s!1)" )"" (replace -1)"" "minimum_inv_prop2" "s" "s!1" "nzx" "nzx!1" "n" "nzn!1" "p" "p!1" ))"" (replace -4 -3 rl)"" (simplify -3)"" (replace -5 -1)"" (replace -3 -1)"" (simplify -1)"" "r!1" "round((2 ^ (2 + 2 * p!1 + 2 * s!1)) / nzn!1)" )"1" replace -1)"1" "inv_p" "s" "s!1" "nzx" "nzx!1" "p" "p!1" "nzn" "nzn!1" "r" "r!1" ))"1" replace -5 -1)"1" replace -2)"1" replace -7 -1)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil cauchy nil )"bool" cauchy 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 inv nil )"posint" exponentiation nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )"even_int" integersnil )"nzreal" nil )"bool" cauchy nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{y: posreal | y >= x}" nil )"int" integers nil )"nonneg_int" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posnat" exponentiation nil )"posrat" nil )"(total_order?[real])" nil )"nzreal" nil )nil integers nil )nil inv nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"int" prelude_aux nil )"nzrat" rationalsnil )"posreal" nil )"(total_order?[real])" nil )nil inv nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3250067368"" (skosimp)"" (rewrite "minimum_inv_impl_def" * :dir rl)"" (expand "minimum_inv" )"" (typepred "min_nat.min({s | 3 <= abs(nzcx!1(s))})" )"1" (replace -3 * rl)"1" (typepred "nzcx!1" )"1" (expand "cauchy_nzreal?" )"1" (skosimp)"1" (expand "cauchy_prop" )"1" (inst-cp - "s!1" )"1" (inst - "p!1+2*s!1+2" )"1" (flatten)"1" case "abs(nzcx!1(s!1))<=abs(nzcx!1(p!1+2*s!1+2))" )"1" (replace -9 -1)"1" expand "abs" -1 2)"1" (assert ) nil nil ))nil ))nil )"2" (replace -8)"2" expand "abs" 1 2)"2" "2" "div_mult_pos_lt2" "py" " 2 ^ (p!1 + 2 * s!1 + 2)" "x" "x!1" "z" "1" ))"2" "div_mult_pos_lt1" "py" " 2 ^ (p!1 + 2 * s!1 + 2)" "x" "x!1" "z" "-1" ))"2" assert )"2" case "abs(x!1 * 2 ^ s!1) <= 1/2^(2+p!1+s!1)" )"1" "both_sides_expt_gt1_le" "gt1x" "2" "i" "-(2+p!1+s!1)" "j" "-2" ))"1" assert )"1" rewrite "expt_inverse" "1" rewrite "expt_inverse" "1" expand "^" -1 2)"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" case "abs(nzcx!1(s!1)) <=2" )"1" assert )nil nil )"2" case "abs(x!1 * 2 ^ s!1) <=1/4" )"1" "X2S" "x!1 * 2 ^ s!1" )"1" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "abs_mult" 1)"2" expand "abs" 1 2)"2" rewrite "div_mult_pos_le2" "2" "expt_plus" "n0x" "2" "i" "2 + p!1 + s!1" "j" "s!1" ))"2" rewrite "associative_mult" "2" replace "2" "2" "2 ^ (2 + p!1 + 2 * s!1)" )"2" "div_mult_pos_le2" "py" "2 ^ (2 + p!1 + s!1 + s!1)" "x" "abs(x!1)" "z" "1" ))"2" replace "2" "2" "DRL" "2 ^ (2 + p!1 + 2 * s!1)" )"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 ))nil )"2" (rewrite "minimum_inv_exists" ) nil nil ))nil ))nil ))nil ))nil )nil inv 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 )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" nil )"[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )nil real_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"{y: posreal | y >= x}" nil )"real" exponentiation nil )"nzreal" real_typesnil )"int" integers nil )"[T, T -> boolean]" equalities nil )nil exponentiation nil )nil exponentiation nil )"even_int" integers nil )"nzint" integers nil )nil real_props nil )"{j: posint | j >= i}" nil )"posreal" nil )nil exponentiation nil )nil integers nil )nil integers nil )"even_int" integersnil )"posint" nil )nil number_fields nil )nil real_props nil )"odd_int" integersnil )"odd_int" integers nil )"nzrat" rationalsnil )"posrat" nil )nil reals nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil abs_lems "reals/" )"int" integers nil )"nzreal" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"bool" cauchy nil )"posint" exponentiation nil )nil inv nil )"nat" inv nil ))nil ))nil 3250067368"" (skosimp)"" (typepred "nzcx!1" )"" (expand "cauchy_nzreal?" )"" (skosimp)"" "minimum_inv_prop3" "s" "minimum_inv(nzcx!1)" "nzx" "x!1" "nzcx" "nzcx!1" ))"" (assert )"" (rewrite "minimum_inv_impl_def" )"" (inst + "1/x!1" ) 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 )"nzreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil inv nil )"nat" inv nil )nil reals nil )"boolean" notequal nil )nil inv nil )"posint" exponentiation nil )"even_int" integersnil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil ))nil ))nil 3250067368"" (skosimp)"" (lemma "minimum_inv_prop3" ("nzcx" "nzcx!1" "nzx" "nzx!1" ))"" (inst - "minimum_inv(nzcx!1)" )"" (expand "cauchy_nz_inv" )"" (rewrite "minimum_inv_impl_def" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil cauchy nil )"bool" cauchy 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 inv nil )"cauchy_nzreal" inv nil )"nzreal" nil )"posint" nil )"posint" exponentiation nil )"even_int" integersnil )"nonneg_int" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"int" integers nil )nil inv nil )"nat" inv nil ))nil ))nil 3250067368"" (skosimp)"" (lemma "inv_nz_lemma" ("nzx" "nzx!1" "nzcx" "nzcx!1" ))"" (assert )"" (expand "cauchy_inv" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil reals nil )"boolean" notequal nil )nil cauchy nil )"bool" cauchy 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 inv nil )"cauchy_nzreal" inv nil )"nzreal" nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.446 Sekunden
(vorverarbeitet am 2026-04-25)
¤ *© Formatika GbR, Deutschland
2026-05-26
