|
(epsilon_lemmas
(prod_bound 0
(prod_bound-1 nil 3253549178
("" (skosimp)
(("" (lemma "triangle")
(("" (inst -1 "(x1!1 - y1!1) * x2!1" "(x2!1 - y2!1) * y1!1")
(("" (auto-rewrite "abs_mult")
(("" (do-rewrite)
(("" (assert)
((""
(case "abs(x2!1 - y2!1) * abs(y1!1) <= e2!1 * abs(y1!1)")
(("1"
(case "abs(x1!1 - y1!1) * abs(x2!1) < e1!1 * (abs(y2!1) + e2!1)")
(("1" (assert) nil nil)
("2" (delete -1 -2 2)
(("2" (rewrite "lt_times_lt_pos1" 1)
(("2" (lemma "abs_diff")
(("2" (inst -1 "x2!1" "y2!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (delete -1 2)
(("2" (rewrite "le_times_le_pos" 1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((triangle formula-decl nil real_props nil)
(le_times_le_pos formula-decl nil real_props nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_times_lt_pos1 formula-decl nil real_props nil)
(abs_nat formula-decl nil abs_lems "reals/")
(abs_diff formula-decl nil abs_lems "reals/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" 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) (<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(abs_mult formula-decl nil 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(prod_epsilon 0
(prod_epsilon-1 nil 3253549178
("" (skolem!)
((""
(case "EXISTS (u, v, w : posreal) :
u * v <= e!1/3 and abs(y1!1) * v < e!1/3 and abs(y2!1) * w < e!1/3")
(("1" (skosimp)
(("1" (inst 1 "min(u!1, w!1)" "v!1")
(("1"
(case "min(u!1, w!1) * v!1 <= u!1 * v!1 and abs(y2!1) * min(u!1, w!1) <= abs(y2!1) * w!1")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (delete -1 -2 -3 2)
(("2" (split)
(("1" (rewrite "both_sides_times_pos_le1")
(("1" (assert) nil nil)) nil)
("2" (rewrite "le_times_le_pos") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete 2)
(("2" (name "f" "e!1/3")
(("2" (replace -1)
(("2"
(case "FORALL (x : nonneg_real) : x * (f / (x+1)) < f")
(("1" (inst-cp -1 "abs(y1!1)")
(("1" (inst -1 "abs(y2!1)")
(("1"
(inst 1 "abs(y1!1) + 1" "f / (abs(y1!1) + 1)"
"f / (abs(y2!1) + 1)")
(("1" (split)
(("1" (rewrite "div_cancel1")
(("1" (assert) nil nil)) nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (delete -1 2)
(("2" (skolem!)
(("2" (rewrite "times_div1")
(("2" (rewrite "div_mult_pos_lt1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(le_times_le_pos formula-decl nil real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(div_cancel1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(times_div1 formula-decl nil real_props nil))
nil))
(inv_bound_TCC1 0
(inv_bound_TCC1-1 nil 3253549178
("" (skosimp)
(("" (rewrite "zero_times3") (("" (assert) nil nil)) nil)) nil)
((zero_times3 formula-decl nil 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)
(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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil 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)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(inv_bound 0
(inv_bound-1 nil 3253549178
("" (skosimp)
(("" (assert)
(("" (lemma "abs_eq_0" ("x" "x1!1"))
(("" (replace 1)
(("" (ground)
(("" (auto-rewrite "zero_times3")
((""
(case "abs(1 / x1!1 - 1 / y1!1) = abs(x1!1 - y1!1) / (abs(y1!1) * abs(x1!1))")
(("1" (lemma "lt_div_lt_pos2")
(("1"
(inst - "abs(x1!1 - y1!1)"
"abs(y1!1) * (abs(y1!1) - e1!1)"
"abs(y1!1) * abs(x1!1)" "e1!1")
(("1" (split)
(("1" (assert)
(("1" (replace -2) (("1" (propax) nil nil))
nil))
nil)
("2" (propax) nil nil)
("3" (delete -1 5)
(("3" (rewrite "both_sides_times_pos_le2")
(("3"
(use "abs_diff" ("x" "y1!1" "y" "x1!1"))
(("3" (rewrite "abs_diff_commute" -2)
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (delete -1 5)
(("2" (case "abs(y1!1) * (abs(y1!1) - e1!1) > 0")
(("1" (assert) nil nil)
("2" (delete 2)
(("2" (rewrite "pos_times_gt") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (delete 5 -1)
(("2"
(auto-rewrite "minus_div1" "abs_div" "abs_mult")
(("2" (assert)
(("2" (rewrite "abs_diff_commute" 1)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals 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)
(minus_div1 formula-decl nil real_props nil)
(abs_mult formula-decl nil real_props nil)
(abs_div formula-decl nil real_props nil)
(lt_div_lt_pos2 formula-decl nil real_props nil)
(pos_times_gt formula-decl nil real_props nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_diff_commute formula-decl nil abs_lems "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs_diff formula-decl nil abs_lems "reals/")
(e1!1 skolem-const-decl "posreal" epsilon_lemmas nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(y1!1 skolem-const-decl "real" epsilon_lemmas nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals 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)
(- const-decl "[numfield, numfield -> numfield]" 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs_eq_0 formula-decl nil abs_lems "reals/")
(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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(inv_epsilon1 0
(inv_epsilon1-1 nil 3253549178
("" (skosimp)
(("" (lemma "abs_eq_0" ("x" "y1!1"))
(("" (assert)
(("" (case "EXISTS (c : posreal) : c < e!1 / (1 + e!1)")
(("1" (skolem!)
(("1" (inst 3 "abs(y1!1) * c!1")
(("1" (split)
(("1"
(lemma "both_sides_times_pos_lt2"
("pz" "abs(y1!1)" "x" "c!1" "y" "1"))
(("1" (assert)
(("1"
(case "e!1 / (1 + e!1) < (1 + e!1) / (1 + e!1)")
(("1" (rewrite "div_simp")
(("1" (assert) nil nil)) nil)
("2" (rewrite "both_sides_div_pos_lt1") nil
nil))
nil))
nil))
nil)
("2" (lemma "both_sides_times_pos_lt2")
(("2" (inst -1 "abs(y1!1)" "c!1" "e!1 * (1 - c!1)")
(("2" (assert)
(("2" (delete 2)
(("2" (rewrite "div_mult_pos_lt2") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "pos_times_gt") nil nil))
nil))
nil)
("2" (delete 2 3 4)
(("2" (inst 1 "e!1 / (2 + e!1)")
(("2" (rewrite "both_sides_div_pos_lt2") nil nil)) nil))
nil))
nil))
nil))
nil))
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)
(abs_eq_0 formula-decl nil abs_lems "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(< const-decl "bool" reals 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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(y1!1 skolem-const-decl "real" epsilon_lemmas nil)
(c!1 skolem-const-decl "posreal" epsilon_lemmas nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_lt2 formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(div_simp formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos_times_gt formula-decl nil real_props nil)
(both_sides_div_pos_lt2 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(inv_epsilon_TCC1 0
(inv_epsilon_TCC1-1 nil 3253549178
("" (skosimp*)
(("" (rewrite "zero_times3") (("" (assert) nil nil)) nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(zero_times3 formula-decl nil 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)
(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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil 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))
nil))
(inv_epsilon 0
(inv_epsilon-1 nil 3253549178
("" (skosimp)
(("" (lemma "abs_eq_0" ("x" "y1!1"))
(("" (assert)
(("" (lemma "inv_epsilon1" ("y1" "y1!1" "e" "e!1 * abs(y1!1)"))
(("1" (assert)
(("1" (skosimp)
(("1" (inst 3 "e1!1")
(("1" (assert)
(("1" (rewrite "div_mult_pos_lt1")
(("1" (delete -2 4)
(("1"
(lemma "posreal_mult_closed"
("x" "abs(y1!1)" "y" "abs(y1!1) - e1!1"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "posreal_mult_closed") nil nil))
nil))
nil))
nil))
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)
(abs_eq_0 formula-decl nil abs_lems "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(inv_epsilon1 formula-decl nil epsilon_lemmas 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)
(posreal_mult_closed formula-decl nil real_axioms nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(varying_epsilon 0
(varying_epsilon-1 nil 3461939779
("" (skosimp)
(("" (split)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (lemma "archimedean" ("px" "x!1-y!1"))
(("1" (skosimp)
(("1" (inst - "1/n!1") (("1" (assert) nil nil)) nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(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)
(archimedean formula-decl nil real_props nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.6 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.
|
