Quelle riesz_linear_functionals.prf Sprache: Lisp

(riesz_linear_functionals
(additive_op?_TCC1 0
  (additive_op?_TCC1-1 nil 3492864848
   ("" (lemma "funs_sum_closed") (("" (propax) nil nil)) nil)
   ((funs_sum_closed formula-decl nil riesz_linear_functionals nil))
   nil))
(const_inv_op?_TCC1 0
  (const_inv_op?_TCC1-1 nil 3492864848
   ("" (lemma "funs_const_closed") (("" (propax) nil nil)) nil)
   ((funs_const_closed formula-decl nil riesz_linear_functionals nil))
   nil))
(linear_op_zero_TCC1 0
  (linear_op_zero_TCC1-1 nil 3492874942
   ("" (lemma "funs_contain_zero") (("" (assert) nil nil)) nil)
   ((funs_contain_zero formula-decl nil riesz_linear_functionals nil))
   nil))
(linear_op_zero 0
  (linear_op_zero-1 nil 3492874942
   ("" (skeep)
    (("" (expand "linear_op?")
      (("" (flatten)
        (("" (expand "const_inv_op?")
          (("" (inst - "LAMBDA (y:INTab): 0" "0")
            (("1" (expand "*") (("1" (assert) nil nil)) nil)
             ("2" (lemma "funs_contain_zero") (("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((linear_op? const-decl "bool" riesz_linear_functionals nil)
    (const_inv_op? const-decl "bool" riesz_linear_functionals nil)
    (funs_contain_zero formula-decl nil riesz_linear_functionals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (Funs formal-subtype-decl nil riesz_linear_functionals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (a formal-const-decl "real" riesz_linear_functionals nil)
    (< const-decl "bool" reals nil)
    (b formal-const-decl "{bb: real | a < bb}" riesz_linear_functionals
     nil)
    (INTab type-eq-decl nil riesz_interval_funs nil)
    (Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
     riesz_linear_functionals nil))
   shostak)))

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.