Quelle interval_expr_trig.prf Sprache: Lisp

(interval_expr_trig
(Pi_Inclusion 0
  (Pi_Inclusion-2 nil 3567446620
   ("" (skeep)
    (("" (expand "Includes?")
      (("" (expand "pi_safe") (("" (rewrite "Pi_inclusion") nil nil))
        nil))
      nil))
    nil)
   ((Includes? const-decl "bool" interval nil)
    (Pi_inclusion formula-decl nil interval_trig nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pi_safe const-decl "[Unit -> real]" interval_expr_trig nil))
   nil)
  (Pi_Inclusion-1 nil 3567446620 ("" (judgement-tcc) nil nil) nil nil))
(Sin_Inclusion 0
  (Sin_Inclusion-1 nil 3567441159
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep) (("" (rewrite "Sin_inclusion") nil nil)) nil)) nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (Sin_inclusion formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(Sin_Fundamental 0
  (Sin_Fundamental-1 nil 3567441159
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Sin_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Sin_fundamental formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(SIN_n_TCC1 0
  (SIN_n_TCC1-1 nil 3567424354 ("" (assert) nil nil)
   ((Sin_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_trig nil)
    (Sin_Inclusion application-judgement "(Inclusion?(PreTrue, sin))"
     interval_expr_trig nil))
   nil))
(Cos_Inclusion 0
  (Cos_Inclusion-2 nil 3567441187
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep) (("" (rewrite "Cos_inclusion") nil nil)) nil)) nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (Cos_inclusion formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Cos_Inclusion-1 nil 3567441159 ("" (judgement-tcc) nil nil) nil
   nil))
(Cos_Fundamental 0
  (Cos_Fundamental-2 nil 3567441252
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Cos_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Cos_fundamental formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Cos_Fundamental-1 nil 3567441159 ("" (judgement-tcc) nil nil) nil
   nil))
(COS_n_TCC1 0
  (COS_n_TCC1-2 nil 3567424511 ("" (assert) nil nil)
   ((Cos_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_trig nil)
    (Cos_Inclusion application-judgement "(Inclusion?(PreTrue, cos))"
     interval_expr_trig nil))
   nil)
  (COS_n_TCC1-1 nil 3567424479 ("" (subtype-tcc) nil nil) nil nil))
(Tan_Inclusion 0
  (Tan_Inclusion-1 nil 3567449214
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep :preds? t)
        (("" (expand "tan_safe")
          (("" (case-replace "Tan?(x)")
            (("1" (rewrite "Tan_inclusion") nil nil)
             ("2" (hide 2)
              (("2" (lemma "TAN_Tan")
                (("2" (inst?)
                  (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (tan_safe const-decl "real" interval_expr_trig nil)
    (TAN_Tan formula-decl nil interval_trig nil)
    (Tan_inclusion formula-decl nil interval_trig nil)
    (Interval type-eq-decl nil interval nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (TAN? const-decl "bool" interval_trig nil)
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (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))
   nil))
(Tan_Fundamental 0
  (Tan_Fundamental-1 nil 3567449214
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Tan_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Tan_fundamental formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (TAN? const-decl "bool" interval_trig nil))
   nil))
(TAN_Precondition 0
  (TAN_Precondition-1 nil 3567680644 ("" (judgement-tcc) nil 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (TAN? const-decl "bool" interval_trig nil)
    (Precondition? const-decl "bool" interval nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
(TAN_n_TCC1 0
  (TAN_n_TCC1-1 nil 3567449214 ("" (subtype-tcc) nil nil)
   ((Tan_Fundamental application-judgement "(Fundamental?(TAN?(n)))"
     interval_expr_trig nil)
    (Tan_Inclusion application-judgement
     "(Inclusion?(TAN?(n), tan_safe))" interval_expr_trig nil))
   nil))
(Atan_Inclusion 0
  (Atan_Inclusion-2 nil 3567441192
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep) (("" (rewrite "Atan_inclusion") nil nil)) nil))
      nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (Atan_inclusion formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Atan_Inclusion-1 nil 3567441159 ("" (judgement-tcc) nil nil) nil
   nil))
(Atan_Fundamental 0
  (Atan_Fundamental-2 nil 3567441256
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Atan_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Atan_fundamental formula-decl nil interval_trig nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (PRED type-eq-decl nil defined_types nil)
    (Precondition? const-decl "bool" interval nil)
    (PreTrue const-decl "(Precondition?)" interval_expr 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Atan_Fundamental-1 nil 3567441159 ("" (judgement-tcc) nil nil) nil
   nil))
(ATAN_n_TCC1 0
  (ATAN_n_TCC1-2 nil 3567425386 ("" (assert) nil nil)
   ((Atan_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_trig nil)
    (Atan_Inclusion application-judgement "(Inclusion?(PreTrue, atan))"
     interval_expr_trig nil))
   nil)
  (ATAN_n_TCC1-1 nil 3567425328 ("" (subtype-tcc) nil nil) nil nil)))

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.