Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: right_left_cosets.prf Sprache: Lisp

Original von: PVS^©

(deriv_domains
(IMP_derivatives_def_TCC1 0
  (IMP_derivatives_def_TCC1-1 nil 3471264254 3477816156
   ("" (expand "deriv_domain?")
    (("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil))
      nil))
    nil)
   proved
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (>= const-decl "bool" reals 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)
    (TRUE const-decl "bool" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil))
   33333 60 t nil))
(IMP_derivatives_def_TCC2 0
  (IMP_derivatives_def_TCC2-1 nil 3471264254 3477816177
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   proved
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   17936 30 t nil))
(IMP_derivatives_def_TCC3 0
  (IMP_derivatives_def_TCC3-1 nil 3471264323 3477816197
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (typepred "x!1")
        (("" (inst + "min(abs(x!1/2),e!1/2)")
          (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   proved
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (e!1 skolem-const-decl "posreal" deriv_domains nil)
    (x!1 skolem-const-decl "posreal" deriv_domains nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   15573 190 t nil))
(IMP_derivatives_def_TCC4 0
  (IMP_derivatives_def_TCC4-1 nil 3471264323 3477816210
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   proved
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (>= 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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   9534 40 t nil))
(IMP_derivatives_def_TCC5 0
  (IMP_derivatives_def_TCC5-1 nil 3471264606 3477816225
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (typepred "x!1")
        (("" (inst + -e!1/2) (("" (grind) nil nil)) nil)) nil))
      nil))
    nil)
   proved
   ((real_lt_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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         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)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   7893 100 t nil))
(IMP_derivatives_def_TCC6 0
  (IMP_derivatives_def_TCC6-1 nil 3471264606 3477816240
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1-1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   proved
   ((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types 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)
    (real_minus_real_is_real application-judgement "real" reals 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)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   10837 30 t nil))
(IMP_derivatives_def_TCC7 0
  (IMP_derivatives_def_TCC7-1 nil 3471611038 3477816253
   ("" (expand "deriv_domain?")
    (("" (skosimp*)
      (("" (typepred "x!1")
        (("" (flatten)
          (("" (case "x!1 > 0")
            (("1" (inst-cp + e!1/2)
              (("1" (grind) nil nil)
               ("2" (flatten) (("2" (assert) nil nil)) nil))
              nil)
             ("2" (inst-cp + -e!1/2)
              (("1" (grind) nil nil)
               ("2" (flatten) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (x!1 skolem-const-decl "nzreal" deriv_domains nil)
    (e!1 skolem-const-decl "posreal" deriv_domains nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (> const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   8762 130 t nil))
(IMP_derivatives_def_TCC8 0
  (IMP_derivatives_def_TCC8-1 nil 3471611038 3477816266
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (typepred "x!1")
        (("" (flatten)
          (("" (inst + "x!1/2") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   proved
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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)
    (/= const-decl "boolean" notequal 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil))
   9520 40 t nil)))

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