|
(util
(eq_correct_1 0
(eq_correct_1-1 nil 3470478491
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "eq")
(("1" (flatten)
(("1" (mult-cases -1)
(("1" (case-replace "sq(a) = sq(-a)")
(("1" (case-replace "sq(e) = sq(-e)")
(("1" (hide (-1 -2))
(("1" (case "sqrt(sq(-a)*b) = sqrt(sq(-e))")
(("1" (rewrite "sqrt_times")
(("1" (assert) nil nil)) nil)
("2" (replaces -3) nil nil))
nil))
nil)
("2" (rewrite "sq_neg") nil nil))
nil)
("2" (rewrite "sq_neg") nil nil))
nil)
("2" (case "sqrt(sq(a)*b) = sqrt(sq(e))")
(("1" (rewrite "sqrt_times") (("1" (assert) nil nil))
nil)
("2" (replaces -3) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "eq")
(("2" (copy -1)
(("2" (both-sides-f -1 "sq")
(("2" (rewrite "sq_times")
(("2" (assert)
(("2" (hide -1)
(("2" (replaces -1 :dir rl)
(("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((eq const-decl "bool" util 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)
(pos_times_ge formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sqrt_sq formula-decl nil sqrt "reals/")
(sqrt_times formula-decl nil sqrt "reals/")
(sq_neg formula-decl nil sq "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_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)
(neg_times_ge formula-decl nil real_props nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_times formula-decl nil sq "reals/"))
shostak))
(eq_neg 0
(eq_neg-1 nil 3470499696 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(eq const-decl "bool" util nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(gt_correct_1 0
(gt_correct_1-1 nil 3460570945
("" (skeep)
(("" (expand "gt")
(("" (case "a>=0")
(("1" (assert)
(("1" (split 1)
(("1" (flatten)
(("1" (mult-by -2 "sqrt(b)")
(("1" (case "e < 0")
(("1" (assert) nil nil)
("2" (assert)
(("2" (real-props)
(("2" (both-sides-f 2 "sq")
(("1" (rewrite "sq_times") nil nil)
("2" (rewrite "sq_gt") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (both-sides-f -1 "sq")
(("1" (rewrite "sq_times") nil nil)
("2" (rewrite "sq_gt") nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (split)
(("1" (flatten)
(("1" (neg-formula 1)
(("1" (both-sides-f 1 "sq")
(("1" (sq-simp) (("1" (assert) nil nil)) nil)
("2" (rewrite "sq_gt") nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (case "e < 0")
(("1" (assert)
(("1" (neg-formula -2)
(("1" (both-sides-f -2 "sq")
(("1" (sq-simp) (("1" (assert) nil nil)) nil)
("2" (rewrite "sq_gt")
(("2" (neg-formula 1)
(("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (mult-by 2 "sqrt(b)")
(("2" (real-props) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((gt const-decl "bool" util nil)
(b skolem-const-decl "nnreal" util nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(neg_neg formula-decl nil extra_tegies nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(neg_times_ge formula-decl nil real_props nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(both_sides_times_neg_gt1 formula-decl nil real_props nil)
(sq_neg formula-decl nil sq "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_times_neg_le1_imp formula-decl nil extra_real_props
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_one_times formula-decl nil extra_tegies nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(< const-decl "bool" reals nil)
(pos_times_ge formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(sq_gt formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(sq_times formula-decl nil sq "reals/")
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(> const-decl "bool" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_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))
shostak))
(lt_correct_1 0
(lt_correct_1-1 nil 3460645954
("" (skeep)
(("" (expand "lt")
(("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil))
nil)
((lt const-decl "bool" util 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_times_real_is_real application-judgement "real" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(- const-decl "[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)
(gt_correct_1 formula-decl nil util nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(ge_correct_1 0
(ge_correct_1-1 nil 3460646107
("" (skeep)
(("" (expand "ge")
(("" (rewrite "lt_correct_1") (("" (ground) nil nil)) nil)) nil))
nil)
((ge const-decl "bool" util 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_times_real_is_real application-judgement "real" reals nil)
(nnreal 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)
(lt_correct_1 formula-decl nil util nil))
shostak))
(le_correct_1 0
(le_correct_1-1 nil 3460646250
("" (skeep)
(("" (expand "le")
(("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil))
nil)
((le const-decl "bool" util nil)
(real_le_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_times_real_is_real application-judgement "real" reals nil)
(nnreal 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)
(gt_correct_1 formula-decl nil util nil))
shostak))
(gt_correct_2 0
(gt_correct_2-1 nil 3460646699
("" (skeep)
(("" (expand "gt")
(("" (rewrite "lt_correct_1")
(("" (rewrite "lt_correct_1")
(("" (rewrite "gt_correct_1")
(("" (lemma "gt_correct_1")
(("" (inst -1 "a" "b" "c*sqrt(d) + e")
(("" (replaces -1 :dir rl)
(("" (expand "gt")
(("" (rewrite "sq_plus")
(("" (rewrite "sq_times") (("" (ground) 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_minus_real_is_real application-judgement "real" reals nil)
(gt const-decl "bool" util nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_plus formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_times formula-decl nil sq "reals/")
(gt const-decl "bool" util nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_correct_1 formula-decl nil util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal 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)
(lt_correct_1 formula-decl nil util nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(lt_correct_2 0
(lt_correct_2-1 nil 3460648253
("" (skeep)
(("" (expand "lt")
(("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(lt const-decl "bool" util 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_plus_real_is_real application-judgement "real" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(- const-decl "[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)
(gt_correct_2 formula-decl nil util nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(ge_correct_2 0
(ge_correct_2-1 nil 3460648277
("" (skeep)
(("" (expand "ge")
(("" (rewrite "lt_correct_2") (("" (ground) nil nil)) nil)) nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(ge const-decl "bool" util 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_plus_real_is_real application-judgement "real" reals nil)
(nnreal 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)
(lt_correct_2 formula-decl nil util nil))
shostak))
(le_correct_2 0
(le_correct_2-1 nil 3460648299
("" (skeep)
(("" (expand "le")
(("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(le const-decl "bool" util nil)
(real_le_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_plus_real_is_real application-judgement "real" reals nil)
(nnreal 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)
(gt_correct_2 formula-decl nil util nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
