Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trigx.prf Sprache: Lisp

Original von: PVS^©

(trigx
(sin_nz_TCC1 0
  (sin_nz_TCC1-1 nil 3394178341
   ("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)
   ((sin_pi2 formula-decl nil trig_basic "trig_fnd/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/"))
   nil))
(cos_nz_TCC1 0
  (cos_nz_TCC1-1 nil 3394178341
   ("" (rewrite "cos_0") (("" (assert) nil nil)) nil)
   ((cos_0 formula-decl nil trig_basic "trig_fnd/")) nil))
(cauchy_sin_nz_TCC1 0
  (cauchy_sin_nz_TCC1-1 nil 3394178341
   ("" (expand "cauchy_sin_nz?")
    (("" (lemma "lemma_div2n" ("x" "pi" "cx" "cauchy_pi" "n" "1"))
      (("" (rewrite "pi_lemma")
        (("" (expand "div2n")
          (("" (rewrite "expt_x1")
            (("" (inst + "pi / 2")
              (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pi const-decl "posreal" atan "trig_fnd/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (cauchy_pi const-decl "cauchy_real" atanx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (lemma_div2n formula-decl nil shift nil)
    (div2n const-decl "real" shift nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (sin_pi2 formula-decl nil trig_basic "trig_fnd/")
    (posint_exp application-judgement "posint" exponentiation nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (expt_x1 formula-decl nil exponentiation nil)
    (pi_lemma formula-decl nil atanx nil)
    (cauchy_sin_nz? const-decl "bool" trigx nil))
   nil))
(cauchy_cos_nz_TCC1 0
  (cauchy_cos_nz_TCC1-1 nil 3394178341
   ("" (expand "cauchy_cos_nz?")
    (("" (inst + "0")
      (("1" (expand "cauchy_prop")
        (("1" (skosimp)
          (("1" (assert)
            (("1" (expand "cauchy_zero") (("1" (propax) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "cos_0") (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (cos_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_zero const-decl "cauchy_nnreal" cauchy nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_times_int_is_int application-judgement "int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cos_0 formula-decl nil trig_basic "trig_fnd/")
    (cauchy_cos_nz? const-decl "bool" trigx nil))
   nil))
(subtype_TCC1 0
  (subtype_TCC1-1 nil 3394178341
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "cauchy_sin_nz?")
        (("" (skosimp)
          (("" (expand "cauchy_real?") (("" (inst + "nsx!1") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_sin_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_sin_nz? const-decl "bool" trigx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_real? const-decl "bool" cauchy nil))
   nil))
(subtype_TCC2 0
  (subtype_TCC2-1 nil 3394178341
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "cauchy_cos_nz?")
        (("" (skosimp)
          (("" (expand "cauchy_real?") (("" (inst + "ncx!1") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_cos_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_cos_nz? const-decl "bool" trigx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_real? const-decl "bool" cauchy nil))
   nil))
(cauchy_sec_TCC1 0
  (cauchy_sec_TCC1-1 nil 3394179601
   ("" (skosimp)
    (("" (typepred "cncx!1")
      (("" (expand "cauchy_cos_nz?")
        (("" (skosimp)
          (("" (typepred "ncx!1")
            (("" (expand "cauchy_nzreal?")
              (("" (inst + "cos(ncx!1)")
                (("" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1"))
                  (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_cos_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_cos_nz? const-decl "bool" trigx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cos_lemma formula-decl nil sincosx nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil))
   nil))
(cauchy_cosec_TCC1 0
  (cauchy_cosec_TCC1-1 nil 3394179601
   ("" (skosimp)
    (("" (typepred "cnsx!1")
      (("" (expand "cauchy_sin_nz?")
        (("" (skosimp)
          (("" (typepred "nsx!1")
            (("" (expand "cauchy_nzreal?")
              (("" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1"))
                (("" (inst + "sin(nsx!1)") (("" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_sin_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_sin_nz? const-decl "bool" trigx nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (sin_lemma formula-decl nil sincosx nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil))
   nil))
(sec_TCC1 0
  (sec_TCC1-1 nil 3394179601
   ("" (skosimp) (("" (typepred "ncx!1") (("" (assert) nil nil)) nil))
    nil)
   ((cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (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)
    (/= const-decl "boolean" notequal 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)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/"))
   nil))
(cosec_TCC1 0
  (cosec_TCC1-1 nil 3394179601
   ("" (skosimp) (("" (typepred "nsx!1") (("" (assert) nil nil)) nil))
    nil)
   ((sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (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)
    (/= const-decl "boolean" notequal 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)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/"))
   nil))
(sec_lemma 0
  (sec_lemma-1 nil 3394180068
   ("" (skosimp)
    (("" (expand "sec")
      (("" (expand "cauchy_sec")
        (("" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1"))
          (("" (assert)
            ((""
              (lemma "inv_lemma"
               ("nzx" "cos(ncx!1)" "nzcx" "cauchy_cos(cncx!1)"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sec const-decl "nzreal" trigx nil)
    (cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_cos_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_cos_nz? const-decl "bool" trigx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (cos_lemma formula-decl nil sincosx nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (cauchy_cos const-decl "cauchy_real" sincosx nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (inv_lemma formula-decl nil inv nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cauchy_sec const-decl "cauchy_nzreal" trigx nil))
   shostak))
(cosec_lemma 0
  (cosec_lemma-1 nil 3394180131
   ("" (skosimp)
    (("" (expand "cosec")
      (("" (expand "cauchy_cosec")
        (("" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1"))
          (("" (assert)
            ((""
              (lemma "inv_lemma"
               ("nzx" "sin(nsx!1)" "nzcx" "cauchy_sin(cnsx!1)"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cosec const-decl "nzreal" trigx nil)
    (sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_sin_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_sin_nz? const-decl "bool" trigx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sin_lemma formula-decl nil sincosx nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (cauchy_sin const-decl "cauchy_real" sincosx nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (inv_lemma formula-decl nil inv nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cauchy_cosec const-decl "cauchy_nzreal" trigx nil))
   shostak))
(tan_lemma_TCC1 0
  (tan_lemma_TCC1-1 nil 3394179601
   ("" (skosimp)
    (("" (typepred "ncx!1")
      (("" (expand "Tan?") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (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)
    (/= const-decl "boolean" notequal 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? const-decl "bool" sincos_def "trig_fnd/"))
   nil))
(tan_lemma 0
  (tan_lemma-1 nil 3394180209
   ("" (skosimp)
    (("" (expand "tan")
      (("" (expand "cauchy_tan")
        (("" (lemma "sin_lemma" ("x" "ncx!1" "cx" "cncx!1"))
          (("" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1"))
            (("" (assert)
              ((""
                (lemma "div_lemma"
                 ("x" "sin(ncx!1)" "cx" "cauchy_sin(cncx!1)" "nzy"
                  "cos(ncx!1)" "nzcy" "cauchy_cos(cncx!1)"))
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tan const-decl "real" sincos_def "trig_fnd/")
    (cos_nz nonempty-type-eq-decl nil trigx nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_cos_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_cos_nz? const-decl "bool" trigx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sin_lemma formula-decl nil sincosx nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_lemma formula-decl nil div nil)
    (cauchy_sin const-decl "cauchy_real" sincosx nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_cos const-decl "cauchy_real" sincosx nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (cos_lemma formula-decl nil sincosx nil)
    (cauchy_tan const-decl "cauchy_real" trigx nil))
   shostak))
(cot_lemma 0
  (cot_lemma-1 nil 3394180301
   ("" (skosimp)
    (("" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1"))
      (("" (lemma "cos_lemma" ("x" "nsx!1" "cx" "cnsx!1"))
        (("" (assert)
          ((""
            (lemma "div_lemma"
             ("nzy" "sin(nsx!1)" "nzcy" "cauchy_sin(cnsx!1)" "x"
              "cos(nsx!1)" "cx" "cauchy_cos(cnsx!1)"))
            (("1" (expand "cot")
              (("1" (expand "cauchy_cot") (("1" (assert) nil nil))
                nil))
              nil)
             ("2" (expand "cauchy_nzreal?")
              (("2" (inst + "sin(nsx!1)") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_nz nonempty-type-eq-decl nil trigx nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (cauchy_sin_nz nonempty-type-eq-decl nil trigx nil)
    (cauchy_sin_nz? const-decl "bool" trigx nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (sin_lemma formula-decl nil sincosx nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (cot const-decl "real" trigx nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cauchy_cot const-decl "cauchy_real" trigx nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (div_lemma formula-decl nil div nil)
    (cauchy_cos const-decl "cauchy_real" sincosx nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil)
    (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_sin const-decl "cauchy_real" sincosx nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (cos_lemma formula-decl nil sincosx nil))
   shostak)))

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