Quelle csequence_insert.prf Sprache: Lisp

(csequence_insert
(insert_TCC1 0
  (insert_TCC1-1 nil 3513474439 ("" (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))
   nil))
(insert_TCC2 0
  (insert_TCC2-1 nil 3513474439 ("" (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(insert_TCC3 0
  (insert_TCC3-1 nil 3513474439 ("" (termination-tcc) nil nil) nil
   nil))
(insert_finite 0
  (insert_finite-1 nil 3513474439
   ("" (induct "index")
    (("1" (reduce) nil nil)
     ("2" (expand* "insert" "is_finite") nil nil)
     ("3" (skosimp* t)
      (("3" (expand "insert" +)
        (("3" (expand "is_finite" (-1 +))
          (("3" (ground) (("3" (inst - "rest(fseq!1)" "t!1") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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))
(insert_infinite 0
  (insert_infinite-1 nil 3513474439
   ("" (induct "index")
    (("1" (skolem-typepred)
      (("1" (expand "insert")
        (("1" (expand "is_finite" -) (("1" (propax) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp* t)
      (("2" (expand "insert" -3)
        (("2" (expand "is_finite" (-3 +))
          (("2" (ground) (("2" (inst - "rest(iseq!1)" "t!1") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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))
(insert_first 0
  (insert_first-1 nil 3513474782
   ("" (expand "insert") (("" (propax) nil nil)) nil)
   ((insert def-decl "nonempty_csequence" csequence_insert nil))
   shostak))
(insert_rest 0
  (insert_rest-1 nil 3513474789
   ("" (expand "insert" 1 1) (("" (propax) nil nil)) nil)
   ((insert def-decl "nonempty_csequence" csequence_insert nil))
   shostak))
(insert_length 0
  (insert_length-1 nil 3513474968
   ("" (induct "index")
    (("1" (expand "insert")
      (("1" (expand "length" 1 1) (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "insert" +)
        (("2" (expand "length" +)
          (("2" (lift-if)
            (("2" (rewrite "length_empty?_rew")
              (("2" (ground)
                (("2" (inst - "rest(fseq!1)" "t!1")
                  (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((length_empty?_rew formula-decl nil csequence_length nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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)
    (insert_finite application-judgement "nonempty_finite_csequence"
     csequence_insert nil))
   shostak))
(insert_index_TCC1 0
  (insert_index_TCC1-1 nil 3513474439 ("" (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(insert_index 0
  (insert_index-1 nil 3513475083
   ("" (auto-rewrite "index?_prop")
    (("" (auto-rewrite "insert_length")
      (("" (skolem!)
        (("" (smash)
          (("1" (use "insert_finite" ("fseq" "cseq!1")) nil nil)
           ("2" (use "insert_infinite") (("2" (assert) nil nil)) nil)
           ("3" (use "insert_infinite") (("3" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((index?_prop formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_insert 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (insert_length formula-decl nil csequence_insert 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)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (insert_finite judgement-tcc nil csequence_insert 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)
    (insert_infinite application-judgement "infinite_csequence"
     csequence_insert nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_insert nil)
    (insert_infinite judgement-tcc nil csequence_insert nil))
   shostak))
(insert_nth_TCC1 0
  (insert_nth_TCC1-1 nil 3513474439
   ("" (skolem!)
    (("" (rewrite "insert_index")
      (("" (lift-if)
        (("" (ground)
          (("" (use "index?_lt" ("n" "n!1 - 1"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (insert_index formula-decl nil csequence_insert nil)
    (T formal-type-decl nil csequence_insert 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)
    (csequence type-decl nil csequence_codt nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (< const-decl "bool" reals 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (index?_lt formula-decl nil csequence_nth nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(insert_nth 0
  (insert_nth-1 nil 3513475567
   ("" (induct "index")
    (("1" (skolem!)
      (("1" (expand "insert")
        (("1" (expand "nth" 1 2) (("1" (propax) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "insert" +)
        (("2" (expand "nth" +)
          (("2" (use "index?_0")
            (("2" (use "index?_lt")
              (("2" (lift-if)
                (("2" (lift-if)
                  (("2" (ground)
                    (("2" (inst - "rest(cseq!1)" "t!1" "n!1 - 1")
                      (("2" (lift-if)
                        (("2" (lift-if)
                          (("2" (lift-if) (("2" (ground) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skolem!) (("3" (use "insert_nth_TCC1") nil nil)) nil))
    nil)
   ((insert_nth_TCC1 subtype-tcc nil csequence_insert nil)
    (index?_lt formula-decl nil csequence_nth nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (index?_0 formula-decl nil csequence_nth nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nth def-decl "T" csequence_nth nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types 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)
    (T formal-type-decl nil csequence_insert nil)
    (csequence type-decl nil csequence_codt nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (< const-decl "bool" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   shostak))
(insert_0 0
  (insert_0-1 nil 3513476241
   ("" (expand "insert") (("" (propax) nil nil)) nil)
   ((insert def-decl "nonempty_csequence" csequence_insert nil))
   shostak))
(insert_add 0
  (insert_add-1 nil 3513476246
   ("" (expand "insert" 1 2) (("" (propax) nil nil)) nil)
   ((insert def-decl "nonempty_csequence" csequence_insert nil))
   shostak))
(insert_last_TCC1 0
  (insert_last_TCC1-1 nil 3513474439
   ("" (skosimp) (("" (use "index?_nonempty") nil nil)) 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)
    (index!1 skolem-const-decl "nat" csequence_insert nil)
    (fseq!1 skolem-const-decl "finite_csequence[T]" csequence_insert
     nil)
    (index?_nonempty formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_insert nil))
   nil))
(insert_last 0
  (insert_last-1 nil 3513476319
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (ground)
        (("1"
          (expand* "insert" "index?" "last" "nth" "length" "length")
          nil nil)
         ("2" (expand "insert" +)
          (("2" (expand "last")
            (("2" (expand "nth" +)
              (("2" (expand "length" +)
                (("2" (expand "length" 1 2)
                  (("2" (expand "index?" +)
                    (("2" (use "length_empty?_rew")
                      (("2" (smash)
                        (("1" (expand "nth" +) (("1" (propax) nil nil))
                          nil)
                         ("2" (expand "nth" 4 1)
                          (("2" (propax) nil nil)) nil)
                         ("3"
                          (lemma "length_empty?_rew"
                           ("cseq"
                            "insert(t!1, index!1 - 1, rest(cseq!1))"))
                          (("3" (assert)
                            (("3"
                              (use "insert_finite"
                                   ("fseq"
                                    "rest(cseq!1)"
                                    "index"
                                    "index!1 - 1"))
                              nil nil))
                            nil))
                          nil)
                         ("4"
                          (lemma "length_empty?_rew"
                           ("cseq"
                            "insert(t!1, index!1 - 1, rest(cseq!1))"))
                          (("4" (assert)
                            (("4"
                              (use "insert_finite"
                                   ("fseq"
                                    "rest(cseq!1)"
                                    "index"
                                    "index!1 - 1"))
                              nil nil))
                            nil))
                          nil)
                         ("5"
                          (lemma "length_empty?_rew"
                           ("cseq" "rest(cseq!1)"))
                          (("5" (assert)
                            (("5" (expand "index?")
                              (("5" (propax) nil nil)) nil))
                            nil))
                          nil)
                         ("6" (inst - "t!1" "index!1 - 1")
                          (("6" (assert) nil nil)) nil)
                         ("7" (inst - "t!1" "index!1 - 1")
                          (("7" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (skosimp*) (("4" (use "index?_nonempty") nil nil)) nil)
     ("5" (skosimp*)
      (("5" (use "insert_finite" ("fseq" "fseq!2")) nil nil)) nil))
    nil)
   ((index?_nonempty formula-decl nil csequence_nth nil)
    (index!1 skolem-const-decl "nat" csequence_insert nil)
    (fseq!2 skolem-const-decl "csequence[T]" csequence_insert nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (insert_finite judgement-tcc nil csequence_insert nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nth def-decl "T" csequence_nth nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_insert nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (last const-decl "T" csequence_nth nil)
    (nonempty_finite_csequence type-eq-decl nil csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (index? def-decl "bool" csequence_nth 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil))
   shostak))
(insert_beyond 0
  (insert_beyond-1 nil 3513476824
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "insert" +)
        (("3" (lift-if)
          (("3" (lift-if)
            (("3" (ground)
              (("3" (rewrite "length_empty?_rew")
                (("3" (decompose-equality 3)
                  (("3" (inst - "t!1" "index!1 - 1")
                    (("3" (expand "length" (-4 1))
                      (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_minus_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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_insert nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def 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)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_insert nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (> const-decl "bool" reals 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))
(insert_insert_TCC1 0
  (insert_insert_TCC1-1 nil 3513474439 ("" (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(insert_insert 0
  (insert_insert-1 nil 3513476975
   ("" (skolem + ("t!1" "u!1" "_" "_" "_"))
    (("" (induct "n")
      (("1" (skolem!)
        (("1" (expand "insert" 1 1)
          (("1" (expand "insert" 1 3)
            (("1" (expand "insert" 1 4)
              (("1" (reduce)
                (("1" (expand "insert" 1 2) (("1" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (lemma "length_empty?_rew" ("cseq" "cseq!1"))
          (("2" (hide 1)
            (("2" (prop)
              (("1" (reveal 1)
                (("1" (assert)
                  (("1" (expand "insert" 1 2)
                    (("1" (expand "insert" 1 1)
                      (("1" (expand "insert" 1 3)
                        (("1" (expand "insert" 1 4)
                          (("1" (expand "insert" +)
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (reveal 1)
                (("2" (expand "insert" +)
                  (("2" (smash)
                    (("1" (expand "insert" +) (("1" (propax) nil nil))
                      nil)
                     ("2" (decompose-equality 2)
                      (("2" (expand "insert" 1 1)
                        (("2" (propax) nil nil)) nil))
                      nil)
                     ("3" (decompose-equality 2)
                      (("3" (inst - "m!1 - 1" "rest(cseq!1)")
                        (("3" (expand "is_finite" +)
                          (("3" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("4" (decompose-equality 3)
                      (("4" (inst - "m!1 - 1" "rest(cseq!1)")
                        (("4" (expand "is_finite" +)
                          (("4" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (reveal 1)
                (("3" (expand "length" 1)
                  (("3" (expand "insert" +)
                    (("3" (smash)
                      (("1" (expand "insert" +)
                        (("1" (propax) nil nil)) nil)
                       ("2" (decompose-equality 2)
                        (("2" (expand "insert" 1 1)
                          (("2" (propax) nil nil)) nil))
                        nil)
                       ("3" (decompose-equality 2)
                        (("3" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("3" (expand "is_finite" -1)
                            (("3" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("4" (decompose-equality 3)
                        (("4" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("4" (assert) nil nil)) nil))
                        nil)
                       ("5" (decompose-equality 4)
                        (("5" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("5" (assert) nil nil)) nil))
                        nil)
                       ("6" (decompose-equality 3)
                        (("6" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("6" (assert) nil nil)) nil))
                        nil)
                       ("7" (decompose-equality 4)
                        (("7" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("7" (assert) nil nil)) nil))
                        nil)
                       ("8" (decompose-equality 3)
                        (("8" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("8" (expand "is_finite" +)
                            (("8" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("9" (decompose-equality 4)
                        (("9" (inst - "m!1 - 1" "rest(cseq!1)")
                          (("9" (expand "is_finite" +)
                            (("9" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (skosimp) (("3" (assert) nil nil)) nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (> const-decl "bool" reals nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (<= const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(insert_extensionality 0
  (insert_extensionality-1 nil 3513477483
   ("" (induct "index")
    (("1" (expand "insert")
      (("1" (skosimp) (("1" (decompose-equality) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "insert" -2)
        (("2" (lift-if)
          (("2" (lift-if)
            (("2" (lift-if)
              (("2" (ground)
                (("1" (decompose-equality) nil nil)
                 ("2" (decompose-equality) nil nil)
                 ("3" (decompose-equality)
                  (("3" (inst? -)
                    (("3" (decompose-equality 3) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((csequence_add_extensionality formula-decl nil csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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))
   shostak))
(insert_some 0
  (insert_some-1 nil 3513477534
   ("" (induct "index")
    (("1" (expand "insert")
      (("1" (expand "some" 1 1) (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "some" +)
        (("2" (expand "insert" +)
          (("2" (lift-if)
            (("2" (lift-if)
              (("2" (lift-if)
                (("2" (ground)
                  (("1" (expand "some" -1) (("1" (propax) nil nil))
                    nil)
                   ("2" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("2" (assert) nil nil)) nil)
                   ("3" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("3" (assert) nil nil)) nil)
                   ("4" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("4" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (some inductive-decl "boolean" csequence_codt nil)
    (PRED type-eq-decl nil defined_types nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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))
   shostak))
(insert_every 0
  (insert_every-1 nil 3513477592
   ("" (induct "index")
    (("1" (expand "insert")
      (("1" (expand "every" 1 1) (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "every" +)
        (("2" (expand "insert" +)
          (("2" (lift-if)
            (("2" (lift-if)
              (("2" (lift-if)
                (("2" (ground)
                  (("1" (expand "every" +) (("1" (propax) nil nil))
                    nil)
                   ("2" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("2" (assert) nil nil)) nil)
                   ("3" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("3" (assert) nil nil)) nil)
                   ("4" (inst - "p!1" "t!1" "rest(cseq!1)")
                    (("4" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (insert def-decl "nonempty_csequence" csequence_insert nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (every coinductive-decl "boolean" csequence_codt nil)
    (PRED type-eq-decl nil defined_types nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_insert 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))
   shostak)))

quality100%

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