|
(complementary_orders
(complement_complement 0
(complement_complement-1 nil 3318701342
("" (skolem-typepred)
(("" (expand* "complement?" "o" "id")
(("" (flatten)
(("" (decompose-equality) (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(id const-decl "(bijective?[T, T])" identity nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complement? const-decl "bool" complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(image_complement 0
(image_complement-1 nil 3318701387
("" (skosimp* t)
(("" (decompose-equality)
(("" (expand "image")
(("" (iff)
(("" (prop)
(("1" (skosimp* t)
(("1" (use "complement_complement")
(("1" (assert) nil nil)) nil))
nil)
("2" (inst + "C!1(x!1)")
(("1" (rewrite "complement_complement") nil nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(image const-decl "set[R]" function_image nil)
(x!1 skolem-const-decl "T" complementary_orders nil)
(C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
nil)
(rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
(S!1 skolem-const-decl "set[T]" complementary_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complement_complement formula-decl nil complementary_orders 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-nonempty-type-decl nil complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(complement? const-decl "bool" complementary_orders nil))
shostak))
(inverse_complement 0
(inverse_complement-1 nil 3318701457
("" (skolem-typepred)
(("" (decompose-equality)
(("" (rewrite "bijective_inverse[T, T]")
(("1" (rewrite "complement_complement") nil nil)
("2" (lemma "left_inj_surj[T, T]")
(("2" (inst - "C!1" "C!1")
(("1" (expand "bijective?") (("1" (propax) nil nil)) nil)
("2" (expand* "left_inverse?" "complement?" "o" "id")
(("2" (flatten) (("2" (decompose-equality) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inverse const-decl "D" function_inverse nil)
(left_inj_surj formula-decl nil function_inverse_def nil)
(id const-decl "(bijective?[T, T])" identity nil)
(O const-decl "T3" function_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
nil)
(rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
(left_inverse? const-decl "bool" function_inverse_def nil)
(complement_complement formula-decl nil complementary_orders nil)
(bijective? const-decl "bool" functions nil)
(bijective_inverse formula-decl nil function_inverse nil)
(complement? const-decl "bool" complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(le_complement 0
(le_complement-1 nil 3318701551
("" (skolem-typepred)
(("" (prop)
(("1" (expand* "complement?" "preserves" "converse")
(("1" (flatten)
(("1" (inst - "C!1(t1!1)" "C!1(t2!1)")
(("1" (assert)
(("1" (rewrite "complement_complement")
(("1" (rewrite "complement_complement") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand* "complement?" "preserves" "converse")
(("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((complement_complement formula-decl nil complementary_orders nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(preserves const-decl "bool" functions nil)
(complement? const-decl "bool" complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(upper_bound_complement 0
(upper_bound_complement-1 nil 3318701679
("" (skolem!)
(("" (prop)
(("1" (expand* "lower_bound?" "upper_bound?")
(("1" (skolem-typepred)
(("1" (inst - "C!1(r!1)")
(("1" (use "le_complement" ("t2" "C!1(t!1)"))
(("1" (assert)
(("1" (rewrite "complement_complement") nil nil)) nil))
nil)
("2" (expand "image")
(("2" (skolem-typepred)
(("2" (use "complement_complement" ("t" "x!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "lower_bound?" "upper_bound?")
(("2" (skolem-typepred)
(("2" (inst - "C!1(r!1)")
(("1" (rewrite "le_complement") nil nil)
("2" (expand "image") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
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-nonempty-type-decl nil complementary_orders nil)
(set type-eq-decl nil sets nil)
(image const-decl "set[R]" function_image nil)
(pred type-eq-decl nil defined_types nil)
(complement? const-decl "bool" complementary_orders nil)
(le_complement formula-decl nil complementary_orders nil)
(complement_complement formula-decl nil complementary_orders nil)
(S!1 skolem-const-decl "set[T]" complementary_orders nil)
(rel!1 skolem-const-decl "pred[[T, T]]" complementary_orders nil)
(C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
nil)
(r!1 skolem-const-decl "(image(C!1, S!1))" complementary_orders
nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(r!1 skolem-const-decl "(S!1)" complementary_orders nil))
shostak))
(bounded_above_complement 0
(bounded_above_complement-1 nil 3318701876
("" (skolem!)
(("" (expand* "bounded_above?" "bounded_below?")
(("" (prop)
(("1" (skolem!)
(("1" (inst + "C!1(t!1)")
(("1" (use "upper_bound_complement")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skolem!)
(("2" (inst + "C!1(t!1)")
(("2" (use "upper_bound_complement")
(("2" (rewrite "complement_complement")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" bounded_orders nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(complement_complement formula-decl nil complementary_orders nil)
(upper_bound_complement formula-decl nil complementary_orders nil)
(set type-eq-decl nil sets nil)
(complement? const-decl "bool" complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil complementary_orders nil))
shostak))
(least_upper_bound_complement 0
(least_upper_bound_complement-1 nil 3318701959
("" (skolem!)
(("" (expand* "least_upper_bound?" "greatest_lower_bound?")
(("" (prop)
(("1" (use "upper_bound_complement") (("1" (assert) nil nil))
nil)
("2" (skosimp)
(("2" (hide -2)
(("2" (inst - "C!1(r!1)")
(("2" (use "upper_bound_complement")
(("2" (rewrite "complement_complement")
(("2" (assert)
(("2"
(use "le_complement"
("t1" "C!1(r!1)" "t2" "t!1"))
(("2" (assert)
(("2" (rewrite "complement_complement") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (use "upper_bound_complement") (("3" (assert) nil nil))
nil)
("4" (skosimp)
(("4" (hide -2)
(("4" (inst - "C!1(r!1)")
(("4" (use "upper_bound_complement")
(("4" (assert)
(("4" (rewrite "le_complement") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((greatest_lower_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(complement_complement formula-decl nil complementary_orders nil)
(le_complement formula-decl nil complementary_orders nil)
(upper_bound_complement formula-decl nil complementary_orders nil)
(complement? const-decl "bool" complementary_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil complementary_orders nil))
shostak))
(least_bounded_above_complement 0
(least_bounded_above_complement-1 nil 3318702440
("" (skolem!)
(("" (expand* "least_bounded_above?" "greatest_bounded_below?")
(("" (prop)
(("1" (skolem!)
(("1" (use "least_upper_bound_complement")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (skolem!)
(("2" (inst + "C!1(t!1)")
(("2" (use "least_upper_bound_complement")
(("2" (rewrite "complement_complement")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((greatest_bounded_below? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(complement_complement formula-decl nil complementary_orders nil)
(complement? const-decl "bool" complementary_orders nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound_complement formula-decl nil complementary_orders
nil))
shostak))
(lub_complement_TCC1 0
(lub_complement_TCC1-1 nil 3318701312
("" (skolem!)
(("" (use "least_bounded_above_complement") (("" (assert) nil nil))
nil))
nil)
((least_bounded_above_complement formula-decl nil
complementary_orders nil)
(complement? const-decl "bool" complementary_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil complementary_orders nil))
nil))
(lub_complement 0
(lub_complement-1 nil 3318702643
("" (skolem!)
(("" (invoke (name-replace "T" "%1" :hide? nil) (! 1 r 1))
(("" (use "unique_least_upper_bound")
(("" (rewrite "glb_def")
(("" (use "least_upper_bound_complement")
(("" (rewrite "complement_complement")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((least_bounded_above? const-decl "bool" bounded_orders nil)
(complement? const-decl "bool" complementary_orders nil)
(image const-decl "set[R]" function_image nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(glb_def formula-decl nil bounded_orders nil)
(complement_complement formula-decl nil complementary_orders nil)
(least_upper_bound_complement formula-decl nil complementary_orders
nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(T skolem-const-decl
"(LAMBDA (t: T): greatest_lower_bound?(t, image(C!1, S!1), rel!1))"
complementary_orders nil)
(S!1 skolem-const-decl
"(LAMBDA (S: set[T]): least_bounded_above?(S, rel!1))"
complementary_orders nil)
(C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
nil)
(rel!1 skolem-const-decl "(antisymmetric?[T])" complementary_orders
nil)
(unique_least_upper_bound formula-decl nil bounded_orders nil))
shostak))
(glb_complement_TCC1 0
(glb_complement_TCC1-1 nil 3318701312
("" (skolem!)
((""
(use "least_bounded_above_complement"
("S" "image[T, T](C!1, S!1)"))
(("" (rewrite "image_complement") (("" (assert) nil nil)) nil))
nil))
nil)
((least_bounded_above_complement formula-decl nil
complementary_orders nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(image const-decl "set[R]" function_image nil)
(pred type-eq-decl nil defined_types nil)
(complement? const-decl "bool" complementary_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(image_complement formula-decl nil complementary_orders nil))
nil))
(glb_complement 0
(glb_complement-1 nil 3318702699
("" (skolem!)
(("" (invoke (name-replace "T" "%1" :hide? nil) (! 1 r 1))
(("" (use "unique_greatest_lower_bound")
(("" (rewrite "lub_def")
(("" (use "least_upper_bound_complement")
(("" (rewrite "image_complement") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((greatest_bounded_below? const-decl "bool" bounded_orders nil)
(complement? const-decl "bool" complementary_orders nil)
(image const-decl "set[R]" function_image nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil complementary_orders nil)
(lub_def formula-decl nil bounded_orders nil)
(image_complement formula-decl nil complementary_orders nil)
(least_upper_bound_complement formula-decl nil complementary_orders
nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(T skolem-const-decl
"(LAMBDA (t: T): least_upper_bound?(t, image(C!1, S!1), rel!1))"
complementary_orders nil)
(S!1 skolem-const-decl
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, rel!1))"
complementary_orders nil)
(C!1 skolem-const-decl "(complement?(rel!1))" complementary_orders
nil)
(rel!1 skolem-const-decl "(antisymmetric?[T])" complementary_orders
nil)
(unique_greatest_lower_bound formula-decl nil bounded_orders nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.38Angebot
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
|
