Quelle fseqs_ops_def.prf Sprache: Lisp

(fseqs_ops_def
(delete_TCC1 0
  (delete_TCC1-1 nil 3411486742 ("" (subtype-tcc) nil nil) nil nil))
(delete_TCC2 0
  (delete_TCC2-1 nil 3411486742
   ("" (skosimp*)
    (("" (lift-if)
      (("" (typepred "nefs!1`seq")
        (("" (prop)
          (("1" (inst?) (("1" (assert) nil nil)) nil)
           ("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs_ops_def nil)
    (default formal-const-decl "T" fseqs_ops_def nil)
    (barray type-eq-decl nil fseqs_def nil)
    (fseq type-eq-decl nil fseqs_def nil)
    (> const-decl "bool" reals nil)
    (ne_fseq type-eq-decl nil fseqs_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(insert_TCC1 0
  (insert_TCC1-1 nil 3411486742 ("" (subtype-tcc) nil 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(insert_TCC2 0
  (insert_TCC2-1 nil 3411486742
   ("" (skosimp*)
    (("" (typepred "fs!1`seq")
      (("" (lift-if)
        (("" (prop)
          (("1" (inst?) (("1" (assert) nil nil)) nil)
           ("2" (inst?) (("2" (assert) nil nil)) nil)
           ("3" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (fseq type-eq-decl nil fseqs_def nil)
    (barray type-eq-decl nil fseqs_def nil)
    (default formal-const-decl "T" fseqs_ops_def nil)
    (T formal-type-decl nil fseqs_ops_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (i!1 skolem-const-decl "nat" fseqs_ops_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(addend_TCC1 0
  (addend_TCC1-1 nil 3489912526 ("" (subtype-tcc) nil 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(insert_delete 0
  (insert_delete-1 nil 3411487018
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) (("1" (postpone) nil nil)) nil)
       ("2" (grind)
        (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil))
          nil)
         ("2" (postpone) nil nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil fseqs_ops_def nil)
    (default formal-const-decl "T" fseqs_ops_def nil)
    (barray type-eq-decl nil fseqs_def nil)
    (fseq type-eq-decl nil fseqs_def nil)
    (delete const-decl "fseq" fseqs_ops_def nil)
    (ne_fseq type-eq-decl nil fseqs_def nil)
    (> const-decl "bool" reals nil)
    (insert const-decl "fseq" fseqs_ops_def nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(add_first_rest 0
  (add_first_rest-1 nil 3411487139
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil)
       ("2" (apply-extensionality 1 :hide? t)
        (("2" (expand "rest")
          (("2" (expand "first")
            (("2" (expand "^")
              (("2" (lift-if)
                (("2" (prop)
                  (("1" (typepred "x!1")
                    (("1" (typepred "nefs!1`seq")
                      (("1" (grind :exclude "default")
                        (("1" (typepred "nefs!1`seq")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (grind :exclude "default")
                    (("2" (typepred "nefs!1`seq")
                      (("2" (inst?) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil fseqs_ops_def nil)
    (default formal-const-decl "T" fseqs_ops_def nil)
    (barray type-eq-decl nil fseqs_def nil)
    (fseq type-eq-decl nil fseqs_def nil)
    (rest const-decl "fseq" fseqs_ops_def nil)
    (ne_fseq type-eq-decl nil fseqs_def 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)
    (first const-decl "T" fseqs_ops_def nil)
    (add const-decl "fseq" fseqs_ops_def nil)
    (insert const-decl "fseq" fseqs_ops_def nil)
    (^ const-decl "fseq" fseqs_def nil)
    (empty_seq const-decl "fsq" fseqs_def nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (empty_seq_fseq name-judgement "fseq" fseqs_ops_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil))
   shostak))
(some_p_trivial 0
  (some_p_trivial-1 nil 3489912526
   ("" (skeep)
    (("" (expand "some")
      (("" (inst + "fs`length+1") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((some const-decl "bool" fseqs_ops_def nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fseq type-eq-decl nil fseqs_def nil)
    (barray type-eq-decl nil fseqs_def nil)
    (default formal-const-decl "T" fseqs_ops_def nil)
    (T formal-type-decl nil fseqs_ops_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
(map_TCC1 0
  (map_TCC1-1 nil 3489912526 ("" (subtype-tcc) nil 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil)))

quality100%

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