products/Sources/formale Sprachen/PVS/reals/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©
(atanx
 (cauchy_ssmallreal_TCC1 0
  (cauchy_ssmallreal_TCC1-1 nil 3288497283
   ("" (expand "cauchy_ssmallreal?")
    (("" (inst + "0")
      (("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (ssmallreal nonempty-type-eq-decl nil atanx nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_ssmallreal? const-decl "bool" atanx nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   shostak))
 (subtype_TCC1 0
  (subtype_TCC1-1 nil 3288497283
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_ssmallreal?")
        (("" (skosimp*)
          (("" (expand "cauchy_real?") (("" (inst + "x!2") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_ssmallreal nonempty-type-eq-decl nil atanx nil)
    (cauchy_ssmallreal? const-decl "bool" atanx 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)
    (ssmallreal nonempty-type-eq-decl nil atanx nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   shostak))
 (cauchy_vsmallreal_TCC1 0
  (cauchy_vsmallreal_TCC1-1 nil 3288497283
   ("" (expand "cauchy_vsmallreal?")
    (("" (inst + "0")
      (("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (vsmallreal nonempty-type-eq-decl nil atanx nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_vsmallreal? const-decl "bool" atanx nil))
   shostak))
 (subtype_TCC2 0
  (subtype_TCC2-1 nil 3288497283
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_vsmallreal?")
        (("" (expand "cauchy_real?")
          (("" (skosimp*) (("" (inst + "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_vsmallreal nonempty-type-eq-decl nil atanx nil)
    (cauchy_vsmallreal? const-decl "bool" atanx 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)
    (cauchy_real? const-decl "bool" cauchy nil)
    (vsmallreal nonempty-type-eq-decl nil atanx nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (cauchy_atan_drx_series_TCC1 0
  (cauchy_atan_drx_series_TCC1-1 nil 3392689913
   ("" (skosimp)
    (("" (expand "cauchy_nzreal?")
      (("" (inst + "1+2*n!1")
        (("" (expand "cauchy_prop")
          (("" (skosimp)
            (("" (expand "cauchy_int") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_times_int_is_int application-judgement "int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (cauchy_int const-decl "cauchy_real" int 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)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers
     nil))
   nil))
 (cauchy_atan_drx_series_TCC2 0
  (cauchy_atan_drx_series_TCC2-1 nil 3392689913
   ("" (skosimp)
    (("" (hide 1)
      (("" (expand "cauchy_nzreal?")
        (("" (inst + "1+2*n!1")
          (("" (expand "cauchy_prop")
            (("" (skosimp)
              (("" (expand "cauchy_int") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_times_int_is_int application-judgement "int" integers nil))
   nil))
 (atan_series_lemma 0
  (atan_series_lemma-1 nil 3288496910
   ("" (expand "atan_series_coef")
    (("" (expand "cauchy_atan_drx_series")
      (("" (skosimp*)
        (("" (lemma "int_lemma" ("n" "1+2*n!1"))
          (("" (lemma "int_lemma" ("n" "1"))
            (("" (lemma "int_lemma" ("n" "-1"))
              (("" (assert)
                (("" (typepred "n!1")
                  (("" (lemma "expt_minus1" ("i" "n!1"))
                    (("" (case-replace "even?(n!1)")
                      (("1" (assert)
                        (("1" (flatten)
                          (("1" (replace -2)
                            (("1"
                              (lemma "div_lemma"
                               ("x"
                                "1"
                                "cx"
                                "cauchy_int(1)"
                                "nzy"
                                "1+2*n!1"
                                "nzcy"
                                "cauchy_int(1 + 2 * n!1)"))
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert)
                        (("2" (rewrite "even_or_odd")
                          (("2" (assert)
                            (("2" (replace -2)
                              (("2"
                                (lemma
                                 "div_lemma"
                                 ("x"
                                  "-1"
                                  "cx"
                                  "cauchy_int(-1)"
                                  "nzy"
                                  "1+2*n!1"
                                  "nzcy"
                                  "cauchy_int(1 + 2 * n!1)"))
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_atan_drx_series const-decl "cauchy_real" atanx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_lemma formula-decl nil int nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (even? const-decl "bool" integers nil)
    (div_lemma formula-decl nil div nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_int const-decl "cauchy_real" int nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (expt_minus1 formula-decl nil prelude_aux nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (atan_series_coef const-decl "rat" atan "trig_fnd/")
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (int_exp application-judgement "int" exponentiation nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_times_int_is_int application-judgement "int" integers nil))
   shostak))
 (cauchy_atan_drxx_TCC1 0
  (cauchy_atan_drxx_TCC1-1 nil 3288497284
   ("" (expand "cauchys_real?")
    (("" (inst + "atan_series_coef")
      (("" (expand "cauchys_prop")
        (("" (skosimp*)
          (("" (lemma "atan_series_lemma" ("n" "n!1"))
            (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (atan_series_coef const-decl "rat" atan "trig_fnd/")
    (atan_series_lemma formula-decl nil atanx nil)
    (cauchys_prop const-decl "bool" sum nil)
    (cauchys_real? const-decl "bool" sum nil))
   shostak))
 (cauchy_atan_drxx_prop_TCC1 0
  (cauchy_atan_drxx_prop_TCC1-1 nil 3288506197
   ("" (skosimp*) (("" (typepred "vsx!1") (("" (assert) nil nil)) nil))
    nil)
   ((vsmallreal nonempty-type-eq-decl nil atanx nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (cauchy_atan_drxx_prop_TCC2 0
  (cauchy_atan_drxx_prop_TCC2-1 nil 3288506197
   ("" (skosimp*)
    (("" (typepred "vsx!1")
      (("" (lemma "sqrt_eq_0")
        (("" (inst - "vsx!1") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((vsmallreal nonempty-type-eq-decl nil atanx nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (sqrt_eq_0 formula-decl nil sqrt "reals/"))
   shostak))
 (cauchy_atan_drxx_prop 0
  (cauchy_atan_drxx_prop-1 nil 3288524114
   ("" (skosimp*)
    (("" (typepred "vsx!1")
      (("" (expand "cauchy_atan_drxx")
        ((""
          (lemma "powerseries_lemma"
           ("x" "vsx!1" "cx" "cvsx!1" "xs" "atan_series_coef" "cxs"
            "cauchy_atan_drx_series"))
          (("" (replace -4)
            (("" (lemma "atan_series_lemma")
              (("" (replace -1)
                (("" (hide -1)
                  (("" (expand "cauchy_prop")
                    (("" (skosimp*)
                      (("" (inst -1 "2+p!1")
                        (("" (inst -1 "2+p!1")
                          (("" (flatten -1)
                            ((""
                              (name-replace "CPS"
                               "cauchy_powerseries(cvsx!1, cauchy_atan_drx_series, 2 + p!1)(2 + p!1)")
                              ((""
                                (case-replace "2^(2+p!1)=4*2^p!1")
                                (("1"
                                  (lemma
                                   "lemma_A2"
                                   ("r"
                                    "round(CPS/4)"
                                    "p"
                                    "CPS"
                                    "q"
                                    "4"))
                                  (("1"
                                    (assert)
                                    (("1"
                                      (flatten -1)
                                      (("1"
                                        (lemma
                                         "atan_series"
                                         ("x"
                                          "sqrt(vsx!1)"
                                          "n"
                                          "2+p!1"))
                                        (("1"
                                          (expand "atan_series_n")
                                          (("1"
                                            (expand "atan_series_term")
                                            (("1"
                                              (case
                                               "FORALL (n:nat): sqrt(vsx!1) ^ (1 + 2 * n) = sqrt(vsx!1)* vsx!1^n")
                                              (("1"
                                                (case-replace
                                                 "sigma(0, 2 + p!1,
                 LAMBDA (n: nat):
                   (sqrt(vsx!1) ^ (1 + 2 * n)) * atan_series_coef(n)) = sqrt(vsx!1)*sigma(0, 2 + p!1,LAMBDA (n: nat): vsx!1^n * atan_series_coef(n))")
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (inst - "3+p!1")
                                                    (("1"
                                                      (replace -1 -2)
                                                      (("1"
                                                        (expand
                                                         "powerseries")
                                                        (("1"
                                                          (case-replace
                                                           "(LAMBDA (i:nat):
                  IF i = 0 THEN atan_series_coef(i)
                  ELSE atan_series_coef(i) * vsx!1 ^ i
                  ENDIF) = (LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))")
                                                          (("1"
                                                            (hide
                                                             -1
                                                             -2
                                                             -6)
                                                            (("1"
                                                              (name-replace
                                                               "PS"
                                                               "sigma(0, 2 + p!1,
                  LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))")
                                                              (("1"
                                                                (name-replace
                                                                 "RR"
                                                                 "round(CPS / 4)")
                                                                (("1"
                                                                  (expand
                                                                   "<="
                                                                   -6)
                                                                  (("1"
                                                                    (split
                                                                     -6)
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (lemma
                                                                         "sqrt_pos"
                                                                         ("px"
                                                                          "vsx!1"))
                                                                        (("1"
                                                                          (lemma
                                                                           "expt_pos"
                                                                           ("px"
                                                                            "vsx!1"
                                                                            "i"
                                                                            "3+p!1"))
                                                                          (("1"
                                                                            (lemma
                                                                             "sqrt_lt"
                                                                             ("nny"
                                                                              "vsx!1"
                                                                              "nnz"
                                                                              "sq(1/2)"))
                                                                            (("1"
                                                                              (rewrite
                                                                               "sqrt_sq")
                                                                              (("1"
                                                                                (expand
                                                                                 "sq"
                                                                                 -1)
                                                                                (("1"
                                                                                  (rewrite
                                                                                   "abs_mult"
                                                                                   -5)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "abs"
                                                                                     -5
                                                                                     2)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "abs"
                                                                                       -5
                                                                                       2)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "both_sides_div_pos_le1"
                                                                                           ("x"
                                                                                            "abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS)"
                                                                                            "y"
                                                                                            "(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1)"
                                                                                            "pz"
                                                                                            "sqrt(vsx!1)"))
                                                                                          (("1"
                                                                                            (replace
                                                                                             -1
                                                                                             -6
                                                                                             rl)
                                                                                            (("1"
                                                                                              (hide
                                                                                               -1)
                                                                                              (("1"
                                                                                                (case-replace
                                                                                                 "(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1) / sqrt(vsx!1) = vsx!1 ^ (3 + p!1) / (7 + 2 * p!1)")
                                                                                                (("1"
                                                                                                  (hide
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (case-replace
                                                                                                     "abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS) / sqrt(vsx!1) = abs(atan(sqrt(vsx!1)) / sqrt(vsx!1) -PS)")
                                                                                                    (("1"
                                                                                                      (hide
                                                                                                       -1)
                                                                                                      (("1"
                                                                                                        (name-replace
                                                                                                         "TMP1"
                                                                                                         "atan(sqrt(vsx!1)) / sqrt(vsx!1)")
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "both_sides_expt_pos_lt"
                                                                                                           ("px"
                                                                                                            "vsx!1"
                                                                                                            "py"
                                                                                                            "1/4"
                                                                                                            "pm"
                                                                                                            "3+p!1"))
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            (("1"
                                                                                                              (hide
                                                                                                               -12)
                                                                                                              (("1"
                                                                                                                (case
                                                                                                                 "abs(TMP1 - PS)*2^p!1 < 1/4")
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   "abs"
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (case
                                                                                                                     "TMP1)
                                                                                                                    (("1"
                                                                                                                      (assert)
                                                                                                                      (("1"
                                                                                                                        (lemma
                                                                                                                         "posreal_times_posreal_is_posreal"
                                                                                                                         ("px"
                                                                                                                          "-(TMP1 - PS)"
                                                                                                                          "py"
                                                                                                                          "2 ^ p!1"))
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil)
                                                                                                                     ("2"
                                                                                                                      (assert)
                                                                                                                      (("2"
                                                                                                                        (lemma
                                                                                                                         "posreal_times_posreal_is_posreal"
                                                                                                                         ("px"
                                                                                                                          "TMP1-PS"
                                                                                                                          "py"
                                                                                                                          "2 ^ p!1"))
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (lemma
                                                                                                                   "both_sides_div_pos_lt2"
                                                                                                                   ("pz"
                                                                                                                    "vsx!1 ^ (3 + p!1)"
                                                                                                                    "px"
                                                                                                                    "7 + 2 * p!1"
                                                                                                                    "py"
                                                                                                                    "1"))
                                                                                                                  (("2"
                                                                                                                    (hide
                                                                                                                     2)
                                                                                                                    (("2"
                                                                                                                      (assert)
                                                                                                                      (("2"
                                                                                                                        (lemma
                                                                                                                         "both_sides_expt_pos_lt"
                                                                                                                         ("px"
                                                                                                                          "1/4"
                                                                                                                          "py"
                                                                                                                          "1/2"
                                                                                                                          "pm"
                                                                                                                          "3+p!1"))
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          (("2"
                                                                                                                            (lemma
                                                                                                                             "both_sides_expt_lt1_lt"
                                                                                                                             ("lt1x"
                                                                                                                              "1/2"
                                                                                                                              "i"
                                                                                                                              "3+p!1"
                                                                                                                              "j"
                                                                                                                              "2+p!1"))
                                                                                                                            (("2"
                                                                                                                              (assert)
                                                                                                                              (("2"
                                                                                                                                (lemma
                                                                                                                                 "inv_expt"
                                                                                                                                 ("n0x"
                                                                                                                                  "2"
                                                                                                                                  "i"
                                                                                                                                  "2+p!1"))
                                                                                                                                (("2"
                                                                                                                                  (lemma
                                                                                                                                   "expt_pos"
                                                                                                                                   ("px"
                                                                                                                                    "2"
                                                                                                                                    "i"
                                                                                                                                    "p!1"))
                                                                                                                                  (("2"
                                                                                                                                    (lemma
                                                                                                                                     "div_mult_pos_lt2"
                                                                                                                                     ("py"
                                                                                                                                      "2^p!1"
                                                                                                                                      "x"
                                                                                                                                      "abs(TMP1 - PS)"
                                                                                                                                      "z"
                                                                                                                                      "1/4"))
                                                                                                                                    (("2"
                                                                                                                                      (replace
                                                                                                                                       -1
                                                                                                                                       1
                                                                                                                                       rl)
                                                                                                                                      (("2"
                                                                                                                                        (case-replace
                                                                                                                                         "1 / 4 / 2 ^ p!1 = 1 / 2 ^ (2 + p!1)")
                                                                                                                                        (("1"
                                                                                                                                          (assert)
                                                                                                                                          nil
                                                                                                                                          nil)
                                                                                                                                         ("2"
                                                                                                                                          (hide-all-but
                                                                                                                                           (-2
                                                                                                                                            1))
                                                                                                                                          (("2"
                                                                                                                                            (case-replace
                                                                                                                                             "2 ^ (2 + p!1) = 4*2^p!1")
                                                                                                                                            (("1"
                                                                                                                                              (name-replace
                                                                                                                                               "TMP4"
                                                                                                                                               "2^p!1")
                                                                                                                                              (("1"
                                                                                                                                                (assert)
                                                                                                                                                nil
                                                                                                                                                nil))
                                                                                                                                              nil)
                                                                                                                                             ("2"
                                                                                                                                              (hide-all-but
                                                                                                                                               1)
                                                                                                                                              (("2"
                                                                                                                                                (lemma
                                                                                                                                                 "expt_plus"
                                                                                                                                                 ("n0x"
                                                                                                                                                  "2"
                                                                                                                                                  "i"
                                                                                                                                                  "2"
                                                                                                                                                  "j"
                                                                                                                                                  "p!1"))
                                                                                                                                                (("2"
                                                                                                                                                  (replace
                                                                                                                                                   -1)
                                                                                                                                                  (("2"
                                                                                                                                                    (expand
                                                                                                                                                     "^"
                                                                                                                                                     1
                                                                                                                                                     1)
                                                                                                                                                    (("2"
                                                                                                                                                      (expand
                                                                                                                                                       "expt")
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "expt")
                                                                                                                                                        (("2"
                                                                                                                                                          (expand
                                                                                                                                                           "expt")
                                                                                                                                                          (("2"
                                                                                                                                                            (propax)
                                                                                                                                                            nil
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide-all-but
                                                                                                       (-3
                                                                                                        1))
                                                                                                      (("2"
                                                                                                        (lemma
                                                                                                         "abs_div")
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -
                                                                                                           "sqrt(vsx!1)"
                                                                                                           "atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "abs"
                                                                                                             -1
                                                                                                             3)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (hide-all-but
                                                                                                   (-3
                                                                                                    1))
                                                                                                  (("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (replace
                                                                       -1
                                                                       *
                                                                       rl)
                                                                      (("2"
                                                                        (rewrite
                                                                         "sqrt_0")
                                                                        (("2"
                                                                          (expand
                                                                           "PS")
                                                                          (("2"
                                                                            (case-replace
                                                                             "sigma(0, 2 + p!1,
                LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n)) =1")
                                                                            (("1"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.62 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.


Bot Zugriff