|
(function_props_aux
(inverse_image_composition 0
(inverse_image_composition-1 nil 3449912055
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "inverse_image")
(("" (expand "o ")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((T1 formal-type-decl nil function_props_aux nil)
(boolean nonempty-type-decl nil booleans nil)
(O const-decl "T3" function_props nil)
(T3 formal-type-decl nil function_props_aux 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)
(T2 formal-type-decl nil function_props_aux nil)
(member const-decl "bool" sets nil))
shostak))
(composition_inverse_alt_TCC1 0
(composition_inverse_alt_TCC1-1 nil 3301539767
("" (skosimp)
(("" (typepred "f1!1")
(("" (typepred "f2!1")
(("" (expand "bijective?")
(("" (flatten)
(("" (expand "surjective?")
(("" (skosimp*)
(("" (inst - "r!1")
(("" (skosimp)
(("" (inst - "x!1")
(("" (skosimp) (("" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(T2 formal-type-decl nil function_props_aux nil)
(T1 formal-type-decl nil function_props_aux 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)
(T3 formal-type-decl nil function_props_aux nil))
shostak))
(composition_inverse_alt_TCC2 0
(composition_inverse_alt_TCC2-1 nil 3301539767
("" (skosimp*)
(("" (typepred "f1!1")
(("" (expand "bijective?")
(("" (expand "surjective?")
(("" (flatten)
(("" (inst - "r!1")
(("" (skosimp) (("" (inst + "x!1") nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(T2 formal-type-decl nil function_props_aux nil)
(T1 formal-type-decl nil function_props_aux 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))
shostak))
(composition_inverse_alt_TCC3 0
(composition_inverse_alt_TCC3-1 nil 3301539767
("" (skosimp)
(("" (typepred "f2!1")
(("" (expand "bijective?")
(("" (expand "surjective?")
(("" (flatten)
(("" (skosimp)
(("" (inst - "r!1")
(("" (skosimp) (("" (inst + "x!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(T3 formal-type-decl nil function_props_aux nil)
(T2 formal-type-decl nil function_props_aux 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))
shostak))
(composition_inverse_alt 0
(composition_inverse_alt-1 nil 3301540008
("" (skosimp)
(("" (typepred "f1!1")
(("" (typepred "f2!1")
(("" (apply-extensionality :hide? t)
(("1"
(lemma "composition_bijective[T1,T2,T3]"
("f1" "f1!1" "f2" "f2!1"))
(("1"
(lemma "unique_bijective_inverse_alt[T1,T3]"
("f" "f2!1 o f1!1" "r" "x!1"))
(("1"
(lemma "unique_bijective_inverse_alt[T2,T3]"
("f" "f2!1" "r" "x!1"))
(("1"
(lemma "unique_bijective_inverse_alt[T1,T2]"
("f" "f1!1" "r" "inverse_alt(f2!1)(x!1)"))
(("1" (expand "o" 1 2)
(("1" (expand "bijective?")
(("1" (flatten)
(("1" (expand "injective?")
(("1"
(inst - "inverse_alt(f2!1 o f1!1)(x!1)"
"inverse_alt(f1!1)(inverse_alt(f2!1)(x!1))")
(("1" (split -4)
(("1" (propax) nil nil)
("2"
(replace -3)
(("2"
(expand "o" 1)
(("2"
(replace -1)
(("2"
(replace -2)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-8 1))
(("2"
(expand "surjective?")
(("2"
(flatten)
(("2"
(skosimp)
(("2"
(inst - "r!1")
(("2"
(skosimp)
(("2" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but (1 -6))
(("3"
(expand "surjective?")
(("3"
(skosimp*)
(("3"
(inst - "r!1")
(("3"
(skosimp)
(("3" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide-all-but (-4 1))
(("4"
(expand "surjective?")
(("4"
(skosimp*)
(("4"
(inst - "r!1")
(("4"
(skosimp)
(("4" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 1))
(("2" (expand "bijective?")
(("2" (expand "surjective?")
(("2" (flatten)
(("2" (skosimp)
(("2" (inst - "r!1")
(("2"
(skosimp)
(("2" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-3 1))
(("2" (expand "bijective?")
(("2" (expand "surjective?")
(("2" (flatten)
(("2" (skosimp)
(("2" (inst - "r!1")
(("2" (skosimp)
(("2" (inst + "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (expand "bijective?")
(("2" (expand "surjective?")
(("2" (flatten)
(("2" (skosimp)
(("2" (inst - "r!1")
(("2" (skosimp)
(("2" (inst + "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (expand "bijective?")
(("2" (expand "surjective?")
(("2" (flatten)
(("2" (skosimp)
(("2" (inst - "r!1")
(("2" (skosimp) (("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide -1)
(("3" (expand "bijective?")
(("3" (expand "surjective?")
(("3" (flatten)
(("3" (skosimp)
(("3" (inst - "r!1")
(("3" (skosimp) (("3" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "bijective?")
(("4" (expand "surjective?")
(("4" (flatten)
(("4" (skosimp)
(("4" (inst - "r!1")
(("4" (skosimp)
(("4" (inst - "x!1")
(("4" (skosimp) (("4" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(T2 formal-type-decl nil function_props_aux nil)
(T1 formal-type-decl nil function_props_aux nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(O const-decl "T3" function_props 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)
(unique_bijective_inverse_alt application-judgement
"{d | f(d) = r}" function_inverse_alt nil)
(bijective_inverse_alt_is_bijective application-judgement
"(bijective?[R, D])" function_inverse_alt 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)
(unique_bijective_inverse_alt judgement-tcc nil
function_inverse_alt nil)
(injective? const-decl "bool" functions nil)
(composition_bijective judgement-tcc nil function_props nil)
(T3 formal-type-decl nil function_props_aux nil))
shostak)))
¤ Dauer der Verarbeitung: 0.28 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.
|
