SSL interval_expr_lnexp.prf Sprache: Lisp

(interval_expr_lnexp
(ln_safe_TCC1 0
  (ln_safe_TCC1-1 nil 3567425561 ("" (subtype-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)
    (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/"))
   nil))
(Ln_Inclusion 0
  (Ln_Inclusion-2 nil 3567440894
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep :preds? t)
        (("" (expand "ln_safe")
          (("" (case-replace "x <= 0")
            (("1" (hide 1) (("1" (grind) nil nil)) nil)
             ("2" (assert) (("2" (rewrite "Ln_inclusion") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (ln_safe const-decl "real" interval_expr_lnexp 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)
    (Interval type-eq-decl nil interval nil)
    (Ln_inclusion formula-decl nil interval_lnexp nil)
    (|##| const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Pos_Precondition name-judgement "(Precondition?)" interval nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)
  (Ln_Inclusion-1 nil 3567440888 ("" (judgement-tcc) nil nil) nil nil))
(Ln_Fundamental 0
  (Ln_Fundamental-1 nil 3567440888
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Ln_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Ln_fundamental formula-decl nil interval_lnexp 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)
    (Pos? const-decl "bool" 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))
   nil))
(LN_n_TCC1 0
  (LN_n_TCC1-2 nil 3567425678 ("" (assert) nil nil)
   ((Ln_Fundamental application-judgement "(Fundamental?(Pos?))"
     interval_expr_lnexp nil)
    (Ln_Inclusion application-judgement "(Inclusion?(Pos?, ln_safe))"
     interval_expr_lnexp nil))
   nil)
  (LN_n_TCC1-1 nil 3567425561 ("" (subtype-tcc) nil nil) nil nil))
(Exp_Inclusion 0
  (Exp_Inclusion-2 nil 3568635461
   ("" (skeep)
    (("" (expand "Inclusion?")
      (("" (skeep)
        (("" (expand "exp_safe")
          (("" (rewrite "Exp_inclusion") nil nil)) nil))
        nil))
      nil))
    nil)
   ((Inclusion? const-decl "bool" interval nil)
    (exp_safe const-decl "posreal" interval_expr_lnexp 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_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)
    (PreTrue const-decl "(Precondition?)" interval_expr nil)
    (Precondition? const-decl "bool" interval nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Exp_inclusion formula-decl nil interval_lnexp nil))
   nil)
  (Exp_Inclusion-1 nil 3568635426 ("" (judgement-tcc) nil nil) nil
   nil))
(Exp_Fundamental 0
  (Exp_Fundamental-2 nil 3568635497
   ("" (skeep)
    (("" (expand "Fundamental?")
      (("" (skeep) (("" (rewrite "Exp_fundamental") nil nil)) nil))
      nil))
    nil)
   ((Fundamental? const-decl "bool" interval nil)
    (Exp_fundamental formula-decl nil interval_lnexp 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)
  (Exp_Fundamental-1 nil 3568635426 ("" (judgement-tcc) nil nil) nil
   nil))
(EXP_n_TCC1 0
  (EXP_n_TCC1-1 nil 3568635426 ("" (subtype-tcc) nil nil)
   ((Exp_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_lnexp nil)
    (Exp_Inclusion application-judgement
     "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil))
   nil))
(E_Inclusion 0
  (E_Inclusion-2 nil 3568635873
   ("" (skeep)
    (("" (expand "Includes?")
      (("" (expand "e_safe")
        (("" (expand "En")
          (("" (expand "e")
            (("" (rewrite "Exp_inclusion")
              (("" (hide 2) (("" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Includes? const-decl "bool" interval nil)
    (En const-decl "(Pos?)" interval_lnexp nil)
    (Exp_inclusion formula-decl nil interval_lnexp nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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)
    ([\|\|] const-decl "Interval" 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Exp_Inclusion application-judgement
     "(Inclusion?(PreTrue, exp_safe))" interval_expr_lnexp nil)
    (Exp_Fundamental application-judgement "(Fundamental?(PreTrue))"
     interval_expr_lnexp nil)
    (Proper_Exp application-judgement "ProperInterval" interval_lnexp
     nil)
    (e_bound name-judgement "{x: posreal | e_lb < e AND e < e_ub}"
     exp_approx "lnexp_fnd/")
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (r2i_Pos application-judgement "(Pos?)" interval nil)
    (r2i_Nneg application-judgement "(NonNeg?)" interval nil)
    (exp_1 formula-decl nil ln_exp "lnexp_fnd/")
    (|##| const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (e const-decl "posreal" ln_exp "lnexp_fnd/")
    (e_safe const-decl "[Unit -> real]" interval_expr_lnexp nil))
   nil)
  (E_Inclusion-1 nil 3568635847 ("" (judgement-tcc) nil nil) nil nil)))

quality100%

¤ 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.0.23Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.