| products/sources/formale sprachen/PVS/sigma_set/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: convergence_set.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(convergence_set
(convergent_zero 0 (convergent_zero-1 nil 3406348940 ("" (skosimp) (("" (expand "convergent?") (("" (case-replace "nonzero_elts(LAMBDA t: 0, X!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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (countable_emptyset formula-decl nil countable_props "sets_aux/") (convergent_empty formula-decl nil countable_convergence 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 convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (convergent_plus 0 (convergent_plus-1 nil 3406349137 ("" (skosimp) (("" (expand "convergent?") (("" (flatten) (("" (split) (("1" (lemma "countable_subset" ("S" "nonzero_elts(f!1 + g!1, X!1)" "Count" "union(nonzero_elts(f!1, X!1),nonzero_elts(g!1, X!1))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "nonzero_elts") (("2" (expand "union") (("2" (expand "member") (("2" (skosimp) (("2" (expand "+") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "countable_union" ("Count1" "nonzero_elts(f!1, X!1)" "Count2" "nonzero_elts(g!1, X!1)")) (("2" (propax) nil nil)) nil)) nil) ("2" (case "subset?(nonzero_elts(f!1 + g!1, X!1),union(nonzero_elts(f!1, X!1),nonzero_ (("1" (name-replace "FX" "nonzero_elts(f!1, X!1)") (("1" (name-replace "GX" "nonzero_elts(g!1, X!1)") (("1" (name-replace "FGX" "nonzero_elts(f!1+g!1, X!1)") (("1" (lemma "countable_union" ("Count1" "FX" "Count2" "GX")) (("1" (lemma "convergent_disjoint_union" ("g" "f!1" "X" "FX" "Y" "difference(union(FX, GX),FX)")) (("1" (lemma "convergent_disjoint_union" ("g" "g!1" "X" "GX" "Y" "difference(union(FX, GX),GX)")) (("1" (replace -6) (("1" (replace -8) (("1" (case-replace "union(GX, difference(union(FX, GX), GX))=union(FX, GX)") (("1" (hide -1) (("1" (case-replace "union(FX, difference(union(FX, GX), FX))=union(FX, GX)") (("1" (hide -1) (("1" (split -1) (("1" (split -2) (("1" (lemma "convergent_plus" ("X" "union(FX,GX)" "f" "f!1" "g" "g!1")) (("1" (assert) (("1" (lemma "convergent_subset" ("X" "FGX" "Y" "union(FX, GX)" "g" "f!1+g!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (lemma "convergent_zeros" ("g" "f!1" "X" "difference(union(FX, GX), FX)")) (("3" (assert) (("3" (hide 2) (("3" (skosimp) (("3" (typepred "t!1") (("3" (hide-all-but (-1 1)) (("3" (expand "FX") (("3" (expand "nonzero_elts") (("3" (expand "union") (("3" (expand "difference") (("3" (expand "member") (("3" (flatten) (("3" (expand "GX") (("3" (expand "nonzero_elts") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (hide -1 2) (("3" (lemma "convergent_zeros" ("g" "g!1" "X" "difference(union(FX, GX), GX)")) (("3" (assert) (("3" (hide-all-but 1) (("3" (skosimp) (("3" (typepred "t!1") (("3" (expand "GX") (("3" (expand "FX") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil 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" (rewrite "countable_difference") nil nil)) nil) ("2" (rewrite "countable_difference") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_elts") (("2" (expand "union") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "+ ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (countable_union judgement-tcc nil countable_props "sets_aux/") (subset? const-decl "bool" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (countable_subset formula-decl nil countability "sets_aux/") (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) (nonzero_elts const-decl "set[T]" convergence_set nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (union const-decl "set" sets nil) (T formal-type-decl nil convergence_set nil) (= const-decl "[T, T -> boolean]" equalities nil) (convergent_disjoint_union formula-decl nil countable_convergence nil) (difference const-decl "set" sets nil) (countable_difference judgement-tcc nil countable_props "sets_aux/") (/= const-decl "boolean" notequal nil) (GX skolem-const-decl "set[T]" convergence_set nil) (FX skolem-const-decl "set[T]" convergence_set nil) (NOT const-decl "[bool -> bool]" booleans nil) (convergent_zeros formula-decl nil countable_convergence nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (convergent_plus formula-decl nil countable_convergence nil) (convergent_subset formula-decl nil countable_convergence nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) shostak)) (convergent_scal 0 (convergent_scal-1 nil 3406349233 ("" (skosimp) (("" (expand "convergent?") (("" (flatten) (("" (case-replace "a!1=0") (("1" (case-replace "nonzero_elts(0 * f!1, X!1)=emptyset[T]") (("1" (rewrite "countable_emptyset") (("1" (rewrite "convergent_empty") nil nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "nonzero_elts") (("2" (flatten) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "nonzero_elts(a!1 * f!1, X!1)=nonzero_elts(f!1, X!1)") (("1" (assert) (("1" (hide -1 -2) (("1" (lemma "convergent_scal" ("X" "nonzero_elts(f!1, X!1)" "a" "a!1" "f" "f!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (apply-extensionality :hide? t) (("2" (expand "nonzero_elts") (("2" (expand "*") (("2" (assert) (("2" (case-replace "f!1(x!1)=0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (real_times_real_is_real application-judgement "real" reals nil) (countable_emptyset formula-decl nil countable_props "sets_aux/") (convergent_empty formula-decl nil countable_convergence nil) (emptyset const-decl "set" sets nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (nonzero_elts const-decl "set[T]" convergence_set nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-type-decl nil convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (convergent_scal formula-decl nil countable_convergence nil)) shostak)) (convergent_opp 0 (convergent_opp-1 nil 3406350311 ("" (skosimp) (("" (lemma "convergent_scal" ("X" "X!1" "f" "f!1" "a" "-1")) (("" (assert) (("" (case-replace "-1*f!1=-f!1") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (expand "*") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 convergence_set nil) (convergent_scal formula-decl nil convergence_set nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (convergent_diff 0 (convergent_diff-1 nil 3406350375 ("" (skosimp) (("" (lemma "convergent_opp" ("X" "X!1" "f" "g!1")) (("" (assert) (("" (lemma "convergent_plus" ("X" "X!1" "f" "f!1" "g" "-g!1")) (("" (assert) (("" (case-replace "f!1 + -g!1=f!1 - g!1") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (expand "+") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 convergence_set nil) (convergent_opp formula-decl nil convergence_set nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (convergent_plus formula-decl nil convergence_set nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (convergent_le 0 (convergent_le-1 nil 3406357616 ("" (skosimp) (("" (expand "convergent?") (("" (flatten) (("" (case "subset?(nonzero_elts(g!1, X!1),nonzero_elts(f!1, X!1))") (("1" (lemma "countable_subset" ("S" "nonzero_elts(g!1, X!1)" "Count" "nonzero_elts(f!1, X!1)")) (("1" (assert) (("1" (lemma "convergent_subset" ("X" "nonzero_elts(g!1, X!1)" "Y" "nonzero_elts(f!1, X!1)" "g" "f!1")) (("1" (assert) (("1" (lemma "convergent_le" ("g" "g!1" "f" "f!1" "X" "nonzero_elts(g!1, X!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "subset?") (("2" (expand "nonzero_elts") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (subset? 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) (T formal-type-decl nil convergence_set nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (convergent_le formula-decl nil countable_convergence nil) (convergent_subset formula-decl nil countable_convergence nil) (countable_subset formula-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (convergent_empty 0 (convergent_empty-1 nil 3406350597 ("" (skosimp) (("" (expand "convergent?") (("" (case-replace "nonzero_elts(g!1, emptyset[T])=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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (countable_emptyset formula-decl nil countable_props "sets_aux/") (convergent_empty formula-decl nil countable_convergence 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 convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (convergent_singleton 0 (convergent_singleton-1 nil 3406350738 ("" (skosimp) (("" (expand "convergent?") (("" (expand "absconvergent?") (("" (case "g!1(t!1)=0") (("1" (case-replace "nonzeros(g!1, singleton(t!1))=emptyset[real]") (("1" (assert) (("1" (rewrite "countable_emptyset") nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "nonzeros") (("2" (expand "extend") (("2" (prop) (("2" (skosimp) (("2" (expand "singleton") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "nonzeros(g!1, singleton(t!1)) = singleton(g!1(t!1))") (("1" (hide -1) (("1" (rewrite "countable_singleton") (("1" (flatten) (("1" (rewrite "finite_singleton") nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (expand "nonzeros") (("2" (expand "extend") (("2" (case-replace "x!1=g!1(t!1)") (("1" (assert) (("1" (inst + "t!1") nil nil)) nil) ("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" convergence_set nil) (convergent? const-decl "bool" countable_convergence nil)) shostak)) (convergent_subset 0 (convergent_subset-1 nil 3406356738 ("" (skosimp) (("" (expand "convergent?") (("" (flatten) (("" (case "subset?(nonzero_elts(g!1, X!1),nonzero_elts(g!1, Y!1))") (("1" (lemma "countable_subset" ("S" "nonzero_elts(g!1, X!1)" "Count" "nonzero_elts(g!1, Y!1)")) (("1" (assert) (("1" (lemma "convergent_subset" ("X" "nonzero_elts(g!1, X!1)" "Y" "nonzero_elts(g!1, Y!1)" "g" "g!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "subset?") (("2" (expand "nonzero_elts") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (subset? 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) (T formal-type-decl nil convergence_set 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/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (member const-decl "bool" sets nil)) shostak)) (convergent_intersection 0 (convergent_intersection-1 nil 3406353573 ("" (skosimp) (("" (split) (("1" (lemma "convergent_subset" ("X" "intersection(X!1, Y!1)" "Y" "X!1" "g" "g!1")) (("1" (rewrite "intersection_subset1") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "convergent_subset" ("X" "intersection(X!1, Y!1)" "Y" "Y!1" "g" "g!1")) (("2" (rewrite "intersection_commutative") (("2" (rewrite "intersection_subset1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((intersection_subset1 formula-decl nil sets_lemmas nil) (convergent_subset formula-decl nil convergence_set nil) (T formal-type-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) (intersection 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) (intersection_commutative formula-decl nil sets_lemmas nil)) shostak)) (convergent_difference 0 (convergent_difference-1 nil 3406353696 ("" (skosimp) (("" (lemma "convergent_subset" ("X" "difference(X!1, Y!1)" "Y" "X!1" "g" "g!1")) (("" (rewrite "difference_subset") (("" (assert) nil nil)) nil)) nil)) 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) (T formal-type-decl nil convergence_set nil) (convergent_subset formula-decl nil convergence_set nil) (difference_subset formula-decl nil sets_lemmas nil)) shostak)) (convergent_disjoint_union 0 (convergent_disjoint_union-1 nil 3406356330 ("" (skosimp) (("" (expand "convergent?") (("" (flatten) (("" (case-replace "nonzero_elts(g!1, union(X!1, Y!1))=union(nonzero_elts(g!1, X!1),nonzero_elts(g! (("1" (hide -1) (("1" (rewrite "countable_union") (("1" (lemma "convergent_disjoint_union" ("X" "nonzero_elts(g!1, X!1)" "Y" "nonzero_elts(g!1, Y!1)" "g" "g!1")) (("1" (assert) (("1" (hide-all-but (-1 1)) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "nonzero_elts") (("1" (skosimp) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "nonzero_elts") (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "g!1(x!1)=0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (T formal-type-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) (= const-decl "[T, T -> boolean]" equalities 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) (union const-decl "set" sets nil) (countable_union judgement-tcc nil countable_props "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (convergent_disjoint_union formula-decl nil countable_convergence nil)) shostak)) (convergent_union 0 (convergent_union-1 nil 3406355915 ("" (skosimp) (("" (lemma "convergent_difference" ("X" "X!1" "Y" "Y!1" "g" "g!1")) (("" (assert) (("" (lemma "difference_disjoint" ("a" "Y!1" "b" "X!1")) (("" (lemma "convergent_disjoint_union" ("X" "Y!1" "Y" "difference(X!1, Y!1)" "g" "g!1")) (("" (assert) (("" (rewrite "union_difference" -1 :dir rl) (("" (rewrite "union_commutative") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 convergence_set nil) (convergent_difference formula-decl nil convergence_set nil) (difference_disjoint formula-decl nil sets_lemmas nil) (union_commutative formula-decl nil sets_lemmas nil) (union_difference formula-decl nil sets_lemmas nil) (convergent_disjoint_union formula-decl nil convergence_set nil) (difference const-decl "set" sets nil)) shostak)) (convergent_add 0 (convergent_add-1 nil 3406355712 ("" (skosimp) (("" (rewrite "add_as_union") (("" (lemma "convergent_union" ("g" "g!1" "X" "X!1" "Y" "singleton(t!1)")) (("" (assert) (("" (hide-all-but 1) (("" (expand "convergent?") (("" (case-replace "g!1(t!1)=0") (("1" (case-replace "nonzero_elts(g!1, singleton(t!1))=emptyset[T]") (("1" (rewrite "countable_emptyset") (("1" (rewrite "countable_convergence.convergent_empty") nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (case-replace "nonzero_elts(g!1, singleton(t!1))=singleton(t!1)") (("1" (rewrite "countable_singleton") (("1" (rewrite "countable_convergence.convergent_singleton") nil nil)) nil) ("2" (hide 3) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add_as_union formula-decl nil sets_lemmas 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 convergence_set nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" convergence_set nil) (nonempty_union2 application-judgement "(nonempty?)" sets nil) (convergent? const-decl "bool" convergence_set nil) (convergent_singleton formula-decl nil countable_convergence nil) (countable_singleton formula-decl nil countable_props "sets_aux/") (emptyset const-decl "set" sets nil) (nonzero_elts const-decl "set[T]" convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" convergence_set nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (convergent_empty formula-decl nil countable_convergence nil) (countable_emptyset formula-decl nil countable_props "sets_aux/") (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (convergent_union formula-decl nil convergence_set nil) (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)) shostak)) (convergent_remove 0 (convergent_remove-1 nil 3406355843 ("" (skosimp) (("" (lemma "convergent_subset" ("X" "remove(t!1, X!1)" "Y" "X!1" "g" "g!1")) (("" (rewrite "subset_remove") (("" (assert) nil nil)) nil)) nil)) 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) (remove 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) (T formal-type-decl nil convergence_set nil) (convergent_subset formula-decl nil convergence_set nil) (subset_remove formula-decl nil sets_lemmas nil)) shostak)) (convergent_abs 0 (convergent_abs-1 nil 3406355601 ("" (skosimp) (("" (expand "convergent?") (("" (case-replace "nonzero_elts(abs(g!1), X!1)=nonzero_elts(g!1, X!1)") (("1" (hide -1) (("1" (rewrite "convergent_abs") (("1" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "nonzero_elts") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" convergence_set nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (/= const-decl "boolean" notequal nil) (minus_even_is_even application-judgement "even_int" integers nil) (convergent_abs formula-decl nil countable_convergence nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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 convergence_set nil)) shostak))) ¤ Dauer der Verarbeitung: 0.53 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.Bot Zugriff |
