Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 23 kB image not shown  

Quelle  listn.prf   Sprache: Lisp

 
(listn
 (listn_ext_TCC1 0
  (listn_ext_TCC1-1 nil 3613234257 ("" (subtype-tcc) nil nil) nil nil))
 (listn_ext_TCC2 0
  (listn_ext_TCC2-1 nil 3613234257 ("" (subtype-tcc) nil nil) nil nil))
 (listn_ext 0
  (listn_ext-1 nil 3613234257
   ("" (induct "n")
    (("1" (skosimp :preds? t)
      (("1" (hide -3)
        (("1" (case-replace "l1!1=null")
          (("1" (case-replace "l2!1=null") (("1" (grind) nil nil)) nil)
           ("2" (grind) nil nil))
          nil))
        nil))
      nil)
     ("2" (skosimp)
      (("2" (skosimp 1 :preds? t)
        (("2" (case-replace "l1!1 = null")
          (("1" (expand "length" -2) (("1" (assert) nil nil)) nil)
           ("2" (case-replace "l2!1 = null")
            (("1" (expand "length" -3) (("1" (assert) nil nil)) nil)
             ("2" (inst -3 "cdr(l1!1)" "cdr(l2!1)")
              (("1" (lemma "list_cons_extensionality")
                (("1" (inst -1 "l1!1" "l2!1")
                  (("1" (assert)
                    (("1" (split -3)
                      (("1" (assert)
                        (("1" (inst -4 "0")
                          (("1" (expand "nth") (("1" (propax) nil nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp)
                        (("2" (inst -3 "i!1+1")
                          (("2" (expand "nth" -3)
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil) ("3" (assert) nil nil))
                  nil))
                nil)
               ("2" (expand "length" -2) (("2" (assert) nil nil)) nil)
               ("3" (assert) nil nil)
               ("4" (expand "length" -1) (("4" (assert) nil nil)) nil)
               ("5" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (j!1 skolem-const-decl "nat" listn nil)
    (l1!1 skolem-const-decl "listn(1 + j!1)" listn nil)
    (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
    (l2!1 skolem-const-decl "listn(1 + j!1)" listn nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (list_cons_extensionality formula-decl nil list_adt nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (listn type-eq-decl nil listn nil)
    (length def-decl "nat" list_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (list type-decl nil list_adt nil)
    (T formal-type-decl nil listn nil)
    (pred type-eq-decl nil defined_types 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))
   nil))
 (listn_0 0
  (listn_0-1 nil 3500321250 ("" (grind) nil nil)
   ((length def-decl "nat" list_props nil)) nil))
 (setnth_TCC1 0
  (setnth_TCC1-1 nil 3500321250 ("" (subtype-tcc) nil nil) nil nil))
 (setnth_TCC2 0
  (setnth_TCC2-1 nil 3500321250 ("" (subtype-tcc) nil nil) nil nil))
 (setnth_TCC3 0
  (setnth_TCC3-1 nil 3500321250 ("" (grind) nil nil)
   ((listn_0 name-judgement "listn(0)" listn 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)
    (length def-decl "nat" list_props nil))
   nil))
 (setnth_TCC4 0
  (setnth_TCC4-2 nil 3500321924 ("" (grind) nil nil)
   ((listn_0 name-judgement "listn(0)" listn 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nth def-decl "T" list_props nil)
    (length def-decl "nat" list_props nil))
   nil)
  (setnth_TCC4-1 nil 3500321250 ("" (subtype-tcc) nil nil) nil nil))
 (setnth_TCC5 0
  (setnth_TCC5-1 nil 3500321250 ("" (subtype-tcc) nil nil)
   ((listn_0 name-judgement "listn(0)" listn 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (setnth_TCC6 0
  (setnth_TCC6-1 nil 3500321250 ("" (termination-tcc) nil nil)
   ((listn_0 name-judgement "listn(0)" listn 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)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
   nil))
 (setnth_TCC7 0
  (setnth_TCC7-2 nil 3500321998
   ("" (skosimp* :preds? t)
    (("" (replace -2)
      (("" (name-replace "V4__" "v!1(r!1, n!1 - 1, f!1)" :hide? t)
        (("1" (typepred "V4__")
          (("1" (expand "length" 2)
            (("1" (assert)
              (("1" (skosimp 2)
                (("1" (expand "nth" 2)
                  (("1" (case-replace "i!1=0")
                    (("1" (assert) nil nil)
                     ("2" (inst -2 "i!1-1")
                      (("1" (assert) nil nil)
                       ("2" (hide 4)
                        (("2" (assert)
                          (("2" (typepred "i!1")
                            (("2" (replace -4)
                              (("2"
                                (expand "length" -1)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 3) (("2" (grind) nil nil)) nil)
         ("3" (hide 3) (("3" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (l!1 skolem-const-decl "list[T]" listn nil)
    (i!1 skolem-const-decl "below(length(l!1))" listn nil)
    (r!1 skolem-const-decl "list[T]" listn 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)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (listn type-eq-decl nil listn nil)
    (length def-decl "nat" list_props nil)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
    (strict_well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (list type-decl nil list_adt nil)
    (T formal-type-decl nil listn nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (listn_0 name-judgement "listn(0)" listn 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))
   nil)
  (setnth_TCC7-1 nil 3500321250 ("" (subtype-tcc) nil nil) nil nil))
 (normalize_fseq_TCC1 0
  (normalize_fseq_TCC1-1 nil 3549014873
   ("" (skeep)
    (("" (case "NOT list2finseq[T](fslist)`length = f`length")
      (("1" (hide 2)
        (("1" (expand "list2finseq")
          (("1" (replace -1)
            (("1" (expand "finseq2list")
              (("1"
                (case "FORALL (nk:nat|nk<=length(f)): length(finseq2list_rec(f, nk)) = nk")
                (("1" (inst?) nil nil)
                 ("2" (hide 2)
                  (("2" (induct "nk")
                    (("1" (expand "finseq2list_rec")
                      (("1" (assert) nil nil)) nil)
                     ("2" (skeep)
                      (("2" (assert)
                        (("2" (expand "finseq2list_rec" +)
                          (("2" (assert)
                            (("2" (expand "length" +)
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (replace -1)
        (("2" (assert)
          (("2" (decompose-equality +)
            (("2" (decompose-equality +)
              (("2" (typepred "x!1")
                (("2" (expand "list2finseq")
                  (("2" (replace -3)
                    (("2" (expand "finseq2list" +)
                      (("2" (replace -2)
                        (("2" (assert)
                          (("2"
                            (case "FORALL (xxn:nat): xxn<=x!1 IMPLIES nth(finseq2list_rec(f, xxn + (length(f)-x!1)), xxn) = f`seq(x!1)")
                            (("1" (inst - "x!1")
                              (("1" (assert) nil nil)) nil)
                             ("2" (hide 2)
                              (("2"
                                (induct "xxn")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "finseq2list_rec")
                                      (("1"
                                        (expand "nth")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skeep)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "finseq2list_rec" +)
                                      (("2"
                                        (expand "nth")
                                        (("2"
                                          (lift-if)
                                          (("2" (ground) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide 2)
                                  (("3"
                                    (assert)
                                    (("3"
                                      (case
                                       "FORALL (npt:nat): npt<=f`length IMPLIES length[T](finseq2list_rec[T](f,npt)) = npt")
                                      (("1"
                                        (skeep)
                                        (("1"
                                          (inst?)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (induct "npt")
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (expand
                                                 "finseq2list_rec")
                                                (("1"
                                                  (expand "length")
                                                  (("1"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skeep)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand
                                                 "finseq2list_rec"
                                                 +)
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (expand "length" +)
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("4"
                                  (skeep)
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (assert)
                              (("3"
                                (case
                                 "FORALL (npt:nat): npt<=f`length IMPLIES length[T](finseq2list_rec[T](f,npt)) = npt")
                                (("1"
                                  (skeep)
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide (2 3))
                                  (("2"
                                    (induct "npt")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (expand "finseq2list_rec")
                                        (("1"
                                          (expand "length")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skeep)
                                      (("2"
                                        (expand "finseq2list_rec" +)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (expand "length" +)
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("4" (skeep) (("4" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((list2finseq const-decl "finseq[T]" list2finseq nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (list type-decl nil list_adt nil)
    (T formal-type-decl nil listn nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (finseq2list const-decl "list[T]" list2finseq nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (upto_induction formula-decl nil bounded_nat_inductions nil)
    (upto nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types 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) (<= const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (finseq2list_rec def-decl "list[T]" list2finseq nil)
    (< const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (f skolem-const-decl "finseq[T]" listn nil)
    (x!1 skolem-const-decl "below[list2finseq[T](fslist)`length]" listn
     nil)
    (fslist skolem-const-decl "list[T]" listn nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" list_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (listn_0 name-judgement "listn(0)" listn nil))
   nil))
 (normalize_fseq_def 0
  (normalize_fseq_def-1 nil 3549728320
   ("" (skeep) (("" (assert) nil nil)) nil) nil shostak)))

100%


¤ Dauer der Verarbeitung: 0.26 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.