Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_subsequence.prf Sprache: Isabelle

Original von: PVS^©

(csequence_concatenate
(concatenate_struct_TCC1 0
  (concatenate_struct_TCC1-1 nil 3513603892 ("" (subtype-tcc) nil nil)
   nil nil))
(concatenate_struct_TCC2 0
  (concatenate_struct_TCC2-1 nil 3513603892 ("" (subtype-tcc) nil nil)
   nil nil))
(o_finite 0
  (o_finite-1 nil 3513603892
   (""
    (measure-induct+ "length(fseq1) + length(fseq2)" ("fseq1" "fseq2")
     :skolem-typepreds? t)
    (("" (expand* "o" "concatenate_struct")
      (("" (expand "coreduce" +)
        (("" (expand "is_finite" +)
          (("" (smash)
            (("1" (expand "is_finite" -2)
              (("1" (inst - "x!1" "rest(x!2)")
                (("1" (expand "length" -3 4) (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (expand "is_finite" -1)
              (("2" (inst - "rest(x!1)" "x!2")
                (("2" (expand "length" -3 3) (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (x!1 skolem-const-decl "finite_csequence[T]" csequence_concatenate
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (x!2 skolem-const-decl "finite_csequence[T]" csequence_concatenate
     nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (< const-decl "bool" reals 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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (naturalnumber 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)
    (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_concatenate nil)
    (measure_induction formula-decl nil measure_induction nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil))
   nil))
(o_finiteness 0
  (o_finiteness-1 nil 3513604048
   ("" (skosimp)
    ((""
      (lemma
       "measure_induction[{seqs : [csequence, csequence] | is_finite(seqs`1 o seqs`2)}, nat, LAMBDA (cseqs: {seqs : [csequence, csequence] | is_finite(seqs`1 o seqs`2)}): length(cseqs`1 o cseqs`2), restrict[[real, real], [nat, nat], bool](<)]")
      (("1"
        (inst -
         "LAMBDA (cseqs: [csequence, csequence] | is_finite(cseqs`1 o cseqs`2)): is_finite(cseqs`1) AND is_finite(cseqs`2)")
        (("1" (split)
          (("1" (inst - "(cseq1!1, cseq2!1)") nil nil)
           ("2" (delete -1 2)
            (("2" (skosimp :preds? t)
              (("2" (expand* "o" "concatenate_struct" "restrict")
                (("2" (expand "coreduce" -1)
                  (("2" (expand "is_finite" -1)
                    (("2" (hide 1)
                      (("2" (smash)
                        (("1" (reveal 1)
                          (("1" (expand "is_finite" +)
                            (("1" (propax) nil nil)) nil))
                          nil)
                         ("2" (reveal 1)
                          (("2" (expand "is_finite" +)
                            (("2" (propax) nil nil)) nil))
                          nil)
                         ("3" (reveal 1)
                          (("3" (inst - "(x!1`1, rest(x!1`2))")
                            (("1" (expand "is_finite" 1 2)
                              (("1"
                                (expand "coreduce" -3 2)
                                (("1"
                                  (expand "length" -3 2)
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand* "o" "concatenate_struct")
                              nil nil))
                            nil))
                          nil)
                         ("4" (reveal 1)
                          (("4" (inst - "(rest(x!1`1), x!1`2)")
                            (("1" (expand "is_finite" 1 1)
                              (("1"
                                (expand "coreduce" -2 2)
                                (("1"
                                  (expand "length" -2 2)
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand* "o" "concatenate_struct")
                              nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide-all-but 1)
        (("2" (lemma "wf_nat") (("2" (grind) nil nil)) nil)) nil))
      nil))
    nil)
   ((< const-decl "bool" reals nil)
    (restrict const-decl "R" restrict 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)
    (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)
    (O const-decl "csequence" csequence_concatenate 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_concatenate nil)
    (measure_induction formula-decl nil measure_induction nil)
    (irreflexive_restrict application-judgement "(irreflexive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (strict_order_restrict application-judgement "(strict_order?[S])"
     restrict_order_props nil)
    (trichotomous_restrict application-judgement "(trichotomous?[S])"
     restrict_order_props nil)
    (strict_total_order_restrict application-judgement
     "(strict_total_order?[S])" restrict_order_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (cseq2!1 skolem-const-decl "csequence[T]" csequence_concatenate
     nil)
    (cseq1!1 skolem-const-decl "csequence[T]" csequence_concatenate
     nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (x!1 skolem-const-decl
     "{seqs: [csequence, csequence] | is_finite(seqs`1 o seqs`2)}"
     csequence_concatenate nil)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (wf_nat formula-decl nil naturalnumbers nil))
   shostak))
(o_infinite1 0
  (o_infinite1-1 nil 3513603892
   ("" (skolem-typepred) (("" (forward-chain "o_finiteness") nil nil))
    nil)
   ((o_finiteness formula-decl nil csequence_concatenate nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans 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_concatenate nil))
   nil))
(o_infinite2 0
  (o_infinite2-1 nil 3513603892
   ("" (skolem-typepred) (("" (forward-chain "o_finiteness") nil nil))
    nil)
   ((o_finiteness formula-decl nil csequence_concatenate nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans 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_concatenate nil))
   nil))
(o_empty 0
  (o_empty-1 nil 3513604377
   ("" (expand* "o" "concatenate_struct" "coreduce")
    (("" (reduce) nil nil)) nil)
   ((O const-decl "csequence" csequence_concatenate 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)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil))
   shostak))
(o_nonempty 0
  (o_nonempty-1 nil 3513604397
   ("" (skolem!) (("" (use "o_empty") (("" (ground) nil nil)) nil))
    nil)
   ((o_empty formula-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_concatenate nil))
   shostak))
(o_nonempty_left 0
  (o_nonempty_left-1 nil 3513603892
   ("" (expand* "o" "concatenate_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)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (O const-decl "csequence" csequence_concatenate nil))
   nil))
(o_nonempty_right 0
  (o_nonempty_right-1 nil 3513603892
   ("" (expand* "o" "concatenate_struct" "coreduce")
    (("" (reduce) 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_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (O const-decl "csequence" csequence_concatenate 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)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil))
   nil))
(o_empty_left 0
  (o_empty_left-1 nil 3513604432
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst - "LAMBDA cseq1, cseq2: cseq1 = eseq!1 o cseq2"
         "eseq!1 o cseq!1" "cseq!1")
        (("" (hide 2)
          (("" (expand* "bisimulation?" "o" "concatenate_struct")
            (("" (skosimp)
              (("" (expand "coreduce" -)
                (("" (reduce-with-ext) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_concatenate nil)
    (coinduction formula-decl nil 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)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (eseq!1 skolem-const-decl "empty_csequence[T]"
     csequence_concatenate nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(o_empty_right 0
  (o_empty_right-1 nil 3513604548
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst - "LAMBDA cseq1, cseq2: cseq1 = cseq2 o eseq!1"
         "cseq!1 o eseq!1" "cseq!1")
        (("" (hide 2)
          (("" (expand* "bisimulation?" "o" "concatenate_struct")
            (("" (skosimp)
              (("" (expand "coreduce" -)
                (("" (reduce-with-ext) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_concatenate nil)
    (coinduction formula-decl nil 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)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (eseq!1 skolem-const-decl "empty_csequence[T]"
     csequence_concatenate nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(o_first_TCC1 0
  (o_first_TCC1-1 nil 3513603892
   ("" (skosimp)
    (("" (rewrite "o_nonempty") (("" (assert) nil nil)) nil)) nil)
   ((o_nonempty formula-decl nil csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil))
   nil))
(o_first 0
  (o_first-1 nil 3513604630
   ("" (grind)
    (("" (hide -1)
      (("" (expand* "concatenate_struct" "coreduce")
        (("" (lift-if) (("" (assert) nil nil)) 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)
    (O const-decl "csequence" csequence_concatenate nil)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil))
   shostak))
(o_rest 0
  (o_rest-1 nil 3513604699
   ("" (skosimp)
    (("" (lift-if)
      (("" (ground)
        (("1" (rewrite "o_empty_left") nil nil)
         ("2" (expand* "o" "concatenate_struct")
          (("2" (expand "coreduce" 2 1) (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (O const-decl "csequence" csequence_concatenate 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)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil))
   shostak))
(o_first_rest 0
  (o_first_rest-1 nil 3513604732
   ("" (skosimp)
    (("" (expand* "o" "concatenate_struct")
      (("" (expand "coreduce" +) (("" (reduce-with-ext) nil nil)) nil))
      nil))
    nil)
   ((concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (csequence_struct type-decl nil csequence_codt_coreduce nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (inj_empty? adt-recognizer-decl "[csequence_struct -> boolean]"
     csequence_codt_coreduce nil)
    (inj_nonempty? adt-recognizer-decl "[csequence_struct -> boolean]"
     csequence_codt_coreduce nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (inj_empty_cseq adt-constructor-decl "(inj_empty?)"
     csequence_codt_coreduce nil)
    (inj_add adt-constructor-decl "[[T, domain] -> (inj_nonempty?)]"
     csequence_codt_coreduce nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans 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))
   shostak))
(o_length 0
  (o_length-1 nil 3513604770
   (""
    (measure-induct+ "length(fseq1) + length(fseq2)" ("fseq1" "fseq2")
     :skolem-typepreds? t)
    (("" (expand* "o" "concatenate_struct")
      (("" (expand "coreduce" +)
        (("" (smash)
          (("1" (rewrite "length_empty?_rew") nil nil)
           ("2" (expand "length" 2 1)
            (("2" (expand "is_finite" -2)
              (("2" (inst - "x!1" "rest(x!2)")
                (("2" (expand "length" -3 4)
                  (("2" (expand "length" 2 3) (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "is_finite" -1)
            (("3" (inst - "rest(x!1)" "x!2")
              (("3" (expand "length" -3 3)
                (("3" (expand "length" 2 2)
                  (("3" (expand "length" 2 1) (("3" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((concatenate_struct const-decl "csequence_struct"
     csequence_concatenate nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (x!2 skolem-const-decl "finite_csequence[T]" csequence_concatenate
     nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (x!1 skolem-const-decl "finite_csequence[T]" csequence_concatenate
     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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (o_finite application-judgement "finite_csequence"
     csequence_concatenate nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (< const-decl "bool" reals 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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (naturalnumber 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)
    (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_concatenate nil)
    (measure_induction formula-decl nil measure_induction nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
(o_index 0
  (o_index-1 nil 3513604892
   ("" (skolem!)
    (("" (use "index?_prop")
      (("" (use "o_finiteness")
        (("" (use "o_length")
          (("" (lemma "o_finite") (("" (reduce) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((index?_prop formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_concatenate 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)
    (O const-decl "csequence" csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (o_length formula-decl nil csequence_concatenate nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (o_finite application-judgement "finite_csequence"
     csequence_concatenate nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (o_finite judgement-tcc nil csequence_concatenate nil)
    (o_finiteness formula-decl nil csequence_concatenate nil))
   shostak))
(o_nth_TCC1 0
  (o_nth_TCC1-1 nil 3513603892
   ("" (skosimp :preds? t)
    (("" (assert)
      (("" (rewrite "o_index")
        (("" (use "index?_infinite")
          (("" (rewrite "index?_finite") (("" (assert) nil nil)) 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)
    (index?_infinite formula-decl nil csequence_nth nil)
    (cseq2!1 skolem-const-decl "csequence[T]" csequence_concatenate
     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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (o_index formula-decl nil csequence_concatenate 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_concatenate 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)
    (O const-decl "csequence" csequence_concatenate nil)
    (indexes type-eq-decl nil csequence_nth nil))
   nil))
(o_nth_TCC2 0
  (o_nth_TCC2-1 nil 3513603892
   ("" (skosimp :preds? t)
    (("" (rewrite "o_index")
      (("" (rewrite "index?_prop") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((o_index formula-decl nil csequence_concatenate nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_lt_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)
    (index?_prop formula-decl nil csequence_nth 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_concatenate 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)
    (O const-decl "csequence" csequence_concatenate nil)
    (indexes type-eq-decl nil csequence_nth nil))
   nil))
(o_nth 0
  (o_nth-1 nil 3513604987
   ("" (measure-induct+ "n" ("cseq1" "cseq2" "n") :skolem-typepreds? t)
    (("1" (expand "nth" +)
      (("1" (lift-if)
        (("1" (prop)
          (("1" (replace -1)
            (("1" (use "index?_0")
              (("1" (assert)
                (("1" (forward-chain "o_first")
                  (("1" (lift-if)
                    (("1" (rewrite "length_empty?_rew")
                      (("1" (ground) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (case "empty?(x!1)")
            (("1" (rewrite "o_empty_left")
              (("1" (rewrite "length_empty?_rew")
                (("1" (ground) nil nil)) nil))
              nil)
             ("2" (assert)
              (("2" (rewrite "o_rest")
                (("1" (inst - "rest(x!1)" "x!2" "x!3 - 1")
                  (("1" (assert)
                    (("1" (expand "nth" -2 2)
                      (("1" (expand "is_finite" +)
                        (("1" (expand "length" +)
                          (("1" (lift-if) (("1" (ground) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (rewrite "index?_0")
                  (("2" (use "index?_lt") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (forward-chain "o_nth_TCC2") nil nil)
     ("3" (forward-chain "o_nth_TCC1") nil nil)
     ("4" (forward-chain "o_nth_TCC2") nil nil)
     ("5" (forward-chain "o_nth_TCC1") nil nil)
     ("6" (forward-chain "o_nth_TCC2") nil nil)
     ("7" (forward-chain "o_nth_TCC1") nil nil)
     ("8" (forward-chain "o_nth_TCC2") nil nil)
     ("9" (forward-chain "o_nth_TCC1") nil nil))
    nil)
   ((o_nth_TCC1 subtype-tcc nil csequence_concatenate nil)
    (o_nth_TCC2 subtype-tcc nil csequence_concatenate nil)
    (index?_0 formula-decl nil csequence_nth nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (index?_lt formula-decl nil csequence_nth nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (nth def-decl "T" csequence_nth nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (O const-decl "csequence" csequence_concatenate 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_concatenate 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))
(o_add 0
  (o_add-1 nil 3513605162
   ("" (skolem!)
    (("" (decompose-equality)
      (("1" (rewrite "o_first") nil nil)
       ("2" (rewrite "o_rest") nil nil))
      nil))
    nil)
   ((o_nonempty_left application-judgement "nonempty_csequence"
     csequence_concatenate nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil))
   shostak))
(o_last_TCC1 0
  (o_last_TCC1-1 nil 3513603892
   ("" (skosimp)
    (("" (forward-chain "o_finiteness")
      (("" (assert)
        (("" (expand* "o" "concatenate_struct" "coreduce") nil nil))
        nil))
      nil))
    nil)
   ((o_finiteness formula-decl nil csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate 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))
   nil))
(o_last_TCC2 0
  (o_last_TCC2-1 nil 3513603892
   ("" (skosimp)
    (("" (forward-chain "o_finiteness") (("" (assert) nil nil)) nil))
    nil)
   ((o_finiteness formula-decl nil csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil))
   nil))
(o_last 0
  (o_last-1 nil 3513605242
   ("" (skosimp)
    (("" (rewrite "length_nonempty?_rew")
      (("" (assert)
        (("" (forward-chain "o_finiteness")
          (("" (expand "last")
            (("" (rewrite "o_length")
              (("" (rewrite "o_nth")
                (("" (rewrite "length_empty?_rew")
                  (("" (reduce) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((length_nonempty?_rew formula-decl nil csequence_length nil)
    (csequence type-decl nil csequence_codt nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (o_finiteness formula-decl nil csequence_concatenate nil)
    (o_length formula-decl nil csequence_concatenate 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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (o_nth formula-decl nil csequence_concatenate nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (last const-decl "T" csequence_nth nil))
   shostak))
(o_infinite 0
  (o_infinite-1 nil 3513605309
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst -
         "LAMBDA cseq1, cseq2: is_infinite(cseq2) AND (EXISTS cseq: cseq1 = cseq2 o cseq)"
         "iseq!1 o cseq!1" "iseq!1")
        (("1" (assert) (("1" (inst + "cseq!1") nil nil)) nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp*)
              (("2" (replace -1)
                (("2" (hide -1)
                  (("2" (expand "is_finite" 1)
                    (("2" (use "o_nonempty_left")
                      (("2" (smash)
                        (("1" (inst + "cseq!2")
                          (("1" (rewrite "o_rest") nil nil)) nil)
                         ("2" (rewrite "o_first") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_concatenate nil)
    (coinduction formula-decl nil csequence_codt nil)
    (o_nonempty_left judgement-tcc nil csequence_concatenate nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (o_infinite1 application-judgement "infinite_csequence"
     csequence_concatenate nil)
    (o_nonempty_left application-judgement "nonempty_csequence"
     csequence_concatenate nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (O const-decl "csequence" csequence_concatenate nil))
   shostak))
(o_assoc 0
  (o_assoc-1 nil 3513605418
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst -
         "LAMBDA cseq1, cseq2: EXISTS (s1, s2, s3: csequence): cseq1 = s1 o (s2 o s3) AND cseq2 = (s1 o s2) o s3"
         "cseq!1 o (cseq1!1 o cseq2!1)" "(cseq!1 o cseq1!1) o cseq2!1")
        (("1" (assert)
          (("1" (inst + "cseq!1" "cseq1!1" "cseq2!1") nil nil)) nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp*)
              (("2" (smash)
                (("1" (lemma "o_empty")
                  (("1" (inst-cp - "s1!1" "s2!1 o s3!1")
                    (("1" (inst - "s2!1" "s3!1")
                      (("1" (ground) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (lemma "o_empty")
                  (("2" (inst-cp - "s1!1 o s2!1" "s3!1")
                    (("2" (inst - "s1!1" "s2!1")
                      (("2" (ground) nil nil)) nil))
                    nil))
                  nil)
                 ("3" (replace*)
                  (("3" (hide -1 -2)
                    (("3" (lemma "o_empty")
                      (("3" (inst-cp - "s1!1 o s2!1" "s3!1")
                        (("3" (inst-cp - "s1!1" "s2!1 o s3!1")
                          (("3" (inst-cp - "s1!1" "s2!1")
                            (("3" (inst - "s2!1" "s3!1")
                              (("3"
                                (auto-rewrite "o_rest")
                                (("3"
                                  (auto-rewrite "o_empty_left")
                                  (("3"
                                    (smash)
                                    (("1"
                                      (inst
                                       +
                                       "rest(s1!1)"
                                       "s2!1"
                                       "s3!1")
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (inst
                                       +
                                       "s1!1"
                                       "s2!1"
                                       "rest(s3!1)")
                                      (("2" (assert) nil nil))
                                      nil)
                                     ("3"
                                      (inst
                                       +
                                       "rest(s1!1)"
                                       "s2!1"
                                       "s3!1")
                                      nil
                                      nil)
                                     ("4"
                                      (inst
                                       +
                                       "IF empty?(s1!1) THEN s1!1 ELSE rest(s1!1) ENDIF"
                                       "IF empty?(s1!1) THEN rest(s2!1) ELSE s2!1 ENDIF"
                                       "s3!1")
                                      (("1" (reduce) nil nil)
                                       ("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("4" (replace*)
                  (("4" (hide-all-but 1)
                    (("4" (expand* "o" "concatenate_struct" "coreduce")
                      (("4" (reduce) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_concatenate nil)
    (coinduction formula-decl nil csequence_codt nil)
    (concatenate_struct const-decl "csequence_struct"
     csequence_concatenate 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (s1!1 skolem-const-decl "csequence[T]" csequence_concatenate nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (o_empty formula-decl nil csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (O const-decl "csequence" csequence_concatenate nil))
   shostak))
(o_extensionality_left 0
  (o_extensionality_left-1 nil 3513605812
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (case "empty?(cseq!1)")
        (("1" (rewrite "o_empty_left")
          (("1" (rewrite "o_empty_left") nil nil)) nil)
         ("2" (ground)
          (("2" (inst - "cseq1!1" "cseq2!1")
            (("2" (assert)
              (("2" (lemma "o_rest")
                (("2" (inst-cp - "cseq!1" "cseq2!1")
                  (("2" (inst - "cseq!1" "cseq1!1")
                    (("2" (use "o_nonempty") (("2" (ground) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((o_nonempty formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(o_extensionality_right 0
  (o_extensionality_right-1 nil 3513605951
   ("" (skosimp)
    (("" (case "is_finite(cseq1!1) AND is_finite(cseq2!1)")
      (("1" (ground)
        (("1" (lemma "is_finite_induction")
          (("1"
            (inst -
             "LAMBDA cseq1: FORALL fseq, cseq2: is_infinite(cseq2) OR cseq1 o fseq /= cseq2 o fseq OR cseq1 = cseq2")
            (("1" (split)
              (("1" (inst - "cseq1!1")
                (("1" (assert)
                  (("1" (inst - "fseq!1" "cseq2!1")
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil)
               ("2" (delete -1 -2 -3 2)
                (("2" (skosimp*)
                  (("2" (case "empty?(cseq!1) OR empty?(cseq2!2)")
                    (("1" (ground)
                      (("1" (rewrite "o_empty_left")
                        (("1" (use "o_length")
                          (("1"
                            (lemma "length_empty?_rew"
                             ("cseq" "cseq2!2"))
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (rewrite "o_empty_left")
                        (("2" (use "o_length")
                          (("2"
                            (lemma "length_empty?_rew"
                             ("cseq" "cseq2!2"))
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("3"
                        (rewrite "o_empty_left" :subst
                         ("eseq" "cseq2!2"))
                        (("3" (use "o_length")
                          (("1"
                            (lemma "length_empty?_rew"
                             ("cseq" "cseq!1"))
                            (("1" (expand "is_finite" -1)
                              (("1" (assert) nil nil)) nil))
                            nil)
                           ("2" (expand "is_finite" +)
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (ground)
                      (("2" (inst - "fseq!2" "rest(cseq2!2)")
                        (("2" (expand "is_finite" -3)
                          (("2" (ground)
                            (("1" (lemma "o_rest")
                              (("1"
                                (inst-cp - "cseq2!2" "fseq!2")
                                (("1"
                                  (inst - "cseq!1" "fseq!2")
                                  (("1"
                                    (rewrite "o_nonempty")
                                    (("1"
                                      (rewrite "o_nonempty")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2"
                              (lemma "csequence_add_extensionality")
                              (("2"
                                (inst - "cseq!1" "cseq2!2")
                                (("2"
                                  (assert)
                                  (("2"
                                    (lemma "o_first")
                                    (("2"
                                      (inst-cp - "cseq2!2" "fseq!2")
                                      (("2"
                                        (inst - "cseq!1" "fseq!2")
                                        (("2"
                                          (rewrite "o_nonempty")
                                          (("2"
                                            (rewrite "o_nonempty")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (split)
        (("1" (rewrite "o_infinite")
          (("1" (rewrite "o_infinite")
            (("1" (use "o_finite") (("1" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (rewrite "o_infinite" :subst ("iseq" "cseq2!1"))
          (("2" (rewrite "o_infinite")
            (("2" (use "o_finite") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite inductive-decl "bool" csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_concatenate nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (o_nonempty formula-decl nil csequence_concatenate nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (o_length formula-decl nil csequence_concatenate nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_concatenate nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (/= const-decl "boolean" notequal nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (o_infinite formula-decl nil csequence_concatenate nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (o_finite judgement-tcc nil csequence_concatenate nil))
   shostak))
(o_some 0
  (o_some-1 nil 3513606243
   ("" (skolem!)
    (("" (auto-rewrite "o_empty")
      (("" (ground)
        (("1" (rewrite "o_infinite") nil nil)
         ("2" (lemma "some_induction")
          (("2"
            (inst - "p!1"
             "LAMBDA cseq: FORALL cseq1, cseq2: cseq = cseq1 o cseq2 IMPLIES some(p!1)(cseq1) OR some(p!1)(cseq2)")
            (("2" (split)
              (("1" (inst - "cseq1!1 o cseq2!1")
                (("1" (assert)
                  (("1" (inst - "cseq1!1" "cseq2!1")
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil)
               ("2" (delete -1 2 3)
                (("2" (skosimp*)
                  (("2" (lift-if)
                    (("2" (replace -2)
                      (("2" (hide -2)
                        (("2" (prop)
                          (("1" (rewrite "o_first")
                            (("1" (expand "some")
                              (("1"
                                (lift-if)
                                (("1" (ground) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (use "o_rest")
                            (("2" (expand "some" 2)
                              (("2"
                                (lift-if)
                                (("2"
                                  (ground)
                                  (("1"
                                    (rewrite "o_empty_left")
                                    (("1"
                                      (expand "some" +)
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (inst - "rest(cseq1!2)" "cseq2!2")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (lemma "some_weak_induction")
          (("3" (inst - "p!1" "LAMBDA cseq: some(p!1)(cseq o cseq2!1)")
            (("3" (split)
              (("1" (inst - "cseq1!1") (("1" (assert) nil nil)) nil)
               ("2" (delete -1 2)
                (("2" (skosimp)
                  (("2" (expand "some" +)
                    (("2" (reduce)
                      (("1" (rewrite "o_first" 2)
                        (("1" (use "o_empty") (("1" (assert) nil nil))
                          nil))
                        nil)
                       ("2" (rewrite "o_rest")
                        (("2" (use "o_empty") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("4" (case "empty?(cseq1!1)")
          (("1" (rewrite "o_empty_left") nil nil)
           ("2" (generalize-skolem-constants)
            (("2" (induct "cseq1_1" :name "is_finite_induction")
              (("1" (assert) nil nil)
               ("2" (skosimp*)
                (("2" (prop)
                  (("2" (expand "some" +)
                    (("2" (reduce)
                      (("1" (rewrite "o_rest" 3)
                        (("1" (rewrite "o_empty_left" 3) nil nil)
                         ("2" (use "o_empty") (("2" (assert) nil nil))
                          nil))
                        nil)
                       ("2" (rewrite "o_rest")
                        (("2" (use "o_empty") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite_induction formula-decl nil csequence_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (some_weak_induction formula-decl nil csequence_codt nil)
    (some_induction formula-decl nil csequence_codt nil)
    (o_empty formula-decl nil csequence_concatenate nil)
    (o_first formula-decl nil csequence_concatenate nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (o_rest formula-decl nil csequence_concatenate nil)
    (some inductive-decl "boolean" csequence_codt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (PRED type-eq-decl nil defined_types nil)
    (o_infinite formula-decl nil csequence_concatenate nil)
    (T formal-type-decl nil csequence_concatenate 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))
   shostak))
(o_every 0
  (o_every-1 nil 3513606532
   ("" (skolem!)
    (("" (lemma "every_some_rew")
      (("" (inst-cp - "p!1" "cseq2!1")
        (("" (inst-cp - "p!1" "cseq1!1")
          (("" (inst - "p!1" "cseq1!1 o cseq2!1")
            (("" (use "o_some") (("" (ground) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_concatenate nil)
    (every_some_rew formula-decl nil csequence_props nil)
    (o_some formula-decl nil csequence_concatenate nil)
    (pred_NOT const-decl "bool" csequence_props nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (csequence type-decl nil csequence_codt nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.72 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.