|
(isomorphism_equivalence
(isomorphism_reflexive 0
(isomorphism_reflexive-1 nil 3315072687
("" (grind)
(("" (inst + "identity[T]")
(("" (expand "identity") (("" (propax) nil nil)) nil)) nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(identity const-decl "(bijective?[T, T])" identity nil)
(reflexive? const-decl "bool" relations nil)
(isomorphic? const-decl "bool" isomorphism nil)
(isomorphism? const-decl "bool" isomorphism nil)
(T formal-type-decl nil isomorphism_equivalence nil))
shostak))
(isomorphism_symmetric 0
(isomorphism_symmetric-1 nil 3315072724
("" (expand* "isomorphic?" "isomorphism?" "symmetric?")
(("" (skosimp* t)
(("" (use "bijective_inverse_exists")
(("" (expand "exists1")
(("" (skosimp*)
(("" (assert)
(("" (lemma "bij_inv_is_bij_alt" ("f" "f!1" "g" "x!2"))
(("" (inst + "x!2")
(("" (skolem!)
(("" (inst - "x!2(d1!1)" "x!2(d2!1)")
(("" (expand "inverse?")
(("" (inst-cp - "d2!1")
(("" (inst - "d1!1")
(("" (split)
(("1"
(split)
(("1" (ground) nil nil)
("2"
(expand* "bijective?" "surjective?")
(("2"
(flatten)
(("2" (inst -6 "d2!1") nil nil))
nil))
nil))
nil)
("2"
(expand* "bijective?" "surjective?")
(("2"
(flatten)
(("2" (inst -6 "d1!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(T formal-type-decl nil isomorphism_equivalence nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(exists1 const-decl "bool" exists1 nil)
(x!2 skolem-const-decl "[T -> T]" isomorphism_equivalence nil)
(surjective? const-decl "bool" functions nil)
(inverse? const-decl "bool" function_inverse_def nil)
(bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(isomorphic? const-decl "bool" isomorphism nil)
(symmetric? const-decl "bool" relations nil)
(isomorphism? const-decl "bool" isomorphism nil))
shostak))
(isomorphism_transitive 0
(isomorphism_transitive-1 nil 3315072868
("" (expand* "isomorphic?" "isomorphism?" "transitive?")
(("" (skosimp*)
(("" (inst + "f!2 o f!1")
(("" (skolem!)
(("" (inst?)
(("" (inst?) (("" (expand "o") (("" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil isomorphism_equivalence nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(O const-decl "T3" function_props nil)
(composition_bijective application-judgement "(bijective?[T1, T3])"
function_props nil)
(composition_surjective application-judgement
"(surjective?[T1, T3])" function_props nil)
(composition_injective application-judgement "(injective?[T1, T3])"
function_props nil)
(isomorphic? const-decl "bool" isomorphism nil)
(transitive? const-decl "bool" relations nil)
(isomorphism? const-decl "bool" isomorphism nil))
shostak))
(isomorphism_equivalence 0
(isomorphism_equivalence-1 nil 3315072679
("" (expand "equivalence?")
(("" (lemma "isomorphism_reflexive")
(("" (lemma "isomorphism_symmetric")
(("" (lemma "isomorphism_transitive") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((isomorphism_reflexive formula-decl nil isomorphism_equivalence
nil)
(isomorphism_transitive formula-decl nil isomorphism_equivalence
nil)
(isomorphism_symmetric formula-decl nil isomorphism_equivalence
nil)
(equivalence? const-decl "bool" relations nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.40Angebot
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
|
