|
(mod_div_lems
(mod_div 0
(mod_div-1 nil 3407856356 ("" (grind) nil nil)
((nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(div const-decl "integer" div nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sgn const-decl "int" real_defs nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil))
shostak))
(mod_rem 0
(mod_rem-1 nil 3407856353
("" (skosimp*)
(("" (lemma "floor_neg")
(("" (inst -1 "i!1/j!1")
(("" (expand "rem")
(("" (expand "div")
(("" (expand "mod")
(("" (expand "sgn")
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (lift-if)
(("" (expand "abs")
(("" (expand "integer?")
(("" (ground)
(("1"
(lift-if)
(("1" (ground) nil nil))
nil)
("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((floor_neg formula-decl nil floor_ceil nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(rem const-decl "{k | abs(k) < abs(j)}" rem nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(abs_nat_rew formula-decl nil abs_rews nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(integer? const-decl "bool" integers nil)
(sgn const-decl "int" real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(div const-decl "integer" div nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nonzero_integer nonempty-type-eq-decl nil integers 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)
(/ 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)
(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)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot
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
|
