| products/Sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: inv.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(inv
(expt_x2_TCC1 0 (expt_x2_TCC1-1 nil 3250067368 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (expt_x2 0 (expt_x2-1 nil 3250067368 ("" (grind) nil nil) ((expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil)) nil)) (expt_times2_TCC1 0 (expt_times2_TCC1-1 nil 3250067368 ("" (subtype-tcc) nil nil) nil nil)) (expt_times2_TCC2 0 (expt_times2_TCC2-1 nil 3250067368 ("" (subtype-tcc) nil nil) nil nil)) (expt_times2 0 (expt_times2-1 nil 3250067368 ("" (skosimp*) (("" (lemma "expt_plus" ("n0x" "nzx!1" "i" "s!1" "j" "s!1")) (("" (assert) nil nil)) nil)) nil) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (expt_plus formula-decl nil exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_times_int_is_int application-judgement "int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil)) nil)) (minimum_inv_exists 0 (minimum_inv_exists-1 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" (inst -5 "p!1+4") (("1" (expand "member") (("1" (inst -4 "p!1+4") (("1" (rewrite "abs_nonpos") (("1" (lemma "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" (flatten) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "-x!1 * 2 ^ p!1" "pz" "2^p!1")) (("1" (lemma "div_mult_pos_lt1" ("z" "1" "py" "2^p!1" "x" "-x!1")) (("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)) 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" (inst - "p!1+4") (("1" (inst - "p!1+4") (("1" (expand "member") (("1" (rewrite "abs_nonneg") (("1" (lemma "div_mult_pos_lt1" ("z" "1" "py" "2^p!1" "x" "x!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "x!1 * 2 ^ p!1" "pz" "2^p!1")) (("1" (lemma "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" (grind) 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) ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (epsilon_log2 formula-decl nil appendix nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (npreal type-eq-decl nil real_types nil) (abs_nonpos formula-decl nil prelude_aux nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_int_is_int application-judgement "int" integers nil) (^ const-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_times_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (expt_plus formula-decl nil exponentiation nil) (empty? const-decl "bool" sets nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_neg_characteristic formula-decl nil unique nil) (cauchy_negreal? const-decl "bool" cauchy nil) (cauchy_negreal nonempty-type-eq-decl nil cauchy nil) (nnreal type-eq-decl nil real_types nil) (abs_nonneg formula-decl nil prelude_aux nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cauchy_pos_characteristic formula-decl nil unique nil) (cauchy_posreal? const-decl "bool" cauchy nil) (cauchy_posreal nonempty-type-eq-decl nil cauchy nil) (cauchy_dich5 formula-decl nil unique nil)) nil)) (minimum_inv_TCC1 0 (minimum_inv_TCC1-1 nil 3250067368 ("" (lemma "minimum_inv_exists") (("" (propax) nil nil)) nil) ((minimum_inv_exists formula-decl nil inv nil)) nil)) (minimum_inv_prop0 0 (minimum_inv_prop0-1 nil 3250067368 ("" (skosimp*) (("" (expand "minimum_inv") (("" (lemma "minimum_inv_exists" ("nzcx" "nzcx!1")) (("" (lemma "min_def" ("a" "s!1" "S" "{s | 3 <= abs(nzcx!1(s))}")) (("1" (grind) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((minimum_inv const-decl "nat" inv nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (min_def formula-decl nil min_nat nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minimum? const-decl "bool" min_nat nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (minimum_inv_exists formula-decl nil inv nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)) nil)) (minimum_inv_prop1 0 (minimum_inv_prop1-1 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" (lemma "unique_cauchy" ("x" "x!1" "y" "x!2" "cx" "nzcx!1")) (("1" (replace -4 -1) (("1" (replace -10 -1) (("1" (simplify -1) (("1" (replace -1) (("1" (rewrite "abs_nonpos" 1) (("1" (lemma "cauchy_neg_characteristic" ("ncx" "nzcx!1" "p" "s!1")) (("1" (rewrite "abs_nonpos" -8) (("1" (flatten) (("1" (lemma "both_sides_plus_le1" ("x" "3" "y" "-nzcx!1(s!1)" "z" "-1")) (("1" (lemma "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" (lemma "cauchy_pos_characteristic" ("pcx" "nzcx!1" "p" "s!1")) (("1" (rewrite "abs_nonneg" -4) (("1" (expand "cauchy_posreal?") (("1" (skolem!) (("1" (lemma "unique_cauchy" ("x" "x!1" "y" "x!2" "cx" "nzcx!1")) (("1" (replace -3 -1) (("1" (replace -8 -1) (("1" (simplify -1) (("1" (replace -1) (("1" (typepred "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) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (cauchy_negreal? const-decl "bool" cauchy nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (cauchy_neg_characteristic formula-decl nil unique nil) (cauchy_negreal nonempty-type-eq-decl nil cauchy nil) (int_plus_int_is_int application-judgement "int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minimum_inv const-decl "nat" inv nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (both_sides_plus_le1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (abs_nonpos formula-decl nil prelude_aux nil) (npreal type-eq-decl nil real_types nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (unique_cauchy formula-decl nil unique nil) (nnreal type-eq-decl nil real_types nil) (abs_nonneg formula-decl nil prelude_aux nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_posreal nonempty-type-eq-decl nil cauchy nil) (cauchy_posreal? const-decl "bool" cauchy nil) (cauchy_pos_characteristic formula-decl nil unique nil) (cauchy_dich5 formula-decl nil unique nil) (minimum_inv_prop0 formula-decl nil inv nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil)) nil)) (minimum_inv_prop2 0 (minimum_inv_prop2-1 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) (("" (lemma "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) (("" (hide (-1 -2 -4 -5)) (("" (split -4) (("1" (rewrite "abs_nonpos") (("1" (lemma "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) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (trich_lt formula-decl nil real_props nil) (expt_plus formula-decl nil exponentiation nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnreal type-eq-decl nil real_types nil) (abs_nonneg formula-decl nil prelude_aux nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (npreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (abs_nonpos formula-decl nil prelude_aux nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_le1 formula-decl nil real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (expt_ge1 formula-decl nil exponentiation nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil)) nil)) (minimum_inv_aux_TCC1 0 (minimum_inv_aux_TCC1-1 nil 3392691345 ("" (skosimp*) (("" (typepred "s!1") (("" (assert) nil nil)) nil)) nil) ((minimum_inv const-decl "nat" inv nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (<= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (minimum_inv_aux_TCC2 0 (minimum_inv_aux_TCC2-1 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) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minimum_inv_exists formula-decl nil inv nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (minimum_inv const-decl "nat" inv nil)) nil)) (minimum_inv_aux_TCC3 0 (minimum_inv_aux_TCC3-1 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" (typepred "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (typepred "s!1") (("1" (expand "minimum_inv") (("1" (name-replace "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (minimum_inv const-decl "nat" inv nil) (<= const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (minimum_inv_exists formula-decl nil inv nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil)) nil)) (minimum_inv_impl_TCC1 0 (minimum_inv_impl_TCC1-1 nil 3392691816 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (minimum_inv_impl_def 0 (minimum_inv_impl_def-1 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) = minimum_inv(nzcx!1)") (("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" (typepred "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" (prop) (("1" (assert) (("1" (hide 1) (("1" (expand "minimum_inv") (("1" (typepred "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (name-replace "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (inst - "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" (lift-if) (("2" (prop) (("2" (hide 1 -3) (("2" (expand "minimum_inv") (("2" (typepred "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (name-replace "MIN" "min_nat.min({s | 3 <= abs(nzcx!1(s))})") (("1" (inst - "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) ((minimum_inv_impl const-decl "nat" inv nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (j!1 skolem-const-decl "nat" inv nil) (MIN skolem-const-decl "{a | 3 <= abs(nzcx!1(a)) AND (FORALL (x: nat): 3 <= abs(nzcx!1(x)) IMPLIES a <= x)}" inv nil) (minimum_inv_exists formula-decl nil inv nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nzcx!1 skolem-const-decl "cauchy_nzreal" inv nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (minimum_inv const-decl "nat" inv nil) (= const-decl "[T, T -> boolean]" equalities nil) (minimum_inv_aux def-decl "nat" inv nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (inv_p0 0 (inv_p0-1 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) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (expt_plus formula-decl nil exponentiation nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (^ const-decl "real" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (expt_ge1 formula-decl nil exponentiation nil)) nil)) (inv_p1 0 (inv_p1-1 nil 3250067368 ("" (skosimp*) (("" (lemma "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 ">=") (("" (lemma "both_sides_minus_le1" ("z" "1" "x" "1" "y" "2 ^ (2+ p!1 + s!1)")) (("" (replace -2 -1) (("" (lemma "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) (("" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "2 + p!1 + s!1")) (("" (expand "^" -1 2) (("" (expand "expt") (("" (expand "expt") (("" (replace -1 -2 rl) (("" (lemma "lt_le_transitivity" ("x" "2 ^ (2 + p!1 + s!1)" "y" "2 ^ (3 + p!1 + s!1) - 1" "z" "pn!1")) (("" (lemma "total_le") (("" (expand "total_order?") (("" (expand "partial_order?") (("" (expand "preorder?") (("" (expand "transitive?") (("" (flatten) (("" (inst -2 "2 ^ (2 + p!1 + s!1)" "2 ^ (3 + p!1 + s!1) - 1" "pn!1 - 1") (("" (replace -7) (("" (replace -10) (("" (replace -11) (("" (simplify) (("" (lemma "both_sides_expt_gt1_lt" ("gt1x" "2" "i" "3 + 2 * p!1 + 2 * s!1" "j" "4 + 2 * p!1 + 2 * s!1")) (("" (simplify -1) (("" (lemma "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 -4) (("" (replace -7) (("" (simplify) (("" (lemma "expt_times2" ("nzx" "2" "s" "2 + p!1 + s!1")) (("" (replace -1 -2 rl) (("" (simplify) (("" (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) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (lt_equiv_le_plus_one formula-decl nil prelude_aux nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (expt def-decl "real" exponentiation nil) (total_le formula-decl nil real_props nil) (partial_order? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (expt_times2 formula-decl nil inv nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (preorder? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_plus_le1 formula-decl nil real_props nil) (both_sides_minus_le1 formula-decl nil real_props nil) (above nonempty-type-eq-decl nil integers nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.67 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
