(infinite_pigeonholenil 3314537897"" (skolem!)"" (decompose-equality)"" (expand * "fullset" "IUnion" "Union" )"" (inst + "f!1(x!1)" )"" expand * "inverse_image" "inverse_image" "member" "singleton" )nil nil ))nil ))nil ))nil ))nil )nil booleans nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )nil infinite_pigeonhole nil )"set[T]" indexed_sets nil )"set[D]" function_image nil )"bool" sets nil )"(singleton?)" sets nil )nil booleans nil )nil infinite_pigeonhole nil )"bool" sets nil )"set[D]" function_image nil ))nil 3314538195"" (skolem!)"" (use "Union_inverse_image" )"" (rewrite "IUnion_Union" )"" (use "Union_finite[D]" )"" (replace -2 :dir rl :hide? t)"" (rewrite "finite_full" :dir rl)"" (rewrite "domain_infiniteness" )"" (prop)"1" (hide-all-but 1)"1" (expand "image" )"1" (rewrite "finite_image" )"1" (rewrite "finite_full" :dir rl)"1" (forward-chain "range_finiteness" ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "every" )"2" (skolem-typepred)"2" (expand * "image" "image" )"2" (expand "inverse_image" -)"2" (skolem!)"2" (replace -1 :hide? t)"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil infinite_pigeonhole nil )nil infinite_pigeonhole nil )nil infinite_pigeonhole nil )nil finite_sets_of_sets nil )"set" sets nil )"set[R]" function_image nil )nil sets nil )nil defined_types nil )nil finite_sets nil )nil infinite_pigeonhole nil )nil function_image_aux nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"set[R]" function_image nil )"bool" sets nil )nil infinite_pigeonhole nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(singleton?)" sets nil )"bool" sets nil )"set[D]" function_image nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil indexed_sets nil ))quality 100%
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
