Quelle csequence_nth.prf Sprache: Lisp

(csequence_nth
(index?_TCC1 0
  (index?_TCC1-1 nil 3513452743 ("" (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))
(index?_TCC2 0
  (index?_TCC2-1 nil 3513452743 ("" (termination-tcc) nil nil) nil
   nil))
(index?_0 0
  (index?_0-1 nil 3513452758
   ("" (expand "index?") (("" (propax) nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)) shostak))
(index?_ub 0
  (index?_ub-1 nil 3513452798
   ("" (induct "n")
    (("1" (expand* "index?" "is_finite") (("1" (reduce) nil nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "index?" +)
        (("2" (expand "is_finite" +)
          (("2" (inst - "rest(cseq!1)") (("2" (ground) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (index? def-decl "bool" csequence_nth nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth 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))
(index?_lt 0
  (index?_lt-1 nil 3513452862
   ("" (measure-induct+ "i" ("cseq" "i"))
    (("" (typepred "x!2")
      (("" (skosimp)
        (("" (expand "index?" (-1 +))
          (("" (ground)
            (("" (inst - "rest(x!1)" "x!2 - 1")
              (("" (inst - "n!1 - 1") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth 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)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (measure_induction formula-decl nil measure_induction nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
(index?_finite 0
  (index?_finite-1 nil 3513452922
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "index?" +)
        (("3" (expand "length" +)
          (("3" (lift-if)
            (("3" (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)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_nth 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)
    (index? def-decl "bool" csequence_nth 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))
(index?_finite_bound 0
  (index?_finite_bound-1 nil 3513452978
   ("" (skolem!)
    (("" (use "index?_finite")
      (("" (assert) (("" (inst + "length(fseq!1)") nil nil)) nil))
      nil))
    nil)
   ((index?_finite formula-decl nil csequence_nth 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)
    (T formal-type-decl nil csequence_nth 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)
    (number nonempty-type-decl nil numbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(index?_infinite 0
  (index?_infinite-1 nil 3513453017
   ("" (induct "n")
    (("1" (skolem-typepred)
      (("1" (expand* "index?" "is_finite") (("1" (assert) nil nil))
        nil))
      nil)
     ("2" (skosimp* t)
      (("2" (expand "is_finite" +)
        (("2" (expand "index?" +)
          (("2" (ground) (("2" (inst - "rest(iseq!1)") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (index? def-decl "bool" csequence_nth 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_nth 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))
(index?_infinite_full 0
  (index?_infinite_full-1 nil 3513453068
   ("" (skolem!)
    (("" (expand* "full?" "member")
      (("" (prop)
        (("1" (use "index?_infinite") nil nil)
         ("2" (use "index?_finite")
          (("2" (inst - "length(cseq!1)") (("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (full? const-decl "bool" sets nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props 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)
    (number nonempty-type-decl nil numbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_nth 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (index?_infinite formula-decl nil csequence_nth nil))
   shostak))
(index?_prop 0
  (index?_prop-1 nil 3513453116
   ("" (skolem!)
    (("" (use "index?_ub")
      (("" (rewrite "index?_finite") (("" (ground) nil nil)) nil))
      nil))
    nil)
   ((index?_ub formula-decl nil csequence_nth 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)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (index?_finite formula-decl nil csequence_nth nil))
   shostak))
(index?_nonempty 0
  (index?_nonempty-1 nil 3513453138
   ("" (skolem-typepred)
    (("" (expand "index?") (("" (flatten) nil nil)) nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth 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)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(nth_TCC1 0
  (nth_TCC1-1 nil 3513452743
   ("" (skosimp) (("" (use "index?_nonempty") nil nil)) nil)
   ((T formal-type-decl nil csequence_nth nil)
    (csequence type-decl nil csequence_codt 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)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index?_nonempty formula-decl nil csequence_nth nil))
   nil))
(nth_TCC2 0
  (nth_TCC2-1 nil 3513452743
   ("" (skosimp) (("" (use "index?_nonempty") nil nil)) nil)
   ((T formal-type-decl nil csequence_nth nil)
    (csequence type-decl nil csequence_codt 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)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index?_nonempty formula-decl nil csequence_nth nil))
   nil))
(nth_TCC3 0
  (nth_TCC3-1 nil 3513452743
   ("" (skosimp :preds? t)
    (("" (assert)
      (("" (expand "index?" -) (("" (propax) 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)
    (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_nth nil)
    (csequence type-decl nil csequence_codt 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))
(nth_TCC4 0
  (nth_TCC4-1 nil 3513452743 ("" (termination-tcc) nil nil) nil nil))
(nth_extensionality_TCC1 0
  (nth_extensionality_TCC1-1 nil 3513452743 ("" (subtype-tcc) nil nil)
   ((indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth 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)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(nth_extensionality 0
  (nth_extensionality-1 nil 3513453402
   ("" (skosimp)
    (("" (lemma "coinduction")
      ((""
        (inst -
         "LAMBDA cseq1, cseq2: index?(cseq1) = index?(cseq2) AND (FORALL (n: indexes(cseq1)): nth(cseq1, n) = nth(cseq2, n))"
         "cseq1!1" "cseq2!1")
        (("1" (assert) nil nil)
         ("2" (delete -1 -2 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp)
              (("2" (lemma "index?_0")
                (("2" (inst-cp - "y!1")
                  (("2" (inst - "x!1")
                    (("2" (smash)
                      (("1" (skolem!)
                        (("1" (inst - "1 + n!1")
                          (("1" (expand "nth" -)
                            (("1" (propax) nil nil)) nil)
                           ("2" (expand "index?" +)
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (decompose-equality)
                        (("2" (decompose-equality)
                          (("2" (inst - "1 + x!2")
                            (("2" (expand "index?" -)
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("3" (inst - 0)
                        (("3" (expand "nth") (("3" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (skosimp*) (("3" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_nth nil)
    (coinduction formula-decl nil csequence_codt nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (x!1 skolem-const-decl "csequence[T]" csequence_nth nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (n!1 skolem-const-decl "indexes(rest(x!1))" csequence_nth nil)
    (index?_0 formula-decl nil csequence_nth nil)
    (PRED type-eq-decl nil defined_types nil)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nth def-decl "T" 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)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil))
   shostak))
(nth_every 0
  (nth_every-1 nil 3513453611
   ("" (skolem!)
    (("" (prop)
      (("1" (skolem-typepred)
        (("1" (generalize-skolem-constants)
          (("1" (skolem + ("_" "_" "p"))
            (("1"
              (measure-induct+ "i_1" ("cseq_1" "i_1")
               :skolem-typepreds? t)
              (("1" (expand "index?")
                (("1" (expand "every" -3)
                  (("1" (expand "nth" +)
                    (("1" (lift-if)
                      (("1" (ground)
                        (("1" (inst - "rest(x!1)" "x!2 - 1")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (iff) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "every_weak_coinduction")
        (("2"
          (inst - "p!1"
           "LAMBDA cseq: FORALL (i: indexes(cseq)): p!1(nth(cseq, i))")
          (("2" (split)
            (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)
             ("2" (delete -1 2)
              (("2" (skosimp)
                (("2" (lift-if)
                  (("2" (ground)
                    (("1" (inst - 0)
                      (("1" (expand "nth") (("1" (propax) nil nil))
                        nil)
                       ("2" (expand "index?") (("2" (propax) nil nil))
                        nil))
                      nil)
                     ("2" (skolem!)
                      (("2" (inst - "1 + i!1")
                        (("1" (expand "nth" -) (("1" (propax) nil nil))
                          nil)
                         ("2" (expand "index?")
                          (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nth def-decl "T" csequence_nth nil)
    (pred type-eq-decl nil defined_types nil)
    (every coinductive-decl "boolean" csequence_codt nil)
    (PRED type-eq-decl nil defined_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (well_founded? const-decl "bool" orders nil)
    (< const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (measure_induction formula-decl nil measure_induction nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (TRUE const-decl "bool" booleans 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)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt 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)
    (indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth 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)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i!1 skolem-const-decl "indexes(rest(a!1))" csequence_nth nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (a!1 skolem-const-decl "csequence[T]" csequence_nth nil)
    (every_weak_coinduction formula-decl nil csequence_codt nil))
   shostak))
(nth_some 0
  (nth_some-1 nil 3513453839
   ("" (skolem!)
    (("" (prop)
      (("1" (lemma "some_weak_induction")
        (("1"
          (inst - "p!1"
           "LAMBDA cseq: EXISTS (i: indexes(cseq)): p!1(nth(cseq, i))")
          (("1" (split)
            (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)
             ("2" (delete -1 2)
              (("2" (skosimp)
                (("2" (lift-if)
                  (("2" (ground)
                    (("1" (inst + 0)
                      (("1" (expand "nth") (("1" (propax) nil nil))
                        nil)
                       ("2" (expand "index?") (("2" (propax) nil nil))
                        nil))
                      nil)
                     ("2" (skolem!)
                      (("2" (inst + "1 + i!1")
                        (("1" (expand "nth" +) (("1" (propax) nil nil))
                          nil)
                         ("2" (expand "index?")
                          (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skolem-typepred)
        (("2" (generalize-skolem-constants)
          (("2" (skolem + ("_" "_" "p"))
            (("2"
              (measure-induct+ "i_1" ("cseq_1" "i_1")
               :skolem-typepreds? t)
              (("1" (expand "index?")
                (("1" (expand "some" +)
                  (("1" (expand "nth" -3)
                    (("1" (lift-if)
                      (("1" (ground)
                        (("1" (inst - "rest(x!1)" "x!2 - 1")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (iff) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (pred type-eq-decl nil defined_types nil)
    (csequence type-decl nil csequence_codt 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)
    (nth def-decl "T" csequence_nth nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (i!1 skolem-const-decl "indexes(rest(a!1))" csequence_nth nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (a!1 skolem-const-decl "csequence[T]" csequence_nth nil)
    (some_weak_induction formula-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_nth nil)
    (some inductive-decl "boolean" csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (well_founded? const-decl "bool" orders nil)
    (< const-decl "bool" reals nil)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (measure_induction formula-decl nil measure_induction nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (TRUE const-decl "bool" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(last_TCC1 0
  (last_TCC1-1 nil 3513452743
   ("" (skolem-typepred)
    (("" (rewrite "length_nonempty?_rew")
      (("" (assert) (("" (rewrite "index?_finite") nil nil)) nil))
      nil))
    nil)
   ((length_nonempty?_rew formula-decl nil csequence_length nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (index?_finite formula-decl nil csequence_nth 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nonempty_finite_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt 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_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(last_rest_TCC1 0
  (last_rest_TCC1-1 nil 3513452743
   ("" (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_nth 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)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_finite_csequence type-eq-decl nil csequence_props nil))
   nil))
(last_rest 0
  (last_rest-1 nil 3513454103
   ("" (induct "nfseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (assert) nil nil)
     ("4" (skosimp)
      (("4" (expand "last")
        (("4" (expand "length" 2 2)
          (("4" (expand "nth" 2 2)
            (("4" (lemma "length_empty?_rew" ("cseq" "rest(cseq!1)"))
              (("4" (reduce) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     ("5" (skosimp) (("5" (forward-chain "last_rest_TCC1") nil nil))
      nil))
    nil)
   ((last_rest_TCC1 subtype-tcc nil csequence_nth nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nth def-decl "T" csequence_nth nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_nth 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)
    (OR const-decl "[bool, bool -> bool]" booleans 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (is_finite inductive-decl "bool" csequence_props nil))
   shostak)))

quality100%

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