Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: acos.prf Sprache: Lisp

Original von: PVS^©

(acos (nnreal_le_pi_TCC1 0
       (nnreal_le_pi_TCC1-1 nil 3262275870 ("" (assert) nil nil)
        ((real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil))
        shostak))
      (acos_TCC1 0
       (acos_TCC1-1 nil 3262275879
        ("" (skolem 1 ("x"))
         (("" (typepred "asin(x)")
           (("" (expand "abs" -1)
             (("" (case "asin(x) < 0")
               (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
             nil))
           nil))
         nil)
        ((asin const-decl "real_abs_le_pi2" asin nil)
         (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (AND const-decl "[bool, bool -> bool]" booleans nil)
         (pi const-decl "posreal" atan nil)
         (posreal nonempty-type-eq-decl nil real_types nil)
         (> const-decl "bool" reals nil)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (>= const-decl "bool" reals 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)
         (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_minus_real_is_real application-judgement "real" reals
          nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_lt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (< const-decl "bool" reals nil))
        shostak))
      (acos_neg_TCC1 0
       (acos_neg_TCC1-1 nil 3262871574 ("" (grind) nil nil) nil
        shostak))
      (acos_neg 0
       (acos_neg-1 nil 3262871521
        ("" (skolem 1 ("x"))
         (("" (expand "acos")
           (("" (rewrite "asin_neg") (("" (assert) nil nil)) nil))
           nil))
         nil)
        ((posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (acos const-decl "nnreal_le_pi" acos nil)
         (real_plus_real_is_real application-judgement "real" reals
          nil)
         (minus_real_is_real application-judgement "real" reals nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (<= const-decl "bool" reals nil)
         (AND const-decl "[bool, bool -> bool]" booleans nil)
         (bool nonempty-type-eq-decl nil booleans 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)
         (asin_neg formula-decl nil asin nil))
        shostak))
      (acos_0 0
       (acos_0-1 nil 3262276429
        ("" (expand "acos")
         (("" (rewrite "asin_0") (("" (assert) nil nil)) nil)) nil)
        ((asin_0 formula-decl nil asin nil)
         (int_times_even_is_even application-judgement "even_int"
          integers nil)
         (mult_divides1 application-judgement "(divides(n))" divides
          nil)
         (mult_divides2 application-judgement "(divides(m))" divides
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_sqrt_half_TCC1 0
       (acos_sqrt_half_TCC1-1 nil 3263920337
        ("" (expand "abs")
         (("" (typepred "sqrt(1/2)")
           (("" (assert)
             (("" (lemma "sq_le" ("nna" "sqrt(1/2)" "nnb" "1"))
               (("" (rewrite "sq_sqrt")
                 (("" (expand "sq" -1) (("" (propax) nil nil)) nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_gt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (posreal_times_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (sq_sqrt formula-decl nil sqrt "reals/")
         (sq const-decl "nonneg_real" sq "reals/")
         (sq_le formula-decl nil sq "reals/")
         (posrat_div_posrat_is_posrat application-judgement "posrat"
          rationals nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (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)
         (>= const-decl "bool" reals nil)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (nnreal type-eq-decl nil real_types nil)
         (= const-decl "[T, T -> boolean]" equalities nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (* const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
               "reals/")
         (/= const-decl "boolean" notequal nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (> const-decl "bool" reals nil))
        shostak))
      (acos_sqrt_half 0
       (acos_sqrt_half-1 nil 3263920536
        ("" (expand "acos")
         (("" (rewrite "asin_sqrt_half") (("" (assert) nil nil)) nil))
         nil)
        ((asin_sqrt_half formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_1 0
       (acos_1-1 nil 3262276459
        ("" (expand "acos")
         (("" (rewrite "asin_1") (("" (assert) nil nil)) nil)) nil)
        ((asin_1 formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_minus1 0
       (acos_minus1-1 nil 3262276496
        ("" (expand "acos")
         (("" (rewrite "asin_minus1") (("" (assert) nil nil)) nil))
         nil)
        ((asin_minus1 formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_minus_sqrt_half_TCC1 0
       (acos_minus_sqrt_half_TCC1-1 nil 3263920463
        ("" (lemma "acos_sqrt_half_TCC1")
         (("" (assert)
           (("" (mult-by 1 "-1" -) (("" (assert) nil nil)) nil)) nil))
         nil)
        ((minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (posrat_div_posrat_is_posrat application-judgement "posrat"
          rationals nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (mult_divides1 application-judgement "(divides(n))" divides
          nil)
         (odd_times_odd_is_odd application-judgement "odd_int" integers
          nil)
         (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
          real_types 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)
         (<= const-decl "bool" reals nil)
         (nonpos_real nonempty-type-eq-decl nil real_types nil)
         (< const-decl "bool" reals nil)
         (negreal nonempty-type-eq-decl nil real_types nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (>= const-decl "bool" reals nil)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (nnreal type-eq-decl nil real_types nil)
         (= const-decl "[T, T -> boolean]" equalities nil)
         (* const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
               "reals/")
         (/= const-decl "boolean" notequal nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (both_sides_times_neg_le1 formula-decl nil real_props nil)
         (acos_sqrt_half_TCC1 subtype-tcc nil acos nil))
        shostak))
      (acos_minus_sqrt_half 0
       (acos_minus_sqrt_half-1 nil 3263920585
        ("" (expand "acos")
         (("" (rewrite "asin_minus_sqrt_half") (("" (assert) nil nil))
           nil))
         nil)
        ((asin_minus_sqrt_half formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (posreal_times_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/"))
        shostak))
      (acos_strict_decreasing 0
       (acos_strict_decreasing-1 nil 3262276758
        ("" (expand "strict_decreasing?")
         (("" (skolem 1 ("x" "y"))
           (("" (flatten)
             (("" (expand "acos")
               (("" (lemma "asin_strict_increasing")
                 (("" (expand "strict_increasing?")
                   (("" (inst - "x" "y") (("" (assert) nil nil)) nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((acos const-decl "nnreal_le_pi" acos nil)
         (strict_increasing? const-decl "bool" real_fun_preds "reals/")
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (real_lt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (<= const-decl "bool" reals nil)
         (AND const-decl "[bool, bool -> bool]" booleans nil)
         (bool nonempty-type-eq-decl nil booleans 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)
         (asin_strict_increasing formula-decl nil asin nil)
         (strict_decreasing? const-decl "bool" real_fun_preds
          "reals/"))
        shostak))
      (acos_bij 0
       (acos_bij-1 nil 3262277267
        ("" (lemma "asin_bij")
         (("" (expand "bijective?")
           (("" (expand "injective?")
             (("" (expand "surjective?")
               (("" (expand "acos")
                 (("" (flatten)
                   (("" (split 1)
                     (("1" (skolem 1 ("x" "y"))
                       (("1" (inst -1 "x" "y")
                         (("1" (flatten) (("1" (assert) nil nil)) nil))
                         nil))
                       nil)
                      ("2" (hide -1)
                       (("2" (skolem 1 ("y"))
                         (("2" (inst - "pi/2-y")
                           (("1" (skolem - ("x"))
                             (("1" (inst + "x")
                               (("1" (assert) nil nil)) nil))
                             nil)
                            ("2" (hide 2)
                             (("2" (typepred "y")
                               (("2"
                                 (expand "abs")
                                 (("2"
                                   (case "pi/2-y<0")
                                   (("1" (assert) nil nil)
                                    ("2" (assert) nil nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((bijective? const-decl "bool" functions nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (surjective? const-decl "bool" functions nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_minus_real_is_real application-judgement "real" reals
          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 "bool" reals nil)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (> const-decl "bool" reals nil)
         (posreal nonempty-type-eq-decl nil real_types nil)
         (pi const-decl "posreal" atan nil)
         (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (nnreal type-eq-decl nil real_types nil)
         (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
         (real_times_real_is_real application-judgement "real" reals
          nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (<= const-decl "bool" reals nil)
         (AND const-decl "[bool, bool -> bool]" booleans nil)
         (bool nonempty-type-eq-decl nil booleans 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)
         (acos const-decl "nnreal_le_pi" acos nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (injective? const-decl "bool" functions nil)
         (asin_bij formula-decl nil asin nil))
        shostak))
      (acos_sum_TCC1 0
       (acos_sum_TCC1-1 nil 3263920917
        ("" (skosimp*)
         (("" (typepred "nnx!1") (("" (assert) nil nil)) nil)) nil)
        ((<= const-decl "bool" reals nil)
         (nnreal type-eq-decl nil real_types 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)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil))
        shostak))
      (acos_sum_TCC2 0
       (acos_sum_TCC2-1 nil 3263920948
        ("" (skosimp*)
         (("" (typepred "nny!1")
           (("" (lemma "sq_le" ("nna" "nny!1" "nnb" "1"))
             (("" (expand "sq") (("" (assert) nil nil)) nil)) nil))
           nil))
         nil)
        ((<= const-decl "bool" reals nil)
         (nnreal type-eq-decl nil real_types 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)
         (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (sq const-decl "nonneg_real" sq "reals/")
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (sq_le formula-decl nil sq "reals/")
         (nonneg_real nonempty-type-eq-decl nil real_types nil))
        shostak))
      (acos_sum_TCC3 0
       (acos_sum_TCC3-1 nil 3263921002
        ("" (skosimp*)
         (("" (typepred "nnx!1")
           (("" (typepred "nny!1")
             (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
               (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
                 (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
                   (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
                     (("" (rewrite "sq_0")
                       (("" (rewrite "sq_1")
                         (("" (expand ">=")
                           (("" (flatten)
                             (("" (replace -9)
                               ((""
                                 (replace -9)
                                 ((""
                                   (replace -9)
                                   ((""
                                     (replace -9)
                                     ((""
                                       (case "0 <= 1 - sq(nny!1)")
                                       (("1"
                                         (case "0 <= 1 - sq(nnx!1)")
                                         (("1"
                                           (lemma
                                            "sqrt_le"
                                            ("nny"
                                             "1 - sq(nny!1)"
                                             "nnz"
                                             "1"))
                                           (("1"
                                             (lemma
                                              "sqrt_le"
                                              ("nny"
                                               "1 - sq(nnx!1)"
                                               "nnz"
                                               "1"))
                                             (("1"
                                               (assert)
                                               (("1"
                                                 (rewrite "sqrt_1")
                                                 (("1"
                                                   (typepred
                                                    "sqrt(1 - sq(nnx!1)) ")
                                                   (("1"
                                                     (typepred
                                                      "sqrt(1 - sq(nny!1)) ")
                                                     (("1"
                                                       (hide -2 -4)
                                                       (("1"
                                                         (lemma
                                                          "nnreal_times_nnreal_is_nnreal"
                                                          ("nnx"
                                                           "nnx!1"
                                                           "nny"
                                                           "nny!1"))
                                                         (("1"
                                                           (lemma
                                                            "nnreal_times_nnreal_is_nnreal"
                                                            ("nnx"
                                                             "sqrt(1 - sq(nnx!1))"
                                                             "nny"
                                                             "sqrt(1 - sq(nny!1))"))
                                                           (("1"
                                                             (lemma
                                                              "le_times_le_pos"
                                                              ("nnx"
                                                               "sqrt(1 - sq(nny!1))"
                                                               "y"
                                                               "1"
                                                               "nnz"
                                                               "sqrt(1 - sq(nnx!1))"
                                                               "w"
                                                               "1"))
                                                             (("1"
                                                               (assert)
                                                               (("1"
                                                                 (lemma
                                                                  "le_times_le_pos"
                                                                  ("nnx"
                                                                   "nnx!1"
                                                                   "y"
                                                                   "1"
                                                                   "nnz"
                                                                   "nny!1"
                                                                   "w"
                                                                   "1"))
                                                                 (("1"
                                                                   (assert)
                                                                   (("1"
                                                                     (lemma
                                                                      "le_minus_le"
                                                                      ("x"
                                                                       "nnx!1 * nny!1"
                                                                       "y"
                                                                       "1"
                                                                       "w"
                                                                       "0"
                                                                       "z"
                                                                       "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
                                                                     (("1"
                                                                       (lemma
                                                                        "le_minus_le"
                                                                        ("y"
                                                                         "nnx!1 * nny!1"
                                                                         "x"
                                                                         "0"
                                                                         "z"
                                                                         "1"
                                                                         "w"
                                                                         "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
                                                                       (("1"
                                                                         (expand
                                                                          ">=")
                                                                         (("1"
                                                                           (replace
                                                                            -3)
                                                                           (("1"
                                                                             (replace
                                                                              -4)
                                                                             (("1"
                                                                               (replace
                                                                                -5)
                                                                               (("1"
                                                                                 (replace
                                                                                  -6)
                                                                                 (("1"
                                                                                   (expand
                                                                                    "abs"
                                                                                    1)
                                                                                   (("1"
                                                                                     (case
                                                                                      "nnx!1 * nny!1 - (sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1))) < 0")
                                                                                     (("1"
                                                                                       (assert)
                                                                                       nil
                                                                                       nil)
                                                                                      ("2"
                                                                                       (assert)
                                                                                       nil
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil))
                                                                               nil))
                                                                             nil))
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil))
                                                             nil))
                                                           nil))
                                                         nil))
                                                       nil))
                                                     nil))
                                                   nil))
                                                 nil))
                                               nil)
                                              ("2" (assert) nil nil))
                                             nil)
                                            ("2" (assert) nil nil))
                                           nil)
                                          ("2" (assert) nil nil))
                                         nil)
                                        ("2" (assert) nil nil))
                                       nil))
                                     nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((<= const-decl "bool" reals nil)
         (nnreal type-eq-decl nil real_types 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)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (sq_le formula-decl nil sq "reals/")
         (sq_0 formula-decl nil sq "reals/")
         (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (- const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sq const-decl "nonneg_real" sq "reals/")
         (sqrt_le formula-decl nil sqrt "reals/")
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (sqrt_1 formula-decl nil sqrt "reals/")
         (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types
          nil)
         (le_times_le_pos formula-decl nil real_props nil)
         (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
               "reals/")
         (* const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (= const-decl "[T, T -> boolean]" equalities nil)
         (sq_1 formula-decl nil sq "reals/"))
        shostak))
      (acos_sum 0
       (acos_sum-1 nil 3263922185
        ("" (skosimp*)
         (("" (typepred "nnx!1")
           (("" (typepred "nny!1")
             (("" (expand ">=")
               (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
                 (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
                   (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
                     (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
                       (("" (rewrite "sq_0")
                         (("" (rewrite "sq_1")
                           (("" (simplify -1)
                             (("" (simplify -2)
                               ((""
                                 (flatten)
                                 ((""
                                   (replace -7)
                                   ((""
                                     (replace -8)
                                     ((""
                                       (expand "<=" -8)
                                       ((""
                                         (split -8)
                                         (("1"
                                           (expand "<=" -7)
                                           (("1"
                                             (split -7)
                                             (("1"
                                               (expand "<=" -8)
                                               (("1"
                                                 (split -8)
                                                 (("1"
                                                   (expand "<=" -8)
                                                   (("1"
                                                     (split -8)
                                                     (("1"
                                                       (expand
                                                        "acos"
                                                        1)
                                                       (("1"
                                                         (lemma
                                                          "div_cancel1"
                                                          ("x"
                                                           "pi"
                                                           "n0z"
                                                           "2"))
                                                         (("1"
                                                           (replace -1)
                                                           (("1"
                                                             (hide -1)
                                                             (("1"
                                                               (hide
                                                                -5
                                                                -6
                                                                -7
                                                                -8)
                                                               (("1"
                                                                 (lemma
                                                                  "sq_lt"
                                                                  ("nna"
                                                                   "0"
                                                                   "nnb"
                                                                   "nnx!1"))
                                                                 (("1"
                                                                   (lemma
                                                                    "sq_lt"
                                                                    ("nna"
                                                                     "0"
                                                                     "nnb"
                                                                     "nny!1"))
                                                                   (("1"
                                                                     (lemma
                                                                      "sq_lt"
                                                                      ("nnb"
                                                                       "1"
                                                                       "nna"
                                                                       "nnx!1"))
                                                                     (("1"
                                                                       (lemma
                                                                        "sq_lt"
                                                                        ("nnb"
                                                                         "1"
                                                                         "nna"
                                                                         "nny!1"))
                                                                       (("1"
                                                                         (rewrite
                                                                          "sq_0")
                                                                         (("1"
                                                                           (rewrite
                                                                            "sq_1")
                                                                           (("1"
                                                                             (replace
                                                                              -5)
                                                                             (("1"
                                                                               (replace
                                                                                -6)
                                                                               (("1"
                                                                                 (replace
                                                                                  -7)
                                                                                 (("1"
                                                                                   (replace
                                                                                    -8)
                                                                                   (("1"
                                                                                     (simplify)
                                                                                     (("1"
                                                                                       (case
                                                                                        "0 < 1-sq(nnx!1)")
                                                                                       (("1"
                                                                                         (case
                                                                                          "0 < 1-sq(nny!1)")
                                                                                         (("1"
                                                                                           (case
                                                                                            "1-sq(nnx!1)<1")
                                                                                           (("1"
                                                                                             (case
                                                                                              "1-sq(nny!1)<1")
                                                                                             (("1"
                                                                                               (lemma
                                                                                                "sqrt_lt"
                                                                                                ("nny"
                                                                                                 "0"
                                                                                                 "nnz"
                                                                                                 "1-sq(nnx!1)"))
                                                                                               (("1"
                                                                                                 (lemma
                                                                                                  "sqrt_lt"
                                                                                                  ("nny"
                                                                                                   "0"
                                                                                                   "nnz"
                                                                                                   "1-sq(nny!1)"))
                                                                                                 (("1"
                                                                                                   (lemma
                                                                                                    "sqrt_lt"
                                                                                                    ("nnz"
                                                                                                     "1"
                                                                                                     "nny"
                                                                                                     "1-sq(nnx!1)"))
                                                                                                   (("1"
                                                                                                     (lemma
                                                                                                      "sqrt_lt"
                                                                                                      ("nnz"
                                                                                                       "1"
                                                                                                       "nny"
                                                                                                       "1-sq(nny!1)"))
                                                                                                     (("1"
                                                                                                       (replace
                                                                                                        -5)
                                                                                                       (("1"
                                                                                                         (replace
                                                                                                          -6)
                                                                                                         (("1"
                                                                                                           (replace
                                                                                                            -7)
                                                                                                           (("1"
                                                                                                             (replace
                                                                                                              -8)
                                                                                                             (("1"
                                                                                                               (rewrite
                                                                                                                "sqrt_1")
                                                                                                               (("1"
                                                                                                                 (rewrite
                                                                                                                  "sqrt_0")
                                                                                                                 (("1"
                                                                                                                   (simplify)
                                                                                                                   (("1"
                                                                                                                     (lemma
                                                                                                                      "posreal_times_posreal_is_posreal"
                                                                                                                      ("px"
                                                                                                                       "nnx!1"
                                                                                                                       "py"
                                                                                                                       "nny!1"))
                                                                                                                     (("1"
                                                                                                                       (lemma
                                                                                                                        "posreal_times_posreal_is_posreal"
                                                                                                                        ("px"
                                                                                                                         "sqrt(1 - sq(nny!1))"
                                                                                                                         "py"
                                                                                                                         "sqrt(1 - sq(nnx!1))"))
                                                                                                                       (("1"
                                                                                                                         (lemma
                                                                                                                          "lt_times_lt_pos1"
                                                                                                                          ("px"
                                                                                                                           "nnx!1"
                                                                                                                           "y"
                                                                                                                           "1"
                                                                                                                           "nnz"
                                                                                                                           "nny!1"
                                                                                                                           "w"
                                                                                                                           "1"))
                                                                                                                         (("1"
                                                                                                                           (lemma
                                                                                                                            "lt_times_lt_pos1"
                                                                                                                            ("px"
                                                                                                                             "sqrt(1 - sq(nny!1))"
                                                                                                                             "y"
                                                                                                                             "1"
                                                                                                                             "nnz"
                                                                                                                             "sqrt(1 - sq(nnx!1))"
                                                                                                                             "w"
                                                                                                                             "1"))
                                                                                                                           (("1"
                                                                                                                             (assert)
                                                                                                                             (("1"
                                                                                                                               (lemma
                                                                                                                                "lt_minus_lt1"
                                                                                                                                ("x"
                                                                                                                                 "nnx!1 * nny!1"
                                                                                                                                 "y"
                                                                                                                                 "1"
                                                                                                                                 "w"
                                                                                                                                 "0"
                                                                                                                                 "z"
                                                                                                                                 "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"))
                                                                                                                               (("1"
                                                                                                                                 (lemma
                                                                                                                                  "lt_minus_lt1"
                                                                                                                                  ("x"
                                                                                                                                   "0"
                                                                                                                                   "y"
                                                                                                                                   "nnx!1 * nny!1"
                                                                                                                                   "w"
                                                                                                                                   "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"
                                                                                                                                   "z"
                                                                                                                                   "1"))
                                                                                                                                 (("1"
                                                                                                                                   (replace
                                                                                                                                    -3)
                                                                                                                                   (("1"
                                                                                                                                     (expand
                                                                                                                                      ">"
                                                                                                                                      -5)
                                                                                                                                     (("1"
                                                                                                                                       (replace
                                                                                                                                        -5)
                                                                                                                                       (("1"
                                                                                                                                         (split
                                                                                                                                          -1)
                                                                                                                                         (("1"
                                                                                                                                           (split
                                                                                                                                            -2)
                                                                                                                                           (("1"
                                                                                                                                             (simplify
                                                                                                                                              (-1
                                                                                                                                               -2))
                                                                                                                                             (("1"
                                                                                                                                               (expand
                                                                                                                                                "asin")
                                                                                                                                               (("1"
                                                                                                                                                 (rewrite
                                                                                                                                                  "sq_rew"
                                                                                                                                                  1)
                                                                                                                                                 (("1"
                                                                                                                                                   (rewrite
                                                                                                                                                    "sq_rew"
                                                                                                                                                    1)
                                                                                                                                                   (("1"
                                                                                                                                                     (lemma
                                                                                                                                                      "sq_sqrt"
                                                                                                                                                      ("x"
                                                                                                                                                       "1-sq(nnx!1)"))
                                                                                                                                                     (("1"
                                                                                                                                                       (lemma
                                                                                                                                                        "sq_sqrt"
                                                                                                                                                        ("x"
                                                                                                                                                         "1-sq(nny!1)"))
                                                                                                                                                       (("1"
                                                                                                                                                         (assert)
                                                                                                                                                         (("1"
                                                                                                                                                           (name-replace
                                                                                                                                                            "SX"
                                                                                                                                                            "sqrt(1 - sq(nnx!1))")
                                                                                                                                                           (("1"
                                                                                                                                                             (name-replace
                                                                                                                                                              "SY"
                                                                                                                                                              "sqrt(1 - sq(nny!1))")
                                                                                                                                                             (("1"
                                                                                                                                                               (rewrite
                                                                                                                                                                "sq_rew"
                                                                                                                                                                1)
                                                                                                                                                               (("1"
                                                                                                                                                                 (case
                                                                                                                                                                  "1 - sq(nnx!1) * nny!1 * nny!1 - sq(SX) * SY * SY = 1-sq(nnx!1)*sq(nny!1) - sq(SX)*sq(SY)")
                                                                                                                                                                 (("1"
--> --------------------

--> maximum size reached

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

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