|
(sigma_set
(sigma_TCC1 0
(sigma_TCC1-1 nil 3405672135
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "convergent?") (("" (flatten) nil nil)) nil)) nil))
nil)
((convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sigma_TCC2 0
(sigma_TCC2-1 nil 3405672135
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "convergent?" -1) (("" (flatten) nil nil)) nil))
nil))
nil)
((convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sigma_countable_TCC1 0
(sigma_countable_TCC1-1 nil 3406437533
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "convergent?" 1)
(("" (case "subset?(nonzero_elts(f!1, C!1),C!1)")
(("1"
(lemma "countable_subset[T]"
("S" "nonzero_elts(f!1, C!1)" "Count" "C!1"))
(("1" (assert)
(("1"
(lemma "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)
((convergent? const-decl "bool" countable_convergence nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(is_countable const-decl "bool" countability "sets_aux/")
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(convergent_subset formula-decl nil countable_convergence nil)
(countable_subset formula-decl nil countability "sets_aux/")
(/= const-decl "boolean" notequal nil)
(member const-decl "bool" sets nil)
(convergent? const-decl "bool" convergence_set nil))
nil))
(sigma_countable 0
(sigma_countable-1 nil 3406439338
("" (skosimp)
(("" (expand "sigma" 1 1)
((""
(lemma "sigma_disjoint_union"
("f" "f!1" "X" "nonzero_elts(f!1, C!1)" "Y"
"difference(C!1,nonzero_elts(f!1, C!1))"))
(("1"
(case-replace "union(nonzero_elts(f!1, C!1),
difference(C!1, nonzero_elts(f!1, C!1)))=C!1")
(("1" (hide -1)
(("1" (split)
(("1"
(case-replace
"sigma_countable.sigma(difference(C!1, nonzero_elts(f!1, C!1)), f!1)=0")
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2"
(lemma "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"
(flatten)
(("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"
(case-replace "(union[T]
(nonzero_elts[T](f!1, C!1),
difference[T](C!1, nonzero_elts[T](f!1, C!1))))=C!1")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma const-decl "real" sigma_set nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(convergent_zero formula-decl nil countable_convergence nil)
(sigma_zero formula-decl nil sigma_countable nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sigma_eq formula-decl nil sigma_countable nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma const-decl "real" sigma_countable nil)
(countable_intersection2 application-judgement "countable_set[T]"
sigma_set nil)
(disjoint? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(countable_difference application-judgement "countable_set[T]"
sigma_set nil)
(sigma_disjoint_union formula-decl nil sigma_countable nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_countable const-decl "bool" countability "sets_aux/")
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(convergent? const-decl "bool" countable_convergence nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_empty_TCC1 0
(sigma_empty_TCC1-1 nil 3405672135
("" (skosimp) (("" (rewrite "convergent_empty") nil nil)) nil)
((convergent_empty formula-decl nil convergence_set nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T formal-type-decl nil sigma_set nil))
nil))
(sigma_empty 0
(sigma_empty-1 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)
((sigma const-decl "real" sigma_set nil)
(/= const-decl "boolean" notequal nil)
(sigma_empty formula-decl nil sigma_countable nil)
(emptyset const-decl "set" sets nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_set nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(sigma_finite_TCC1 0
(sigma_finite_TCC1-1 nil 3405672135
("" (skosimp)
(("" (expand "convergent?")
(("" (case "subset?(nonzero_elts(g!1, F!1),F!1)")
(("1"
(lemma "finite_subset[T]"
("s" "nonzero_elts(g!1, F!1)" "A" "F!1"))
(("1" (assert)
(("1"
(lemma "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)
((convergent? const-decl "bool" convergence_set nil)
(member const-decl "bool" sets nil)
(finite_subset formula-decl nil finite_sets nil)
(finite_countable judgement-tcc nil countable_props "sets_aux/")
(convergent? const-decl "bool" countable_convergence nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(T formal-type-decl nil sigma_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil))
nil))
(sigma_finite_TCC2 0
(sigma_finite_TCC2-1 nil 3405672135
("" (skosimp)
(("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)
((convergent? const-decl "bool" countable_convergence nil)) nil))
(sigma_finite 0
(sigma_finite-1 nil 3406442906
("" (skosimp)
(("" (lemma "sigma_countable" ("f" "g!1" "C" "F!1"))
(("" (propax) nil nil)) nil))
nil)
((convergent? const-decl "bool" countable_convergence nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(is_countable const-decl "bool" countability "sets_aux/")
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil)
(sigma_countable formula-decl nil sigma_set nil))
shostak))
(sigma_singleton_TCC1 0
(sigma_singleton_TCC1-1 nil 3405672135
("" (skosimp)
(("" (expand "convergent?")
(("" (case "g!1(t!1)=0")
(("1"
(case-replace
"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"
(case-replace
"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)
((convergent? const-decl "bool" convergence_set nil)
(countable_singleton formula-decl nil countable_props "sets_aux/")
(convergent_singleton formula-decl nil convergence_set nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" sigma_set nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" sigma_set nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(emptyset const-decl "set" sets nil)
(convergent_empty formula-decl nil countable_convergence nil)
(countable_emptyset formula-decl nil countable_props "sets_aux/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil sigma_set nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil))
nil))
(sigma_singleton 0
(sigma_singleton-1 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)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" sigma_set nil)
(sigma_countable formula-decl nil sigma_set nil)
(T formal-type-decl nil sigma_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_countable const-decl "bool" countability "sets_aux/")
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" countable_convergence nil)
(sigma_singleton formula-decl nil sigma_countable nil)
(convergent_singleton formula-decl nil countable_convergence nil))
shostak))
(sigma_disjoint_union_TCC1 0
(sigma_disjoint_union_TCC1-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_disjoint_union_TCC2 0
(sigma_disjoint_union_TCC2-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_disjoint_union 0
(sigma_disjoint_union-1 nil 3406442938
("" (skosimp)
(("" (expand "sigma")
((""
(case-replace
"nonzero_elts(f!1, union(X!1, Y!1))=union(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))")
(("1"
(lemma "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)
((sigma const-decl "real" sigma_set nil)
(convergent? const-decl "bool" countable_convergence nil)
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(is_countable const-decl "bool" countability "sets_aux/")
(sigma_disjoint_union formula-decl nil sigma_countable nil)
(intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_union_TCC1 0
(sigma_union_TCC1-1 nil 3405672135
("" (skosimp)
(("" (typepred "f!1")
((""
(lemma "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)
((union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(convergent_subset formula-decl nil convergence_set nil))
nil))
(sigma_union_TCC2 0
(sigma_union_TCC2-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_union_TCC3 0
(sigma_union_TCC3-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_union 0
(sigma_union-1 nil 3406444014
("" (skosimp)
(("" (expand "sigma")
((""
(case-replace
"nonzero_elts(f!1, intersection(X!1, Y!1))=intersection(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))")
(("1"
(case-replace
"nonzero_elts(f!1, union(X!1, Y!1))=union(nonzero_elts(f!1, X!1),nonzero_elts(f!1, Y!1))")
(("1"
(lemma "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)
((sigma const-decl "real" sigma_set nil)
(sigma_union formula-decl nil sigma_countable nil)
(is_countable const-decl "bool" countability "sets_aux/")
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(convergent? const-decl "bool" countable_convergence nil)
(member const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(intersection const-decl "set" sets nil)
(union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_intersection 0
(sigma_intersection-1 nil 3406438550
("" (skosimp)
(("" (lemma "sigma_union" ("f" "f!1" "X" "X!1" "Y" "Y!1"))
(("" (assert) nil nil)) nil))
nil)
((union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil)
(sigma_union formula-decl nil sigma_set nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(sigma_difference_TCC1 0
(sigma_difference_TCC1-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_difference_TCC2 0
(sigma_difference_TCC2-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_difference 0
(sigma_difference-1 nil 3406444522
("" (skosimp)
(("" (expand "sigma")
((""
(case-replace
"nonzero_elts(f!1, difference(X!1, Y!1))=difference(nonzero_elts(f!1, X!1), nonzero_elts(f!1,Y!1))")
(("1"
(case-replace
"nonzero_elts(f!1, difference(Y!1, X!1))=difference(nonzero_elts(f!1, Y!1), nonzero_elts(f!1,X!1))")
(("1"
(lemma "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"
(case-replace
"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)
((sigma const-decl "real" sigma_set nil)
(member const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma_difference formula-decl nil sigma_countable nil)
(is_countable const-decl "bool" countability "sets_aux/")
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(convergent? const-decl "bool" countable_convergence nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_subset_TCC1 0
(sigma_subset_TCC1-1 nil 3405672135
("" (skosimp)
((""
(lemma "convergence_set.convergent_subset"
("Y" "Y!1" "X" "X!1" "g" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_subset_TCC2 0
(sigma_subset_TCC2-1 nil 3405672135
("" (skosimp)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_subset formula-decl nil convergence_set nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(sigma_subset 0
(sigma_subset-1 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)
((T formal-type-decl nil sigma_set nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(difference_subset2 formula-decl nil sets_lemmas nil)
(union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(sigma_difference formula-decl nil sigma_set nil)
(sigma_empty formula-decl nil sigma_set nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(sigma_add_TCC1 0
(sigma_add_TCC1-1 nil 3405672135
("" (skosimp)
((""
(lemma "convergence_set.convergent_add"
("X" "X!1" "t" "t!1" "g" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_add formula-decl nil convergence_set nil))
nil))
(sigma_add 0
(sigma_add-1 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"
(lemma "sigma_union"
("f" "f!1" "X" "X!1" "Y" "singleton(t!1)"))
(("2" (rewrite "sigma_singleton")
(("2"
(case-replace
"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)
((member const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(union const-decl "set" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(sigma_union formula-decl nil sigma_set nil)
(emptyset const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(finite_intersection1 application-judgement "finite_set[T]"
sigma_set nil)
(countable_intersection2 application-judgement "countable_set[T]"
sigma_set nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_set nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(sigma_empty formula-decl nil sigma_set nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sigma_singleton formula-decl nil sigma_set nil)
(nonempty_union2 application-judgement "(nonempty?)" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" sigma_set nil)
(add_as_union formula-decl nil sets_lemmas nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_remove_TCC1 0
(sigma_remove_TCC1-1 nil 3405672135
("" (skosimp)
((""
(lemma "convergence_set.convergent_remove"
("X" "X!1" "t" "t!1" "g" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((T formal-type-decl nil sigma_set nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(convergent_remove formula-decl nil convergence_set nil))
nil))
(sigma_remove 0
(sigma_remove-1 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"
(lemma "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)
((member const-decl "bool" sets nil)
(member_remove formula-decl nil sets_lemmas nil)
(add_remove_member formula-decl nil sets_lemmas nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma_add formula-decl nil sigma_set nil)
(remove const-decl "set" sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" convergence_set nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil))
shostak))
(sigma_choose_rest_TCC1 0
(sigma_choose_rest_TCC1-1 nil 3405672135
("" (skosimp)
(("" (typepred "f!1")
((""
(lemma "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)
((nonempty_set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(rest_subset formula-decl nil sets_lemmas nil)
(convergent_subset formula-decl nil convergence_set nil)
(rest const-decl "set" sets nil))
nil))
(sigma_choose_rest 0
(sigma_choose_rest-1 nil 3406446380
("" (skosimp)
(("" (lemma "choose_rest" ("a" "X!1"))
(("" (typepred "X!1")
(("" (expand "nonempty?")
(("" (assert)
((""
(lemma "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)
((T formal-type-decl nil sigma_set nil)
(nonempty_set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(choose_rest formula-decl nil sets_lemmas nil)
(convergent? const-decl "bool" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(choose const-decl "(p)" sets nil) (rest const-decl "set" sets nil)
(sigma_add formula-decl nil sigma_set nil)
(choose_not_member formula-decl nil sets_lemmas nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(sigma_zero_TCC1 0
(sigma_zero_TCC1-1 nil 3405672135
("" (skosimp) (("" (rewrite "convergent_zero") nil nil)) nil)
((convergent_zero formula-decl nil convergence_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil sigma_set nil))
nil))
(sigma_zero 0
(sigma_zero-1 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)
((sigma const-decl "real" sigma_set nil)
(sigma_empty formula-decl nil sigma_countable nil)
(emptyset const-decl "set" sets nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_set nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
shostak))
(sigma_scal_TCC1 0
(sigma_scal_TCC1-1 nil 3405672135
("" (skosimp) (("" (rewrite "convergent_scal") nil nil)) nil)
((convergent_scal formula-decl nil convergence_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" convergence_set nil)
(T formal-type-decl nil sigma_set nil))
nil))
(sigma_scal 0
(sigma_scal-1 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"
(case-replace
"nonzero_elts(a!1 * f!1, X!1)=nonzero_elts(f!1, X!1)")
(("1" (hide -1)
(("1"
(lemma "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)
((sigma const-decl "real" sigma_set nil)
(convergent? const-decl "bool" countable_convergence nil)
(countable_set nonempty-type-eq-decl nil countability "sets_aux/")
(is_countable const-decl "bool" countability "sets_aux/")
(sigma_scal formula-decl nil sigma_countable nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" sigma_set nil)
(T formal-type-decl nil sigma_set nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonzero_elts const-decl "set[T]" convergence_set nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(convergent? const-decl "bool" convergence_set nil)
(emptyset const-decl "set" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sigma_empty formula-decl nil sigma_countable nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(sigma_opp_TCC1 0
(sigma_opp_TCC1-1 nil 3405672135
("" (skosimp) (("" (rewrite "convergent_opp") nil nil)) nil)
((convergent_opp formula-decl nil convergence_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" convergence_set nil)
(T formal-type-decl nil sigma_set nil))
nil))
(sigma_opp 0
(sigma_opp-1 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)
((convergent? const-decl "bool" convergence_set nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sigma_set nil)
(sigma_scal formula-decl nil sigma_set nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(sigma_plus_TCC1 0
(sigma_plus_TCC1-1 nil 3405672135
("" (skosimp) (("" (rewrite "convergent_plus") nil nil)) nil)
((convergent_plus formula-decl nil convergence_set nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" convergence_set nil)
(T formal-type-decl nil sigma_set nil))
nil))
(sigma_plus 0
(sigma_plus-1 nil 3406446563
("" (skosimp)
(("" (expand "sigma")
((""
(lemma "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"
(lemma "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"
(case-replace
"sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1)),
nonzero_elts(f!1, X!1)),
f!1)=0")
(("1" (replace -2)
(("1" (hide -1 -2)
(("1"
(lemma "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"
(case-replace
"sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1)),
nonzero_elts(g!1, X!1)),
g!1)=0")
(("1" (replace -2)
(("1" (hide -1 -2)
(("1"
(lemma "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"
(split -1)
(("1"
(case-replace
"sigma_countable.sigma(difference(union(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1)),
nonzero_elts(f!1 + g!1, X!1)),
f!1 + g!1)=0")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(lemma
"sigma_eq"
("X"
"difference(union(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1)),
nonzero_elts(f!1 + g!1, X!1))"
"f"
"f!1+g!1"
"g"
"lambda t:0"))
(("1"
(rewrite
"sigma_countable.sigma_zero")
(("1"
(assert)
(("1"
(hide 2)
(("1"
(skosimp)
(("1"
(typepred "t!1")
(("1"
(expand "+ ")
(("1"
(expand
"difference")
(("1"
(expand "union")
(("1"
(expand
"nonzero_elts")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(case-replace
"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"
(hide 2)
(("2"
(rewrite
"countable_convergence.convergent_zero")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(case-replace
"difference(union(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1)),
nonzero_elts(g!1, X!1))=difference(nonzero_elts(f!1, X!1),
nonzero_elts(g!1, X!1))")
(("1"
(lemma "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"
(hide-all-but 1)
(("1"
(skosimp)
(("1"
(typepred "t!1")
(("1"
(expand "difference")
(("1"
(expand "member")
(("1"
(expand "nonzero_elts")
(("1"
(flatten)
(("1"
(assert)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.85 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
