|
(real_fun_preds
(bounded?_lem 0
(bounded?_lem-3 nil 3297509203
("" (skosimp*)
(("" (prop)
(("1" (expand "bounded?")
(("1" (flatten)
(("1" (expand "abs")
(("1" (expand "bounded_above?")
(("1" (expand "bounded_below?")
(("1" (skosimp*)
(("1" (inst + "max(abs(a!1),abs(a!2))")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "max")
(("1" (lift-if)
(("1"
(inst?)
(("1"
(inst?)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (inst?)
(("2" (inst?) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded?")
(("2" (skosimp*)
(("2" (prop)
(("1" (expand "bounded_above?")
(("1" (inst + "B!1")
(("1" (skosimp*)
(("1" (inst?) (("1" (grind) nil nil)) nil)) nil))
nil))
nil)
("2" (expand "bounded_below?")
(("2" (inst + "-B!1")
(("2" (skosimp*)
(("2" (inst?) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds 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)
(minus_real_is_real application-judgement "real" reals nil)
(T_pred const-decl "[real -> boolean]" real_fun_preds nil)
(T formal-subtype-decl nil real_fun_preds nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(bounded_below? const-decl "bool" real_fun_preds nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(bounded? const-decl "bool" real_fun_preds nil))
nil)
(bounded?_lem-2 nil 3297509167
("" (skosimp*)
(("" (prop)
(("1" (expand "bounded?")
(("1" (flatten)
(("1" (expand "abs")
(("1" (expand "bounded_above?")
(("1" (expand "bounded_below?")
(("1" (skosimp*)
(("1" (inst + "max(abs(B!1),abs(a!2))")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "max")
(("1" (lift-if)
(("1"
(inst?)
(("1"
(inst?)
(("1" (grind) nil)))))))))
("2" (inst?)
(("2" (inst?)
(("2"
(grind)
nil)))))))))))))))))))))))))
("2" (expand "bounded?")
(("2" (skosimp*)
(("2" (prop)
(("1" (expand "bounded_above?")
(("1" (inst + "B!1")
(("1" (skosimp*)
(("1" (inst?) (("1" (grind) nil)))))))))
("2" (expand "bounded_below?")
(("2" (inst + "-B!1")
(("2" (skosimp*)
(("2" (inst?) (("2" (grind) nil))))))))))))))))))
nil)
nil nil)
(bounded?_lem-1 nil 3280071776
("" (skosimp*)
(("" (prop)
(("1" (expand "bounded?")
(("1" (flatten)
(("1" (expand "abs")
(("1" (expand "bounded_above?")
(("1" (expand "bounded_below?")
(("1" (skosimp*)
(("1" (inst + "max(abs(a!1),abs(a!2))")
(("1" (skosimp*)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "max")
(("1" (lift-if)
(("1"
(inst?)
(("1"
(inst?)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (inst?)
(("2" (inst?) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded?")
(("2" (skosimp*)
(("2" (prop)
(("1" (expand "bounded_above?")
(("1" (inst + "a!1")
(("1" (skosimp*)
(("1" (inst?) (("1" (grind) nil nil)) nil)) nil))
nil))
nil)
("2" (expand "bounded_below?")
(("2" (inst + "-a!1")
(("2" (skosimp*)
(("2" (inst?) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
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
|
