Quelle  csequence_remove.prf   Sprache: unbekannt

(csequence_remove
 (remove_TCC1 0
  (remove_TCC1-1 nil 3513478083 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (remove_TCC2 0
  (remove_TCC2-1 nil 3513478083 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (remove_TCC3 0
  (remove_TCC3-1 nil 3513478083 ("" (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))
 (remove_TCC4 0
  (remove_TCC4-1 nil 3513478083 ("" (termination-tcc) nil nil) nil
   nil))
 (remove_finite 0
  (remove_finite-1 nil 3513478083
   ("" (induct "index")
    (("1" (skolem-typepred)
      (("1" (expand "remove")
        (("1" (expand "is_finite" -) (("1" (ground) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp* t)
      (("2" (expand "is_finite" (-1 +))
        (("2" (expand "remove" +)
          (("2" (lift-if)
            (("2" (ground) (("2" (inst - "rest(fseq!1)") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (remove def-decl "csequence" csequence_remove 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_remove nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (remove_infinite 0
  (remove_infinite-1 nil 3513478083
   ("" (induct "index")
    (("1" (skolem-typepred)
      (("1" (expand "remove")
        (("1" (expand "is_finite" +) (("1" (ground) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp* t)
      (("2" (expand "is_finite" (-3 +))
        (("2" (expand "remove" -3)
          (("2" (lift-if)
            (("2" (ground) (("2" (inst - "rest(iseq!1)") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (remove def-decl "csequence" csequence_remove 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_remove nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (remove_0 0
  (remove_0-1 nil 3513478205
   ("" (expand "remove") (("" (propax) nil nil)) nil)
   ((remove def-decl "csequence" csequence_remove nil)) shostak))
 (remove_empty 0
  (remove_empty-1 nil 3513478213
   ("" (expand "remove") (("" (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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (remove def-decl "csequence" csequence_remove nil))
   shostak))
 (remove_nonempty 0
  (remove_nonempty-1 nil 3513478241
   ("" (expand "remove") (("" (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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (remove def-decl "csequence" csequence_remove nil))
   shostak))
 (remove_first_TCC1 0
  (remove_first_TCC1-1 nil 3513478083
   ("" (skosimp)
    (("" (rewrite "remove_nonempty") (("" (flatten) nil nil)) nil))
    nil)
   ((remove_nonempty formula-decl nil csequence_remove nil)
    (T formal-type-decl nil csequence_remove 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (remove_first_TCC2 0
  (remove_first_TCC2-1 nil 3513478083
   ("" (skosimp)
    (("" (rewrite "remove_nonempty") (("" (ground) nil nil)) nil)) nil)
   ((remove_nonempty formula-decl nil csequence_remove nil)
    (T formal-type-decl nil csequence_remove 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (remove_first_TCC3 0
  (remove_first_TCC3-1 nil 3513478083
   ("" (skosimp)
    (("" (rewrite "remove_nonempty") (("" (flatten) nil nil)) nil))
    nil)
   ((remove_nonempty formula-decl nil csequence_remove nil)
    (T formal-type-decl nil csequence_remove 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (remove_first 0
  (remove_first-1 nil 3513478308
   ("" (expand "remove") (("" (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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (remove def-decl "csequence" csequence_remove nil))
   shostak))
 (remove_rest_TCC1 0
  (remove_rest_TCC1-1 nil 3513478083
   ("" (skosimp)
    (("" (rewrite "remove_nonempty") (("" (assert) nil nil)) nil)) nil)
   ((remove_nonempty formula-decl nil csequence_remove nil)
    (T formal-type-decl nil csequence_remove nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (remove_rest_TCC2 0
  (remove_rest_TCC2-1 nil 3513478083 ("" (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)
    (T formal-type-decl nil csequence_remove 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)
    (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))
 (remove_rest 0
  (remove_rest-1 nil 3513478348
   ("" (induct "index")
    (("1" (skosimp)
      (("1" (expand "remove") (("1" (propax) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "remove" +)
        (("2" (lift-if)
          (("2" (ground)
            (("1" (expand "remove") (("1" (propax) nil nil)) nil)
             ("2" (expand "remove") (("2" (propax) nil nil)) nil)
             ("3" (decompose-equality 2)
              (("1" (expand "remove") (("1" (propax) nil nil)) nil)
               ("2" (inst - "rest(nseq!1)")
                (("2" (assert)
                  (("2" (expand* "remove" "remove") nil nil)) nil))
                nil)
               ("3" (expand "remove") (("3" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp) (("3" (assert) nil nil)) nil)
     ("4" (skosimp) (("4" (forward-chain "remove_rest_TCC1") nil nil))
      nil))
    nil)
   ((remove_rest_TCC1 subtype-tcc nil csequence_remove nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nseq!1 skolem-const-decl "nonempty_csequence[T]" csequence_remove
     nil)
    (j!1 skolem-const-decl "nat" csequence_remove nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (pred type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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_remove 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (remove def-decl "csequence" csequence_remove nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (remove_upfrom_length 0
  (remove_upfrom_length-1 nil 3513478456
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp* t)
      (("3" (expand "remove" +)
        (("3" (use "length_empty?_rew")
          (("3" (lift-if)
            (("3" (ground)
              (("3" (decompose-equality 2)
                (("3" (inst - "index!1 - 1")
                  (("3" (expand "length" -) (("3" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_remove nil)
    (index!1 skolem-const-decl "upfrom[length(cseq!1)]"
     csequence_remove nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_remove nil)
    (remove def-decl "csequence" csequence_remove nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (upfrom nonempty-type-eq-decl nil int_types 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)
    (finite_csequence nonempty-type-eq-decl nil csequence_props 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))
 (remove_length 0
  (remove_length-1 nil 3513478533
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "remove" +)
        (("3" (expand "length" 1 1)
          (("3" (expand "length" 1 2)
            (("3" (expand "length" 1 3)
              (("3" (expand "index?" +) (("3" (reduce) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (skosimp*)
      (("4" (use "remove_finite" ("fseq" "fseq!2")) nil nil)) nil))
    nil)
   ((remove_finite judgement-tcc nil csequence_remove nil)
    (remove_finite application-judgement "finite_csequence"
     csequence_remove nil)
    (index!1 skolem-const-decl "nat" csequence_remove nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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_remove nil)
    (index? def-decl "bool" csequence_nth nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (remove def-decl "csequence" csequence_remove nil))
   shostak))
 (remove_index 0
  (remove_index-1 nil 3513478587
   ("" (skolem!)
    (("" (case "is_finite(cseq!1)")
      (("1" (use "remove_finite")
        (("1" (use "remove_length")
          (("1" (lemma "index?_finite")
            (("1" (reduce :if-match all) nil nil)) nil))
          nil))
        nil)
       ("2" (use "remove_infinite")
        (("2" (lemma "index?_infinite")
          (("2" (reduce :if-match all) nil nil)) nil))
        nil))
      nil))
    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_remove nil)
    (remove_length formula-decl nil csequence_remove nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (remove def-decl "csequence" csequence_remove nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_remove nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (remove_finite judgement-tcc nil csequence_remove nil)
    (index?_infinite formula-decl nil csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (remove_infinite judgement-tcc nil csequence_remove nil))
   shostak))
 (remove_nth_TCC1 0
  (remove_nth_TCC1-1 nil 3513478083
   ("" (grind :rewrites ("index?_prop" "remove_index")) nil nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (index?_prop formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_remove nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (remove_index formula-decl nil csequence_remove nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (remove def-decl "csequence" csequence_remove nil)
    (index? def-decl "bool" csequence_nth nil)
    (csequence type-decl nil csequence_codt nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (remove_nth 0
  (remove_nth-1 nil 3513478688
   ("" (induct "n")
    (("1" (skolem-typepred)
      (("1" (expand "remove" +)
        (("1" (expand "nth" 1 2)
          (("1" (lift-if)
            (("1" (ground) (("1" (expand* "remove" "index?") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp* t)
      (("2" (expand "remove" +)
        (("2" (expand "nth" +)
          (("2" (smash)
            (("1" (expand* "remove" "index?") nil nil)
             ("2" (inst - "rest(cseq!1)" "m!1 - 1")
              (("2" (assert) nil nil)) nil)
             ("3" (inst - "rest(cseq!1)" "m!1 - 1")
              (("3" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skolem!) (("3" (use "remove_nth_TCC1") nil nil)) nil))
    nil)
   ((remove_nth_TCC1 subtype-tcc nil csequence_remove nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nth def-decl "T" csequence_nth nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil csequence_remove nil)
    (csequence type-decl nil csequence_codt nil)
    (index? def-decl "bool" csequence_nth nil)
    (remove def-decl "csequence" csequence_remove nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (< const-decl "bool" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   shostak))
 (remove_add 0
  (remove_add-1 nil 3513478786
   ("" (expand "remove" 1 2) (("" (propax) nil nil)) nil)
   ((remove def-decl "csequence" csequence_remove nil)) shostak))
 (remove_last_TCC1 0
  (remove_last_TCC1-1 nil 3513478083
   ("" (skosimp :preds? t)
    (("" (rewrite "remove_nonempty")
      (("" (ground)
        (("1" (rewrite "index?_finite") nil nil)
         ("2" (expand* "length" "is_finite")
          (("2" (use "length_nonempty?_rew") (("2" (assert) nil nil))
            nil))
          nil)
         ("3" (rewrite "index?_finite")
          (("3" (expand* "length" "is_finite")
            (("3" (use "length_nonempty?_rew") (("3" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((remove_nonempty formula-decl nil csequence_remove nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (length_nonempty?_rew formula-decl nil csequence_length nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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_remove 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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (remove_last_TCC2 0
  (remove_last_TCC2-1 nil 3513478083
   ("" (skosimp) (("" (expand "remove") (("" (assert) nil nil)) nil))
    nil)
   ((remove def-decl "csequence" csequence_remove nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (remove_last 0
  (remove_last-1 nil 3513478899
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (case "empty?(cseq!1)")
        (("1" (rewrite "remove_nonempty") (("1" (ground) nil nil)) nil)
         ("2" (ground)
          (("2" (rewrite "remove_nonempty")
            (("2" (expand "last")
              (("2" (expand "remove" +)
                (("2" (expand "length" +)
                  (("2" (expand "nth" +)
                    (("2" (smash)
                      (("1" (rewrite "remove_length")
                        (("1" (lift-if) (("1" (assert) nil nil)) nil))
                        nil)
                       ("2" (rewrite "remove_length")
                        (("2" (lift-if)
                          (("2" (ground)
                            (("2" (rewrite "index?_finite") nil nil))
                            nil))
                          nil))
                        nil)
                       ("3" (rewrite "remove_length")
                        (("3" (lift-if)
                          (("3" (ground)
                            (("3" (rewrite "index?_finite") nil nil))
                            nil))
                          nil))
                        nil)
                       ("4" (inst - "index!1 - 1")
                        (("4" (assert)
                          (("4" (rewrite "remove_nonempty")
                            (("4" (expand "length" -)
                              (("4" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("5" (inst - "index!1 - 1")
                        (("5" (assert)
                          (("5" (rewrite "remove_nonempty")
                            (("5" (ground)
                              (("5"
                                (expand "length" 4)
                                (("5" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("6"
                        (lemma "length_empty?_rew"
                         ("cseq" "rest(cseq!1)"))
                        (("6" (assert)
                          (("6" (expand "remove" 2)
                            (("6" (propax) nil nil)) nil))
                          nil))
                        nil)
                       ("7" (expand "length" -7)
                        (("7" (assert) nil nil)) nil)
                       ("8" (expand "length" 3)
                        (("8" (expand "nth" +) (("8" (propax) nil nil))
                          nil))
                        nil)
                       ("9" (rewrite "length_nonempty?_rew") nil nil)
                       ("10" (expand "length" 4 2)
                        (("10" (expand "nth" 4 2)
                          (("10" (propax) nil nil)) nil))
                        nil)
                       ("11" (rewrite "remove_length")
                        (("11" (lift-if) (("11" (assert) nil nil))
                          nil))
                        nil)
                       ("12" (rewrite "remove_length")
                        (("12" (lift-if)
                          (("12" (ground)
                            (("12" (rewrite "index?_finite") nil nil))
                            nil))
                          nil))
                        nil)
                       ("13" (expand "remove" 3)
                        (("13" (expand "length" -5)
                          (("13" (assert) nil nil)) nil))
                        nil)
                       ("14" (inst - "index!1 - 1")
                        (("14" (assert)
                          (("14" (rewrite "remove_nonempty") nil nil))
                          nil))
                        nil)
                       ("15" (inst - "index!1 - 1")
                        (("15" (assert)
                          (("15" (rewrite "remove_nonempty")
                            (("15" (flatten)
                              (("15"
                                (expand "remove" 5)
                                (("15"
                                  (assert)
                                  (("15"
                                    (rewrite "length_nonempty?_rew")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("16" (rewrite "length_nonempty?_rew") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("4" (skosimp*) (("4" (forward-chain "remove_last_TCC2") nil nil))
      nil)
     ("5" (skosimp*) (("5" (forward-chain "remove_last_TCC1") nil nil))
      nil)
     ("6" (skosimp*)
      (("6" (use "remove_finite" ("fseq" "fseq!2")) nil nil)) nil))
    nil)
   ((remove_finite judgement-tcc nil csequence_remove nil)
    (remove_last_TCC1 subtype-tcc nil csequence_remove nil)
    (remove_last_TCC2 subtype-tcc nil csequence_remove nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (remove_length formula-decl nil csequence_remove nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (real_ge_is_total_order name-judgement "(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)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (length_nonempty?_rew formula-decl nil csequence_length nil)
    (remove_nonempty formula-decl nil csequence_remove nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_remove nil)
    (nth def-decl "T" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (last const-decl "T" csequence_nth nil)
    (nonempty_finite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (index? def-decl "bool" csequence_nth nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (remove def-decl "csequence" csequence_remove nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (remove_remove_TCC1 0
  (remove_remove_TCC1-1 nil 3513478083 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (remove_remove 0
  (remove_remove-1 nil 3513479269
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (lift-if)
        (("1" (assert)
          (("1" (expand "remove" 1 2)
            (("1" (expand "remove" 1 2)
              (("1" (lift-if)
                (("1" (ground)
                  (("1" (expand "remove") (("1" (propax) nil nil)) nil)
                   ("2" (lift-if)
                    (("2" (ground)
                      (("1" (expand "remove") (("1" (propax) nil nil))
                        nil)
                       ("2" (rewrite "remove_rest") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "remove" 1 2)
        (("2" (expand "remove" 1 4)
          (("2" (lift-if)
            (("2" (lift-if)
              (("2" (lift-if)
                (("2" (ground)
                  (("1" (expand "remove") (("1" (propax) nil nil)) nil)
                   ("2" (expand "remove" +) (("2" (propax) nil nil))
                    nil)
                   ("3" (expand "remove" 1 1)
                    (("3" (expand "remove" 1 3)
                      (("3" (decompose-equality)
                        (("3" (inst - "rest(cseq!1)" "m!1 - 1")
                          (("3" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("4" (expand "remove" 2 1)
                    (("4" (lift-if)
                      (("4" (ground)
                        (("1" (expand "remove" 1 3)
                          (("1" (propax) nil nil)) nil)
                         ("2" (expand "remove" 2 3)
                          (("2" (lift-if)
                            (("2" (ground)
                              (("1" (rewrite "remove_empty") nil nil)
                               ("2"
                                (decompose-equality)
                                (("1" (rewrite "remove_first") nil nil)
                                 ("2"
                                  (rewrite "remove_rest")
                                  (("2"
                                    (inst - "rest(cseq!1)" "m!1 - 1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp) (("3" (assert) nil nil)) nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (remove_empty formula-decl nil csequence_remove nil)
    (remove_first formula-decl nil csequence_remove nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (remove_rest formula-decl nil csequence_remove nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (remove def-decl "csequence" csequence_remove nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_remove 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (remove_extensionality 0
  (remove_extensionality-1 nil 3513479628
   ("" (induct "n")
    (("1" (skosimp)
      (("1" (expand* "remove" "index?" "nth")
        (("1" (reduce) (("1" (decompose-equality +) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "remove" -2)
        (("2" (expand "index?" -3)
          (("2" (expand "nth" -3)
            (("2" (smash)
              (("1" (decompose-equality -2)
                (("1" (inst - "rest(cseq1!1)" "rest(cseq2!1)")
                  (("1" (assert) (("1" (decompose-equality +) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (decompose-equality)
                (("2" (inst - "rest(cseq1!1)" "rest(cseq2!1)")
                  (("2" (assert)
                    (("2"
                      (forward-chain "csequence_add_extensionality")
                      nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nth def-decl "T" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (index? def-decl "bool" csequence_nth nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (remove def-decl "csequence" csequence_remove nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_remove 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))
 (remove_some 0
  (remove_some-1 nil 3513479748
   ("" (skolem!)
    (("" (use "nth_some")
      (("" (prop)
        (("1" (skolem-typepred)
          (("1" (rewrite "remove_index")
            (("1" (flatten)
              (("1" (rewrite "remove_nth")
                (("1" (lift-if -4)
                  (("1" (split -)
                    (("1" (flatten)
                      (("1" (inst + "i!1") (("1" (assert) nil nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (inst + "i!1 + 1") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp :preds? t)
          (("2" (case "n!1 < index!1")
            (("1" (inst + "n!1")
              (("1" (rewrite "remove_nth") (("1" (assert) nil nil))
                nil)
               ("2" (rewrite "remove_index")
                (("2" (flatten)
                  (("2" (rewrite "index?_finite")
                    (("2" (rewrite "index?_finite")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst + "n!1 - 1")
              (("1" (rewrite "remove_nth") (("1" (assert) nil nil))
                nil)
               ("2" (assert)
                (("2" (rewrite "remove_index")
                  (("2" (prop)
                    (("1" (use "index?_lt" ("n" "n!1 - 1"))
                      (("1" (assert) nil nil)) nil)
                     ("2" (rewrite "index?_finite")
                      (("2" (rewrite "index?_finite")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nth_some formula-decl nil csequence_nth nil)
    (T formal-type-decl nil csequence_remove nil)
    (pred type-eq-decl nil defined_types nil)
    (remove def-decl "csequence" csequence_remove 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (index?_lt formula-decl nil csequence_nth nil)
    (n!1 skolem-const-decl "indexes[T](cseq!1)" csequence_remove nil)
    (index?_finite formula-decl nil csequence_nth nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (< const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (i!1 skolem-const-decl "indexes[T](remove(cseq!1, index!1))"
     csequence_remove nil)
    (index!1 skolem-const-decl "nat" csequence_remove nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_remove 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)
    (remove_nth formula-decl nil csequence_remove nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (remove_index formula-decl nil csequence_remove nil))
   shostak))
 (remove_every 0
  (remove_every-1 nil 3513479895
   ("" (skolem!)
    (("" (use "every_some_rew")
      (("" (use "remove_some")
        (("" (expand "pred_NOT")
          (("" (ground)
            (("1" (skosimp)
              (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
             ("2" (skosimp)
              (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((every_some_rew formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_remove nil)
    (remove def-decl "csequence" csequence_remove 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)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (index? def-decl "bool" csequence_nth nil)
    (indexes type-eq-decl nil csequence_nth nil)
    (pred_NOT const-decl "bool" csequence_props nil)
    (remove_some formula-decl nil csequence_remove nil))
   shostak)))