products/sources/formale Sprachen/PVS/analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: open_sets.prf   Sprache: Lisp

Original von: PVS©
(open_sets
 (open_ball?_lem 0
  (open_ball?_lem-1 nil 3258223423
   ("" (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)
   ((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)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (open?_lem 0
  (open?_lem-1 nil 3258223381
   ("" (skosimp*) (("" (expand "open?") (("" (inst?) nil nil)) nil))
    nil)
   ((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)
    (x!1 skolem-const-decl "T" open_sets nil)
    (S!1 skolem-const-decl "set[T]" open_sets nil))
   shostak))
 (open_intv_open 0
  (open_intv_open-1 nil 3258299476
   ("" (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)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (a!1 skolem-const-decl "T" open_sets nil)
    (b!1 skolem-const-decl "T" open_sets nil)
    (x!1 skolem-const-decl "(LAMBDA (x: T): a!1 < x AND x < b!1)"
     open_sets nil)
    (> const-decl "bool" 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))
   shostak))
 (above_intv_open 0
  (above_intv_open-1 nil 3258299818
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "x!1-a!1")
            (("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (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))
   shostak))
 (below_intv_open 0
  (below_intv_open-1 nil 3258299894
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "a!1-x!1") (("" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (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))
 (union_open 0
  (union_open-1 nil 3258299981
   ("" (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)
   ((open? const-decl "bool" open_sets nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (open_ball? const-decl "bool" open_sets nil)
    (S1!1 skolem-const-decl "set[T]" open_sets nil)
    (S2!1 skolem-const-decl "set[T]" open_sets nil)
    (x!1 skolem-const-decl "(union(S1!1, S2!1))" open_sets 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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))
   shostak))
 (closed_intv_closed 0
  (closed_intv_closed-1 nil 3258299631
   ("" (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)
   ((closed? const-decl "bool" open_sets nil)
    (member const-decl "bool" sets 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)
    (below_intv_open formula-decl nil open_sets nil)
    (above_intv_open formula-decl nil open_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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))
   shostak)))


¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff