(finite_enumerationnil 3322363999"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (skosimp*)"" (lemma "bij_exists" ("S" "X!1" ))"" (skosimp)"" (lemma "bijective_inverse_exists" ("f" "f!1" ))"1" (expand "exists1" )"1" (flatten)"1" (skosimp)"1" (inst - "x!1" )"1" "bij_inv_is_bij_alt" "f" "f!1" "g" "x!1" ))"1" (propax) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" exists1 nil )nil function_inverse_def nil )"bool" function_inverse_def nil )nil nat_types nil )nil function_inverse_defnil )"bool" functions 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 )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil naturalnumbers nil )nil finite_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil finite_enumeration nil )"bool" sets nil )"bool" sets nil ))nil 3322365352"" (skosimp)"" (expand "finite_enumeration" ) (("" (propax) nil nil )) nil ))nil )"[below[card(X)] -> (X)]" nil ))nil 3322365404"" (skosimp)"" (expand "fullset" )"" (expand "image" )"" (expand "restrict" )"" (apply-extensionality :hide? t)"" (lemma "finite_enumeration_bij" ("X" "X!1" ))"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst - "x!1" )"" (skosimp)"" (inst + "x!2" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"R" restrict nil )nil finite_enumeration nil )"bool" functions nil )"bool" functions 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 )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil nat_types nil )"bool" booleans nil )"[below[card(X)] -> (X)]" nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_enumeration nil )"set[R]" function_image nil ))quality 98%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
