|
(abstract_min
(prep0 0
(prep0-1 nil 3507100929
("" (lemma "T_ne")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "is_one")
(("" (inst -2 "size(t!1)")
(("" (inst 1 "t!1") (("" (assert) nil))))))))))))))))
nil)
((nonempty? const-decl "bool" sets nil)
(is_one const-decl "bool" abstract_min nil)
(size formal-const-decl "[T -> nat]" abstract_min nil)
(T formal-type-decl nil abstract_min 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)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(T_ne formula-decl nil abstract_min nil))
nil))
(min_f_TCC1 0
(min_f_TCC1-1 nil 3507100929
("" (lemma "prep0") (("" (propax) nil)) nil)
((prep0 formula-decl nil abstract_min nil)) nil))
(prep1 0
(prep1-1 nil 3507100929
("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "min_f")
(("" (typepred "min({n: nat | is_one(n)})")
(("1" (expand "is_one")
(("1" (skosimp*)
(("1" (inst -4 "S!1") (("1" (assert) nil)))))))
("2" (rewrite "prep0") nil))))))))))
nil)
((empty? const-decl "bool" sets nil)
(min_f const-decl "nat" abstract_min nil)
(prep0 formula-decl nil abstract_min nil)
(T formal-type-decl nil abstract_min 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(is_one const-decl "bool" abstract_min nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(min_TCC1 0
(min_TCC1-1 nil 3507100929
("" (lemma "prep1")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp*)
(("" (expand "member")
(("" (inst?)
(("" (expand "minimal?")
(("" (assert)
(("" (expand "min_f")
(("" (flatten)
(("" (assert)
(("" (skosimp*)
(("" (typepred "min({n: nat | is_one(n)})")
(("1" (inst -2 "size(SS!1)")
(("1"
(hide -1)
(("1"
(assert)
(("1"
(expand "is_one")
(("1"
(inst?)
(("1" (assert) nil)))))))))))
("2" (lemma "prep0")
(("2"
(propax)
nil))))))))))))))))))))))))))))
nil)
((nonempty? const-decl "bool" sets nil)
(T formal-type-decl nil abstract_min nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(minimal? const-decl "bool" abstract_min nil)
(x!1 skolem-const-decl "T" abstract_min nil)
(prep0 formula-decl nil abstract_min nil)
(size formal-const-decl "[T -> nat]" abstract_min nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(is_one const-decl "bool" abstract_min nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(min_f const-decl "nat" abstract_min nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(prep1 formula-decl nil abstract_min nil))
nil))
(min_def 0
(min_def-1 nil 3507100929
("" (typepred "min") (("" (propax) nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil abstract_min nil)
(minimal? const-decl "bool" abstract_min nil)
(min const-decl "{S: T | minimal?(S)}" abstract_min nil))
nil))
(min_in 0
(min_in-1 nil 3507100929
("" (typepred "min")
(("" (expand "minimal?") (("" (flatten) (("" (propax) nil))))))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil abstract_min nil)
(minimal? const-decl "bool" abstract_min nil)
(min const-decl "{S: T | minimal?(S)}" abstract_min nil))
nil))
(min_is_min 0
(min_is_min-1 nil 3507100929
("" (skosimp*)
(("" (typepred "min")
(("" (expand "minimal?")
(("" (flatten) (("" (inst?) (("" (assert) nil))))))))))
nil)
((min const-decl "{S: T | minimal?(S)}" abstract_min nil)
(minimal? const-decl "bool" abstract_min nil)
(T formal-type-decl nil abstract_min nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.29Angebot
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
|
