Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: finite_enumeration.prf Sprache: Lisp

Original von: PVS^©

(absconv_series_aux
(extract_bij_TCC1 0
  (extract_bij_TCC1-1 nil 3323226707
   ("" (expand "fullset")
    (("" (expand "image")
      (("" (skosimp*)
        (("" (typepred "f!1")
          (("" (typepred "x1!1") (("" (inst + "x1!1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((image const-decl "set[R]" function_image nil)
    (extraction type-eq-decl nil sequence_props "analysis/")
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (fullset const-decl "set" sets nil))
   shostak))
(extract_bij 0
  (extract_bij-1 nil 3323226570
   ("" (skosimp)
    (("" (expand "bijective?")
      (("" (typepred "f!1")
        (("" (expand "strict_increasing?")
          (("" (split)
            (("1" (expand "injective?")
              (("1" (skosimp)
                (("1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1"))
                  (("1" (split -1)
                    (("1" (inst - "x1!1" "x2!1")
                      (("1" (assert) nil nil)) nil)
                     ("2" (propax) nil nil)
                     ("3" (inst - "x2!1" "x1!1")
                      (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "surjective?")
              (("2" (skosimp*)
                (("2" (typepred "y!1")
                  (("2" (expand "fullset")
                    (("2" (expand "image")
                      (("2" (skosimp)
                        (("2" (inst + "x!1") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (fullset const-decl "set" sets nil)
    (image const-decl "set[R]" function_image nil)
    (set type-eq-decl nil sets nil)
    (TRUE const-decl "bool" booleans nil)
    (injective? const-decl "bool" functions nil)
    (trich_lt formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (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)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (extraction type-eq-decl nil sequence_props "analysis/"))
   shostak))
(subseq_def 0
  (subseq_def-1 nil 3323227346
   ("" (expand "subseq") (("" (propax) nil nil)) nil)
   ((subseq const-decl "bool" sequence_props "analysis/")) shostak))
(inj_is_bij_extract 0
  (inj_is_bij_extract-1 nil 3323488489
   ("" (skosimp)
    (("" (typepred "inj!1")
      (("" (name "SS" "image(inj!1,fullset[nat])")
        ((""
          (lemma "infinite_injective_image[nat,(SS)]"
           ("S" "fullset[nat]" "f" "inj!1"))
          (("1" (name "F" "enum(SS)")
            (("1" (lemma "extract_bij" ("f" "F"))
              (("1"
                (case "bijective?[nat,(image(inj!1, fullset[nat]))](inj!1)")
                (("1"
                  (lemma
                   "bijective_inverse_exists[nat, (image(inj!1, fullset[nat]))]"
                   ("f" "inj!1"))
                  (("1" (expand "exists1")
                    (("1" (flatten)
                      (("1" (hide -2)
                        (("1" (skolem - "PSI")
                          (("1" (inst + "_" "F")
                            (("1"
                              (lemma
                               "bijective_inverse_exists[nat, ((image(F, fullset[nat])))]"
                               ("f" "F"))
                              (("1"
                                (expand "exists1")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (hide -2)
                                    (("1"
                                      (skolem - ("F_INV"))
                                      (("1"
                                        (lemma "enum_def" ("S" "SS"))
                                        (("1"
                                          (replace -6)
                                          (("1"
                                            (inst
                                             +
                                             "lambda (n:nat): IF SS(n) THEN inj!1(F_INV(n)) ELSE n ENDIF")
                                            (("1"
                                              (apply-extensionality
                                               2
                                               :hide?
                                               t)
                                              (("1"
                                                (expand "o" 1)
                                                (("1"
                                                  (lemma
                                                   "comp_inverse_left_alt"
                                                   ("f"
                                                    "F"
                                                    "g"
                                                    "F_INV"
                                                    "d"
                                                    "x!1"))
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (case-replace
                                                       "SS(F(x!1))")
                                                      (("1"
                                                        (replace
                                                         -2
                                                         1
                                                         rl)
                                                        (("1"
                                                          (expand
                                                           "fullset")
                                                          (("1"
                                                            (expand
                                                             "image")
                                                            (("1"
                                                              (inst
                                                               +
                                                               "x!1")
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "SS")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (replace -2 1)
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (lemma
                                               "bij_inv_is_bij_alt[nat, ((image(F, fullset[nat])))]"
                                               ("f" "F" "g" "F_INV"))
                                              (("1"
                                                (lemma
                                                 "composition_bijective[(SS),nat,(SS)]"
                                                 ("f1"
                                                  "F_INV"
                                                  "f2"
                                                  "inj!1"))
                                                (("1"
                                                  (expand "bijective?")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (split 1)
                                                      (("1"
                                                        (expand
                                                         "injective?")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (case-replace
                                                             "SS(x1!1)")
                                                            (("1"
                                                              (case-replace
                                                               "SS(x2!1)")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x1!1"
                                                                 "x2!1")
                                                                (("1"
                                                                  (expand
                                                                   "o")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                (("2"
                                                                  (replace
                                                                   -15
                                                                   1
                                                                   rl)
                                                                  (("2"
                                                                    (expand
                                                                     "image")
                                                                    (("2"
                                                                      (inst
                                                                       +
                                                                       "F_INV(x1!1)")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (expand
                                                                         "fullset")
                                                                        (("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (case-replace
                                                               "SS(x2!1)")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (replace
                                                                   -15
                                                                   1
                                                                   rl)
                                                                  (("1"
                                                                    (expand
                                                                     "image")
                                                                    (("1"
                                                                      (inst
                                                                       +
                                                                       "F_INV(x2!1)")
                                                                      (("1"
                                                                        (expand
                                                                         "fullset")
                                                                        (("1"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (expand
                                                         "surjective?")
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (case
                                                             "SS(y!1)")
                                                            (("1"
                                                              (inst
                                                               -3
                                                               "y!1")
                                                              (("1"
                                                                (skosimp)
                                                                (("1"
                                                                  (inst
                                                                   +
                                                                   "x!1")
                                                                  (("1"
                                                                    (expand
                                                                     "o")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (inst
                                                               +
                                                               "y!1")
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide-all-but
                                                   (-5 1 -8))
                                                  (("2"
                                                    (expand
                                                     "bijective?")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (split)
                                                        (("1"
                                                          (expand
                                                           "injective?")
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand
                                                           "surjective?")
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (typepred
                                                               "y!1")
                                                              (("2"
                                                                (replace
                                                                 -4
                                                                 -1
                                                                 rl)
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "y!1")
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (hide-all-but
                                                   (-1 -8 1 -2))
                                                  (("3"
                                                    (split 1)
                                                    (("1"
                                                      (skosimp)
                                                      (("1"
                                                        (replace -2)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand
                                                       "bijective?")
                                                      (("2"
                                                        (flatten)
                                                        (("2"
                                                          (split 1)
                                                          (("1"
                                                            (expand
                                                             "injective?")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (typepred
                                                                 "x1!1")
                                                                (("1"
                                                                  (typepred
                                                                   "x2!1")
                                                                  (("1"
                                                                    (replace
                                                                     -6
                                                                     -1
                                                                     rl)
                                                                    (("1"
                                                                      (replace
                                                                       -6
                                                                       -2
                                                                       rl)
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "x1!1"
                                                                         "x2!1")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "surjective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "y!1")
                                                                (("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (typepred
                                                                     "x!1")
                                                                    (("2"
                                                                      (replace
                                                                       -4
                                                                       -1)
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "x!1")
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2" (propax) nil nil))
                                              nil)
                                             ("3"
                                              (skosimp)
                                              (("3"
                                                (replace -2)
                                                (("3"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (propax) nil nil))
                              nil)
                             ("2"
                              (lemma "enum_strictly_monotone"
                               ("S" "SS"))
                              (("2"
                                (expand "strictly_monotone?")
                                (("2"
                                  (expand "strict_increasing?")
                                  (("2"
                                    (expand "F")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (propax) nil nil))
                  nil)
                 ("2" (expand "bijective?")
                  (("2" (flatten)
                    (("2" (split)
                      (("1" (hide-all-but (-5 1))
                        (("1" (expand "injective?")
                          (("1" (propax) nil nil)) nil))
                        nil)
                       ("2" (expand "surjective?")
                        (("2" (skosimp)
                          (("2" (typepred "y!1")
                            (("2" (expand "fullset")
                              (("2"
                                (expand "image")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (inst + "x!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (skosimp)
                  (("3" (expand "fullset")
                    (("3" (expand "image")
                      (("3" (inst + "x1!1") nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (lemma "enum_strictly_monotone" ("S" "SS"))
                (("2" (expand "strictly_monotone?")
                  (("2" (expand "strict_increasing?")
                    (("2" (expand "F" 1) (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "enumerable?")
              (("2" (replace -1 1 rl)
                (("2" (split 1)
                  (("1" (expand "bounded_below?")
                    (("1" (inst + "0")
                      (("1" (expand "lower_bound?")
                        (("1" (skosimp)
                          (("1" (expand "restrict")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "is_finite")
                    (("2" (skosimp)
                      (("2" (inst + "N!1" "f!1")
                        (("1" (hide 2 -3)
                          (("1" (expand "injective?")
                            (("1" (skosimp*)
                              (("1"
                                (typepred "x1!1")
                                (("1"
                                  (typepred "x2!1")
                                  (("1"
                                    (replace -7 -1 rl)
                                    (("1"
                                      (replace -7 -3 rl)
                                      (("1"
                                        (hide -2 -4 -7)
                                        (("1"
                                          (inst - "x1!1" "x2!1")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp)
                          (("2" (replace -2)
                            (("2" (case-replace "SS(x!1)")
                              (("1"
                                (assert)
                                (("1"
                                  (hide-all-but (-1 -3 1))
                                  (("1"
                                    (expand "image")
                                    (("1"
                                      (replace -2 -1 rl)
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (split 1)
              (("1" (skosimp)
                (("1" (expand "SS")
                  (("1" (expand "image")
                    (("1" (inst + "x1!1")
                      (("1" (expand "fullset") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "injective?") (("2" (propax) nil nil))
                nil))
              nil))
            nil)
           ("3" (hide-all-but -1)
            (("3" (expand "fullset")
              (("3" (expand "is_finite")
                (("3" (skosimp)
                  (("3"
                    (lemma
                     "composition_injective[below[N!1 + 1],nat, below[N!1]]")
                    (("3" (inst - "lambda (n:below[N!1+1]): n" "f!1")
                      (("1"
                        (lemma "injection_n_to_m"
                         ("n" "N!1+1" "m" "N!1"))
                        (("1" (split -1)
                          (("1" (assert) nil nil)
                           ("2"
                            (inst +
                             "f!1 o (LAMBDA (n: below[N!1 + 1]): n)")
                            nil nil))
                          nil))
                        nil)
                       ("2" (expand "injective?")
                        (("2" (hide -1) (("2" (skosimp) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (infinite_injective_image judgement-tcc nil infinite_image
     "sets_aux/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders "orders/")
    (bounded_below? const-decl "bool" bounded_orders "orders/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (extract_bij formula-decl nil absconv_series_aux nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (extraction type-eq-decl nil sequence_props "analysis/")
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (enum_strictly_monotone judgement-tcc nil integer_enumerations
     "orders/")
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "((image(F, fullset[nat])))"
     absconv_series_aux nil)
    (y!1 skolem-const-decl "(SS)" absconv_series_aux nil)
    (x2!1 skolem-const-decl "nat" absconv_series_aux nil)
    (x1!1 skolem-const-decl "nat" absconv_series_aux nil)
    (y!1 skolem-const-decl "nat" absconv_series_aux nil)
    (surjective? const-decl "bool" functions nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (O const-decl "T3" function_props nil)
    (comp_inverse_left_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (TRUE const-decl "bool" booleans nil)
    (F_INV skolem-const-decl "[((image(F, fullset[nat]))) -> nat]"
     absconv_series_aux nil)
    (inj!1 skolem-const-decl "(injective?[nat, nat])"
     absconv_series_aux nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (SS skolem-const-decl "set[nat]" absconv_series_aux nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (enum_def formula-decl nil integer_enumerations "orders/")
    (F skolem-const-decl "(strictly_monotone?)" absconv_series_aux nil)
    (exists1 const-decl "bool" exists1 nil)
    (bijective? const-decl "bool" functions nil)
    (strictly_monotone? const-decl "bool" integer_enumerations
     "orders/")
    (enum def-decl "T" integer_enumerations "orders/")
    (enumerable? const-decl "bool" integer_enumerations "orders/")
    (enum_strictly_monotone application-judgement
     "(strictly_monotone?)" countability "sets_aux/")
    (x1!1 skolem-const-decl "nat" absconv_series_aux nil)
    (N!1 skolem-const-decl "nat" absconv_series_aux nil)
    (f!1 skolem-const-decl "[({x | TRUE}) -> below[N!1]]"
     absconv_series_aux nil)
    (below type-eq-decl nil naturalnumbers nil)
    (injection_n_to_m formula-decl nil nat_fun_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (composition_injective judgement-tcc nil function_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (image const-decl "set[R]" function_image nil)
    (fullset const-decl "set" sets nil))
   shostak))
(nonneg_series_inj_conv 0
  (nonneg_series_inj_conv-1 nil 3323433884
   ("" (skosimp)
    (("" (lemma "inj_is_bij_extract" ("inj" "inj!1"))
      (("" (skosimp)
        (("" (replace -1)
          ((""
            (lemma "nonneg_series_bij_conv"
             ("nna" "nna!1" "phi" "phi!1"))
            (("" (assert)
              ((""
                (lemma "subseq_absconvergent"
                 ("a" "nna!1 o (phi!1 o f!1)" "bb" "nna!1 o phi!1"))
                (("1" (split -1)
                  (("1" (lemma "absconvergent_series_is_convergent")
                    (("1" (inst - "nna!1 o (phi!1 o f!1)") nil nil))
                    nil)
                   ("2" (hide-all-but 1)
                    (("2" (expand "subseq")
                      (("2" (inst + "f!1")
                        (("2" (skosimp)
                          (("2" (expand "o") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "o")
                  (("2" (expand "absconvergent?")
                    (("2" (expand "abs" 1)
                      (("2" (hide-all-but (-1 1))
                        (("2"
                          (case-replace
                           "(LAMBDA (n: nat): abs(nna!1(phi!1(n)))) = (LAMBDA (x: nat): nna!1(phi!1(x)))")
                          (("2" (hide-all-but 1)
                            (("2" (apply-extensionality :hide? t)
                              (("1"
                                (expand "abs")
                                (("1" (propax) nil nil))
                                nil)
                               ("2"
                                (skosimp)
                                (("2"
                                  (typepred "nna!1(phi!1(x!1))")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions 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)
    (inj_is_bij_extract formula-decl nil absconv_series_aux nil)
    (abs const-decl "sequence[real]" series "series/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nna!1 skolem-const-decl "sequence[nnreal]" absconv_series_aux nil)
    (phi!1 skolem-const-decl "(bijective?[nat, nat])"
     absconv_series_aux nil)
    (f!1 skolem-const-decl "extraction" absconv_series_aux nil)
    (absconvergent_series_is_convergent judgement-tcc nil
     absconv_series "series/")
    (subseq const-decl "bool" sequence_props "analysis/")
    (subseq_absconvergent formula-decl nil absconv_series "series/")
    (O const-decl "T3" function_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (extraction type-eq-decl nil sequence_props "analysis/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (nonneg_series_bij_conv formula-decl nil series_lems "series/")
    (nnreal type-eq-decl nil real_types nil)
    (sequence type-eq-decl nil sequences nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
(nonneg_series_inj_limit_TCC1 0
  (nonneg_series_inj_limit_TCC1-1 nil 3324005149
   ("" (skosimp)
    (("" (lemma "nonneg_series_inj_conv" ("nna" "nna!1" "inj" "inj!1"))
      (("" (assert) nil nil)) nil))
    nil)
   ((sequence type-eq-decl nil sequences nil)
    (nnreal type-eq-decl nil real_types nil)
    (injective? const-decl "bool" functions 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)
    (nonneg_series_inj_conv formula-decl nil absconv_series_aux nil))
   shostak))
(nonneg_series_inj_limit 0
  (nonneg_series_inj_limit-1 nil 3324004516
   ("" (skosimp)
    (("" (lemma "nonneg_series_inj_conv" ("nna" "nna!1" "inj" "inj!1"))
      (("" (assert)
        (("" (lemma "inj_is_bij_extract" ("inj" "inj!1"))
          (("" (skosimp)
            (("" (replace -1)
              (("" (hide -1)
                ((""
                  (lemma "nonneg_series_bij_conv"
                   ("nna" "nna!1" "phi" "phi!1"))
                  ((""
                    (lemma "nonneg_series_bij_limit"
                     ("nna" "nna!1" "phi" "phi!1"))
                    (("" (assert)
                      ((""
                        (lemma "nonneg_subseq"
                         ("nna" "nna!1 o (phi!1 o f!1)" "nnb"
                          "nna!1 o phi!1" "nny"
                          "limit(series(nna!1 o phi!1))"))
                        (("1" (split -1)
                          (("1" (skosimp)
                            (("1" (replace -3)
                              (("1"
                                (rewrite "limit_equiv" -1)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (rewrite "subseq_def" 1)
                              (("2"
                                (inst + "f!1")
                                (("2"
                                  (expand "o")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (hide 2)
                            (("3" (rewrite "limit_equiv" 1) nil nil))
                            nil))
                          nil)
                         ("2"
                          (lemma "limit_nonneg"
                           ("nna" "series(nna!1 o phi!1)"))
                          (("1" (assert) nil nil)
                           ("2" (hide 2 3)
                            (("2" (expand "o")
                              (("2"
                                (expand "series")
                                (("2"
                                  (hide-all-but 1)
                                  (("2"
                                    (induct "x1")
                                    (("1"
                                      (expand "sigma")
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (skosimp*)
                                      (("2"
                                        (expand "sigma" 1)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sequence type-eq-decl nil sequences nil)
    (nnreal type-eq-decl nil real_types nil)
    (injective? const-decl "bool" functions 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)
    (nonneg_series_inj_conv formula-decl nil absconv_series_aux nil)
    (inj_is_bij_extract formula-decl nil absconv_series_aux nil)
    (nonneg_series_bij_conv formula-decl nil series_lems "series/")
    (bijective? const-decl "bool" functions nil)
    (limit_nonneg formula-decl nil series_lems "series/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sigma_0_neg formula-decl nil sigma_nat "reals/")
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (limit_equiv formula-decl nil convergence_ops "analysis/")
    (subseq_def formula-decl nil absconv_series_aux nil)
    (nonneg_subseq formula-decl nil absconv_series "series/")
    (O const-decl "T3" function_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (extraction type-eq-decl nil sequence_props "analysis/")
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (limit const-decl "real" convergence_sequences "analysis/")
    (series const-decl "sequence[real]" series "series/")
    (nonneg_series_bij_limit formula-decl nil series_lems "series/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(abs_series_inj_conv 0
  (abs_series_inj_conv-2 nil 3462016056
   ("" (skosimp)
    (("" (typepred "aa!1")
      ((""
        (name "AA"
              "lambda (n:nat): IF aa!1(n) >= 0 THEN aa!1(n) ELSE 0 ENDIF")
        ((""
          (name "BB"
                "lambda (n:nat): IF aa!1(n) < 0 THEN -aa!1(n) ELSE 0 ENDIF")
          (("" (case "aa!1=AA-BB")
            (("1" (case "convergent?(series(AA))")
              (("1" (case "convergent?(series(BB))")
                (("1"
                  (lemma "nonneg_series_inj_conv"
                   ("nna" "AA" "inj" "inj!1"))
                  (("1" (assert)
                    (("1"
                      (lemma "nonneg_series_inj_conv"
                       ("nna" "BB" "inj" "inj!1"))
                      (("1" (assert)
                        (("1"
                          (lemma "series_sum_conv"
                           ("a" "AA o inj!1" "b" "-(BB o inj!1)"))
                          (("1" (split -1)
                            (("1" (expand "o")
                              (("1"
                                (replace -6 1)
                                (("1"
                                  (expand "-")
                                  (("1"
                                    (expand "+")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but (-2 1))
                              (("2"
                                (expand "o")
                                (("2" (propax) nil nil))
                                nil))
                              nil)
                             ("3" (hide-all-but (-1 1))
                              (("3"
                                (assert)
                                (("3"
                                  (case-replace
                                   "-1 * series(BB o inj!1) = series(-(BB o inj!1))")
                                  (("1"
                                    (hide-all-but 1)
                                    (("1"
                                      (expand "o")
                                      (("1"
                                        (lemma
                                         "scal_series_conv"
                                         ("a" "BB o inj!1" "c" "-1"))
                                        (("1"
                                          (split -1)
                                          (("1"
                                            (case-replace
                                             "-1 * series(BB o inj!1) = series(-(LAMBDA (x: nat): BB(inj!1(x))))")
                                            (("1"
                                              (hide -1 2)
                                              (("1"
                                                (apply-extensionality
                                                 1
                                                 :hide?
                                                 t)
                                                (("1"
                                                  (expand "-")
                                                  (("1"
                                                    (rewrite
                                                     "series_scal"
                                                     1)
                                                    (("1"
                                                      (expand "o")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2)
                                            (("2"
                                              (lemma
                                               "nonneg_series_inj_conv"
                                               ("nna"
                                                "BB"
                                                "inj"
                                                "inj!1"))
                                              (("2"
                                                (split -1)
                                                (("1"
                                                  (expand
                                                   "convergent?")
                                                  (("1"
                                                    (skosimp)
                                                    (("1"
                                                      (inst + "l!1")
                                                      (("1"
                                                        (expand
                                                         "convergence")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "epsilon!1")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "n!1")
                                                                (("1"
                                                                  (skosimp)
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "i!1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "o ")
                                                                        (("1"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (typepred "aa!1")
                                                    (("2"
                                                      (expand
                                                       "absconvergent?")
                                                      (("2"
                                                        (lemma
                                                         "comparison_test"
                                                         ("b"
                                                          "abs(aa!1)"
                                                          "a"
                                                          "BB"))
                                                        (("2"
                                                          (split -1)
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil)
                                                           ("3"
                                                            (hide-all-but
                                                             1)
                                                            (("3"
                                                              (skosimp)
                                                              (("3"
                                                                (expand
                                                                 "BB")
                                                                (("3"
                                                                  (expand
                                                                   "abs")
                                                                  (("3"
                                                                    (expand
                                                                     "abs")
                                                                    (("3"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.134 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.