|
(set_antisymmetric
(inj_inj_bij 0
(inj_inj_bij-1 nil 3315050511
("" (skosimp*)
((""
(inst +
"LAMBDA (d: D): IF in_closure(f!1, f!2, d) THEN f!1(d) ELSE inverse_alt(f!2)(d) ENDIF")
(("1" (expand "bijective?")
(("1" (split)
(("1" (expand "injective?")
(("1" (skosimp)
(("1" (lift-if)
(("1" (lift-if)
(("1" (lift-if)
(("1" (prop)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil nil)) nil)
("2" (expand "in_closure" +)
(("2" (flatten)
(("2" (inst + "x1!1")
(("2" (assert)
(("2"
(expand*
"image"
"complement"
"difference"
"member")
(("2"
(skolem!)
(("2"
(replace -1)
(("2"
(typepred
"inverse_alt[R, D](f!2)")
(("1"
(expand "inverse?")
(("1"
(inst - "x2!1")
(("1"
(assert)
(("1"
(inst + "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "in_closure" +)
(("3" (flatten)
(("3" (inst + "x2!1")
(("3" (assert)
(("3"
(expand*
"image"
"complement"
"difference"
"member")
(("3"
(skosimp*)
(("3"
(replace -3)
(("3"
(replace -2 :dir rl)
(("3"
(typepred
"inverse_alt[R, D](f!2)")
(("1"
(expand "inverse?")
(("1"
(inst - "f!2(x!1)")
(("1"
(assert)
(("1"
(inst + "x!1")
nil
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(expand* "in_closure" "image" "complement"
"difference" "member")
(("4" (skosimp*)
(("4" (replace -1)
(("4" (replace -3)
(("4"
(typepred "inverse_alt[R, D](f!2)")
(("1"
(expand "inverse?")
(("1"
(inst-cp - "f!2(x!2)")
(("1"
(inst - "f!2(x!1)")
(("1"
(ground)
(("1" (inst + "x!2") nil nil)
("2" (inst + "x!1") nil nil)
("3" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skolem!)
(("2" (case "in_closure(f!1, f!2, f!2(y!1))")
(("1" (expand "in_closure" -)
(("1" (split)
(("1"
(expand* "fullset" "image" "complement"
"difference" "member")
(("1" (inst + "y!1") nil nil)) nil)
("2" (skosimp)
(("2" (inst + "e!1")
(("2" (assert)
(("2" (expand "injective?")
(("2" (inst -4 "f!1(e!1)" "y!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "f!2(y!1)")
(("2" (assert)
(("2" (typepred "inverse_alt[R, D](f!2)")
(("1" (expand "inverse?")
(("1" (inst - "f!2(y!1)")
(("1" (split)
(("1" (expand "injective?")
(("1"
(inst
-3
"inverse_alt(f!2)(f!2(y!1))"
"y!1")
(("1" (assert) nil nil)
("2"
(flatten)
(("2" (inst?) nil nil))
nil))
nil))
nil)
("2" (inst + "y!1") nil nil))
nil))
nil))
nil)
("2" (flatten) (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) (("2" (inst + "f!1(d!1)") nil nil)) nil))
nil))
nil)
((FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(f!2 skolem-const-decl "[R -> D]" set_antisymmetric nil)
(f!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
(in_closure inductive-decl "bool" set_antisymmetric nil)
(R formal-type-decl nil set_antisymmetric nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(D formal-type-decl nil set_antisymmetric nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(inverse? const-decl "bool" function_inverse_def nil)
(inverses nonempty-type-eq-decl nil function_inverse_alt nil)
(inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(image const-decl "set[R]" function_image nil)
(member const-decl "bool" sets nil)
(complement const-decl "set" sets nil)
(injective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(bijective? const-decl "bool" functions nil))
shostak))
(surj_surj_bij 0
(surj_surj_bij-1 nil 3315051063
("" (skosimp*)
(("" (lemma "inj_inj_bij")
(("" (prop)
(("1" (use "surjective_inverse_exists[R, D]")
(("1" (skolem!)
(("1" (use "inj_inv_alt[R, D]") (("1" (inst?) nil nil))
nil))
nil))
nil)
("2" (use "surjective_inverse_exists[D, R]")
(("2" (skolem!)
(("2" (use "inj_inv_alt[D, R]") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inj_inj_bij formula-decl nil set_antisymmetric nil)
(f!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
(g!1 skolem-const-decl "[R -> D]" set_antisymmetric nil)
(surjective_inverse_exists formula-decl nil function_inverse_def
nil)
(R formal-type-decl nil set_antisymmetric nil)
(D formal-type-decl nil set_antisymmetric nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(surjective? const-decl "bool" functions nil)
(f!2 skolem-const-decl "[R -> D]" set_antisymmetric nil)
(inj_inv_alt formula-decl nil function_inverse_def nil)
(g!1 skolem-const-decl "[D -> R]" set_antisymmetric nil)
(inverse? const-decl "bool" function_inverse_def nil))
shostak))
(inj_surj_bij 0
(inj_surj_bij-1 nil 3315051117
("" (skosimp*)
(("" (lemma "inj_inj_bij")
(("" (prop)
(("1" (inst?) nil nil)
("2" (assert)
(("2" (lemma "surjective_inverse_exists[D, R]" ("f" "f!2"))
(("2" (skolem!)
(("2" (use "inj_inv_alt[D, R]") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inj_inj_bij formula-decl nil set_antisymmetric nil)
(inverse? const-decl "bool" function_inverse_def nil)
(g!1 skolem-const-decl "[R -> D]" set_antisymmetric nil)
(f!2 skolem-const-decl "[D -> R]" set_antisymmetric nil)
(inj_inv_alt formula-decl nil function_inverse_def nil)
(surjective_inverse_exists formula-decl nil function_inverse_def
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(surjective? const-decl "bool" functions nil)
(R formal-type-decl nil set_antisymmetric nil)
(D formal-type-decl nil set_antisymmetric nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.5Angebot
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
|
