(function_inverse_alt_auxnil 3301319377"" (skosimp)"" (lemma "inverse_types" )"" (split) (("1" (propax) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil )nil function_inverse_alt_aux nil ))nil 3301319377"" (skosimp*) (("" (inst + "f!1(r!1)" ) nil nil )) nil )nil function_inverse_alt_aux nil )nil function_inverse_alt_aux nil ))nil 3301319427"" (skosimp)"" (apply-extensionality :hide? t)"1" "bijective_inverse_alt_is_bijective[D,R]" ("f" "f!1" ))"1" (lemma "bijective_inverse_is_inverse_alt[R,D]" )"1" (typepred "inverse_alt(f!1)" )"1" (inst -2 "inverse_alt(f!1)" "_" )"1" (inst - "f!1" )"1" (replace -2 * rl) (("1" (propax) nil nil )) nil )"2" (hide 2)"2" (name "G" "inverse_alt[D, R](f!1)" )"2" (replace -1)"2" "bijective_inverse_alt[D,R]" "f" "f!1" "g" "G" ))"2" (expand "inverse?" )"2" (skosimp*)"2" (inst - "r!1" "f!1(r!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "inverse_types" ) (("2" (propax) nil nil ))nil ))nil ))nil )"2" (hide-all-but (1 -2))"2" (flatten)"2" (skosimp*) (("2" (inst + "f!1(r!1)" ) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "inverse_types" ) (("2" (propax) nil nil )) nil ))nil )"2" (flatten)"2" (skosimp*) (("2" (inst + "f!1(r!1)" ) nil nil )) nil )) nil )"3" (lemma "inverse_types" ) (("3" (propax) nil nil )) nil ))nil ))nil )nil function_inverse_alt_aux nil )nil function_inverse_alt_aux nil )"inverses(f)" function_inverse_alt nil )nil function_inverse_alt nil )"bool" function_inverse_def nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" booleans nil )"bool" booleans nil )nil nil )"[D -> R]" function_inverse_alt_aux nil )nil function_inverse_def nil )"[T, T -> boolean]" equalities nil )nil function_inverse_alt_aux nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )nil nil ))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
