(card_functionnil 3313930340"" (skosimp*)"" (expand "is_finite" )"" (skosimp*)"" (inst + "N!1" "f!2 o f!1" )"1" (expand "bijective?" )"1" (flatten)"1" (expand "o" )"1" (expand "restrict" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst -4 "f!1(x1!1)" "f!1(x2!1)" )"1" (assert )"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil ))nil )"2" (expand "fullset" )"2" (propax) nil nil )) nil )"3" (expand "fullset" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" finite_sets nil )"[D -> R]" card_function nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil card_function nil )nil card_function nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"R" restrict nil )"T3" function_props nil )"bool" functions nil )"bool" functions nil ))nil 3313930567"" (expand "fullset" )"" (expand "is_finite" )"" (skosimp*)"" (lemma "bijective_inverse_exists" ("f" "f!1" ))"1" (expand "exists1" )"1" (flatten)"1" (skolem -1 ("g" ))"1" (lemma "bij_inv_is_bij_alt" ("f" "f!1" "g" "g" ))"1" (inst + "N!1" "f!2 o g" )"1" (expand "bijective?" )"1" (flatten)"1" (hide-all-but (-1 -7 1))"1" (expand "restrict" )"1" (expand "injective?" )"1" expand "o" )"1" "1" "g(x1!1)" "g(x2!1)" )"1" assert )"1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" finite_sets nil )nil card_function nil )nil card_function nil )"bool" functions nil )nil booleans nil )nil booleans nil )nil function_inverse_defnil )nil function_inverse_def nil )"bool" function_inverse_def nil )"bool" functions nil )"T3" function_props nil )nil nat_types nil )"bool" reals nil )"bool" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" exists1 nil )"set" sets nil ))nil 3313931578"" (expand "fullset" )"" (expand "is_finite" )"" (skosimp*)"" (inst + "N!1" "f!2 o f!1" )"" (expand "restrict" )"" (expand "injective?" )"" (skosimp*)"" (expand "o" )"" (inst -3 "f!1(x1!1)" "f!1(x2!1)" )"" (assert )"" (inst - "x1!1" "x2!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" finite_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil card_function nil )"bool" booleans nil )"bool" reals nil )nil nat_types nil )nil card_function nil )"T3" function_props nil )"bool" functions nil )"set" sets nil ))nil 3313931479"" (skosimp)"" (lemma "infinite_injection" ("f" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil card_function nil )nil card_function nil )nil card_function nil ))nil 3313931185"" (expand "fullset" )"" (expand "is_finite" )"" (skosimp*)"" (lemma "surjective_inverse_exists" ("f" "f!1" ))"1" (skosimp)"1" (lemma "inj_inv_alt" ("f" "f!1" "g" "g!1" ))"1" (inst + "N!1" "f!2 o g!1" )"1" (expand "restrict" )"1" (expand "o " )"1" (expand "injective?" )"1" (skosimp*)"1" (inst -5 "g!1(x1!1)" "g!1(x2!1)" )"1" (assert )"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"bool" finite_sets nil )nil card_function nil )nil card_function nil )"bool" functions nil )nil booleans nil )nil booleans nil )nil function_inverse_defnil )nil function_inverse_def nil )"bool" function_inverse_def nil )"bool" functions nil )"T3" function_props nil )nil nat_types nil )"bool" reals nil )"bool" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil ))nil 3313931452"" (skosimp*)"" (lemma "infinite_surjection" ("f" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil card_function nil )nil card_function nil )nil card_function nil ))quality 100%
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
