(outer_measurenil 3458456184"" (typepred "A" )"" (expand "subset_algebra?" )"" (flatten)"" (expand "subset_algebra_empty?" )"" (expand "nonempty?" )"" (expand "member" )"" (expand "empty?" )"" (inst - "emptyset[T]" )"" (expand "member" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )"bool" sets nil )"set" sets nil )set type-eq-decl nil sets nil )"(S)" outer_measure nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"subset_algebra" outer_measure nil ))nil ))nil 3458456184"" (typepred "A" )"" (expand "subset_algebra?" )"" (flatten)"" (expand "subset_algebra_empty?" )"" (assert )"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" subset_algebra_def nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"(S)" outer_measure nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"subset_algebra" outer_measure nil ))nil ))nil 3458456184"" (lemma "subset_algebra_fullset" ) (("" (propax) nil nil )) nil )nil subset_algebra nil )nil outer_measure nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"subset_algebra" outer_measure nil ))nil ))nil 3458456184"" (skosimp)"" (lemma "subset_algebra_intersection" )"" (inst - "a!1" "b!1" ) nil nil )) nil ))nil )"subset_algebra" outer_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil outer_measure nil )nil subset_algebra nil )set type-eq-decl nil sets nil ))nil ))nil 3458456184"" (skosimp)"" (lemma "subset_algebra_difference" ("x" "a!1" "y" "b!1" ))"" (expand "finite_disjoint_union?" )"" "lambda (i:nat): if i=0 then difference[T](a!1, b!1) else emptyset endif" "1" )"" (split)"1" (grind) nil nil )"2" (apply-extensionality :hide? t)"2" (expand "IUnion" )"2" (expand "emptyset" )"2" (case-replace "difference[T](a!1, b!1)(x!1)" )"1" (inst + "0" ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (case-replace "i!1=0" )"1" (expand "member" ) (("1" (propax) nil nil )) nil )"2" (assert ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"subset_algebra" outer_measure nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil outer_measure nil )set type-eq-decl nil sets nil )nil subset_algebra nil )"(A)" 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 )nil sequences nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"set" sets nil )"(S)" outer_measure nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"(strict_total_order?[real])" real_props nil )"set[T]" indexed_sets nil )"(S)" nil )"boolean" notequal nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" subset_algebra_def nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
