Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: composition_continuous.pvs Sprache: Lisp

Original von: PVS^©

(countable_convergence
(convergent?_TCC1 0
  (convergent?_TCC1-1 nil 3322366680
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (lemma "countably_infinite_def" ("S" "X!1"))
        (("" (assert) nil nil)) nil))
      nil))
    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 countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (countably_infinite_def formula-decl nil countable_props
     "sets_aux/"))
   shostak))
(convergent_zero 0
  (convergent_zero-1 nil 3323142075
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (expand "o")
            (("" (expand "absconvergent?")
              (("" (expand "abs")
                (("" (expand "abs")
                  (("" (rewrite "zero_series_conv") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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 countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (zero_series_conv formula-decl nil series "series/")
    (abs const-decl "sequence[real]" series "series/")
    (O const-decl "T3" function_props nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_plus 0
  (convergent_plus-1 nil 3351595333
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (assert)
            (("" (expand "absconvergent?")
              (("" (name-replace "DX" "denumerable_enumeration(X!1)")
                ((""
                  (lemma "sum_absconvergent"
                   ("aa" "f!1 o DX" "bb" "g!1 o DX"))
                  (("1" (expand "absconvergent?")
                    (("1" (expand "o ")
                      (("1" (expand "+") (("1" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (expand "o")
                    (("2" (expand "absconvergent?")
                      (("2" (propax) nil nil)) nil))
                    nil)
                   ("3" (expand "o")
                    (("3" (expand "absconvergent?")
                      (("3" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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 countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (sum_absconvergent formula-decl nil absconv_series "series/")
    (sequence type-eq-decl nil sequences nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (O const-decl "T3" function_props nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_scal 0
  (convergent_scal-1 nil 3351595652
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (assert)
          (("" (name-replace "DX" "denumerable_enumeration(X!1)")
            ((""
              (lemma "scal_absconvergent" ("aa" "f!1 o DX" "x" "a!1"))
              (("1" (expand "o")
                (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence nil)
    (O const-decl "T3" function_props nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (sequence type-eq-decl nil sequences nil)
    (scal_absconvergent formula-decl nil absconv_series "series/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities 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 countable_convergence nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(convergent_opp 0
  (convergent_opp-1 nil 3351596230
   ("" (skosimp)
    (("" (lemma "convergent_scal" ("X" "X!1" "f" "f!1" "a" "-1"))
      (("" (expand "-") (("" (expand "*") (("" (assert) 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)
    (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 countable_convergence nil)
    (convergent_scal formula-decl nil countable_convergence nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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/")
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
(convergent_diff 0
  (convergent_diff-1 nil 3351596280
   ("" (skosimp)
    (("" (lemma "convergent_opp" ("X" "X!1" "f" "g!1"))
      (("" (assert)
        (("" (lemma "convergent_plus" ("X" "X!1" "f" "f!1" "g" "-g!1"))
          (("" (assert)
            (("" (expand "-")
              (("" (expand "+") (("" (assert) 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)
    (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 countable_convergence nil)
    (convergent_opp formula-decl nil countable_convergence nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (convergent_plus formula-decl nil countable_convergence nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak))
(convergent_le 0
  (convergent_le-1 nil 3351599438
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (assert)
        (("" (expand "absconvergent?")
          (("" (name-replace "DX" "denumerable_enumeration(X!1)")
            ((""
              (lemma "comparison_test"
               ("b" "abs(f!1 o DX)" "a" "abs(g!1 o DX)"))
              (("" (split -1)
                (("1" (propax) nil nil) ("2" (propax) nil nil)
                 ("3" (hide-all-but (-1 1))
                  (("3" (skosimp)
                    (("3" (inst - "DX(n!1)") (("3" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((absconvergent? const-decl "bool" absconv_series "series/")
    (comparison_test formula-decl nil series "series/")
    (sequence type-eq-decl nil sequences nil)
    (abs const-decl "sequence[real]" series "series/")
    (O const-decl "T3" function_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities 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 countable_convergence nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_zeros 0
  (convergent_zeros-1 nil 3406442125
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (expand "absconvergent?")
            (("" (lemma "zero_series_conv")
              (("" (expand "o ")
                (("" (lemma "countably_infinite_def" ("S" "X!1"))
                  (("" (assert)
                    ((""
                      (case-replace "abs(LAMBDA (x: nat):
                              g!1(denumerable_enumeration(X!1)(x)))=lambda (x:nat): 0")
                      (("" (hide-all-but (1 -4 -1))
                        (("" (apply-extensionality :hide? t)
                          (("" (expand "abs")
                            ((""
                              (inst -
                               "denumerable_enumeration(X!1)(x!1)")
                              ((""
                                (replace -2)
                                ((""
                                  (expand "abs")
                                  (("" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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 countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (zero_series_conv formula-decl nil series "series/")
    (countably_infinite_def formula-decl nil countable_props
     "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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sequence type-eq-decl nil sequences nil)
    (abs const-decl "sequence[real]" series "series/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (O const-decl "T3" function_props nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_empty 0
  (convergent_empty-1 nil 3351591225
   ("" (skosimp)
    (("" (expand "convergent?") (("" (propax) nil nil)) nil)) 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]"
     countable_convergence nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_singleton 0
  (convergent_singleton-1 nil 3351591618
   ("" (skosimp*)
    (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" countable_convergence nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(convergent_subset 0
  (convergent_subset-1 nil 3323142263
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (case-replace "is_finite(Y!1)")
          (("1" (lemma "finite_subset" ("s" "X!1" "A" "Y!1"))
            (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)
           ("2" (assert)
            (("2" (typepred "X!1")
              (("2" (typepred "Y!1")
                (("2" (rewrite "countable_props.countable_card" -1)
                  (("2" (rewrite "countable_props.countable_card" -2)
                    (("2" (hide 1 2)
                      (("2"
                        (lemma "denumerable_enumeration_bij"
                         ("X" "X!1"))
                        (("2"
                          (lemma "denumerable_enumeration_bij"
                           ("X" "Y!1"))
                          (("2"
                            (name-replace "PHI_X"
                             "denumerable_enumeration(X!1)")
                            (("2"
                              (name-replace "PHI_Y"
                               "denumerable_enumeration(Y!1)")
                              (("2"
                                (expand "o")
                                (("2"
                                  (lemma
                                   "bijective_inverse_exists[nat, (X!1)]"
                                   ("f" "PHI_X"))
                                  (("1"
                                    (lemma
                                     "bijective_inverse_exists[nat, (Y!1)]"
                                     ("f" "PHI_Y"))
                                    (("1"
                                      (expand "exists1")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (skolem - ("PSI_Y"))
                                          (("1"
                                            (skolem - ("PSI_X"))
                                            (("1"
                                              (lemma
                                               "bij_inv_is_bij_alt[nat,(X!1)]"
                                               ("f"
                                                "PHI_X"
                                                "g"
                                                "PSI_X"))
                                              (("1"
                                                (lemma
                                                 "bij_inv_is_bij_alt[nat,(Y!1)]"
                                                 ("f"
                                                  "PHI_Y"
                                                  "g"
                                                  "PSI_Y"))
                                                (("1"
                                                  (case
                                                   "FORALL (a:sequence[real],inj:(injective?[nat,nat])):absconvergent?(a) => absconvergent?(a o inj)")
                                                  (("1"
                                                    (case
                                                     "injective?[nat,nat](PSI_Y o PHI_X)")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "g!1 o PHI_Y"
                                                       "PSI_Y o PHI_X")
                                                      (("1"
                                                        (split -2)
                                                        (("1"
                                                          (expand "o")
                                                          (("1"
                                                            (lemma
                                                             "comp_inverse_right_surj_alt[nat,(Y!1)]"
                                                             ("f"
                                                              "PHI_Y"
                                                              "g"
                                                              "PSI_Y"))
                                                            (("1"
                                                              (lemma
                                                               "extensionality"
                                                               ("f"
                                                                "LAMBDA (x_1: nat): g!1(PHI_Y(PSI_Y(PHI_X(x_1))))"
                                                                "g"
                                                                "LAMBDA (x: nat): g!1(PHI_X(x))"))
                                                              (("1"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (typepred
                                                                     "PHI_X(x!1)")
                                                                    (("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        -2
                                                                        -15
                                                                        1))
                                                                      (("2"
                                                                        (expand
                                                                         "subset?")
                                                                        (("2"
                                                                          (inst
                                                                           -3
                                                                           "PHI_X(x!1)")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "PHI_X(x!1)")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "bijective?")
                                                              (("2"
                                                                (flatten)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand "o ")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but
                                                       (-2 -12 -9 1))
                                                      (("2"
                                                        (expand
                                                         "bijective?")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (expand
                                                             "injective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (expand
                                                                 "o")
                                                                (("2"
                                                                  (inst
                                                                   -4
                                                                   "x1!1"
                                                                   "x2!1")
                                                                  (("2"
                                                                    (expand
                                                                     "subset?")
                                                                    (("2"
                                                                      (expand
                                                                       "member")
                                                                      (("2"
                                                                        (inst-cp
                                                                         -6
                                                                         "PHI_X(x1!1)")
                                                                        (("2"
                                                                          (inst
                                                                           -6
                                                                           "PHI_X(x2!1)")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (hide
                                                                               1
                                                                               -3
                                                                               -4)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "PHI_X(x1!1)"
                                                                                 "PHI_X(x2!1)")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (hide -1 -13 2)
                                                      (("3"
                                                        (skosimp)
                                                        (("3"
                                                          (expand
                                                           "subset?")
                                                          (("3"
                                                            (inst
                                                             -
                                                             "PHI_X(x1!1)")
                                                            (("3"
                                                              (expand
                                                               "member")
                                                              (("3"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (expand
                                                         "absconvergent?")
                                                        (("2"
                                                          (lemma
                                                           "abs_series_inj_conv"
                                                           ("aa"
                                                            "abs(a!1)"
                                                            "inj"
                                                            "inj!1"))
                                                          (("1"
                                                            (lemma
                                                             "extensionality"
                                                             ("f"
                                                              "abs(a!1) o inj!1"
                                                              "g"
                                                              "abs(a!1 o inj!1)"))
                                                            (("1"
                                                              (split
                                                               -1)
                                                              (("1"
                                                                (replace
                                                                 -1)
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (expand
                                                                     "abs")
                                                                    (("2"
                                                                      (expand
                                                                       "o")
                                                                      (("2"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "absconvergent?")
                                                            (("2"
                                                              (hide 2)
                                                              (("2"
                                                                (lemma
                                                                 "extensionality"
                                                                 ("f"
                                                                  "abs(a!1)"
                                                                  "g"
                                                                  "abs(abs(a!1))"))
                                                                (("2"
                                                                  (split
                                                                   -1)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (propax) nil nil))
                                    nil)
                                   ("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence nil)
    (T formal-type-decl nil countable_convergence nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (finite_subset formula-decl nil finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (countable_card formula-decl nil countable_props "sets_aux/")
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (bijective? const-decl "bool" functions nil)
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (sequence type-eq-decl nil sequences nil)
    (injective? const-decl "bool" functions nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (Y!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (PSI_Y skolem-const-decl "[(Y!1) -> nat]" countable_convergence
     nil)
    (X!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (PHI_X skolem-const-decl "[nat -> (X!1)]" countable_convergence
     nil)
    (extensionality formula-decl nil functions nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (surjective? const-decl "bool" functions nil)
    (comp_inverse_right_surj_alt formula-decl nil function_inverse_def
     nil)
    (abs_series_inj_conv formula-decl nil absconv_series_aux nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (abs const-decl "sequence[real]" series "series/")
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (O const-decl "T3" function_props nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (denumerable_enumeration_bij formula-decl nil
     denumerable_enumeration nil))
   shostak))
(convergent_intersection 0
  (convergent_intersection-1 nil 3351591237
   ("" (skosimp)
    (("" (split)
      (("1"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
        (("1" (assert)
          (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil))
        nil)
       ("2"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "Y!1" "g" "g!1"))
        (("2" (split)
          (("1" (propax) nil nil)
           ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)
           ("3" (propax) nil nil))
          nil))
        nil))
      nil))
    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)
    (countable_intersection1 application-judgement "countable_set[T]"
     countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (T formal-type-decl nil countable_convergence 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/")
    (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))
   shostak))
(convergent_difference 0
  (convergent_difference-1 nil 3351593239
   ("" (skosimp)
    ((""
      (lemma "convergent_subset"
       ("X" "difference(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
      (("" (assert) (("" (hide-all-but 1) (("" (grind) 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)
    (difference const-decl "set" 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 countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (countable_difference application-judgement "countable_set[T]"
     countable_convergence 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))
   shostak))
(convergent_disjoint_union 0
  (convergent_disjoint_union-2 nil 3462016397
   (""
    (case "FORALL (X:finite_set[T], Y: countable_set[T], g: [T -> real]):
               disjoint?(X, Y) AND convergent?(X)(g) AND convergent?(Y)(g) IMPLIES
                convergent?(union(X, Y))(g)")
    (("1" (skosimp)
      (("1" (expand "convergent?")
        (("1" (case-replace "is_finite(X!1)")
          (("1" (inst - "X!1" "Y!1" "g!1")
            (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)
           ("2" (assert)
            (("2" (case-replace "is_finite(Y!1)")
              (("1" (inst - "Y!1" "X!1" "g!1")
                (("1" (assert)
                  (("1" (split -2)
                    (("1" (rewrite "union_commutative")
                      (("1" (assert) nil nil)) nil)
                     ("2" (rewrite "union_commutative")
                      (("2" (assert) nil nil)) nil)
                     ("3" (hide-all-but (-2 1))
                      (("3" (expand "disjoint?")
                        (("3" (rewrite "intersection_commutative") nil
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (hide -1)
                    (("2" (expand "absconvergent?")
                      (("2"
                        (lemma "denumerable_enumeration_bij"
                         ("X" "X!1"))
                        (("2"
                          (lemma "denumerable_enumeration_bij"
                           ("X" "Y!1"))
                          (("2"
                            (lemma "denumerable_enumeration_bij"
                             ("X" "union(X!1,Y!1)"))
                            (("2"
                              (name-replace "DX"
                               "denumerable_enumeration(X!1)")
                              (("2"
                                (name-replace
                                 "DY"
                                 "denumerable_enumeration(Y!1)")
                                (("2"
                                  (name-replace
                                   "DXY"
                                   "denumerable_enumeration(union(X!1,Y!1))")
                                  (("2"
                                    (lemma
                                     "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                     ("f" "DXY"))
                                    (("1"
                                      (expand "exists1")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (skolem - ("CXY"))
                                          (("1"
                                            (lemma
                                             "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                             ("f" "DXY" "g" "CXY"))
                                            (("1"
                                              (name
                                               "PHI"
                                               "LAMBDA (n:nat): IF even?(n) THEN DX(n/2) ELSE DY((n-1)/2) ENDIF")
                                              (("1"
                                                (case
                                                 "bijective?[nat, (union(X!1, Y!1))](PHI)")
                                                (("1"
                                                  (hide -2)
                                                  (("1"
                                                    (case
                                                     "forall (a:sequence[real]): convergent?(series(a)) => convergent?(series(LAMBDA (n:nat): IF even?(n) THEN a(n/2) ELSE 0 ENDIF))")
                                                    (("1"
                                                      (case
                                                       "FORALL (a: sequence[real]):
                               convergent?(series(a)) =>
                                convergent?(series(LAMBDA (n: nat):
                                                    IF odd?(n) THEN a((n-1)/2) ELSE 0 ENDIF))")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "abs(g!1 o DY)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "abs(g!1 o DX)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "series_sum_conv"
                                                               ("a"
                                                                "(LAMBDA (n: nat):
                                               IF even?(n) THEN abs(g!1 o DX)(n / 2)
                                               ELSE 0
                                               ENDIF)"
                                                                "b"
                                                                "(LAMBDA (n: nat):
                                               IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                                               ELSE 0
                                               ENDIF)"))
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide
                                                                   -2
                                                                   -3)
                                                                  (("1"
                                                                    (lemma
                                                                     "extensionality"
                                                                     ("f"
                                                                      "((LAMBDA (n: nat):
                                                  IF even?(n) THEN abs(g!1 o DX)(n / 2)
                                                  ELSE 0
                                                  ENDIF)
                                                +
                                                (LAMBDA (n: nat):
                                                   IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                                                   ELSE 0
                                                   ENDIF))"
                                                                      "g"
                                                                      "abs(g!1 o PHI)"))
                                                                    (("1"
                                                                      (split
                                                                       -1)
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (hide
                                                                           -1)
                                                                          (("1"
                                                                            (lemma
                                                                             "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                                                             ("f"
                                                                              "PHI"))
                                                                            (("1"
                                                                              (expand
                                                                               "exists1")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (skolem
                                                                                   -
                                                                                   ("PSI"))
                                                                                  (("1"
                                                                                    (hide
                                                                                     -7
                                                                                     -2)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                                                                       ("f"
                                                                                        "PHI"
                                                                                        "g"
                                                                                        "PSI"))
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "composition_bijective[nat,(union(X!1, Y!1)),nat]"
                                                                                         ("f2"
                                                                                          "PSI"
                                                                                          "f1"
                                                                                          "DXY"))
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "comp_inverse_right_alt[nat, (union(X!1, Y!1))]"
                                                                                           ("f"
                                                                                            "PHI"
                                                                                            "g"
                                                                                            "PSI"))
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              -5
                                                                                              4))
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "abs_series_bij_conv_abs"
                                                                                               ("phi"
                                                                                                "PSI o DXY"
                                                                                                "aa"
                                                                                                "abs(g!1 o PHI)"))
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)")
                                                                                                  (("1"
                                                                                                    (hide-all-but
                                                                                                     (-2
                                                                                                      1))
                                                                                                    (("1"
                                                                                                      (apply-extensionality
                                                                                                       1
                                                                                                       :hide?
                                                                                                       t)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "o")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "abs")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "DXY(x!1)")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand
                                                                                                 "absconvergent?")
                                                                                                (("3"
                                                                                                  (hide-all-but
                                                                                                   (-3
                                                                                                    1))
                                                                                                  (("3"
                                                                                                    (case-replace
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.66 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.