(numbers_infinitenil 3314538968"" (expand "is_finite_type" )"" (skolem!)"" "composition_injective[below[N!1 + 1], nat, below[N!1]]" )"" (inst - "LAMBDA (n: below[N!1 + 1]): n" "g!1" )"1" (lemma "injection_n_to_m" )"1" (inst - "N!1" "N!1 + 1" )"1" (assert ) (("1" (inst?) nil nil )) nil )) nil ))nil )"2" (expand "injective?" ) (("2" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil )"nat" numbers_infinite nil )"bool" functions nil )"[nat -> below[N!1]]" numbers_infinite nil )"posint" nil )nil naturalnumbers nil )"T3" function_props nil )nil nat_fun_props nil )"posint" nil )nil function_props 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 )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"bool" finite_sets nil ))nil 3314539260"" (lemma "nat_infinite" )"" (rewrite "finite_full" )"" (rewrite "finite_full" )"" (assert )"" "finite_subset[int]" "A" "fullset[int]" "s" "fullset[nat]" ))"" (rewrite "finite_extension[int, nat]" )"" (expand * "extend" "subset?" "member" "fullset" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 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 extend_set_props nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )"bool" booleans nil )"R" extend nil )nil numbers_infinite nil ))nil 3314539402"" (lemma "nat_infinite" )"" (rewrite "finite_full" )"" (rewrite "finite_full" )"" (assert )"" "finite_subset[rat]" "A" "fullset[rat]" "s" "fullset[nat]" ))"" (rewrite "finite_extension[rat, nat]" )"" (expand * "extend" "subset?" "member" "fullset" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 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 extend_set_props nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )"bool" booleans nil )"R" extend nil )nil rationals nil )nil numbers_infinite nil ))nil 3314539488"" (lemma "nat_infinite" )"" (rewrite "finite_full" )"" (rewrite "finite_full" )"" (assert )"" "finite_subset[real]" "A" "fullset[real]" "s" "fullset[nat]" ))"" (rewrite "finite_extension[real, nat]" )"" (expand * "extend" "subset?" "member" "fullset" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 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 extend_set_props nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )"bool" booleans nil )"R" extend nil )nil numbers_infinite nil ))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
