Quelle csequence_generate.prf Sprache: Lisp

(csequence_generate
(generate_TCC1 0
  (generate_TCC1-1 nil 3513557144
   (""
    (case "FORALL (x: nat, f: [T -> T], t: T): NOT has_length(coreduce[T, [[T -> T], T]](generate_struct)(f, t), x)")
    (("1" (skolem!)
      (("1" (rewrite "is_finite_def")
        (("1" (skolem!) (("1" (inst - "n!1" "f!1" "t!1") nil nil))
          nil))
        nil))
      nil)
     ("2" (delete 2)
      (("2" (induct "x")
        (("1" (skolem!)
          (("1" (expand* "has_length" "generate_struct" "coreduce") nil
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (inst - "f!1" "f!1(t!1)")
            (("2" (expand "generate_struct")
              (("2" (expand "coreduce" -)
                (("2" (expand "has_length" -) (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (is_finite_def formula-decl nil csequence_props 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_generate nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (has_length def-decl "bool" csequence_props nil)
    (csequence_struct type-decl nil csequence_codt_coreduce nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (inj_empty? adt-recognizer-decl "[csequence_struct -> boolean]"
     csequence_codt_coreduce nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (inj_nonempty? adt-recognizer-decl "[csequence_struct -> boolean]"
     csequence_codt_coreduce nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil)
    (generate_struct const-decl "csequence_struct" csequence_generate
     nil))
   nil))
(generate_first 0
  (generate_first-1 nil 3513557263
   ("" (expand* "generate" "generate_struct" "coreduce") nil nil)
   ((coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil)
    (generate_struct const-decl "csequence_struct" csequence_generate
     nil)
    (generate const-decl "infinite_csequence" csequence_generate nil))
   shostak))
(generate_rest 0
  (generate_rest-1 nil 3513557286
   ("" (expand* "generate" "generate_struct")
    (("" (expand "coreduce" 1 1) (("" (propax) nil nil)) nil)) nil)
   ((coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil)
    (generate const-decl "infinite_csequence" csequence_generate nil)
    (generate_struct const-decl "csequence_struct" csequence_generate
     nil))
   shostak))
(generate_nth_TCC1 0
  (generate_nth_TCC1-1 nil 3513557144
   ("" (skolem!) (("" (use "index?_infinite") nil nil)) 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)
    (generate const-decl "infinite_csequence" csequence_generate 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)
    (index?_infinite formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_generate nil))
   nil))
(generate_nth 0
  (generate_nth-1 nil 3513557325
   ("" (induct "n")
    (("1" (skolem!)
      (("1"
        (expand* "iterate" "nth" "generate" "generate_struct"
         "coreduce")
        nil nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "iterate" +)
        (("2" (expand "nth" +)
          (("2" (inst - "f!1" "f!1(t!1)")
            (("2" (rewrite "generate_rest")
              (("2" (rewrite "iterate_invariant") nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skolem!) (("3" (use "generate_nth_TCC1") nil nil)) nil))
    nil)
   ((generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
    (generate_rest formula-decl nil csequence_generate nil)
    (iterate_invariant formula-decl nil function_iterate nil)
    (coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil)
    (generate_struct const-decl "csequence_struct" csequence_generate
     nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (iterate def-decl "T" function_iterate nil)
    (nth def-decl "T" csequence_nth nil)
    (indexes type-eq-decl nil 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_generate nil)
    (csequence type-decl nil csequence_codt nil)
    (index? def-decl "bool" csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (generate const-decl "infinite_csequence" csequence_generate nil))
   shostak))
(generate_add 0
  (generate_add-1 nil 3513557394
   ("" (skosimp)
    (("" (expand* "generate" "generate_struct")
      (("" (expand "coreduce" 1 2) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((generate_struct const-decl "csequence_struct" csequence_generate
     nil)
    (generate const-decl "infinite_csequence" csequence_generate nil)
    (coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil))
   shostak))
(generate_some 0
  (generate_some-1 nil 3513557413
   ("" (auto-rewrite "generate_nth")
    (("" (skolem!)
      (("" (use "nth_some")
        (("" (ground)
          (("1" (skolem!) (("1" (inst?) nil nil)) nil)
           ("2" (skolem!)
            (("2" (inst + "n!1")
              (("2" (use "generate_nth_TCC1") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((generate_nth formula-decl nil csequence_generate 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)
    (n!1 skolem-const-decl "nat" csequence_generate nil)
    (t!1 skolem-const-decl "T" csequence_generate nil)
    (f!1 skolem-const-decl "[T -> T]" csequence_generate nil)
    (generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (generate const-decl "infinite_csequence" csequence_generate nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil csequence_generate nil)
    (nth_some formula-decl nil csequence_nth nil))
   shostak))
(generate_every 0
  (generate_every-1 nil 3513557494
   ("" (auto-rewrite "generate_nth")
    (("" (skolem!)
      (("" (use "nth_every")
        (("" (ground)
          (("1" (skolem!)
            (("1" (inst - "n!1")
              (("1" (use "generate_nth_TCC1") nil nil)) nil))
            nil)
           ("2" (skolem!) (("2" (inst - "i!1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((generate_nth formula-decl nil csequence_generate 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)
    (n!1 skolem-const-decl "nat" csequence_generate nil)
    (t!1 skolem-const-decl "T" csequence_generate nil)
    (f!1 skolem-const-decl "[T -> T]" csequence_generate nil)
    (generate_nth_TCC1 subtype-tcc nil csequence_generate nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (generate const-decl "infinite_csequence" csequence_generate nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil csequence_generate nil)
    (nth_every formula-decl nil csequence_nth nil))
   shostak)))

quality100%

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