Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Hoare_Total_EX.thy Sprache: Lisp

Original von: PVS^©

(interval_chain
(IMP_chain_rule_TCC1 0
  (IMP_chain_rule_TCC1-1 nil 3304701211
   ("" (lemma "deriv_domain_Xt[X]") (("" (propax) nil nil)) nil)
   ((deriv_domain_Xt formula-decl nil interval_deriv 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)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil))
   shostak))
(IMP_chain_rule_TCC2 0
  (IMP_chain_rule_TCC2-2 nil 3304701423
   ("" (expand "not_one_element?")
    (("" (skeep)
      (("" (typepred "x")
        (("" (typepred "X")
          (("" (expand "StrictlyProper?")
            (("" (inst 1 "if x=lb(X) then ub(X) else lb(X) endif")
              (("1" (grind) nil nil) ("2" (grind) nil nil)
               ("3" (grind) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x skolem-const-decl "XT" interval_chain 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil)
    (XT type-eq-decl nil interval_chain nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
(IMP_chain_rule_TCC3 0
  (IMP_chain_rule_TCC3-1 nil 3304701483
   ("" (lemma "deriv_domain_Xt[Y]") (("" (propax) nil nil)) nil)
   ((deriv_domain_Xt formula-decl nil interval_deriv 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)
    (StrictInterval? const-decl "bool" interval nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil))
   shostak))
(IMP_chain_rule_TCC4 0
  (IMP_chain_rule_TCC4-1 nil 3304701436
   ("" (expand "not_one_element?")
    (("" (skeep)
      (("" (typepred "x")
        (("" (typepred "Y")
          (("" (expand "StrictlyProper?")
            (("" (inst 1 "if x=lb(Y) then ub(Y) else lb(Y) endif")
              (("1" (grind) nil nil) ("2" (grind) nil nil)
               ("3" (grind) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x skolem-const-decl "YT" interval_chain 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil)
    (YT type-eq-decl nil interval_chain nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
(Diff_comp_TCC1 0
  (Diff_comp_TCC1-1 nil 3319158888
   ("" (skosimp :preds? t) (("" (inst -2 "t!1") nil 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (XT type-eq-decl nil interval_chain nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil))
   nil))
(Diff_comp 0
  (Diff_comp-1 nil 3319159473
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "composition_derivable_fun")
        (("" (inst -1 "f!1" "g!1")
          (("" (assert) (("" (expand "o") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((f!1 skolem-const-decl
     "(LAMBDA (f: (Diff?[X])): FORALL (t: XT): f(t) ## Y)"
     interval_chain nil)
    (O const-decl "T3" function_props nil)
    (YT type-eq-decl nil interval_chain nil)
    (composition_derivable_fun formula-decl nil chain_rule "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (XT type-eq-decl nil interval_chain nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil))
   nil))
(Deriv_comp_TCC1 0
  (Deriv_comp_TCC1-1 nil 3319158888
   ("" (skosimp :preds? t) (("" (rewrite "Diff_comp") nil nil)) nil)
   ((Diff_comp formula-decl nil interval_chain 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (XT type-eq-decl nil interval_chain nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil))
   nil))
(Deriv_comp 0
  (Deriv_comp-1 nil 3319159512
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_comp_fun")
        (("" (inst -1 "f!1" "g!1")
          (("1" (expand "o")
            (("1" (assert)
              (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (g!1 skolem-const-decl "(Diff?[Y])" interval_chain nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (f!1 skolem-const-decl
     "(LAMBDA (f: (Diff?[X])): FORALL (t: XT): f(t) ## Y)"
     interval_chain nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (O const-decl "T3" function_props nil)
    (YT type-eq-decl nil interval_chain nil)
    (deriv_comp_fun formula-decl nil chain_rule "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (X formal-const-decl "(StrictInterval?)" interval_chain nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (XT type-eq-decl nil interval_chain nil)
    (Y formal-const-decl "(StrictInterval?)" interval_chain nil))
   nil)))

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