|
(poly_rew
(poly_sum 0
(poly_sum-1 nil 3565981489
("" (skeep)
(("" (lemma "sum_polynomial_eq_degree")
(("" (inst?)
(("" (decompose-equality -1)
(("" (inst -1 "x")
(("" (expand "+" -1 1) (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((sum_polynomial_eq_degree formula-decl nil polynomials nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[T -> real]" real_fun_ops nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(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))
(poly_neg 0
(poly_neg-1 nil 3565981917
("" (skeep)
(("" (lemma "neg_polynomial")
(("" (inst? -1)
(("" (decompose-equality -1)
(("" (inst?)
(("" (assert)
(("" (expand "-" -1 1) (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((neg_polynomial formula-decl nil polynomials nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(minus_real_is_real application-judgement "real" reals nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(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))
(poly_diff 0
(poly_diff-1 nil 3565981671
("" (skeep)
((""
(case-replace
"polynomial(p, n)(x) - polynomial(q, n)(x) = polynomial(p, n)(x) + -polynomial(q, n)(x)")
(("1" (hide -1)
(("1" (rewrite "poly_neg")
(("1" (rewrite "poly_sum")
(("1" (expand "polynomial")
(("1" (rewrite "sigma_eq")
(("1" (hide 2)
(("1" (skeep) (("1" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(poly_neg formula-decl nil poly_rew nil)
(minus_real_is_real application-judgement "real" reals nil)
(expt def-decl "real" exponentiation 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)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(<= const-decl "bool" reals nil)
(- const-decl "[T -> real]" real_fun_ops nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(+ const-decl "[T -> real]" real_fun_ops nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sigma_eq formula-decl nil sigma nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(poly_sum formula-decl nil poly_rew nil)
(- const-decl "[T -> real]" real_fun_ops nil))
shostak))
(poly_scal 0
(poly_scal-1 nil 3565985037
("" (skeep)
(("" (lemma "scal_polynomial")
(("" (expand "const_fun")
(("" (inst -1 "p" "n" "k")
(("" (decompose-equality -1)
(("" (inst -1 "x")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((scal_polynomial formula-decl nil polynomials 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(* const-decl "[T -> real]" real_fun_ops nil)
(real_times_real_is_real application-judgement "real" reals nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(* const-decl "[T -> real]" real_fun_ops nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(const_fun const-decl "[T -> real]" real_fun_ops nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
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
|
