products/sources/formale Sprachen/PVS/trig_fnd image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: tan_quad.prf   Sprache: Lisp

Original von: PVS©

(tan_quad
 (tan_value_def_TCC1 0
  (tan_value_def_TCC1-1 nil 3264857198
   ("" (skosimp*) (("" (typepred "x!1") (("" (assertnil nil)) nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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))
   shostak))
 (tan_value_def_TCC2 0
  (tan_value_def_TCC2-1 nil 3264857222
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (assert)
        (("" (expand "abs")
          (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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))
   shostak))
 (tan_value_def_TCC3 0
  (tan_value_def_TCC3-1 nil 3264857251
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "cos_value_strict_decreasing")
        (("" (expand "strict_decreasing?")
          (("" (inst - "abs(x!1)" "pi/2")
            (("" (rewrite "cos_value_pi2")
              (("" (assert)
                (("" (expand "abs")
                  (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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)
    (strict_decreasing? const-decl "bool" real_fun_preds "reals/")
    (cos_value_pi2 formula-decl nil sincos_quad nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_value_strict_decreasing formula-decl nil sincos_quad nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
 (tan_value_def 0
  (tan_value_def-3 nil 3408979579
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "atan_bij")
        (("" (expand "tan_value")
          ((""
            (lemma "comp_inverse_right[real, real_abs_lt_pi2]"
             ("f" "atan" "y" "x!1"))
            (("1" (expand "bijective?")
              (("1" (expand "injective?")
                (("1" (flatten)
                  (("1" (hide -3)
                    (("1"
                      (inst - "inverse(atan)(x!1)"
                       "sin_value(x!1) / cos_value(abs(x!1))")
                      (("1" (split -2)
                        (("1" (propax) nil nil)
                         ("2"
                          (lemma "cos_eqv_sqrt_sin_value"
                           ("q1" "abs(x!1)"))
                          (("1"
                            (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
                            (("1" (replace -1)
                              (("1"
                                (replace -3 1)
                                (("1"
                                  (replace -2 1 rl)
                                  (("1"
                                    (hide -1 -2 -3 2)
                                    (("1"
                                      (lemma
                                       "asin_sin_value"
                                       ("xs" "x!1"))
                                      (("1"
                                        (expand "asin")
                                        (("1"
                                          (lemma
                                           "sin_value_strict_increasing")
                                          (("1"
                                            (expand
                                             "strict_increasing?")
                                            (("1"
                                              (inst-cp - "-pi/2" "x!1")
                                              (("1"
                                                (inst - "x!1" "pi/2")
                                                (("1"
                                                  (rewrite
                                                   "sin_value_pi2")
                                                  (("1"
                                                    (rewrite
                                                     "sin_value_minus_pi2")
                                                    (("1"
                                                      (case "x!1<0")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (case
                                                           "-pi / 2 < x!1")
                                                          (("1"
                                                            (rewrite
                                                             "sq_rew"
                                                             -5)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (rewrite
                                                           "sq_rew"
                                                           -3)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2"
                                (expand "abs")
                                (("2"
                                  (case "x!1<0")
                                  (("1"
                                    (lemma
                                     "sin_value_neg"
                                     ("xs" "x!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (replace -1 1)
                                        (("1"
                                          (rewrite "sq_neg" 1)
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "abs")
                            (("2" (hide 2 3)
                              (("2"
                                (ground)
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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)
    (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (inverse const-decl "D" function_inverse nil)
    (<= const-decl "bool" reals nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
     sincos_quad nil)
    (nnreal type-eq-decl nil real_types nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
    (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_neg formula-decl nil sq "reals/")
    (sin_value_neg formula-decl nil sincos_quad nil)
    (asin_sin_value formula-decl nil sincos_quad nil)
    (sin_value_strict_increasing formula-decl nil sincos_quad nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sin_value_pi2 formula-decl nil sincos_quad nil)
    (sq_rew formula-decl nil sq "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sin_value_minus_pi2 formula-decl nil sincos_quad nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (asin const-decl "real_abs_le_pi2" asin nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (injective? const-decl "bool" functions nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (bijective? const-decl "bool" functions nil)
    (comp_inverse_right formula-decl nil function_inverse nil)
    (atan_bij formula-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil)
  (tan_value_def-2 nil 3408966564
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "atan_bij")
        (("" (expand "tan_value")
          ((""
            (lemma "comp_inverse_right[real, real_abs_lt_pi]"
             ("f" "atan" "y" "x!1"))
            (("1" (expand "bijective?")
              (("1" (expand "injective?")
                (("1" (flatten)
                  (("1" (hide -3)
                    (("1"
                      (inst - "inverse(atan)(x!1)"
                       "sin_value(x!1) / cos_value(abs(x!1))")
                      (("1" (split -2)
                        (("1" (propax) nil nil)
                         ("2"
                          (lemma "cos_eqv_sqrt_sin_value"
                           ("q1" "abs(x!1)"))
                          (("1"
                            (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
                            (("1" (replace -1)
                              (("1"
                                (replace -3 1)
                                (("1"
                                  (replace -2 1 rl)
                                  (("1"
                                    (hide -1 -2 -3 2)
                                    (("1"
                                      (lemma
                                       "asin_sin_value"
                                       ("xs" "x!1"))
                                      (("1"
                                        (expand "asin")
                                        (("1"
                                          (lemma
                                           "sin_value_strict_increasing")
                                          (("1"
                                            (expand
                                             "strict_increasing?")
                                            (("1"
                                              (inst-cp - "-pi/2" "x!1")
                                              (("1"
                                                (inst - "x!1" "pi/2")
                                                (("1"
                                                  (rewrite
                                                   "sin_value_pi2")
                                                  (("1"
                                                    (rewrite
                                                     "sin_value_minus_pi2")
                                                    (("1"
                                                      (case "x!1<0")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (case
                                                           "-pi / 2 < x!1")
                                                          (("1"
                                                            (rewrite
                                                             "sq_rew"
                                                             -5)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (rewrite
                                                           "sq_rew"
                                                           -3)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2"
                                (expand "abs")
                                (("2"
                                  (case "x!1<0")
                                  (("1"
                                    (lemma
                                     "sin_value_neg"
                                     ("xs" "x!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (replace -1 1)
                                        (("1"
                                          (rewrite "sq_neg" 1)
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "abs")
                            (("2" (hide 2 3)
                              (("2"
                                (ground)
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((atan_bij formula-decl nil atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (asin const-decl "real_abs_le_pi2" asin nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (sin_value_minus_pi2 formula-decl nil sincos_quad nil)
    (sq_rew formula-decl nil sq "reals/")
    (sin_value_pi2 formula-decl nil sincos_quad nil)
    (sin_value_strict_increasing formula-decl nil sincos_quad nil)
    (asin_sin_value formula-decl nil sincos_quad nil)
    (sin_value_neg formula-decl nil sincos_quad nil)
    (sq_neg formula-decl nil sq "reals/")
    (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
    (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
     sincos_quad nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (pi const-decl "posreal" atan nil))
   nil)
  (tan_value_def-1 nil 3264857402
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "atan_bij")
        (("" (expand "tan_value")
          ((""
            (lemma "comp_inverse_right[real, real_mpi_ppi]"
             ("f" "atan" "y" "x!1"))
            (("1" (expand "bijective?")
              (("1" (expand "injective?")
                (("1" (flatten)
                  (("1" (hide -3)
                    (("1"
                      (inst - "inverse(atan)(x!1)"
                       "sin_value(x!1) / cos_value(abs(x!1))")
                      (("1" (split -2)
                        (("1" (propax) nil nil)
                         ("2"
                          (lemma "cos_eqv_sqrt_sin_value"
                           ("q1" "abs(x!1)"))
                          (("1"
                            (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
                            (("1" (replace -1)
                              (("1"
                                (replace -3 1)
                                (("1"
                                  (replace -2 1 rl)
                                  (("1"
                                    (hide -1 -2 -3 2)
                                    (("1"
                                      (lemma
                                       "asin_sin_value"
                                       ("xs" "x!1"))
                                      (("1"
                                        (expand "asin")
                                        (("1"
                                          (lemma
                                           "sin_value_strict_increasing")
                                          (("1"
                                            (expand
                                             "strict_increasing?")
                                            (("1"
                                              (inst-cp - "-pi/2" "x!1")
                                              (("1"
                                                (inst - "x!1" "pi/2")
                                                (("1"
                                                  (rewrite
                                                   "sin_value_pi2")
                                                  (("1"
                                                    (rewrite
                                                     "sin_value_minus_pi2")
                                                    (("1"
                                                      (case "x!1<0")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (case
                                                           "-pi / 2 < x!1")
                                                          (("1"
                                                            (rewrite
                                                             "sq_rew"
                                                             -5)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (rewrite
                                                           "sq_rew"
                                                           -3)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2"
                                (expand "abs")
                                (("2"
                                  (case "x!1<0")
                                  (("1"
                                    (lemma
                                     "sin_value_neg"
                                     ("xs" "x!1"))
                                    (("1"
                                      (assert)
                                      (("1"
                                        (replace -1 1)
                                        (("1"
                                          (rewrite "sq_neg" 1)
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "abs")
                            (("2" (hide 2 3)
                              (("2"
                                (ground)
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((atan_bij formula-decl nil atan nil)
    (atan_value const-decl "real" atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (asin const-decl "real_abs_le_pi2" asin nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (sin_value_minus_pi2 formula-decl nil sincos_quad nil)
    (sq_rew formula-decl nil sq "reals/")
    (sin_value_pi2 formula-decl nil sincos_quad nil)
    (sin_value_strict_increasing formula-decl nil sincos_quad nil)
    (asin_sin_value formula-decl nil sincos_quad nil)
    (sin_value_neg formula-decl nil sincos_quad nil)
    (sq_neg formula-decl nil sq "reals/")
    (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
    (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
     sincos_quad nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (pi const-decl "posreal" atan nil))
   shostak))
 (tan_value_0_TCC1 0
  (tan_value_0_TCC1-1 nil 3264857350
   ("" (assert) (("" (assertnil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
 (tan_value_0 0
  (tan_value_0-1 nil 3264858476
   ("" (lemma "tan_value_def" ("x" "0"))
    (("1" (rewrite "sin_value_0")
      (("1" (expand "abs")
        (("1" (rewrite "cos_value_0") (("1" (assertnil nil)) nil))
        nil))
      nil)
     ("2" (expand "abs") (("2" (assertnil nil)) nil))
    nil)
   ((sin_value_0 formula-decl nil sincos_quad nil)
    (cos_value_0 formula-decl nil sincos_quad nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (tan_value_def formula-decl nil tan_quad 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)
    (>= 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_lt_pi2 nonempty-type-eq-decl nil atan nil))
   shostak))
 (tan_value_pi4_TCC1 0
  (tan_value_pi4_TCC1-1 nil 3264857364
   ("" (expand "abs")
    (("" (typepred "pi") (("" (assertnil nil)) nil)) 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil))
   shostak))
 (tan_value_pi4 0
  (tan_value_pi4-1 nil 3264858541
   ("" (lemma "tan_value_def" ("x" "pi/4"))
    (("1" (rewrite "sin_value_pi4")
      (("1" (expand "abs")
        (("1" (assert)
          (("1" (rewrite "cos_value_pi4")
            (("1" (rewrite "div_simp" -1) nil nil)) nil))
          nil))
        nil))
      nil)
     ("2" (expand "abs" 1)
      (("2" (typepred "pi") (("2" (assertnil nil)) nil)) nil))
    nil)
   ((sin_value_pi4 formula-decl nil sincos_quad nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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)
    (nnreal type-eq-decl nil real_types nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_simp formula-decl nil real_props nil)
    (cos_value_pi4 formula-decl nil sincos_quad nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (tan_value_def formula-decl nil tan_quad 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)
    (>= 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_lt_pi2 nonempty-type-eq-decl nil atan nil))
   shostak)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.31Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤





Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff