|
(sq
(sq_TCC1 0 (sq_TCC1-1 nil 3255279994 ("" (ground) nil nil) nil nil))
(sq_nz_pos 0
(sq_nz_pos-1 nil 3255279994 ("" (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)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal 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 nonempty-type-eq-decl nil reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_rew 0
(sq_rew-1 nil 3255279994 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)) nil))
(sq_expt2_TCC1 0
(sq_expt2_TCC1-1 nil 3549709855 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(sq_expt2 0
(sq_expt2-1 nil 3549709856 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil))
shostak))
(sq_neg 0
(sq_neg-1 nil 3255279994 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(sq_pos 0
(sq_pos-1 nil 3255279994
("" (skosimp*) (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)
((sq const-decl "nonneg_real" sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sq_plus_pos 0
(sq_plus_pos-1 nil 3255279994
("" (skolem 1 ("a" "b"))
(("" (case "sq(a)>=0" "sq(b) >= 0")
(("1" (ground) nil nil) ("2" (rewrite "sq_pos") nil nil)
("3" (rewrite "sq_pos") nil nil))
nil))
nil)
((sq const-decl "nonneg_real" sq 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_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_pos formula-decl nil sq nil))
nil))
(sq_times 0
(sq_times-1 nil 3255279994 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sq_plus 0
(sq_plus-1 nil 3255279994 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_minus 0
(sq_minus-1 nil 3255279994 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_neg_minus 0
(sq_neg_minus-1 nil 3255279994 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_abs 0
(sq_abs-1 nil 3255280284 ("" (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)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq const-decl "nonneg_real" sq nil))
shostak))
(sq_abs_neg 0
(sq_abs_neg-1 nil 3255280291 ("" (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)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq const-decl "nonneg_real" sq nil))
shostak))
(sq_0 0
(sq_0-1 nil 3255279994 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)) nil))
(sq_1 0
(sq_1-1 nil 3255279994 ("" (grind) nil nil)
((sq const-decl "nonneg_real" sq nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil))
(sq_eq_0 0
(sq_eq_0-1 nil 3255279994
("" (skosimp*)
(("" (expand "sq")
(("" (lemma "zero_times3")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((sq const-decl "nonneg_real" sq 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)
(zero_times3 formula-decl nil real_props nil))
nil))
(sq_gt_0 0
(sq_gt_0-1 nil 3255279994
("" (skosimp*)
(("" (expand "sq")
(("" (lemma "pos_times_gt")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((sq const-decl "nonneg_real" sq 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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pos_times_gt formula-decl nil real_props nil))
nil))
(sq_div_TCC1 0
(sq_div_TCC1-1 nil 3255279994
("" (skolem 1 "d")
(("" (ground) (("" (rewrite "sq_eq_0") 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)
(sq_eq_0 formula-decl nil sq nil))
nil))
(sq_div 0
(sq_div-1 nil 3255279994 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)
(sq const-decl "nonneg_real" sq nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(sq_plus_eq_0 0
(sq_plus_eq_0-1 nil 3255279994
("" (skolem 1 ("a" "b"))
(("" (ground)
(("1" (lemma "sq_pos")
(("1" (inst -1 "b")
(("1" (case "sq(a)>0")
(("1" (ground) nil nil)
("2" (delete -)
(("2" (expand "sq")
(("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sq_pos")
(("2" (inst -1 "a")
(("2" (case "sq(b)>0")
(("1" (ground) nil nil)
("2" (delete -)
(("2" (expand "sq")
(("2" (rewrite "pos_times_gt") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (grind) nil nil))
nil))
nil)
((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(pos_times_gt formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(sq_pos formula-decl nil sq nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(sq_ge 0
(sq_ge-1 nil 3255279994
("" (skosimp*)
(("" (ground)
(("1" (case "nna!1 < nnb!1")
(("1" (case "sq(nna!1) < sq(nnb!1)")
(("1" (ground) nil nil)
("2" (hide -2 2)
(("2" (lemma "lt_times_lt_pos1")
(("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
(("1" (ground)
(("1" (expand "sq") (("1" (propax) nil nil)) nil))
nil)
("2" (ground)
(("2" (case "nna!1=0")
(("1" (ground)
(("1" (replace -1 :hide? t)
(("1" (expand "sq")
(("1" (ground)
(("1" (rewrite "pos_times_lt") nil nil))
nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil)
("2" (lemma "ge_times_ge_pos")
(("2" (inst?)
(("2" (inst -1 "nnb!1" "nna!1")
(("2" (ground)
(("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_times_lt_pos1 formula-decl nil real_props nil)
(pos_times_lt formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(nna!1 skolem-const-decl "nonneg_real" sq nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_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) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(ge_times_ge_pos formula-decl nil real_props nil))
nil))
(sq_le 0
(sq_le-1 nil 3255279994
("" (lemma "sq_ge")
(("" (skolem 1 ("nna" "nnb"))
(("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
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)
(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)
(sq_ge formula-decl nil sq nil))
nil))
(sq_gt 0
(sq_gt-1 nil 3255279994
("" (skosimp*)
(("" (ground)
(("1" (case "nna!1 <= nnb!1")
(("1" (case "sq(nna!1) <= sq(nnb!1)")
(("1" (ground) nil nil)
("2" (hide -2 2)
(("2" (lemma "le_times_le_pos")
(("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
(("2" (ground)
(("2" (expand "sq") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil)
("2" (lemma "gt_times_gt_pos1")
(("2" (inst?)
(("2" (inst -1 "nnb!1" "nna!1")
(("1" (assert)
(("1" (hide -2)
(("1" (expand "sq") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (case-replace "nnb!1 = 0")
(("1" (hide -1 1)
(("1" (expand "sq" 1 2)
(("1" (lemma "sq_pos")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "sq_eq_0")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq const-decl "nonneg_real" sq nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_times_le_pos formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq_eq_0 formula-decl nil sq nil) (sq_pos formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nnb!1 skolem-const-decl "nonneg_real" sq nil)
(gt_times_gt_pos1 formula-decl nil real_props nil))
nil))
(sq_lt 0
(sq_lt-1 nil 3255279994
("" (skolem 1 ("nna" "nnb"))
(("" (lemma "sq_gt")
(("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
nil)
((sq_gt formula-decl nil sq 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)
(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))
nil))
(sq_eq 0
(sq_eq-1 nil 3255279994
("" (skosimp*)
(("" (case-replace "nna!1 = 0")
(("1" (lemma "sq_eq_0")
(("1" (inst -1 "nnb!1")
(("1" (expand "sq") (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (case-replace "nnb!1 = 0")
(("1" (lemma "sq_eq_0")
(("1" (inst?)
(("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil))
nil)
("2" (ground)
(("2" (lemma "both_sides_expt2_aux")
(("2" (inst -1 "2" "nna!1" "nnb!1")
(("2" (expand "expt")
(("2" (expand "expt")
(("2" (expand "expt")
(("2" (expand "sq") (("2" (propax) nil 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq const-decl "nonneg_real" sq nil)
(sq_eq_0 formula-decl nil sq nil)
(real_gt_is_strict_total_order name-judgement
"(strict_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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(expt def-decl "real" exponentiation nil)
(nnreal_expt application-judgement "nnreal" exponentiation nil)
(both_sides_expt2_aux formula-decl nil exponentiation nil))
nil))
(sq_neg_pos_le 0
(sq_neg_pos_le-1 nil 3255279994
("" (skolem 1 ("a" "c"))
(("" (case "a >= 0")
(("1" (lemma "sq_le")
(("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
("2" (lemma "sq_le")
(("2" (inst -1 "-a" "c")
(("1" (case-replace "sq(-a) = sq(a)")
(("1" (hide -1) (("1" (ground) nil nil)) nil)
("2" (hide -1 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(a skolem-const-decl "real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_le formula-decl nil sq nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(neg_pos_sq_le 0
(neg_pos_sq_le-1 nil 3255279994
("" (skolem 1 ("a" "b"))
(("" (ground)
(("" (case "a > 0")
(("1" (lemma "sq_le")
(("1" (inst -1 "a" "b")
(("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
nil)
("2" (case "-a <= b")
(("1" (lemma "sq_le")
(("1" (inst -1 "-a" "b")
(("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
("2" (ground) nil nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
(sq_le formula-decl nil sq nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(a skolem-const-decl "real" sq nil)
(>= const-decl "bool" reals 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))
nil))
(sq_neg_pos_lt 0
(sq_neg_pos_lt-1 nil 3255279994
("" (skolem 1 ("a" "c"))
(("" (case "a >= 0")
(("1" (lemma "sq_lt")
(("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
("2" (lemma "sq_lt")
(("2" (inst -1 "-a" "c")
(("1" (case-replace "sq(-a) = sq(a)")
(("1" (ground) nil nil)
("2" (hide -1 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(a skolem-const-decl "real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(sq_lt formula-decl nil sq nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(neg_pos_sq_lt 0
(neg_pos_sq_lt-1 nil 3255279994
("" (skolem 1 ("a" "b"))
(("" (ground)
(("" (case "a > 0")
(("1" (lemma "sq_lt")
(("1" (inst -1 "a" "b")
(("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
nil)
("2" (case "-a < b")
(("1" (lemma "sq_lt")
(("1" (inst -1 "-a" "b")
(("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
("2" (ground) nil nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
(sq_lt formula-decl nil sq nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(a skolem-const-decl "real" sq nil)
(>= const-decl "bool" reals 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))
nil))
(sq_le_abs 0
(sq_le_abs-1 nil 3255279994
("" (skosimp*)
(("" (case-replace "b!1 >= 0")
(("1" (lemma "sq_neg_pos_le")
(("1" (inst?)
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil))
nil)
("2" (lemma "sq_neg_pos_le")
(("2" (inst -1 "a!1" "-b!1")
(("1" (case-replace "sq(-b!1) = sq(b!1)")
(("1" (hide -1)
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (hide -1 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (assert) 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(b!1 skolem-const-decl "real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq_neg_pos_le formula-decl nil sq nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_lt_abs 0
(sq_lt_abs-1 nil 3255279994
("" (skosimp*)
(("" (case-replace "b!1 >= 0")
(("1" (lemma "sq_neg_pos_lt")
(("1" (inst?)
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil))
nil)
("2" (lemma "sq_neg_pos_lt")
(("2" (inst -1 "a!1" "-b!1")
(("1" (case-replace "sq(-b!1) = sq(b!1)")
(("1" (hide -1)
(("1" (expand "abs")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (hide -1 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (assert) 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(b!1 skolem-const-decl "real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq_neg_pos_lt formula-decl nil sq nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sq_ge_abs 0
(sq_ge_abs-1 nil 3256039469
("" (skosimp*)
(("" (lemma "sq_le_abs")
(("" (inst -1 "b!1" "a!1") (("" (ground) nil nil)) nil)) nil))
nil)
((sq_le_abs formula-decl nil sq 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 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))
(sq_gt_abs 0
(sq_gt_abs-1 nil 3256039548
("" (skosimp*)
(("" (lemma "sq_lt_abs")
(("" (inst -1 "b!1" "a!1")
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((sq_lt_abs formula-decl nil sq 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 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))
shostak))
(sq_eq_abs 0
(sq_eq_abs-1 nil 3255279994
("" (skosimp*)
(("" (case "a!1 >= 0")
(("1" (case "b!1 >= 0")
(("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)
("2" (case-replace "sq(b!1) = sq(-b!1)")
(("1" (hide -1)
(("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
("2" (hide 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (case "b!1 >= 0")
(("1" (case-replace "sq(a!1) = sq(-a!1)")
(("1" (hide -1)
(("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
("2" (hide 3)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (case-replace "sq(a!1) = sq(-a!1)")
(("1" (case-replace "sq(b!1) = sq(-b!1)")
(("1" (hide -1 -2)
(("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil))
nil)
("2" (hide -1 4)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (hide 4)
(("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
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)
(minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sq const-decl "nonneg_real" sq nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_eq formula-decl nil sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sq_eq_rew 0
(sq_eq_rew-1 nil 3409051947
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(triangle_rectangle 0
(triangle_rectangle-1 nil 3255279994
("" (skolem 1 ("a" "b" "c"))
(("" (flatten)
(("" (case "sq(a)>=0" "sq(b)>=0" "sq(c)>=0")
(("1" (case "sq(a) <= sq(c)")
(("1" (case "sq(b) <= sq(c)")
(("1" (lemma "sq_neg_pos_le")
(("1" (inst-cp -1 "a" "c")
(("1" (inst -1 "b" "c") (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
nil)
("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
nil)
("2" (rewrite "sq_pos") nil nil)
("3" (rewrite "sq_pos") nil nil)
("4" (rewrite "sq_pos") nil nil))
nil))
nil))
nil)
((sq_pos formula-decl nil sq nil) (<= const-decl "bool" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(sq_neg_pos_le formula-decl nil sq 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)
(sq const-decl "nonneg_real" sq nil))
nil))
(triangle_ineq_lt 0
(triangle_ineq_lt-1 nil 3255279994
("" (skosimp*)
(("" (lemma "sq_lt_abs")
(("" (inst?)
(("" (assert)
(("" (lemma "sq_lt_abs")
(("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq_lt_abs formula-decl nil sq nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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))
(triangle_ineq_le 0
(triangle_ineq_le-1 nil 3255279994
("" (skosimp*)
(("" (lemma "sq_le_abs")
(("" (inst?)
(("" (assert)
(("" (lemma "sq_le_abs")
(("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sq_le_abs formula-decl nil sq nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)))
¤ Dauer der Verarbeitung: 0.23 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.
|
