Quelle sigma_set.prf
Sprache: Lisp
(sigma_setnil 3405672135"" (skosimp)"" (typepred "f!1" )"" (expand "convergent?" ) (("" (flatten) nil nil )) nil )) nil ))nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil sigma_set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3405672135"" (skosimp)"" (typepred "f!1" )"" (expand "convergent?" -1) (("" (flatten) nil nil )) nil ))nil ))nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil sigma_set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3406437533"" (skosimp)"" (typepred "f!1" )"" (expand "convergent?" 1)"" (case "subset?(nonzero_elts(f!1, C!1),C!1)" )"1" "countable_subset[T]" "S" "nonzero_elts(f!1, C!1)" "Count" "C!1" ))"1" (assert )"1" "countable_convergence.convergent_subset" "X" "nonzero_elts(f!1, C!1)" "Y" "C!1" "g" "f!1" ))"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" countable_convergence nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil sigma_set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set[T]" convergence_set nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil countable_convergence nil )nil countability "sets_aux/" )"boolean" notequal nil )"bool" sets nil )"bool" convergence_set nil ))nil ))nil 3406439338"" (skosimp)"" (expand "sigma" 1 1)"" "sigma_disjoint_union" "f" "f!1" "X" "nonzero_elts(f!1, C!1)" "Y" "difference(C!1,nonzero_elts(f!1, C!1))" ))"1" "union(nonzero_elts(f!1, C!1), ") "1" (hide -1)"1" (split)"1" "sigma_countable.sigma(difference(C!1, nonzero_elts(f!1, C!1)), f!1)=0" )"1" (assert ) nil nil )"2" (hide -1 2)"2" "sigma_eq" "f" "f!1" "g" "lambda t:0" "X" "difference(C!1, nonzero_elts(f!1, C!1))" ))"1" (split -1)"1" (replace -1)"1" (rewrite "sigma_zero" ) nil nil )) nil )"2" (hide 2)"2" (skosimp)"2" (typepred "t!1" )"2" (expand "nonzero_elts" )"2" expand "difference" )"2" expand "member" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" rewrite "countable_convergence.convergent_zero" )nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "disjoint?" )"2" (expand "difference" )"2" (expand "intersection" )"2" (expand "empty?" )"2" (expand "member" )"2" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "difference" )"2" (expand "union" )"2" (expand "member" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "(union[T] ") "1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )"[T, T -> boolean]" equalities nil )nil countable_convergence nil )nil sigma_countable nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma_countable nil )"real" reals nil )"real" sigma_countable nil )"countable_set[T]" nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"boolean" notequal nil )"countable_set[T]" nil )nil sigma_countable nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"set[T]" convergence_set nil )"bool" countable_convergence nil )"set" sets nil )"set" sets nil )nil sigma_set nil ))nil 3405672135"" (skosimp) (("" (rewrite "convergent_empty" ) nil nil )) nil )nil convergence_set nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil sigma_set nil ))nil ))nil 3405672659"" (skosimp)"" (expand "sigma" )"" (case-replace "nonzero_elts(g!1, emptyset[T])=emptyset[T]" )"1" (rewrite "sigma_empty" ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )"boolean" notequal nil )nil sigma_countable nil )"set" sets nil )"set[T]" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil )"finite_set[T]" sigma_set nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil 3405672135"" (skosimp)"" (expand "convergent?" )"" (case "subset?(nonzero_elts(g!1, F!1),F!1)" )"1" "finite_subset[T]" "s" "nonzero_elts(g!1, F!1)" "A" "F!1" ))"1" (assert )"1" "finite_countable[T]" "x" "nonzero_elts(g!1, F!1)" ))"1" (assert )"1" (expand "convergent?" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "subset?" )"2" (expand "nonzero_elts" )"2" (expand "member" ) (("2" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_set nil )"bool" sets nil )nil finite_sets nil )nil countable_props "sets_aux/" )"bool" countable_convergence nil )"(partial_order?[set[T]])" nil )nil sigma_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"set[T]" convergence_set nil )"bool" finite_sets nil )nil finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil ))nil ))nil 3405672135"" (skosimp)"" (expand "convergent?" ) (("" (propax) nil nil )) nil )) nil )"bool" countable_convergence nil )) nil ))nil 3406442906"" (skosimp)"" (lemma "sigma_countable" ("f" "g!1" "C" "F!1" ))"" (propax) nil nil )) nil ))nil )"bool" countable_convergence nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil )nil sigma_set nil ))nil 3405672135"" (skosimp)"" (expand "convergent?" )"" (case "g!1(t!1)=0" )"1" "nonzero_elts(g!1, singleton[T](t!1))=emptyset[T]" )"1" (rewrite "countable_emptyset" )"1" (rewrite "convergent_empty" ) nil nil )) nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (expand "nonzero_elts" )"2" (expand "singleton" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nonzero_elts(g!1, singleton[T](t!1))=singleton[T](t!1)" )"1" (lemma "convergent_singleton" ("t" "t!1" "g" "g!1" ))"1" (rewrite "countable_singleton" ) nil nil )) nil )"2" (hide 3)"2" (expand "singleton" )"2" (expand "nonzero_elts" )"2" (apply-extensionality :hide? t)"2" (case-replace "x!1=t!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_set nil )nil countable_props "sets_aux/" )nil convergence_set nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"non_empty_finite_set[T]" sigma_set nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" sigma_set nil )nil booleans nil )set type-eq-decl nil sets nil )"set[T]" convergence_set nil )"bool" sets nil )"(singleton?)" sets nil )"set" sets nil )nil countable_convergence nil )nil countable_props "sets_aux/" )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil sigma_set nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil ))nil 3406439219"" (skosimp)"" (rewrite "sigma_countable" )"1" (rewrite "sigma_singleton" ) nil nil )"2" (rewrite "countable_convergence.convergent_singleton" ) nil nil )"3" (rewrite "countable_singleton" ) nil nil ))nil ))nil )"non_empty_finite_set[T]" sigma_set nil )nil sigma_set nil )nil sigma_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" sets nil )"(singleton?)" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" countable_convergence nil )nil sigma_countable nil )nil countable_convergence nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "X" "X!1" "Y" "union(X!1, Y!1)" "g" "f!1" ))"" (assert ) (("" (hide-all-but 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "X" "Y!1" "Y" "union(X!1, Y!1)" "g" "f!1" ))"" (assert ) (("" (hide-all-but 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3406442938"" (skosimp)"" (expand "sigma" )"" "nonzero_elts(f!1, union(X!1, Y!1))=union(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))" )"1" "sigma_disjoint_union" "X" "nonzero_elts(f!1, X!1)" "Y" "nonzero_elts(f!1, Y!1)" "f" "f!1" ))"1" (assert )"1" (hide 2 -1)"1" (expand "disjoint?" )"1" (expand "intersection" )"1" (expand "empty?" )"1" (expand "member" )"1" (skosimp)"1" (expand "nonzero_elts" )"1" (flatten)"1" (inst - "x!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "nonzero_elts" )"2" (expand "union" )"2" (expand "member" )"2" (expand "disjoint?" )"2" (expand "empty?" )"2" (inst - "x!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )"bool" countable_convergence nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil sigma_countable nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"real" reals nil )"set" sets nil )"bool" convergence_set nil )"set[T]" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil ))nil 3405672135"" (skosimp)"" (typepred "f!1" )"" "convergence_set.convergent_subset" "X" "X!1" "Y" "union(X!1, Y!1)" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"set" sets nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil sigma_set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )nil convergence_set nil ))nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "X" "Y!1" "Y" "union(X!1, Y!1)" "g" "f!1" ))"" (assert ) (("" (hide-all-but 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "Y" "union(X!1,Y!1)" "X" "intersection(X!1, Y!1)" "g" "f!1" ))"" (assert ) (("" (hide 2) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3406444014"" (skosimp)"" (expand "sigma" )"" "nonzero_elts(f!1, intersection(X!1, Y!1))=intersection(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))" )"1" "nonzero_elts(f!1, union(X!1, Y!1))=union(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))" )"1" "sigma_union" "f" "f!1" "X" "nonzero_elts(f!1, X!1)" "Y" "nonzero_elts(f!1, Y!1)" ))"1" (propax) nil nil )) nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )nil sigma_countable nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" countable_convergence nil )"bool" sets nil )"boolean" notequal nil )"set" sets nil )"set" sets nil )"bool" convergence_set nil )"set[T]" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil ))nil 3406438550"" (skosimp)"" (lemma "sigma_union" ("f" "f!1" "X" "X!1" "Y" "Y!1" ))"" (assert ) nil nil )) nil ))nil )"set" sets nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil )nil sigma_set nil )"real" reals nil )"real" reals nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "Y" "union(X!1,Y!1)" "X" "difference(X!1, Y!1)" "g" "f!1" ))"" (assert ) (("" (hide 2) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "Y" "union(X!1,Y!1)" "X" "difference(Y!1, X!1)" "g" "f!1" ))"" (assert ) (("" (hide 2) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3406444522"" (skosimp)"" (expand "sigma" )"" "nonzero_elts(f!1, difference(X!1, Y!1))=difference(nonzero_elts(f!1, X!1), nonzero_elts(f!1,Y!1))" )"1" "nonzero_elts(f!1, difference(Y!1, X!1))=difference(nonzero_elts(f!1, Y!1), nonzero_elts(f!1,X!1))" )"1" "sigma_difference" "X" "nonzero_elts(f!1, X!1)" "Y" "nonzero_elts(f!1, Y!1)" "f" "f!1" ))"1" (assert ) nil nil )"2" (hide 2)"2" "union[T](nonzero_elts[T](f!1, X!1), nonzero_elts[T](f!1, Y!1))=nonzero_elts[T](f!1, union(X!1,Y!1))" )"1" (assert )"1" (typepred "f!1" )"1" (expand "convergent?" -1)"1" (propax) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )"bool" sets nil )"boolean" notequal nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil sigma_countable nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" countable_convergence nil )"set" sets nil )"set" sets nil )"bool" convergence_set nil )"set[T]" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "Y" "Y!1" "X" "X!1" "g" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"(partial_order?[set[T]])" nil ))nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_subset" "Y" "Y!1" "X" "difference(Y!1,X!1)" "g" "f!1" ))"" (assert )"" (hide 2)"" (expand "difference" )"" (expand "subset?" )"" (expand "member" ) (("" (skosimp) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil ))nil ))nil 3406438952"" (skosimp)"" (lemma "difference_subset2" ("b" "Y!1" "a" "X!1" ))"" (assert )"" (lemma "sigma_difference" ("X" "X!1" "Y" "Y!1" "f" "f!1" ))"1" (replace -2)"1" (rewrite "sigma_empty" ) (("1" (assert ) nil nil ))nil ))nil )"2" (case-replace "union[T](X!1, Y!1)=Y!1" )"1" (assert ) nil nil )"2" (hide-all-but (1 -2))"2" (apply-extensionality :hide? t)"2" (expand "union" )"2" (expand "subset?" )"2" (expand "member" )"2" (inst - "x!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_set nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil )"set" sets nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sigma_set nil )nil sigma_set nil )"real" reals nil )"bool" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"(partial_order?[set[T]])" nil )"real" reals nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_add" "X" "X!1" "t" "t!1" "g" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil ))nil ))nil 3406438613"" (skosimp)"" (expand "member" )"" (case-replace "X!1(t!1)" )"1" (case-replace "add(t!1, X!1)=X!1" )"1" (hide 2)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil ))nil ))nil )"2" (assert )"2" (rewrite "add_as_union" )"2" "sigma_union" "f" "f!1" "X" "X!1" "Y" "singleton(t!1)" ))"2" (rewrite "sigma_singleton" )"2" "intersection(X!1, singleton(t!1))=emptyset[T]" )"1" (rewrite "sigma_empty" )"1" (assert ) nil nil )) nil )"2" (hide-all-but (1 2))"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"real" reals nil )"set" sets nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(singleton?)" sets nil )"bool" sets nil )nil sigma_set nil )"set" sets nil )"set" sets nil )"finite_set[T]" nil )"countable_set[T]" nil )"real" reals nil )"finite_set[T]" sigma_set nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )nil sigma_set nil )"odd_int" integers nil )nil sigma_set nil )"(nonempty?)" sets nil )"non_empty_finite_set[T]" sigma_set nil )nil sets_lemmas nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"(nonempty?)" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil ))nil 3405672135"" (skosimp)"" "convergence_set.convergent_remove" "X" "X!1" "t" "t!1" "g" "f!1" ))"" (assert ) nil nil )) nil ))nil )nil sigma_set nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil convergence_set nil ))nil ))nil 3406446180"" (skosimp)"" (expand "member" )"" (case-replace "X!1(t!1)" )"1" (lemma "add_remove_member" ("x" "t!1" "a" "X!1" ))"1" (expand "member" )"1" (assert )"1" "sigma_add" "t" "t!1" "X" "remove(t!1, X!1)" "f" "f!1" ))"1" (replace -2)"1" (expand "remove" -1 1)"1" (expand "member" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "member_remove" ("x" "t!1" "a" "X!1" ))"2" (expand "member" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"real" reals nil )"real" reals nil )nil sigma_set nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" convergence_set nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil ))nil 3405672135"" (skosimp)"" (typepred "f!1" )"" "convergence_set.convergent_subset" "X" "rest[T](X!1)" "Y" "X!1" "g" "f!1" ))"" (assert )"" (hide-all-but 1) (("" (rewrite "rest_subset" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil sets nil )"bool" sets nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil sigma_set nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )nil sets_lemmas nil )nil convergence_set nil )"set" sets nil ))nil ))nil 3406446380"" (skosimp)"" (lemma "choose_rest" ("a" "X!1" ))"" (typepred "X!1" )"" (expand "nonempty?" )"" (assert )"" "sigma_add" "f" "f!1" "t" "choose(X!1)" "X" "rest(X!1)" ))"" (lemma "choose_not_member" ("a" "X!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma_set nil )nil sets nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil )"bool" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(p)" sets nil ) (rest const-decl "set" sets nil )nil sigma_set nil )nil sets_lemmas nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3405672135"" (skosimp) (("" (rewrite "convergent_zero" ) nil nil )) nil )nil convergence_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil sigma_set nil ))nil ))nil 3406444856"" (skosimp)"" (expand "sigma" )"" (case-replace "nonzero_elts(LAMBDA t: 0, X!1)=emptyset[T]" )"1" (rewrite "sigma_countable.sigma_empty" ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )nil sigma_countable nil )"set" sets nil )"set[T]" convergence_set nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil )"finite_set[T]" sigma_set nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil 3405672135"" (skosimp) (("" (rewrite "convergent_scal" ) nil nil )) nil )nil convergence_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" convergence_set nil )nil sigma_set nil ))nil ))nil 3406445590"" (skosimp)"" (expand "sigma" )"" (case-replace "a!1=0" )"1" (case-replace "nonzero_elts(0 * f!1, X!1)=emptyset[T]" )"1" (lemma "sigma_countable.sigma_empty" ("g" "0*f!1" ))"1" (replace -1) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" "nonzero_elts(a!1 * f!1, X!1)=nonzero_elts(f!1, X!1)" )"1" (hide -1)"1" "sigma_scal" "a" "a!1" "f" "f!1" "X" "nonzero_elts(f!1, X!1)" ))"1" (propax) nil nil )) nil ))nil )"2" (hide 3)"2" (apply-extensionality :hide? t)"2" (expand "nonzero_elts" )"2" (expand "*" )"2" (case-replace "X!1(x!1)" )"1" (case-replace "f!1(x!1)=0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma_set nil )"bool" countable_convergence nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil sigma_countable nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" sigma_set nil )nil sigma_set nil )nil booleans nil )set type-eq-decl nil sets nil )"set[T]" convergence_set nil )"[T -> real]" real_fun_ops "reals/" )"bool" convergence_set nil )"set" sets nil )"real" reals nil )nil sigma_countable nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil 3405672135"" (skosimp) (("" (rewrite "convergent_opp" ) nil nil )) nil )nil convergence_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" convergence_set nil )nil sigma_set nil ))nil ))nil 3406445499"" (skosimp)"" (lemma "sigma_scal" ("f" "f!1" "X" "X!1" "a" "-1" ))"" (case-replace "-1 * f!1=-f!1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_set nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sigma_set nil )nil sigma_set nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil ))nil 3405672135"" (skosimp) (("" (rewrite "convergent_plus" ) nil nil )) nil )nil convergence_set nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" convergence_set nil )nil sigma_set nil ))nil ))nil 3406446563"" (skosimp)"" (expand "sigma" )"" "sigma_countable.sigma_plus" "X" "union(nonzero_elts(f!1, X!1),nonzero_elts(g!1, X!1))" "f" "f!1" "g" "g!1" ))"1" "sigma_countable.sigma_subset" "X" "nonzero_elts(f!1, X!1)" "Y" "union(nonzero_elts(f!1, X!1), nonzero_elts(g!1, X!1))" "f" "f!1" ))"1" (split -1)"1" "sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1), ") "1" (replace -2)"1" (hide -1 -2)"1" "sigma_countable.sigma_subset" "X" "nonzero_elts(g!1, X!1)" "Y" "union(nonzero_elts(f!1, X!1), nonzero_elts(g!1, X!1))" "f" "g!1" ))"1" (split -1)"1" "sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1), ") "1" (replace -2)"1" (hide -1 -2)"1" "sigma_countable.sigma_subset" "X" "nonzero_elts(f!1 + g!1, X!1)" "Y" "union(nonzero_elts(f!1, X!1), nonzero_elts(g!1, X!1))" "f" "f!1+g!1" ))"1" "1" "sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1), ") "1" (assert ) nil nil )"2" "2" "sigma_eq" "X" "difference(union(nonzero_elts(f!1, X!1), " "f" "f!1+g!1" "g" "lambda t:0" ))"1" rewrite "sigma_countable.sigma_zero" )"1" assert )"1" "1" "1" "t!1" )"1" expand "+ " )"1" expand "difference" )"1" expand "union" )"1" expand "nonzero_elts" )"1" expand "member" )"1" "1" "X!1(t!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "countable_convergence.convergent_zero" )nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "difference(union(nonzero_elts(f!1, X!1), ") "1" "sigma_eq" "X" "difference(nonzero_elts(f!1, X!1), nonzero_elts(g!1, X!1))" "f" "g!1" "g" "lambda t:0" ))"1" rewrite "sigma_countable.sigma_zero" )"1" assert )"1" "1" "1" "t!1" )"1" expand "difference" )"1" expand "member" )"1" expand "nonzero_elts" )"1" "1" assert )quality 100%
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
