|
(relation_inverse_image
(equivClass_is_nonempty 0
(equivClass_is_nonempty-1 nil 3570861010
("" (skolem!)
(("" (flatten)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "member")
(("" (expand "equivClass")
(("" (expand "equivalence?")
(("" (prop)
(("" (expand "reflexive?")
(("" (expand "equivClass")
(("" (expand "image_inverse")
(("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(equivalence? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(equivClass const-decl "pred[T]" relation_inverse_image nil)
(equivClass const-decl "pred[T]" relation_inverse_image nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(nonempty? const-decl "bool" sets nil))
shostak))
(equivClass_equal_is_nonempty 0
(equivClass_equal_is_nonempty-1 nil 3570861063
("" (skolem!)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "member")
(("" (expand "equivClass")
(("" (expand "equivClass")
(("" (expand "image_inverse") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(equivClass const-decl "pred[T]" relation_inverse_image nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(equivClass const-decl "pred[T]" relation_inverse_image nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil))
shostak))
(inverse_image_of_equivalence 0
(inverse_image_of_equivalence-1 nil 3570452661
("" (skolem!)
(("" (prop)
(("" (expand "equivalence?")
(("" (prop)
(("1" (expand "image_inverse")
(("1" (expand "reflexive?")
(("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (expand "image_inverse")
(("2" (inst -2 "f!1(x!1)" "f!1(y!1)") nil nil)) nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (expand "image_inverse") (("3" (inst? -3) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((reflexive? const-decl "bool" relations nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(equivalence? const-decl "bool" relations nil))
shostak))
(preserves_eqv_of_inv_image 0
(preserves_eqv_of_inv_image-1 nil 3570657993
("" (skolem!)
(("" (inst 1 "=")
(("" (expand "equivalence?")
(("" (prop)
(("1" (expand "reflexive?")
(("1" (skolem!)
(("1" (expand "image_inverse") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (flatten)
(("2" (expand "image_inverse")
(("2" (replace -1 1 :dir rl) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (prop)
(("3" (expand "image_inverse")
(("3" (replace -2 1 rl) (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((U formal-nonempty-type-decl nil relation_inverse_image nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(reflexive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(equivalence? const-decl "bool" relations nil))
shostak))
(inverse_image_of_equality 0
(inverse_image_of_equality-1 nil 3570452710
("" (skolem!)
(("" (expand "equivalence?")
(("" (prop)
(("1" (expand "reflexive?")
(("1" (skolem!)
(("1" (expand "image_inverse") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (prop)
(("2" (expand "image_inverse")
(("2" (replace -1 1 :dir rl) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (prop)
(("3" (expand "image_inverse")
(("3" (replace -2 1 :dir rl) (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil))
shostak))
(image_inverse_eq_is_eq_kernel 0
(image_inverse_eq_is_eq_kernel-1 nil 3570525503
("" (skolem!)
(("" (apply-extensionality :hide? t)
(("" (iff)
(("" (prop)
(("1" (expand "EquivalenceKernel")
(("1" (expand "image_inverse")
(("1" (expand "image_inverse") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "image_inverse")
(("2" (expand "EquivalenceKernel")
(("2" (expand "image_inverse") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil relation_inverse_image nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(pred type-eq-decl nil defined_types nil)
(EquivalenceKernel const-decl "equivalence[X1]" KernelDefinition
nil)
(equivalence type-eq-decl nil relations nil)
(equivalence? const-decl "bool" relations nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil))
shostak))
(inv_img_surj_impl_codom_eq 0
(inv_img_surj_impl_codom_eq-1 nil 3570458696
("" (skolem-typepred)
(("" (skolem!)
(("" (flatten)
(("" (expand "surjective?")
(("" (expand "equivalence?")
(("" (prop)
(("1" (expand "reflexive?")
(("1" (skolem!)
(("1" (inst?)
(("1" (skolem!)
(("1" (inst?)
(("1" (expand "image_inverse")
(("1" (replace -1 1 rl)
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (inst-cp -1 "x!1")
(("2" (inst -1 "y!1")
(("2" (skolem!)
(("2" (skolem!)
(("2" (replace -1 1 rl)
(("2" (replace -2 1 rl)
(("2"
(inst -4 "x!3" "x!2")
(("2"
(expand "image_inverse")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (inst-cp -1 "x!1")
(("3" (inst-cp -1 "y!1")
(("3" (inst -1 "z!1")
(("3" (skolem!)
(("3" (skolem!)
(("3" (skolem!)
(("3"
(replace -1 1 rl)
(("3"
(replace -2 1 rl)
(("3"
(replace -3 1 rl)
(("3"
(inst -6 "x!4" "x!3" "x!2")
(("3"
(expand "image_inverse")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(surjective? const-decl "bool" functions nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(right_inv_inv_finv_image_impl_codom_eq 0
(right_inv_inv_finv_image_impl_codom_eq-1 nil 3570899897
("" (skolem!)
(("" (prop)
(("" (expand "equivalence?")
(("" (prop)
(("1" (expand "reflexive?")
(("1" (skolem!)
(("1" (expand "right_inverse?")
(("1" (inst?)
(("1" (expand "image_inverse")
(("1" (replace -1 1 rl) (("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (expand "right_inverse?")
(("2" (inst-cp -1 "x!1")
(("2" (inst -1 "y!1")
(("2" (replace -1 1 rl)
(("2" (replace -2 1 rl)
(("2" (expand "image_inverse")
(("2" (expand "inverse")
(("2"
(inst -4
"(epsilon! (x: T): f!1(x) = x!1)"
"(epsilon! (x: T): f!1(x) = y!1)")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (expand "right_inverse?")
(("3" (inst-cp -1 "x!1")
(("3" (inst-cp -1 "y!1")
(("3" (inst -1 "z!1")
(("3" (replace -1 1 rl)
(("3" (replace -2 1 rl)
(("3" (replace -3 1 rl)
(("3" (expand "image_inverse")
(("3"
(expand "inverse")
(("3"
(inst
-6
"(epsilon! (x: T): f!1(x) = x!1)"
"(epsilon! (x: T): f!1(x) = y!1)"
"(epsilon! (x: T): f!1(x) = z!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((U formal-nonempty-type-decl nil relation_inverse_image nil)
(inverse const-decl "D" function_inverse nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(right_inverse? const-decl "bool" function_inverse_def nil)
(reflexive? const-decl "bool" relations nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(epsilon const-decl "T" epsilons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(equivalence? const-decl "bool" relations nil))
shostak))
(surjective_eqv_image_inv_rel_codomain 0
(surjective_eqv_image_inv_rel_codomain-1 nil 3570659487
("" (skolem-typepred)
(("" (iff)
(("" (split)
(("1" (use "inv_img_surj_impl_codom_eq")
(("1" (prop)
(("1" (expand "image_inverse")
(("1" (expand "image_inverse") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (use "inverse_image_of_equivalence")
(("2" (prop)
(("2" (expand "image_inverse")
(("2" (expand "image_inverse") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inverse_image_of_equivalence formula-decl nil
relation_inverse_image nil)
(inv_img_surj_impl_codom_eq formula-decl nil relation_inverse_image
nil)
(pred type-eq-decl nil defined_types nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(surjective? const-decl "bool" functions nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(right_inv_inv_finv_image_eq_codom_eq 0
(right_inv_inv_finv_image_eq_codom_eq-1 nil 3570901557
("" (skolem!)
(("" (flatten)
(("" (iff)
(("" (prop)
(("1" (use " inv_img_surj_impl_codom_eq")
(("1" (prop) nil nil)
("2" (expand "surjective?")
(("2" (expand "right_inverse?")
(("2" (skolem!)
(("2" (inst? -2)
(("2" (inst 1 "inverse(f!1)(y!1)") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "equivalence?")
(("2" (prop)
(("1" (expand "reflexive?")
(("1" (skolem!)
(("1" (expand "image_inverse")
(("1" (inst?) nil nil)) nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skolem!)
(("2" (expand "image_inverse")
(("2" (inst -2 "f!1(x!1)" "f!1(y!1)") nil nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skolem!)
(("3" (expand "image_inverse")
(("3" (inst -3 "f!1(x!1)" "f!1(y!1)" "f!1(z!1)")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inverse const-decl "D" function_inverse nil)
(right_inverse? const-decl "bool" function_inverse_def nil)
(f!1 skolem-const-decl "[T -> U]" relation_inverse_image nil)
(surjective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U formal-nonempty-type-decl nil relation_inverse_image nil)
(T formal-nonempty-type-decl nil relation_inverse_image nil)
(pred type-eq-decl nil defined_types nil)
(inv_img_surj_impl_codom_eq formula-decl nil relation_inverse_image
nil)
(image_inverse const-decl "pred[[T, T]]" relation_inverse_image
nil)
(reflexive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(equivalence? const-decl "bool" relations nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.44Angebot
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
|
