(infinite_setsnil 3317054230"" (skolem!)"" (rewrite "add_as_union" )"" (use "infinite_countable_union" ) nil nil )) nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" finite_sets nil )nil infinite_sets_def nil )nil infinite_sets nil )"non_empty_finite_set" infinite_sets nil )"infinite_set[T]" nil )nil countable_props nil )"bool" countability nil )nil countability nil )"bool" sets nil )"(singleton?)" sets nil ))nil 3317054261"" (skolem!)"" (case "member(t!1, Inf!1)" )"1" (forward-chain "add_remove_member[T]" )"1" (use "infinite_add_card" )"1" (rewrite "card_eq_symmetric[T, T]" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (forward-chain "member_remove[T]" )"2" (lemma "card_eq_is_reflexive" )"2" (expand "reflexive?" )"2" (inst - "Inf!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil infinite_sets_def nil )"bool" finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil infinite_sets nil )nil infinite_sets nil )"set" sets nil )"infinite_set[T]" nil )"equivalence[set[T]]" nil )"infinite_set[T]" infinite_setsnil )nil card_comp_set_props nil )"bool" sets nil )"(nonempty?)" sets nil )nil sets_lemmas nil )nil card_single nil )"bool" relations nil )nil sets_lemmas nil ))nil 3317054357"" (skolem!)"" (prop)"1" (inst?)"1" (lemma "card_lt_is_irreflexive" )"1" (expand "irreflexive?" ) (("1" (inst?) nil nil )) nil ))nil ))nil )"2" (skolem-typepred)"2" (expand * "card_lt" "is_finite" )"2" (skosimp*)"2" "composition_injective[(S!1), (Fin!1), below[N!1]]" )"2" (inst + "N!1" "f!1 o f!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil card_single nil )"bool" relations nil )nil finite_sets nil )nil infinite_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )"set[T]" infinite_sets nil )"bool" card_comp_set nil )nil function_props 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 )"[(S!1) -> (Fin!1)]" infinite_sets nil )"bool" functions nil )"finite_set[T]" infinite_sets nil )"[(Fin!1) -> below[N!1]]" infinite_sets nil )"nat" infinite_sets nil )"T3" function_props nil )NOT const-decl "[bool -> bool]" booleans nil ))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
