Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_list.prf Sprache: Lisp

Original von: PVS^©

(csequence_list
(from_list_TCC1 0
  (from_list_TCC1-1 nil 3513689704 ("" (subtype-tcc) nil nil) nil nil))
(from_list_TCC2 0
  (from_list_TCC2-1 nil 3513689704 ("" (termination-tcc) nil nil)
   ((<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
   nil))
(from_list_TCC3 0
  (from_list_TCC3-1 nil 3513689704
   ("" (expand "is_finite") (("" (propax) nil nil)) nil)
   ((is_finite inductive-decl "bool" csequence_props nil)) nil))
(from_list_length 0
  (from_list_length-1 nil 3513689766
   ("" (induct "l")
    (("1" (expand* "from_list" "length") nil nil)
     ("2" (skosimp)
      (("2" (expand "from_list" +)
        (("2" (expand "length" +) (("2" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((list_induction formula-decl nil list_adt nil)
    (T formal-type-decl nil csequence_list nil)
    (length def-decl "nat" list_props nil)
    (from_list def-decl "finite_csequence" csequence_list nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props 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)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil))
   shostak))
(from_list_index 0
  (from_list_index-1 nil 3513689797
   ("" (induct "l")
    (("1" (expand* "from_list" "length" "index?") nil nil)
     ("2" (skosimp*)
      (("2" (expand "from_list" +)
        (("2" (expand "length" +)
          (("2" (expand "index?" +)
            (("2" (ground)
              (("1" (inst - "n!1 - 1") (("1" (assert) nil nil)) nil)
               ("2" (inst - "n!1 - 1") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (list_induction formula-decl nil list_adt nil)
    (T formal-type-decl nil csequence_list nil)
    (length def-decl "nat" list_props nil)
    (< const-decl "bool" reals nil)
    (from_list def-decl "finite_csequence" csequence_list nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (index? def-decl "bool" csequence_nth nil)
    (csequence type-decl nil csequence_codt nil)
    (IFF const-decl "[bool, bool -> bool]" booleans 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)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil))
   shostak))
(from_list_nth_TCC1 0
  (from_list_nth_TCC1-1 nil 3513689704
   ("" (skolem!) (("" (rewrite "from_list_index") nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (from_list_index formula-decl nil csequence_list nil)
    (T formal-type-decl nil csequence_list nil)
    (list type-decl nil list_adt 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil nat_types nil))
   nil))
(from_list_nth 0
  (from_list_nth-1 nil 3513689877
   ("" (induct "l")
    (("1" (skolem-typepred)
      (("1" (expand "length") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp* t)
      (("2" (expand "from_list" +)
        (("2" (expand "nth" +)
          (("2" (expand "length")
            (("2" (lift-if)
              (("2" (ground) (("2" (inst - "n!1 - 1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (lemma "from_list_nth_TCC1") (("3" (propax) nil nil)) nil))
    nil)
   ((from_list_nth_TCC1 subtype-tcc nil csequence_list nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (list_induction formula-decl nil list_adt nil)
    (T formal-type-decl nil csequence_list nil)
    (nth def-decl "T" list_props nil)
    (nth def-decl "T" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (list type-decl nil list_adt 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (csequence type-decl nil csequence_codt nil)
    (index? def-decl "bool" csequence_nth nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (from_list def-decl "finite_csequence" csequence_list nil))
   shostak))
(to_list_TCC1 0
  (to_list_TCC1-1 nil 3513689704 ("" (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)
    (T formal-type-decl nil csequence_list nil)
    (csequence type-decl nil csequence_codt nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil))
   nil))
(to_list_TCC2 0
  (to_list_TCC2-1 nil 3513689704
   ("" (skosimp :preds? t)
    (("" (expand "is_finite" -) (("" (assert) nil nil)) nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil csequence_list nil)
    (csequence type-decl nil csequence_codt nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil))
   nil))
(to_list_TCC3 0
  (to_list_TCC3-1 nil 3513689704 ("" (termination-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)
    (T formal-type-decl nil csequence_list nil)
    (csequence type-decl nil csequence_codt nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length 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))
(to_list_length 0
  (to_list_length-1 nil 3513689988
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp)
      (("3" (ground)
        (("1" (expand* "to_list" "length") nil nil)
         ("2" (expand "to_list" +)
          (("2" (expand "length" +)
            (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_list nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (to_list def-decl "list" csequence_list nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (length def-decl "nat" list_props 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)
    (list type-decl nil list_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(to_list_index 0
  (to_list_index-1 nil 3513690035
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (split)
        (("1" (expand* "to_list" "length" "index?")
          (("1" (assert) nil nil)) nil)
         ("2" (flatten)
          (("2" (assert)
            (("2" (expand "to_list" +)
              (("2" (expand "length" +)
                (("2" (expand "index?" +)
                  (("2" (lift-if)
                    (("2" (ground)
                      (("1" (inst - "n!1 - 1") (("1" (assert) nil nil))
                        nil)
                       ("2" (inst - "n!1 - 1") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_list nil)
    (index? def-decl "bool" csequence_nth nil)
    (to_list def-decl "list" csequence_list nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (length def-decl "nat" list_props nil)
    (list type-decl nil list_adt nil) (< const-decl "bool" reals nil)
    (IFF 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)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(to_list_nth_TCC1 0
  (to_list_nth_TCC1-1 nil 3513689704
   ("" (skolem!) (("" (rewrite "to_list_index") nil nil)) nil)
   ((to_list_index formula-decl nil csequence_list nil)
    (T formal-type-decl nil csequence_list nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props 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)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil))
   nil))
(to_list_nth 0
  (to_list_nth-1 nil 3513690129
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp* t)
      (("3" (expand "index?")
        (("3" (expand "to_list" +)
          (("3" (expand "nth" +) (("3" (reduce) nil nil)) nil)) nil))
        nil))
      nil)
     ("4" (skosimp*) (("4" (use "to_list_nth_TCC1") nil nil)) nil))
    nil)
   ((to_list_nth_TCC1 subtype-tcc nil csequence_list nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (n!1 skolem-const-decl "indexes[T](cseq!1)" csequence_list nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_list nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_list nil)
    (nth def-decl "T" csequence_nth nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props 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)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (< const-decl "bool" reals nil) (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (to_list def-decl "list" csequence_list nil))
   shostak))
(to_from_list 0
  (to_from_list-1 nil 3513690168
   ("" (induct "l")
    (("1" (expand* "from_list" "to_list") nil nil)
     ("2" (skosimp)
      (("2" (expand "from_list" +)
        (("2" (expand "to_list" +) (("2" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((list_induction formula-decl nil list_adt nil)
    (T formal-type-decl nil csequence_list nil)
    (from_list def-decl "finite_csequence" csequence_list nil)
    (to_list def-decl "list" csequence_list nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil))
   shostak))
(from_to_list 0
  (from_to_list-1 nil 3513690211
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp)
      (("3" (expand "to_list" +)
        (("3" (expand "from_list" +) (("3" (reduce-with-ext) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_list nil)
    (to_list def-decl "list" csequence_list nil)
    (from_list def-decl "finite_csequence" csequence_list nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (list type-decl nil list_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak)))

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