|
(function_image_bis
(image_emptyset 0
(image_emptyset-1 nil 3358818238
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "emptyset")
(("" (expand "image") (("" (skosimp) nil nil)) nil)) nil))
nil))
nil)
((R formal-type-decl nil function_image_bis nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset const-decl "set" sets nil)
(image const-decl "set[R]" function_image nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(D formal-type-decl nil function_image_bis nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(inverse_image_emptyset 0
(inverse_image_emptyset-1 nil 3358818259
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "emptyset")
(("" (expand "inverse_image")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D formal-type-decl nil function_image_bis nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset const-decl "set" sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(R formal-type-decl nil function_image_bis nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(member const-decl "bool" sets nil))
shostak))
(surjective_image_inverse_image 0
(surjective_image_inverse_image-1 nil 3358755254
("" (skosimp)
(("" (expand "inverse_image")
(("" (expand "member")
(("" (expand "image")
(("" (apply-extensionality 1 :hide? t)
(("" (case-replace "Y!1(x!1)")
(("1" (typepred "surj!1")
(("1" (case "EXISTS (x:D): TRUE")
(("1"
(lemma "comp_inverse_right_surj[D,R]"
("f" "surj!1"))
(("1" (inst - "x!1")
(("1" (inst + "inverse(surj!1)(x!1)")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (expand "surjective?")
(("2" (inst - "x!1")
(("2" (skosimp) (("2" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inverse_image const-decl "set[D]" function_image nil)
(image const-decl "set[R]" function_image nil)
(TRUE const-decl "bool" booleans nil)
(x!1 skolem-const-decl "R" function_image_bis nil)
(inverse const-decl "D" function_inverse nil)
(surj!1 skolem-const-decl "(surjective?[D, R])" function_image_bis
nil)
(Y!1 skolem-const-decl "set[R]" function_image_bis nil)
(inv_surj_is_inj application-judgement "(injective?[R, D])"
function_inverse nil)
(comp_inverse_right_surj formula-decl nil function_inverse nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(D formal-type-decl nil function_image_bis nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(surjective? const-decl "bool" functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(R formal-type-decl nil function_image_bis nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil))
shostak))
(injective_inverse_image_image 0
(injective_inverse_image_image-1 nil 3358755174
("" (skosimp)
(("" (typepred "inj!1")
(("" (expand "image")
(("" (expand "inverse_image")
(("" (expand "member")
(("" (apply-extensionality 1 :hide? t)
(("" (case-replace "X!1(x!1)")
(("1" (inst + "x!1") nil nil)
("2" (assert)
(("2" (skosimp)
(("2" (typepred "x!2")
(("2" (expand "injective?")
(("2" (inst - "x!1" "x!2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((injective? const-decl "bool" functions nil)
(R formal-type-decl nil function_image_bis nil)
(D formal-type-decl nil function_image_bis nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inverse_image const-decl "set[D]" function_image nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(X!1 skolem-const-decl "set[D]" function_image_bis nil)
(x!1 skolem-const-decl "D" function_image_bis nil)
(member const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil))
shostak))
(bijective_image_iff_inverse_image 0
(bijective_image_iff_inverse_image-1 nil 3358764413
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (replace -1 1 rl)
(("1" (rewrite "injective_inverse_image_image") nil nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1 1 rl)
(("2" (rewrite "surjective_image_inverse_image") nil nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(R formal-type-decl nil function_image_bis nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(D formal-type-decl nil function_image_bis nil)
(injective_inverse_image_image formula-decl nil function_image_bis
nil)
(surjective? const-decl "bool" functions nil)
(surjective_image_inverse_image formula-decl nil function_image_bis
nil))
shostak))
(bijective_image_inverse_alt_TCC1 0
(bijective_image_inverse_alt_TCC1-1 nil 3358764794
("" (expand "empty?")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "bij!1")
(("" (expand "bijective?")
(("" (flatten)
(("" (expand "surjective?")
(("" (inst - "x!1")
(("" (skosimp) (("" (inst + "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(bijective? const-decl "bool" functions nil)
(R formal-type-decl nil function_image_bis nil)
(D formal-type-decl nil function_image_bis nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(surjective? const-decl "bool" functions nil)
(empty? const-decl "bool" sets nil))
nil))
(bijective_image_inverse_alt 0
(bijective_image_inverse_alt-1 nil 3358765036
("" (skosimp*)
(("" (case-replace "empty?(Y!1)")
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "emptyset")
(("1" (expand "inverse_image")
(("1" (expand "member")
(("1" (expand "empty?")
(("1" (inst - "bij!1(x!1)")
(("1" (expand "member") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (apply-extensionality 2 :hide? t)
(("1" (expand "image")
(("1" (expand "inverse_image")
(("1" (expand "member")
(("1" (case-replace "Y!1(bij!1(x!1))")
(("1" (inst + "bij!1(x!1)")
(("1" (typepred "bij!1")
(("1"
(lemma
"bijective_inverse_alt_is_bijective[D,R]"
("f" "bij!1"))
(("1" (typepred "inverse_alt(bij!1)")
(("1" (expand "inverse?")
(("1" (inst - "bij!1(x!1)")
(("1"
(split -1)
(("1"
(expand "bijective?" -4)
(("1"
(flatten)
(("1"
(expand "injective?")
(("1"
(inst
-
"x!1"
"inverse_alt(bij!1)(bij!1(x!1))")
(("1" (assert) nil nil)
("2"
(flatten)
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil)
("2" (flatten) (("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (skosimp)
(("2" (expand "empty?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (case "bij!1(x!1)=x!2")
(("1" (assert) nil nil)
("2"
(hide 2 -2)
(("2"
(typepred "bij!1")
(("2"
(lemma
"unique_bijective_inverse_alt[D,R]"
("f" "bij!1" "r" "x!2"))
(("1" (assert) nil nil)
("2"
(flatten)
(("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "empty?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (skosimp)
(("2" (typepred "bij!1")
(("2" (expand "bijective?")
(("2" (flatten)
(("2" (expand "surjective?")
(("2" (inst - "x!1")
(("2"
(skosimp)
(("2" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((R formal-type-decl nil function_image_bis nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(bijective? const-decl "bool" functions nil)
(emptyset const-decl "set" sets nil)
(D formal-type-decl nil function_image_bis nil)
(inverse_alt const-decl "inverses(f)" function_inverse_alt nil)
(inverses nonempty-type-eq-decl nil function_inverse_alt nil)
(inverse? const-decl "bool" function_inverse_def nil)
(image const-decl "set[R]" function_image nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(TRUE const-decl "bool" booleans nil)
(FALSE const-decl "bool" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(unique_bijective_inverse_alt application-judgement
"{d | f(d) = r}" function_inverse_alt nil)
(bijective_inverse_alt_is_bijective judgement-tcc nil
function_inverse_alt nil)
(x!1 skolem-const-decl "D" function_image_bis nil)
(bij!1 skolem-const-decl "(bijective?[D, R])" function_image_bis
nil)
(Y!1 skolem-const-decl "set[R]" function_image_bis nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(unique_bijective_inverse_alt judgement-tcc nil
function_inverse_alt nil)
(surjective? const-decl "bool" functions nil)
(bijective_inverse_alt_is_bijective application-judgement
"(bijective?[R, D])" function_inverse_alt nil))
shostak)))
¤ Dauer der Verarbeitung: 0.6 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.
|
