(countable_indexed_setsnil 3423550499"" (skosimp)"" (expand "is_countable" )"" (skosimp)"" (typepred "f!1" )"" "ZZ" "lambda (n:nat): if (exists (X:(XS!1)): f!1(X) = n) then choose({X:(XS!1) | f!1(X) = n}) else emptyset[T] endif" )"1" (inst + "ZZ" )"1" (split 1)"1" (hide -1)"1" (apply-extensionality :hide? t)"1" (case-replace "Union(XS!1)(x!1)" )"1" (expand "Union" )"1" (skosimp)"1" (typepred "a!1" )"1" (expand "IUnion" )"1" expand "ZZ" )"1" expand "emptyset" )"1" "f!1(a!1)" )"1" case "nonempty?({X: (XS!1) | f!1(X) = f!1(a!1)})" )"1" "EXISTS (X: (XS!1)): f!1(X) = f!1(a!1)" )"1" "1" "choose_member[(XS!1)]" "a" "{X: (XS!1) | f!1(X) = f!1(a!1)}" ))"1" "1" expand "member" )"1" expand "injective?" )"1" "choose({X: (XS!1) | f!1(X) = f!1(a!1)})" "a!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" (inst + "a!1" ) nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "a!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" (expand "IUnion" )"2" (skosimp)"2" expand "ZZ" )"2" expand "emptyset" )"2" "2" expand "Union" )"2" "2" "X!1" )"2" case "nonempty?[(XS!1)]({X: (XS!1) | f!1(X) = i!1})" )"1" "choose_member[(XS!1)]" "a" "{X: (XS!1) | f!1(X) = i!1}" ))"1" "1" expand "member" )"1" "X!1" )"1" expand "injective?" )"1" "choose[(XS!1)]({X: (XS!1) | f!1(X) = i!1})" "X!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "X!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (skosimp)"2" (expand "ZZ" )"2" "EXISTS (X: (XS!1)): f!1(X) = n!1" )"1" (hide 1)"1" (skosimp)"1" "choose_member[(XS!1)]" "a" "{X: (XS!1) | f!1(X) = n!1}" ))"1" "1" expand "member" )"1" expand "injective?" )"1" "X!1" )"1" "choose[(XS!1)]({X: (XS!1) | f!1(X) = n!1})" "X!1" )"1" (assert ) nil nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "X!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "empty?" )"2" "X!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 *)"2" (rewrite "emptyset_is_empty?" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (typepred "X!1" )"2" (inst - "X!1" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countability nil )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sets nil )nil defined_types nil )nil countable_indexed_sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sequences nil )nil sets_lemmas nil )"finite_set" finite_sets nil )"nat" countable_indexed_sets nil )"(XS!1)" countable_indexed_sets nil )"(injective?[(XS!1), nat])" nil )"setofsets[T]" countable_indexed_sets nil )"bool" sets nil )nil sets_lemmas nil )"bool" sets nil )"[nat -> setof[T]]" countable_indexed_setsnil )"nat" countable_indexed_sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"set[T]" indexed_sets nil )"set" sets nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil )"set" sets nil ))nil 3423553206"" (skosimp)"" (lemma "Union_IUnion" ("XS" "Complement(XS!1)" ))"" (split -1)"1" (skosimp)"1" (rewrite "Demorgan2" - :dir rl)"1" (inst + "IComplement(YS!1)" )"1" (rewrite "IDemorgan1" + :dir rl)"1" (replace -1 1 rl)"1" (rewrite "complement_complement" )"1" (skosimp)"1" (expand "Complement" -2)"1" (expand "IComplement" )"1" (inst - "n!1" )"1" (split -2)"1" "1" rewrite "emptyset_is_empty?" )"1" replace -1)"1" rewrite "complement_emptyset" )"1" rewrite "fullset_is_full?" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "b!1" )"2" replace -2)"2" rewrite "complement_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "is_countable" )"2" (skosimp)"2" (typepred "f!1" )"2" "lambda (x:(Complement(XS!1))): f!1(complement(x))" )"1" (expand "injective?" )"1" (skosimp)"1" "complement[T](x1!1)" "complement[T](x2!1)" )"1" (rewrite "complement_equal" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "Complement" )"2" (skosimp)"2" (typepred "b!1" )"2" (replace -2)"2" rewrite "complement_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setofsets[T]" sets_lemmas nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil countable_indexed_sets nil )nil countable_indexed_sets nil )"set" sets nil )"setofsets[T]" countable_indexed_sets nil )"(injective?[(XS!1), nat])" nil )nil sets_lemmas nil )"bool" functions nil )"bool" countability 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 )set type-eq-decl nil sets nil )nil sequences nil )"set[T]" indexed_sets_aux nil )nil sets_lemmas nil )"finite_set" finite_sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"set" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil sets_lemmas nil )"set" sets nil )nil indexed_sets_aux nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil sets_lemmas nil ))quality 100%
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
