|
(shift
(cauchy_div2n_TCC1 0
(cauchy_div2n_TCC1-1 nil 3251040549 ("" (grind) nil 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(cauchy_div2n_TCC2 0
(cauchy_div2n_TCC2-1 nil 3251040561
("" (skosimp*)
(("" (typepred "cx!1")
(("" (expand "cauchy_real?")
(("" (skosimp*)
(("" (inst 1 "x!1/2^n!1")
(("" (expand "cauchy_prop")
(("" (skosimp*)
(("" (case "p!1>=n!1")
(("1" (replace -1 1)
(("1" (inst -2 "p!1-n!1")
(("1"
(lemma "expt_div"
("n0x" "2" "i" "p!1" "j" "n!1"))
(("1" (replace -1 -3 rl)
(("1" (grind) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (replace 1 2)
(("2" (name "RR" "round(cx!1(p!1)/2^n!1)")
(("2" (inst -2 "p!1")
(("2" (lemma "expt_pos" ("px" "2" "i" "n!1"))
(("2"
(lemma "lemma_A2"
("r" "RR" "p" "cx!1(p!1)" "q" "2^n!1"))
(("2" (replace -3)
(("2"
(skosimp*)
(("2"
(lemma
"div_mult_pos_lt1"
("z"
"x!1*2^p!1"
"py"
"2^n!1"
"x"
"RR+1"))
(("2"
(lemma
"div_mult_pos_lt2"
("x"
"RR-1"
"z"
"x!1*2^p!1"
"py"
"2^n!1"))
(("2"
(lemma
"both_sides_expt_gt1_ge"
("gt1x" "2" "i" "n!1" "j" "1"))
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? 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)
(cauchy_prop const-decl "bool" cauchy nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(p!1 skolem-const-decl "nat" shift nil)
(n!1 skolem-const-decl "nat" shift nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals 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)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_div formula-decl nil exponentiation nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(round const-decl "int" prelude_aux nil)
(expt_pos formula-decl nil exponentiation 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)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_expt_gt1_ge formula-decl nil exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt_x1 formula-decl nil exponentiation nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(lemma_A2 formula-decl nil appendix nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(cauchy_mul2n_TCC1 0
(cauchy_mul2n_TCC1-1 nil 3251041439
("" (skosimp*)
(("" (typepred "cx!1")
(("" (expand "cauchy_real?")
(("" (skosimp*)
(("" (inst 1 "x!1*2^n!1")
(("" (expand "cauchy_prop")
(("" (skosimp*)
(("" (inst - "p!1+n!1")
((""
(lemma "expt_plus" ("n0x" "2" "i" "p!1" "j" "n!1"))
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? 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)
(posint_exp application-judgement "posint" exponentiation 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)
(cauchy_prop const-decl "bool" cauchy nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_plus formula-decl nil exponentiation nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(lemma_div2n 0
(lemma_div2n-1 nil 3251034397
("" (expand "cauchy_prop")
(("" (expand "cauchy_div2n")
(("" (expand "div2n")
(("" (skosimp*)
(("" (case "p!1>=n!1")
(("1" (replace -1 1)
(("1" (inst -2 "p!1-n!1")
(("1"
(lemma "expt_div" ("n0x" "2" "i" "p!1" "j" "n!1"))
(("1" (replace -1 -3 rl) (("1" (grind) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (replace 1 2)
(("2" (name "RR" "round(cx!1(p!1)/2^n!1)")
(("2" (inst -2 "p!1")
(("2" (lemma "expt_pos" ("px" "2" "i" "n!1"))
(("2"
(lemma "lemma_A2"
("r" "RR" "p" "cx!1(p!1)" "q" "2^n!1"))
(("2" (replace -3)
(("2" (skosimp*)
(("2"
(lemma "div_mult_pos_lt1"
("z" "x!1*2^p!1" "py" "2^n!1" "x" "RR+1"))
(("2"
(lemma "div_mult_pos_lt2"
("x"
"RR-1"
"z"
"x!1*2^p!1"
"py"
"2^n!1"))
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(lemma
"both_sides_expt_gt1_ge"
("gt1x" "2" "i" "n!1" "j" "1"))
(("2"
(rewrite "expt_x1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_div2n const-decl "cauchy_real" shift nil)
(lemma_A2 formula-decl nil appendix nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(expt_x1 formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_expt_gt1_ge formula-decl nil exponentiation nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals 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)
(expt_pos formula-decl nil exponentiation nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(round const-decl "int" prelude_aux nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(cauchy_real? const-decl "bool" cauchy nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(expt_div formula-decl nil exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(n!1 skolem-const-decl "nat" shift nil)
(p!1 skolem-const-decl "nat" shift nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(bool nonempty-type-eq-decl nil booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(div2n const-decl "real" shift nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil))
shostak))
(lemma_mul2n 0
(lemma_mul2n-1 nil 3251034151
("" (expand "cauchy_prop")
(("" (expand "cauchy_mul2n")
(("" (expand "mul2n")
(("" (skosimp*)
(("" (inst - "n!1+p!1")
(("" (lemma "expt_plus" ("n0x" "2" "i" "n!1" "j" "p!1"))
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_mul2n const-decl "cauchy_real" shift nil)
(expt_plus formula-decl nil exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(^ const-decl "real" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "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)
(posint_times_posint_is_posint application-judgement "posint"
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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mul2n const-decl "real" shift nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil))
shostak)))
¤ Dauer der Verarbeitung: 0.21 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.
|
