Quelle  trigx.prf   Sprache: unbekannt

(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)))

quality100%

[ Verzeichnis aufwärts0.7unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]