|
(continuous_lambda
(id_cont 0
(id_cont-1 nil 3443541122
("" (lemma "identity_cont_fun")
(("" (expand "I") (("" (propax) nil nil)) nil)) nil)
((I const-decl "(bijective?[T, T])" identity nil)
(identity_cont_fun formula-decl nil continuous_functions 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil))
nil))
(const_cont 0
(const_cont-1 nil 3443541239
("" (lemma "const_cont_fun")
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil)
((const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(const_cont_fun formula-decl nil continuous_functions 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil))
nil))
(add_cont 0
(add_cont-1 nil 3443542815
("" (skeep)
(("" (lemma "sum_cont_fun")
(("" (inst -1 "f" "g")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(sum_cont_fun formula-decl nil continuous_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(sub_cont 0
(sub_cont-1 nil 3443542940
("" (skeep)
(("" (lemma "diff_cont_fun")
(("" (inst -1 "f" "g")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(diff_cont_fun formula-decl nil continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
nil))
(neg_cont 0
(neg_cont-1 nil 3443543144
("" (skeep)
(("" (lemma "neg_cont_fun")
(("" (inst -1 "f")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(neg_cont_fun formula-decl nil continuous_functions nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(mult_cont 0
(mult_cont-1 nil 3443542990
("" (skeep)
(("" (lemma "prod_cont_fun")
(("" (inst -1 "f" "g")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(prod_cont_fun formula-decl nil continuous_functions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
nil))
(div_cont 0
(div_cont-1 nil 3443543020
("" (skeep)
(("" (lemma "div_cont_fun")
(("" (inst -1 "f" "nzf")
(("" (expand "/") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(div_cont_fun formula-decl nil continuous_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(nz_continuous_fun type-eq-decl nil continuous_functions nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
nil))
(scal_mult_cont 0
(scal_mult_cont-1 nil 3443541125
("" (skeep)
(("" (rewrite "mult_cont") (("" (rewrite "const_cont") nil nil))
nil))
nil)
((mult_cont formula-decl nil continuous_lambda 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil)
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(real_times_real_is_real application-judgement "real" reals nil)
(const_cont formula-decl nil continuous_lambda nil))
shostak))
(scal_div1_cont 0
(scal_div1_cont-1 nil 3443543077
("" (skeep)
(("" (rewrite "div_cont") (("" (rewrite "const_cont") nil nil))
nil))
nil)
((div_cont formula-decl nil continuous_lambda 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil)
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_continuous_fun type-eq-decl nil continuous_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(const_cont formula-decl nil continuous_lambda nil))
shostak))
(scal_div2_cont 0
(scal_div2_cont-1 nil 3443543112
("" (skeep)
(("" (rewrite "div_cont") (("" (rewrite "const_cont") nil nil))
nil))
nil)
((div_cont formula-decl nil continuous_lambda 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil)
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_continuous_fun type-eq-decl nil continuous_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(const_cont formula-decl nil continuous_lambda nil))
shostak))
(pow_cont_TCC1 0
(pow_cont_TCC1-1 nil 3443542015
("" (skosimp) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(pow_cont 0
(pow_cont-1 nil 3443543278
("" (skeep)
(("" (lemma "expt_fun_continuous")
(("" (inst -1 "f" "n")
(("" (expand "^" -1) (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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_fun_continuous formula-decl nil continuous_functions nil)
(^ const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(sq_cont 0
(sq_cont-1 nil 3443541122
("" (skeep)
(("" (expand "sq") (("" (rewrite "mult_cont") nil nil)) nil)) nil)
((real_times_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(mult_cont formula-decl nil continuous_lambda nil))
nil))
(sqrt_cont_TCC1 0
(sqrt_cont_TCC1-2 nil 3445362785
("" (skeep :preds? t)
(("" (expand "pos_continuous?")
(("" (inst -2 "x") (("" (assert) nil nil)) nil)) nil))
nil)
((pos_continuous? const-decl "bool" continuous_lambda 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)
(T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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))
nil)
(sqrt_cont_TCC1-1 nil 3443542015
("" (skeep :preds? t)
(("" (expand "pos_continuous")
(("" (inst -2 "x") (("" (assert) nil nil)) nil)) nil))
nil)
nil nil))
(sqrt_cont 0
(sqrt_cont-2 nil 3445362819
("" (skeep)
(("" (lemma "composition_cont_fun[T,posreal]")
(("" (inst -1 "pf" "LAMBDA(x:posreal):sqrt(x)")
(("1" (assert)
(("1" (expand "o")
(("1" (hide 2)
(("1" (lemma "sqrt_continuous")
(("1" (expand "restrict") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (typepred "pf")
(("2" (expand "pos_continuous?")
(("2" (inst -2 "x1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(composition_cont_fun formula-decl nil composition_continuous nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(restrict const-decl "R" restrict nil)
(sqrt_continuous formula-decl nil sqrt_derivative nil)
(O const-decl "T3" function_props nil)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(pos_continuous? const-decl "bool" continuous_lambda nil)
(pos_continuous_fun type-eq-decl nil continuous_lambda nil)
(pf skolem-const-decl "pos_continuous_fun" continuous_lambda nil))
nil)
(sqrt_cont-1 nil 3443543750
("" (skeep)
(("" (lemma "composition_cont_fun[T,posreal]")
(("" (inst -1 "pf" "LAMBDA(x:posreal):sqrt(x)")
(("1" (assert)
(("1" (expand "o")
(("1" (hide 2)
(("1" (lemma "sqrt_continuous")
(("1" (expand "restrict") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (typepred "pf")
(("2" (expand "pos_continuous")
(("2" (inst -2 "x1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((composition_cont_fun formula-decl nil composition_continuous nil)
(sqrt_continuous formula-decl nil sqrt_derivative nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions
nil))
shostak))
(abs_cont 0
(abs_cont-1 nil 3443549095
("" (skeep)
(("" (lemma "composition_cont_fun[T,real]")
(("" (inst -1 "f" "abs")
(("" (expand "o")
(("" (assert)
(("" (hide 2)
(("" (expand "continuous?")
(("" (skeep)
(("" (expand "continuous?")
(("" (skolem 1 "eps")
(("" (inst 1 "eps")
(("" (skeep) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil continuous_lambda nil)
(T_pred const-decl "[real -> boolean]" continuous_lambda 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)
(composition_cont_fun formula-decl nil composition_continuous nil)
(O const-decl "T3" function_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(continuous? const-decl "bool" continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(max_cont 0
(max_cont-1 nil 3443783422
("" (skolem 1 ("f1" "f2"))
((""
(case-replace
"(LAMBDA(x):max(f1(x),f2(x))) = (LAMBDA(x):(f1(x)+f2(x)+abs(f1(x)-f2(x)))/2)")
(("1" (hide -1)
(("1" (rewrite "scal_div1_cont")
(("1" (rewrite "add_cont")
(("1" (rewrite "add_cont")
(("1" (rewrite "abs_cont")
(("1" (rewrite "sub_cont") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("1" (rewrite "max_abs") nil nil)
("2" (hide 2)
(("2" (skeep)
(("2" (lemma "max_abs")
(("2" (inst -1 "f1(x)" "f2(x)")
(("2" (replaces -1 :dir rl) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(/= const-decl "boolean" notequal 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(scal_div1_cont formula-decl nil continuous_lambda nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sub_cont formula-decl nil continuous_lambda nil)
(abs_cont formula-decl nil continuous_lambda nil)
(add_cont formula-decl nil continuous_lambda nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(f1 skolem-const-decl "continuous_fun[T]" continuous_lambda nil)
(f2 skolem-const-decl "continuous_fun[T]" continuous_lambda nil)
(max_abs formula-decl nil min_max "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(min_cont 0
(min_cont-1 nil 3443548048
("" (skolem 1 ("f1" "f2"))
((""
(case-replace
"(LAMBDA(x):min(f1(x),f2(x))) = (LAMBDA(x):-max(-f1(x),-f2(x)))")
(("1" (hide -)
(("1" (rewrite "neg_cont")
(("1" (rewrite "max_cont")
(("1" (rewrite "neg_cont") nil nil)
("2" (rewrite "neg_cont") nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("1" (grind) nil nil)
("2" (skeep)
(("2" (rewrite "min_max" :dir rl) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals 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)
(T_pred const-decl "[real -> boolean]" continuous_lambda nil)
(T formal-subtype-decl nil continuous_lambda nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(neg_cont formula-decl nil continuous_lambda nil)
(max_cont formula-decl nil continuous_lambda nil)
(f1 skolem-const-decl "continuous_fun[T]" continuous_lambda nil)
(f2 skolem-const-decl "continuous_fun[T]" continuous_lambda 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)
(min_max formula-decl nil min_max "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.8 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.
|
