|
(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)))
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
