(my_list_induction (less_wf 0 (less_wf-1 nil 3667405436 ("" (expand "well_founded?") (("" (skolem 1 P) (("" (flatten) (("" (skolem -1 Y) (("" (expand "less") (("" (lemma naturalnumbers.wf_nat) (("" (expand "well_founded?") (("" (inst -1 "(LAMBDA(n:nat):EXISTS(l:(P)):length(l)=n)") (("" (split) (("1" (skosimp*) (("1" (typepred y!1) (("1" (skolem -1 L) (("1" (inst 1 L) (("1" (skolem 1 G) (("1" (inst -2 "length(G)") (("1" (assert) nil nil) ("2" (typepred G) (("2" (inst 1 G) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (inst 1 "length(Y)") (("2" (inst 1 Y) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((well_founded? const-decl "bool" orders nil) (less const-decl "bool" my_list_induction nil) (NOT const-decl "[bool -> bool]" booleans nil) (P skolem-const-decl "pred[list[X]]" my_list_induction nil) (G skolem-const-decl "(P)" my_list_induction nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt nil) (X formal-type-decl nil my_list_induction 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) (wf_nat formula-decl nil naturalnumbers nil)) shostak)) (list_length_induction 0 (list_length_induction-1 nil 3667403384 ("" (lemma "wf_induction[list[X],less].wf_induction") (("1" (propax) nil nil) ("2" (rewrite less_wf) nil nil)) nil) ((less_wf formula-decl nil my_list_induction nil) (pred type-eq-decl nil defined_types nil) (well_founded? const-decl "bool" orders nil) (wf_induction formula-decl nil wf_induction nil) (X formal-type-decl nil my_list_induction nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (less const-decl "bool" my_list_induction nil)) shostak))) (my_list_props (occ_TCC1 0 (occ_TCC1-1 nil 3667035231 ("" (termination-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) nil)) (occ_TCC2 0 (occ_TCC2-1 nil 3667035231 ("" (termination-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) nil)) (occ_nth 0 (occ_nth-1 nil 3667035247 ("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (HD TL)) (("2" (flatten) (("2" (expand nth 1) (("2" (skeep) (("2" (expand occ -2) (("2" (lift-if) (("2" (split -2) (("1" (flatten) (("1" (inst 1 0) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -2 x) (("2" (assert) (("2" (skolem -2 I) (("2" (flatten) (("2" (inst 2 "I+1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (list_induction formula-decl nil list_adt nil) (X formal-type-decl nil my_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (occ def-decl "nat" my_list_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) (> 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (nth_occ 0 (nth_occ-1 nil 3667036386 ("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (HD TL)) (("2" (flatten) (("2" (skeep) (("2" (expand nth 1) (("2" (lift-if 1) (("2" (expand occ 1) (("2" (split 1) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten) (("1" (inst -2 "i-1") (("1" (split -2) (("1" (assert) nil nil) ("2" (expand length -2) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst -1 "i-1") (("1" (split) (("1" (propax) nil nil) ("2" (expand length -1) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (list_induction formula-decl nil list_adt nil) (X formal-type-decl nil my_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (occ def-decl "nat" my_list_props nil) (> const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (perm_null 0 (perm_null-1 nil 3667035958 ("" (skeep) (("" (lemma "list_cons_eta[X]") (("" (inst -1 l) (("1" (replace -1 -2 rl) (("1" (expand "perm?") (("1" (inst -2 "car(l)") (("1" (expand "occ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((X formal-type-decl nil my_list_props nil) (list_cons_eta formula-decl nil list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (occ def-decl "nat" my_list_props nil) (perm? const-decl "bool" my_list_props nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)) shostak)) (perm_commutative 0 (perm_commutative-1 nil 3667035748 ("" (skeep) (("" (expand "perm?") (("" (skeep) (("" (inst -1 x) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((perm? const-decl "bool" my_list_props nil) (X formal-type-decl nil my_list_props nil)) shostak)) (append_occ 0 (append_occ-1 nil 3667035804 ("" (induct l1) (("1" (grind) nil nil) ("2" (skolem 1 (HD TL)) (("2" (flatten) (("2" (skeep) (("2" (skeep) (("2" (expand append 1) (("2" (expand occ 1 (1 2)) (("2" (lift-if) (("2" (inst -1 l2) (("2" (inst -1 x) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (list_induction formula-decl nil list_adt nil) (X formal-type-decl nil my_list_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (append def-decl "list[T]" list_props nil) (occ def-decl "nat" my_list_props 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) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (length_append 0 (length_append-1 nil 3667457451 ("" (induct-and-simplify l1) nil nil) ((list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (length def-decl "nat" list_props nil) (append def-decl "list[T]" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (X formal-type-decl nil my_list_props nil) (list_induction formula-decl nil list_adt nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (nth_append_TCC1 0 (nth_append_TCC1-1 nil 3667447307 ("" (skeep) (("" (lemma length_append) (("" (inst? -1) (("" (assert) nil nil)) nil)) nil)) nil) ((length_append formula-decl nil my_list_props 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) (list type-decl nil list_adt nil) (X formal-type-decl nil my_list_props nil)) nil)) (nth_append_TCC2 0 (nth_append_TCC2-1 nil 3667447307 ("" (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) (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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (nth_append 0 (nth_append-1 nil 3667447318 ("" (induct l1) (("1" (grind) nil nil) ("2" (skolem 1 (H T)) (("2" (flatten) (("2" (skeep) (("2" (skeep) (("2" (inst -1 l2) (("2" (expand append 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten 1) (("1" (expand nth 1) (("1" (lift-if) (("1" (split) (("1" (propax) nil nil) ("2" (flatten) (("2" (inst -2 "i-1") (("1" (expand length -3 1) (("1" (split -2) (("1" (lift-if -1) (("1" (split -1) (("1" (flatten -1) nil nil) ("2" (flatten -1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert 1) (("2" (grind 1) nil nil)) nil)) nil)) nil) ("2" (expand length -1) (("2" (expand length -2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert 1) (("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep 1) (("3" (grind 1) nil nil)) nil) ("4" (skeep 1) (("4" (lemma length_append) (("4" (inst? -1) (("4" (replace -1 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (append def-decl "list[T]" list_props nil) (length def-decl "nat" list_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (list type-decl nil list_adt nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (X formal-type-decl nil my_list_props nil) (list_induction formula-decl nil list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (i skolem-const-decl "nat" my_list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length_append formula-decl nil my_list_props nil)) shostak))) (SPLIT (split_TCC1 0 (split_TCC1-1 nil 3667407453 ("" (termination-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (>= const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil)) nil)) (split_length 0 (split_length-1 nil 3667407485 ("" (induct-and-simplify l) nil nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (split def-decl "[list[nat], list[nat]]" SPLIT 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) (list_induction formula-decl nil list_adt 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (split_occ 0 (split_occ-1 nil 3667407525 ("" (induct-and-simplify l) nil nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (occ def-decl "nat" my_list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (split def-decl "[list[nat], list[nat]]" SPLIT 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) (list_induction formula-decl nil list_adt 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (split_lwb_upb 0 (split_lwb_upb-1 nil 3667407762 ("" (assert) (("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (H T)) (("2" (flatten) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (upb const-decl "bool" SPLIT nil) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (lwb const-decl "bool" SPLIT 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) (list_induction formula-decl nil list_adt nil) (length def-decl "nat" list_props nil) (nth def-decl "T" list_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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)) shostak))) (QS (qs_TCC1 0 (qs_TCC1-1 nil 3329457968 ("" (skosimp*) (("" (lemma split_length) (("" (inst? -1) (("" (assert) (("" (replace -2) (("" (expand length 1 2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((split_length formula-decl nil SPLIT 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) (length def-decl "nat" list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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)) (qs_TCC2 0 (qs_TCC2-1 nil 3329457968 ("" (skosimp*) (("" (replace -1) (("" (expand length 1 2) (("" (lemma split_length) (("" (inst? -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((split_length formula-decl nil SPLIT 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (length def-decl "nat" list_props nil)) nil))) (SORTED (sorted?_TCC1 0 (sorted?_TCC1-1 nil 3667449016 ("" (termination-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (sorted_append 0 (sorted_append-1 nil 3667449025 ("" (skeep) (("" (expand sorted? 1) (("" (skeep) (("" (lemma nth_append) (("" (inst -1 l1 l2 i) (("" (lemma nth_append) (("" (inst -1 l1 l2 j) (("" (split -2) (("1" (lift-if -1) (("1" (split -1) (("1" (flatten -1) (("1" (replace -2 1) (("1" (split -3) (("1" (lift-if -1) (("1" (split -1) (("1" (flatten -1) (("1" (replace -2 1) (("1" (expand sorted? -5) (("1" (inst -5 i j) (("1" (split -5) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten -1) (("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -10) (("2" (assert) (("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -9) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten -1) (("2" (replace -1 2) (("2" (split -2) (("1" (lift-if -1) (("1" (split -1) (("1" (flatten -1) (("1" (assert) nil nil)) nil) ("2" (flatten -1) (("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -9) (("2" (assert 1) (("2" (replace -2 3) (("2" (assert 3) (("2" (expand sorted? -5) (("2" (inst -5 (i-length (l1)) (j-length (l1))) (("1" (split -5) (("1" (propax) nil nil) ("2" (assert 1) (("2" (grind 1) nil nil)) nil) ("3" (grind 1) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -8) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -1) (("1" (lift-if -1) (("1" (split -1) (("1" (flatten -1) (("1" (assert 1) (("1" (grind 1) nil nil)) nil)) nil) ("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -8) (("2" (assert 1) (("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma length_append) (("2" (inst -1 l1 l2) (("2" (replace -1 -7) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (i skolem-const-decl "nat" SORTED nil) (l1 skolem-const-decl "list[nat]" SORTED nil) (length_append formula-decl nil my_list_props nil) (nth def-decl "T" list_props nil) (upb const-decl "bool" SPLIT nil) (lwb const-decl "bool" SPLIT nil) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nth_append formula-decl nil my_list_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sorted? const-decl "bool" SORTED nil)) shostak))) (QS_props (qs_perm 0 (qs_perm-1 nil 3658125991 ("" (lemma list_length_induction) (("" (inst? -1) (("" (copy -1) (("" (split -1) (("1" (propax) nil nil) ("2" (skeep 1) (("2" (expand qs 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten 1) (("1" (grind 1) nil nil)) nil) ("2" (flatten 1) (("2" (assert 2) (("2" (expand perm? 2) (("2" (skeep 2) (("2" (lemma append_occ) (("2" (inst -1 "qs(split(car(g),cdr(g))`1)" "cons(car(g),qs(split(car(g),cdr(g))`2))" x) (("2" (replace -1 2) (("2" (lemma split_occ) (("2" (inst -1 "car(g)" "cdr(g)") (("2" (assert -1) (("2" (inst -1 x) (("2" (lemma split_length) (("2" (inst -1 "car(g)" "cdr(g)") (("2" (assert -1) (("2" (expand occ 2 3) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten 1) nil nil) ("2" (flatten 1) (("2" (split 2) (("1" (flatten 1) (("1" (expand occ 1 2) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten 1) (("1" (assert 1) (("1" (copy -6) (("1" (inst -1 "split(car(g),cdr(g))`1") (("1" (split -1) (("1" (inst -7 "split(car(g),cdr(g))`2") (("1" (split -7) (("1" (expand perm? (-1 -2)) (("1" (inst -1 x) (("1" (inst -2 x) (("1" (replace -1 1) (("1" (replace -2 1) (("1" (assert 1) (("1" (replace -6 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand less 1) (("2" (grind 1) nil nil)) nil)) nil)) nil) ("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten 1) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten 1) (("2" (expand occ 2 2) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten 1) nil nil) ("2" (flatten 1) (("2" (copy -4) (("2" (inst -1 "split(car(g),cdr(g))`1") (("2" (inst -5 "split(car(g),cdr(g))`2") (("2" (split -1) (("1" (expand perm? -1) (("1" (inst -1 x) (("1" (replace -1 2) (("1" (split -5) (("1" (expand perm? -1) (("1" (inst -1 x) (("1" (replace -1 2) (("1" (replace -4 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind 1) nil nil)) nil)) nil)) nil)) nil) ("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (perm? const-decl "bool" my_list_props nil) (qs def-decl "list[nat]" QS nil) (occ def-decl "nat" my_list_props nil) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (split_occ formula-decl nil SPLIT nil) (split_length formula-decl nil SPLIT nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length def-decl "nat" list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (less const-decl "bool" my_list_induction nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (append_occ formula-decl nil my_list_props nil) (list_length_induction formula-decl nil my_list_induction 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)) shostak)) (occ_upb 0 (occ_upb-1 nil 3658132514 ("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (H T)) (("2" (flatten) (("2" (skeep) (("2" (skeep) (("2" (inst? -1) (("2" (split) (("1" (expand occ -3) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (expand upb -4) (("1" (inst -4 0) (("1" (expand length -4) (("1" (assert) (("1" (split) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -2 x) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand upb -1) (("2" (expand upb 1) (("2" (skeep) (("2" (inst -2 "i+1") (("2" (split) (("1" (expand nth -1) (("1" (propax) nil nil)) nil) ("2" (expand length 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (nth def-decl "T" list_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (length def-decl "nat" list_props nil) (list_induction formula-decl nil list_adt 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) (< const-decl "bool" reals nil) (occ def-decl "nat" my_list_props nil) (> const-decl "bool" reals nil) (upb const-decl "bool" SPLIT nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil)) shostak)) (occ_lwb 0 (occ_lwb-1 nil 3658137865 ("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (H T)) (("2" (flatten) (("2" (skolem 1 N) (("2" (flatten) (("2" (skolem 1 X) (("2" (flatten) (("2" (inst? -1) (("2" (split) (("1" (expand occ -3) (("1" (lift-if) (("1" (split) (("1" (expand "lwb") (("1" (inst -3 0) (("1" (expand length -3) (("1" (assert) (("1" (split) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -2 X) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand lwb -1) (("2" (expand lwb 1) (("2" (skolem 1 I) (("2" (flatten) (("2" (inst -3 "I+1") (("2" (expand length -3) (("2" (assert) (("2" (expand nth 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (nth def-decl "T" list_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length def-decl "nat" list_props nil) (list_induction formula-decl nil list_adt 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) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (occ def-decl "nat" my_list_props nil) (> const-decl "bool" reals nil) (lwb const-decl "bool" SPLIT nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil)) nil)) (upb_perm 0 (upb_perm-1 nil 3658132945 ("" (skosimp*) (("" (lemma occ_upb) (("" (inst? -1) (("" (assert) (("" (expand "upb") (("" (skosimp*) (("" (expand "perm?") (("" (lemma nth_occ) (("" (inst? -1) (("" (assert) (("" (inst? -3) (("" (lemma occ_nth) (("" (inst -1 l!1 "nth(lp!1, i!1)") (("" (assert) (("" (skosimp*) (("" (inst? -4) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((occ_upb formula-decl nil QS_props nil) (nth_occ formula-decl nil my_list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (occ_nth formula-decl nil my_list_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (perm? const-decl "bool" my_list_props nil) (upb const-decl "bool" SPLIT nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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)) (lwb_perm 0 (lwb_perm-1 nil 3658138209 ("" (skosimp*) (("" (lemma occ_lwb) (("" (inst? -1) (("" (assert) (("" (expand "lwb") (("" (skosimp*) (("" (expand "perm?") (("" (lemma nth_occ) (("" (inst? -1) (("" (assert) (("" (inst? -3) (("" (lemma occ_nth) (("" (inst -1 l!1 "nth(lp!1, i!1)") (("" (assert) (("" (skosimp*) (("" (inst? -4) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((occ_lwb formula-decl nil QS_props nil) (nth_occ formula-decl nil my_list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (occ_nth formula-decl nil my_list_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (perm? const-decl "bool" my_list_props nil) (lwb const-decl "bool" SPLIT nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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)) (qs_sorted 0 (qs_sorted-1 nil 3658128963 ("" (lemma list_length_induction) (("" (postpone) nil nil)) nil) ((list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (sorted? const-decl "bool" SORTED nil) (qs def-decl "list[nat]" QS nil) (split_lwb_upb formula-decl nil SPLIT nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (split_length formula-decl nil SPLIT nil) (sorted_append formula-decl nil SORTED nil) (lwb_perm formula-decl nil QS_props nil) (qs_perm formula-decl nil QS_props nil) (perm_commutative formula-decl nil my_list_props nil) (nth def-decl "T" list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (lwb const-decl "bool" SPLIT nil) (upb_perm formula-decl nil QS_props nil) (less const-decl "bool" my_list_induction nil) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length def-decl "nat" list_props nil) (list_length_induction formula-decl nil my_list_induction 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)) shostak)))