Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: fseqs_ops.prf Sprache: Lisp

Original von: PVS^©

(fseqs_ops
(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-nonempty-type-decl nil fseqs_ops nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil) (> const-decl "bool" reals nil)
    (ne_fseq type-eq-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (default const-decl "T" fseqs 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)
   ((default const-decl "T" fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (T formal-nonempty-type-decl nil fseqs_ops 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 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)
    (T formal-nonempty-type-decl nil fseqs_ops nil)
    (default const-decl "T" fseqs 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-nonempty-type-decl nil fseqs_ops nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (delete const-decl "fseq" fseqs_ops nil)
    (ne_fseq type-eq-decl nil fseqs nil)
    (> const-decl "bool" reals nil)
    (insert const-decl "fseq" fseqs_ops 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-nonempty-type-decl nil fseqs_ops nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (rest const-decl "fseq" fseqs_ops nil)
    (ne_fseq type-eq-decl nil fseqs 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 nil)
    (add const-decl "fseq" fseqs_ops nil)
    (insert const-decl "fseq" fseqs_ops nil)
    (^ const-decl "fseq" fseqs nil)
    (empty_seq const-decl "fsq" fseqs nil)
    (default const-decl "T" fseqs 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 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 nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (T formal-nonempty-type-decl nil fseqs_ops 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)
    (T formal-nonempty-type-decl nil fseqs_ops nil)
    (default const-decl "T" fseqs nil))
   nil)))

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.