Quelle monotone_sequences.prf Sprache: Lisp

(monotone_sequences
(reflexive_closure_ascending 0
  (reflexive_closure_ascending-1 nil 3314543892
   ("" (skolem-typepred)
    (("" (expand* "ascending?" "reflexive_closure" "union" "member")
      (("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (ascending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil monotone_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(reflexive_closure_descending 0
  (reflexive_closure_descending-1 nil 3314543932
   ("" (skolem-typepred)
    (("" (expand* "descending?" "reflexive_closure" "union" "member")
      (("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil monotone_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(ascending_lem 0
  (ascending_lem-1 nil 3314543958
   ("" (skolem-typepred)
    (("" (expand* "preserves" "restrict")
      (("" (induct "x2")
        (("1" (skosimp) (("1" (assert) nil nil)) nil)
         ("2" (skosimp*)
          (("2" (case-replace "x1!1 = j!1")
            (("1" (hide -2)
              (("1" (expand "ascending?")
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (inst?)
              (("2" (assert)
                (("2" (expand "transitive?")
                  (("2"
                    (inst - "seq!1(x1!1)" "seq!1(j!1)"
                     "seq!1(1 + j!1)")
                    (("2" (assert)
                      (("2" (hide 2 -1)
                        (("2" (expand "ascending?")
                          (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict const-decl "R" restrict nil)
    (preserves const-decl "bool" functions nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (ascending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil monotone_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(descending_lem 0
  (descending_lem-1 nil 3314544287
   ("" (skolem-typepred)
    (("" (rewrite "ascending_lem")
      (("" (expand* "ascending?" "converse" "descending?") nil nil))
      nil))
    nil)
   ((transitive_converse application-judgement "(transitive?[T])"
     relation_converse_props nil)
    (ascending_lem formula-decl nil monotone_sequences nil)
    (converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (ascending? const-decl "bool" monotone_sequences nil)
    (strict_total_order_restrict application-judgement
     "(strict_total_order?[S])" restrict_order_props nil)
    (trichotomous_restrict application-judgement "(trichotomous?[S])"
     restrict_order_props nil)
    (strict_order_restrict application-judgement "(strict_order?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (irreflexive_restrict application-judgement "(irreflexive?[S])"
     restrict_order_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (T formal-type-decl nil monotone_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(ascending_subsequence 0
  (ascending_subsequence-1 nil 3314544355
   ("" (skolem-typepred)
    (("" (lemma "preserves_composition[nat, nat, T]")
      (("" (inst?)
        (("" (invoke (inst - "%1" "%1" "lt!1") (! -2 0 1))
          (("" (expand "preserves" -2)
            (("" (assert)
              (("" (hide -2)
                (("" (split)
                  (("1" (hide -3)
                    (("1" (expand* "ascending?" "preserves" "restrict")
                      (("1" (skolem!)
                        (("1" (inst?) (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "ascending_lem") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preserves_composition formula-decl nil function_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (irreflexive_restrict application-judgement "(irreflexive?[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)
    (strict_order_restrict application-judgement "(strict_order?[S])"
     restrict_order_props nil)
    (trichotomous_restrict application-judgement "(trichotomous?[S])"
     restrict_order_props nil)
    (strict_total_order_restrict application-judgement
     "(strict_total_order?[S])" restrict_order_props nil)
    (preserves const-decl "bool" functions nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (ascending_lem formula-decl nil monotone_sequences nil)
    (ascending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences nil)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (T formal-type-decl nil monotone_sequences nil)
    (< const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (preserves const-decl "bool" functions nil)
    (PRED type-eq-decl nil defined_types 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))
   shostak))
(descending_subsequence 0
  (descending_subsequence-1 nil 3314544571
   ("" (skolem-typepred)
    (("" (use "ascending_subsequence" ("lt" "converse(lt!1)"))
      (("1" (expand* "ascending?" "converse" "descending?") nil nil)
       ("2" (expand* "ascending?" "converse" "descending?") nil nil))
      nil))
    nil)
   ((converse const-decl "pred[[T2, T1]]" relation_defs nil)
    (ascending_subsequence formula-decl nil monotone_sequences nil)
    (transitive_converse application-judgement "(transitive?[T])"
     relation_converse_props nil)
    (seq!1 skolem-const-decl "(descending?(lt!1))" monotone_sequences
     nil)
    (lt!1 skolem-const-decl "(transitive?[T])" monotone_sequences nil)
    (ascending? const-decl "bool" monotone_sequences nil)
    (descending? const-decl "bool" monotone_sequences nil)
    (sequence type-eq-decl nil sequences nil)
    (pred type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (T formal-type-decl nil monotone_sequences nil)
    (< const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (preserves const-decl "bool" functions nil)
    (PRED type-eq-decl nil defined_types 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))
   shostak)))

quality100%

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