Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 4 kB

Quelle bounded_nats.prf Sprache: Lisp

(bounded_nats
(every_nonempty_set_has_least 0
  (every_nonempty_set_has_least-1 nil 3314637118
   ("" (skolem-typepred)
    (("" (use "non_empty_bounded_below_has_least")
      ((""
        (expand* "non_empty_bounded_below?" "nonempty?" "empty?"
         "member")
        (("" (skolem!)
          (("" (lemma "non_empty_finite_bounded_below")
            (("" (inst - "{t: T | x!1(t) AND t <= x!2}")
              (("1" (expand "non_empty_bounded_below?")
                (("1" (flatten)
                  (("1"
                    (expand* "bounded_below?" "lower_bound?"
                     "restrict")
                    (("1" (skolem!)
                      (("1" (inst + "t!1")
                        (("1" (skolem!)
                          (("1" (inst-cp - "x!2")
                            (("1" (inst - "r!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (split)
                (("1" (expand "is_finite")
                  (("1"
                    (inst + "1 + x!2"
                     "LAMBDA (n: ({t: T | x!1(t) AND t <= x!2})): n")
                    (("1" (expand "injective?")
                      (("1" (skosimp) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (expand* "empty?" "member")
                  (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((non_empty_bounded_below_has_least judgement-tcc nil
     bounded_integers nil)
    (x!1 skolem-const-decl "(nonempty?[T])" bounded_nats nil)
    (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (x!2 skolem-const-decl "T" bounded_nats nil)
    (<= const-decl "bool" reals nil)
    (is_finite const-decl "bool" finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (r!1 skolem-const-decl "(x!1)" bounded_nats nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     restrict_order_props nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     restrict_order_props nil)
    (injective? const-decl "bool" functions nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (non_empty_finite_bounded_below judgement-tcc nil
     non_empty_bounded_sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_nats nil)
    (T_pred const-decl "[nat -> boolean]" bounded_nats 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 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.