| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: intervals_real.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(interval_reals
(open_ball?_lem 0 (open_ball?_lem-1 nil 3258223423 3292322828 ("" (skosimp*) (("" (prop) (("1" (expand "open_ball?") (("1" (skosimp*) (("1" (expand "open_ball") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst + "delta!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_ball?") (("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "open_ball") (("2" (inst + "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((subset? const-decl "bool" sets 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) (bool nonempty-type-eq-decl nil booleans 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) (member const-decl "bool" sets nil) (open_ball const-decl "set[T]" open_sets nil) (open_ball? const-decl "bool" open_sets nil)) 30503 110 nil nil)) (open?_lem 0 (open?_lem-1 nil 3258223381 3292322828 ("" (skosimp*) (("" (expand "open?") (("" (inst?) nil nil)) nil)) nil) unchecked ((open? const-decl "bool" open_sets 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) (T_pred const-decl "[real -> boolean]" open_sets nil) (T formal-subtype-decl nil open_sets nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) nil nil) 20 20 t shostak)) (Open_empty 0 (Open_empty-1 nil 3320064681 3320064682 ("" (skosimp*) nil nil) proved nil 1331 130 t shostak)) (open_intv_open 0 (open_intv_open-1 nil 3258299476 3292322828 ("" (skosimp*) (("" (expand "open?") (("" (skosimp*) (("" (expand "open_ball?") (("" (inst + "min(x!1 -a!1,b!1-x!1)") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((open? const-decl "bool" open_sets nil) (open_ball? const-decl "bool" open_sets nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, 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) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_pred const-decl "[real -> boolean]" open_sets nil) (T formal-subtype-decl nil open_sets nil) (< const-decl "bool" reals nil) nil nil nil (> const-decl "bool" reals nil)) 224 220 t shostak)) (above_intv_open 0 (above_intv_open-1 nil 3258299818 3292322829 ("" (skosimp*) (("" (expand "open?") (("" (skosimp*) (("" (expand "open_ball?") (("" (inst + "x!1-a!1") (("" (skosimp*) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((open? const-decl "bool" open_sets nil) (open_ball? const-decl "bool" open_sets nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (T formal-subtype-decl nil open_sets nil) (T_pred const-decl "[real -> boolean]" open_sets nil) (- 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)) 99 100 t shostak)) (below_intv_open 0 (below_intv_open-1 nil 3258299894 3292322829 ("" (skosimp*) (("" (expand "open?") (("" (skosimp*) (("" (expand "open_ball?") (("" (inst + "a!1-x!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((open? const-decl "bool" open_sets nil) (open_ball? const-decl "bool" open_sets nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (T formal-subtype-decl nil open_sets nil) (T_pred const-decl "[real -> boolean]" open_sets nil) (- 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)) 103 110 nil nil)) (union_open 0 (union_open-1 nil 3258299981 3292322829 ("" (skosimp*) (("" (expand "open?") (("" (skosimp*) (("" (expand "open_ball?") (("" (typepred "x!1") (("" (expand "union") (("" (expand "member") (("" (split -2) (("1" (hide -4) (("1" (inst?) (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3) (("2" (inst?) (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((open? const-decl "bool" open_sets nil) (open_ball? const-decl "bool" open_sets nil) nil nil 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) (member const-decl "bool" sets 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) (T_pred const-decl "[real -> boolean]" open_sets nil) (T formal-subtype-decl nil open_sets nil) (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)) 165 170 t shostak)) (closed_intv_closed 0 (closed_intv_closed-1 nil 3258299631 3292322829 ("" (skosimp*) (("" (expand "closed?") (("" (case-replace "complement(LAMBDA (x): a!1 <= x AND x <= b!1) = union(above_intv(b!1),below_intv(a!1))") (("1" (hide -1) (("1" (lemma "union_open") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (lemma "above_intv_open ") (("1" (inst?) (("1" (assert) (("1" (lemma "below_intv_open ") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((closed? const-decl "bool" open_sets nil) (member const-decl "bool" sets nil) (below_intv_open formula-decl nil open_sets nil) (above_intv_open formula-decl nil open_sets nil) (union_open formula-decl nil open_sets nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (union const-decl "set" sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (complement const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil open_sets nil) (T_pred const-decl "[real -> boolean]" open_sets 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)) 203 160 t shostak))) ¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
