Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: interval_lnexp.prf Sprache: Lisp

Original von: PVS^©

(interval_lnexp
(Exp_TCC1 0
  (Exp_TCC1-1 nil 3318619234 ("" (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)
    (>= 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
(Exp_fundamental 0
  (Exp_fundamental-1 nil 3568634161
   ("" (skeep)
    (("" (expand "Exp")
      (("" (lemma "exp_lb_increasing")
        (("" (lemma "exp_ub_increasing")
          (("" (inst - "n")
            (("" (inst - "n")
              (("" (expand "increasing?")
                (("" (inst - "ub(X)" "ub(Y)")
                  (("" (inst - "lb(Y)" "lb(X)")
                    (("" (assert)
                      (("" (expand "<<")
                        (("" (expand "[||]") (("" (ground) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Exp const-decl "(Pos?)" interval_lnexp nil)
    (exp_ub_increasing formula-decl nil exp_approx "lnexp_fnd/")
    (Interval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (increasing? const-decl "bool" real_fun_preds "reals/")
    (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)
    (exp_lb_increasing formula-decl nil exp_approx "lnexp_fnd/"))
   nil))
(Ln_TCC1 0
  (Ln_TCC1-1 nil 3318619234 ("" (subtype-tcc) nil nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(Ln_TCC2 0
  (Ln_TCC2-1 nil 3318619234 ("" (subtype-tcc) nil nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(Ln_fundamental 0
  (Ln_fundamental-1 nil 3558352527
   ("" (skeep)
    (("" (expand "Ln")
      (("" (copy -3)
        (("" (expand "<<" -1)
          (("" (flatten)
            (("" (copy -4)
              (("" (expand "Proper?" -1)
                (("" (case "lb(Y)>0")
                  (("1" (assert)
                    (("1" (expand "[||]")
                      (("1" (expand "<<")
                        (("1" (flatten)
                          (("1" (lemma "ln_lb_increasing")
                            (("1" (inst?)
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "ln_ub_increasing")
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (expand "Pos?")
                      (("2" (expand "Gt") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Ln const-decl "Interval" interval_lnexp nil)
    (<< const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (ln_ub_increasing formula-decl nil ln_approx "lnexp_fnd/")
    (ln_lb_increasing formula-decl nil ln_approx "lnexp_fnd/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Pos_Precondition name-judgement "(Precondition?)" interval nil)
    (Pos? const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
(Exp_inclusion 0
  (Exp_inclusion-1 nil 3317039172
   ("" (skeep)
    (("" (expand "##")
      (("" (expand* "exp" "Exp")
        (("" (assert)
          (("" (flatten)
            (("" (lemma "exp_bounds")
              (("" (split)
                (("1" (inst -1 "n" "lb(X)")
                  (("1" (flatten)
                    (("1" (lemma "exp_increasing")
                      (("1" (expand "increasing?")
                        (("1" (inst -1 "lb(X)" "x")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (inst -1 "n" "ub(X)")
                  (("2" (flatten)
                    (("2" (lemma "exp_increasing")
                      (("2" (expand "increasing?")
                        (("2" (inst -1 "x" "ub(X)")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((|##| const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil)
    (exp_bounds formula-decl nil exp_approx "lnexp_fnd/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (exp_increasing formula-decl nil ln_exp "lnexp_fnd/")
    (increasing? const-decl "bool" real_fun_preds "reals/")
    (Exp const-decl "(Pos?)" interval_lnexp nil))
   shostak))
(Ln_inclusion_TCC1 0
  (Ln_inclusion_TCC1-1 nil 3317040534 ("" (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   shostak))
(Ln_inclusion 0
  (Ln_inclusion-1 nil 3317040548
   ("" (skeep)
    (("" (expand "Ln")
      (("" (lift-if)
        (("" (split 1)
          (("1" (flatten)
            (("1" (expand "##")
              (("1" (assert)
                (("1" (expand ">")
                  (("1" (flatten)
                    (("1" (lemma "ln_bounds")
                      (("1" (split)
                        (("1" (inst -1 "n" "lb(X)")
                          (("1" (flatten)
                            (("1" (lemma "ln_increasing")
                              (("1"
                                (expand "increasing?")
                                (("1"
                                  (inst -1 "lb(X)" "x")
                                  (("1" (assert) nil nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (inst -1 "n" "ub(X)")
                          (("2" (flatten)
                            (("2" (lemma "ln_increasing")
                              (("2"
                                (expand "increasing?")
                                (("2"
                                  (inst -1 "x" "ub(X)")
                                  (("1" (assert) nil nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (flatten) (("2" (hide 2) (("2" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Ln const-decl "Interval" interval_lnexp nil)
    (|##| const-decl "bool" interval nil)
    (> const-decl "bool" reals nil)
    (ln_bounds formula-decl nil ln_approx "lnexp_fnd/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (Interval type-eq-decl nil interval nil)
    (ln_increasing formula-decl nil ln_exp "lnexp_fnd/")
    (x skolem-const-decl "real" interval_lnexp nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (increasing? const-decl "bool" real_fun_preds "reals/")
    (ub_interval formula-decl nil interval nil)
    (lb_interval formula-decl nil interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Pos_Precondition name-judgement "(Precondition?)" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
(Proper_Ln 0
  (Proper_Ln-1 nil 3579731922
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst?)
        (("" (assert)
          (("" (skeep)
            (("" (lemma "Member_Proper")
              (("" (inst? -1 :where 1)
                (("" (inst -1 "ln(x)")
                  (("1" (assert)
                    (("1" (rewrite "Ln_inclusion") nil nil)) nil)
                   ("2" (hide-all-but (-1 -3 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Pos_Precondition name-judgement "(Precondition?)" interval nil)
    (Member_Proper formula-decl nil interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x skolem-const-decl "real" interval_lnexp nil)
    (> const-decl "bool" reals nil)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (Ln_inclusion formula-decl nil interval_lnexp nil)
    (Gt const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ln const-decl "Interval" interval_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)
    (PosInterval type-eq-decl nil proper_arith nil)
    (Pos? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval 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))
   nil))
(Proper_Exp 0
  (Proper_Exp-1 nil 3579731922
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst?)
        (("" (assert)
          (("" (skeep)
            (("" (lemma "Member_Proper")
              (("" (inst? -1 :where 1)
                (("" (inst -1 "exp(x)")
                  (("" (assert)
                    (("" (rewrite "Exp_inclusion") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Member_Proper formula-decl nil interval nil)
    (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (= const-decl "[T, T -> boolean]" equalities 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)
    (Exp_inclusion formula-decl nil interval_lnexp nil)
    (Exp const-decl "(Pos?)" interval_lnexp nil)
    (Pos? const-decl "bool" interval 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)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval 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))
   nil))
(proper_Exp_TCC1 0
  (proper_Exp_TCC1-1 nil 3579731922 ("" (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)
    (>= 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)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Exp const-decl "(Pos?)" interval_lnexp nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil)))

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