|
(interval_bolzano
(bolzano_bisect_TCC1 0
(bolzano_bisect_TCC1-1 nil 3321034255 ("" (grind-reals) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(Proper_size application-judgement "nnreal" interval nil))
nil))
(bolzano_bisect_TCC2 0
(bolzano_bisect_TCC2-1 nil 3321034255 ("" (grind-reals) nil nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(Proper_size application-judgement "nnreal" interval nil))
nil))
(bolzano_bisect_TCC3 0
(bolzano_bisect_TCC3-1 nil 3321034255 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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)
(slice const-decl "real" interval nil)
(midpoint const-decl "real" interval nil)
([\|\|] const-decl "Interval" interval nil)
(HalfLeft const-decl "Interval" interval nil)
(HalfRight const-decl "Interval" interval nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil)
(<< const-decl "bool" interval nil))
nil))
(bolzano_bisect_TCC4 0
(bolzano_bisect_TCC4-3 nil 3321037604
("" (skosimp* :preds? t)
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (lemma "log_nat_incr")
(("2"
(inst -1 "2" "size(Y1!1) / eps!1"
"size(X!1) / eps!1")
(("2" (assert)
(("2" (hide 3)
(("2" (lemma "Halves")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Proper_HalfRight application-judgement "ProperInterval" interval
nil)
(Proper_HalfLeft application-judgement "ProperInterval" interval
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(above nonempty-type-eq-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(size const-decl "real" interval nil)
(Halves formula-decl nil interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(log_nat_incr formula-decl nil log_nat "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(ProperInterval type-eq-decl nil interval nil)
(posint_exp application-judgement "posint" exponentiation nil)
(Proper_size application-judgement "nnreal" interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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))
nil))
(bolzano_bisect_TCC5 0
(bolzano_bisect_TCC5-2 nil 3321037619
("" (skosimp* :preds? t)
(("" (lemma "Halves_Incl")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (typepred "v!1(Prop?!1, Y1!1, eps!1)")
(("1" (lemma "Incl_trans")
(("1" (inst? -1 :where 2)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (lemma "bolzano_bisect_TCC4")
(("2" (inst?)
(("2" (assert)
(("2" (inst?)
(("2" (assert)
(("2" (inst -1 "Y2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Halves_Incl formula-decl nil interval nil)
(Proper_HalfRight application-judgement "ProperInterval" interval
nil)
(Proper_HalfLeft application-judgement "ProperInterval" interval
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(<< const-decl "bool" interval nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
"reals/")
(^ 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers 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)
(size const-decl "real" interval nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Incl_trans formula-decl nil interval nil)
(bolzano_bisect_TCC4 termination-tcc nil interval_bolzano nil)
(ProperInterval type-eq-decl nil interval nil)
(posint_exp application-judgement "posint" exponentiation nil)
(Proper_size application-judgement "nnreal" interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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))
nil))
(bolzano_bisect_TCC6 0
(bolzano_bisect_TCC6-2 nil 3321057051 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ProperInterval type-eq-decl nil interval nil)
(size const-decl "real" interval nil)
(slice const-decl "real" interval nil)
(midpoint const-decl "real" interval nil)
([\|\|] const-decl "Interval" interval nil)
(HalfLeft const-decl "Interval" interval nil)
(HalfRight const-decl "Interval" interval nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(bolzano_bisect_TCC7 0
(bolzano_bisect_TCC7-1 nil 3403639539
("" (skosimp* :preds? t)
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (lemma "log_nat_incr")
(("2"
(inst -1 "2" "size(Y2!1) / eps!1"
"size(X!1) / eps!1")
(("2" (assert)
(("2" (hide 3)
(("2" (lemma "Halves")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Proper_HalfRight application-judgement "ProperInterval" interval
nil)
(Proper_HalfLeft application-judgement "ProperInterval" interval
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(above nonempty-type-eq-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(size const-decl "real" interval nil)
(Halves formula-decl nil interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(log_nat_incr formula-decl nil log_nat "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(ProperInterval type-eq-decl nil interval nil)
(posint_exp application-judgement "posint" exponentiation nil)
(Proper_size application-judgement "nnreal" interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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))
nil)
(bolzano_bisect_TCC7-2 nil 3321094616
("" (skosimp* :preds? t)
(("" (lemma "Halves_Incl")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (name-replace "Y1" "HalfLeft(X!1)" :hide? nil)
(("" (name-replace "Y2" "HalfRight(X!1)" :hide? nil)
(("" (lift-if)
(("" (ground)
(("1" (typepred "v!1(Prop?!1, Y1, eps!1)")
(("1" (lemma "Incl_trans")
(("1" (inst? -1 :where 1)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "Continuous?" -5)
(("2" (inst? -5)
(("2" (assert)
(("2" (typepred "v!1(Prop?!1, Y2, eps!1)")
(("2" (lemma "Incl_trans")
(("2"
(inst? -1 :where 1)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Proper? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(HalfRight const-decl "Interval" interval nil)
(Incl_trans formula-decl nil interval nil)
(size const-decl "real" interval nil)
(log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
"reals/")
(<< const-decl "bool" interval nil)
(HalfLeft const-decl "Interval" interval nil)
(Halves_Incl formula-decl nil interval nil))
nil))
(bolzano_bisect_TCC8 0
(bolzano_bisect_TCC8-2 nil 3403640475
("" (skosimp* :preds? t)
(("" (lemma "Halves_Incl")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (typepred "v!1(Prop?!1, Y2!1, eps!1)")
(("1" (lemma "Incl_trans")
(("1" (inst? -1 :where 3)
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (expand "Continuous?")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (lemma "bolzano_bisect_TCC7")
(("2" (inst?)
(("2" (assert)
(("2" (inst -1 "Y1!1")
(("2" (assert)
(("2" (inst -1 "Y2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "Continuous?")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Halves_Incl formula-decl nil interval nil)
(Proper_HalfRight application-judgement "ProperInterval" interval
nil)
(Proper_HalfLeft application-judgement "ProperInterval" interval
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(<< const-decl "bool" interval nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
"reals/")
(^ 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers 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)
(size const-decl "real" interval nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Prop?!1 skolem-const-decl "(Continuous?)" interval_bolzano nil)
(Y2!1 skolem-const-decl "ProperInterval" interval_bolzano nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Incl_trans formula-decl nil interval nil)
(bolzano_bisect_TCC7 termination-tcc nil interval_bolzano nil)
(ProperInterval type-eq-decl nil interval nil)
(posint_exp application-judgement "posint" exponentiation nil)
(Proper_size application-judgement "nnreal" interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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))
nil)
(bolzano_bisect_TCC8-1 nil 3403636065 ("" (subtype-tcc) nil nil) nil
nil))
(SqrtProp 0
(SqrtProp-1 nil 3321040119 ("" (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)
(nnreal type-eq-decl nil real_types nil)
(Proper? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(slice const-decl "real" interval nil)
(midpoint const-decl "real" interval nil)
([\|\|] const-decl "Interval" interval nil)
(HalfLeft const-decl "Interval" interval nil)
(sq const-decl "nonneg_real" sq "reals/")
(SqrtProp? const-decl "bool" interval_bolzano nil)
(HalfRight const-decl "Interval" interval nil)
(Continuous? const-decl "bool" interval_bolzano nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(sqrt_bisect_TCC1 0
(sqrt_bisect_TCC1-1 nil 3321038737
("" (grind) (("" (cancel-by 1 "x!1") nil nil)) nil)
((zero_times1 formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(pos_div_gt formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(CBD_1 skolem-const-decl "nnreal" interval_bolzano nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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_times_pos_le1 formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(nnreal type-eq-decl nil real_types nil)
(SqrtProp? const-decl "bool" interval_bolzano nil)
(sq const-decl "nonneg_real" sq "reals/")
(Proper? const-decl "bool" interval nil)
([\|\|] const-decl "Interval" interval nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
nil))
(sqrt_bisect_TCC2 0
(sqrt_bisect_TCC2-1 nil 3321039634
("" (expand "NonNeg?")
(("" (skeep)
((""
(typepred
"bolzano_bisect(SqrtProp?(x), [| 0, max(1, x) |], eps)")
(("" (expand* "Proper?" "<<" "Ge")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((Ge const-decl "bool" interval nil)
(lb_interval formula-decl nil interval nil)
(ub_interval formula-decl nil interval nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Proper_size application-judgement "nnreal" interval nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(SqrtProp application-judgement "(Continuous?)" interval_bolzano
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(Continuous? const-decl "bool" interval_bolzano 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)
(>= const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<< const-decl "bool" interval nil)
(<= const-decl "bool" reals nil)
(size const-decl "real" interval nil)
(bolzano_bisect def-decl
"{Y | Y << X AND Prop?(Y) AND size(Y) <= eps}" interval_bolzano
nil)
(nnreal type-eq-decl nil real_types nil)
(SqrtProp? const-decl "bool" interval_bolzano nil)
([\|\|] const-decl "Interval" interval nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(NonNeg? const-decl "bool" interval nil))
nil))
(sqrt_bisect_inclusion 0
(sqrt_bisect_inclusion-1 nil 3321038934
("" (skeep)
(("" (typepred "sqrt_bisect(x, eps)")
(("" (expand "sqrt_bisect")
((""
(typepred
"bolzano_bisect(SqrtProp?(x), [| 0, max(1, x) |], eps)")
((""
(name-replace "AA"
"bolzano_bisect(SqrtProp?(x), [| 0, max(1, x) |], eps)")
(("" (expand* "NonNeg?" "SqrtProp?" "Member?" "Ge")
(("" (flatten)
(("" (both-sides-f -3 "sqrt")
(("1" (rewrite "sqrt_sq")
(("1" (both-sides-f -4 "sqrt")
(("1" (rewrite "sqrt_sq")
(("1" (expand "##") (("1" (assert) nil nil))
nil))
nil)
("2" (rewrite "sqrt_le") nil nil))
nil))
nil)
("2" (rewrite "sqrt_le") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt_bisect const-decl "(NonNeg?)" interval_bolzano 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)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" 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)
(NonNeg? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
([\|\|] const-decl "Interval" interval nil)
(SqrtProp? const-decl "bool" interval_bolzano nil)
(bolzano_bisect def-decl
"{Y | Y << X AND Prop?(Y) AND size(Y) <= eps}" interval_bolzano
nil)
(size const-decl "real" interval nil)
(<= const-decl "bool" reals nil)
(<< const-decl "bool" interval nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Continuous? const-decl "bool" interval_bolzano nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(SqrtProp application-judgement "(Continuous?)" interval_bolzano
nil)
(Ge const-decl "bool" interval nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(|##| const-decl "bool" interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(Proper_size application-judgement "nnreal" interval nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_le formula-decl nil sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(= const-decl "[T, T -> boolean]" equalities nil))
shostak)))
¤ Dauer der Verarbeitung: 0.11 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.
|
