(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 const-decl "bool" my_list_induction nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (X formal-type-decl nil my_list_induction nil) (wf_induction formula-decl nil wf_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (less_wf formula-decl nil my_list_induction nil)) shostak))) (my_list_props (occ_TCC1 0 (occ_TCC1-1 nil 3667035231 ("" (termination-tcc) nil nil) ((length def-decl "nat" list_props 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)) nil)) (occ_TCC2 0 (occ_TCC2-1 nil 3667035231 ("" (termination-tcc) nil nil) ((length def-decl "nat" list_props 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)) 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) ((list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (occ def-decl "nat" my_list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (X formal-type-decl nil my_list_props nil) (list_induction formula-decl nil list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) ((list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (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) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (> const-decl "bool" reals nil) (occ def-decl "nat" my_list_props nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props 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) (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) (i skolem-const-decl "nat" my_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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) ((l skolem-const-decl "list[X]" my_list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (perm? const-decl "bool" my_list_props nil) (occ def-decl "nat" my_list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (list_cons_eta formula-decl nil list_adt nil) (X formal-type-decl nil my_list_props nil)) shostak)) (perm_commutative 0 (perm_commutative-1 nil 3667035748 ("" (skeep) (("" (expand "perm?") (("" (skeep) (("" (inst -1 x) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((X formal-type-decl nil my_list_props nil) (perm? const-decl "bool" 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) ((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) (occ def-decl "nat" my_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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (length_append 0 (length_append-1 nil 3667457451 ("" (induct-and-simplify l1) nil nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" 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) (length def-decl "nat" 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)) (nth_append_TCC1 0 (nth_append_TCC1-1 nil 3667447307 ("" (skeep) (("" (lemma length_append) (("" (inst? -1) (("" (assert) nil nil)) nil)) nil)) nil) ((X formal-type-decl nil my_list_props nil) (list type-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) (length_append formula-decl nil my_list_props nil)) nil)) (nth_append_TCC2 0 (nth_append_TCC2-1 nil 3667447307 ("" (subtype-tcc) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers 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_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers 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)) (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) ((length def-decl "nat" list_props 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types 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)) (split_length 0 (split_length-1 nil 3667407485 ("" (induct-and-simplify l) nil nil) ((posint_plus_nnint_is_posint application-judgement "posint" 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil)) shostak)) (split_occ 0 (split_occ-1 nil 3667407525 ("" (induct-and-simplify l) nil 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) (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) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (occ def-decl "nat" my_list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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" (skeep 1) (("2" (split 1) (("1" (expand split 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten 1) (("1" (expand upb 1) (("1" (skeep 1) (("1" (expand nth 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten 1) nil nil) ("2" (flatten 1) (("2" (inst -3 "m") (("2" (flatten -3) (("2" (expand upb -3) (("2" (inst -3 "i-1") (("1" (split -3) (("1" (propax) nil nil) ("2" (assert) (("2" (grind 1) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -1 m) (("2" (flatten -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 m) (("2" (flatten -1) (("2" (expand split 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten 1) nil nil) ("2" (flatten 1) (("2" (expand lwb 2) (("2" (skeep 2) (("2" (expand nth -2) (("2" (lift-if -2) (("2" (split -2) (("1" (flatten -1) nil nil) ("2" (flatten -1) (("2" (expand lwb -4) (("2" (inst -4 "i-1") (("1" (split -4) (("1" (propax) nil nil) ("2" (grind 1) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((i skolem-const-decl "nat" SPLIT nil) (nth def-decl "T" list_props 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) (i skolem-const-decl "nat" SPLIT 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) (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) (lwb const-decl "bool" SPLIT nil) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (upb const-decl "bool" SPLIT nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) ((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) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_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) (split_length formula-decl nil SPLIT 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) ((length def-decl "nat" 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) (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) (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) (split_length formula-decl nil SPLIT nil)) nil))) (SORTED (sorted?_TCC1 0 (sorted?_TCC1-1 nil 3667449016 ("" (termination-tcc) nil 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types 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)) (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) (l1 skolem-const-decl "list[nat]" SORTED nil) (i skolem-const-decl "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) ((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_length_induction formula-decl nil my_list_induction nil) (append_occ formula-decl nil my_list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (less const-decl "bool" 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (split_length formula-decl nil SPLIT nil) (split_occ formula-decl nil SPLIT nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt 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 def-decl "[list[nat], list[nat]]" SPLIT nil) (occ def-decl "nat" my_list_props nil) (qs def-decl "list[nat]" QS nil) (perm? const-decl "bool" my_list_props nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) ((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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (upb const-decl "bool" SPLIT nil) (> const-decl "bool" reals nil) (occ def-decl "nat" my_list_props nil) (< const-decl "bool" reals 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) (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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth def-decl "T" list_props 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)) 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) ((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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (lwb const-decl "bool" SPLIT nil) (> const-decl "bool" reals nil) (occ def-decl "nat" my_list_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_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) (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)) 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) ((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) (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) (upb const-decl "bool" SPLIT nil) (perm? const-decl "bool" my_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (occ_nth formula-decl nil my_list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth_occ formula-decl nil my_list_props nil) (occ_upb formula-decl nil QS_props 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) ((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) (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) (lwb const-decl "bool" SPLIT nil) (perm? const-decl "bool" my_list_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (occ_nth formula-decl nil my_list_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth_occ formula-decl nil my_list_props nil) (occ_lwb formula-decl nil QS_props nil)) nil)) (qs_sorted 0 (qs_sorted-1 nil 3658128963 ("" (lemma list_length_induction) (("" (inst? -1) (("" (split -1) (("1" (propax) nil nil) ("2" (skeep 1) (("2" (expand qs 1) (("2" (lift-if 1) (("2" (split 1) (("1" (grind 1) nil nil) ("2" (flatten 1) (("2" (assert 2) (("2" (lemma sorted_append) (("2" (inst -1 "car(g)" "qs(split(car(g),cdr(g))`1)" "cons(car(g),qs(split(car(g),cdr(g))`2))") (("2" (split -1) (("1" (propax) nil nil) ("2" (copy -1) (("2" (inst -1 "split(car(g),cdr(g))`1") (("2" (split -1) (("1" (propax) nil nil) ("2" (lemma split_length) (("2" (inst -1 "car(g)" "cdr(g)") (("2" (assert -1) (("2" (expand less 1) (("2" (assert 1) (("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand sorted? 1) (("3" (skeep 1) (("3" (expand nth 1) (("3" (lift-if 1) (("3" (split 1) (("1" (flatten 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten 1) (("1" (assert) nil nil)) nil) ("2" (flatten 1) (("2" (lemma split_lwb_upb) (("2" (inst -1 "car(g)" "cdr(g)") (("2" (assert -1) (("2" (flatten -1) (("2" (lemma lwb_perm) (("2" (inst -1 "split(car(g),cdr(g))`2" "qs(split(car(g),cdr(g))`2)") (("2" (split -1) (("1" (inst -1 "car(g)") (("1" (split -1) (("1" (expand lwb -1) (("1" (inst -1 "j-1") (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) (("2" (grind 1) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (lemma qs_perm) (("2" (inst -1 "split(car(g),cdr(g))`2") (("2" (lemma perm_commutative) (("2" (inst -1 "qs(split(car(g),cdr(g))`2)" "split(car(g),cdr(g))`2") (("2" (split -1) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten 1) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten 1) (("1" (grind) nil nil)) nil) ("2" (flatten 1) (("2" (inst -3 "split(car(g),cdr(g))`2") (("2" (split -3) (("1" (expand sorted? -1) (("1" (inst -1 "i-1" "j-1") (("1" (split -1) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (assert) (("3" (grind 1) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (lemma split_length) (("2" (inst? -1) (("2" (assert -1) (("2" (grind 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma split_lwb_upb) (("4" (inst -1 "car(g)" "cdr(g)") (("4" (assert -1) (("4" (flatten -1) (("4" (lemma upb_perm) (("4" (inst -1 "split(car(g),cdr(g))`1" "qs(split(car(g),cdr(g))`1)") (("4" (split -1) (("1" (inst -1 "car(g)") (("1" (split -1) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil) ("2" (lemma qs_perm) (("2" (inst? -1) (("2" (lemma perm_commutative) (("2" (inst -1 "qs(split(car(g),cdr(g))`1)" "split(car(g),cdr(g))`1") (("2" (split -1) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (lemma split_lwb_upb) (("5" (inst -1 "car(g)" "cdr(g)") (("5" (assert -1) (("5" (flatten -1) (("5" (lemma lwb_perm) (("5" (inst -1 "split(car(g),cdr(g))`2" "qs(split(car(g),cdr(g))`2)") (("5" (split -1) (("1" (inst -1 "car(g)") (("1" (split -1) (("1" (expand lwb 1) (("1" (skeep 1) (("1" (expand nth -5) (("1" (lift-if -5) (("1" (split -5) (("1" (assert -1) nil nil) ("2" (flatten -1) (("2" (expand lwb -2) (("2" (inst -2 "i-1") (("1" (split -2) (("1" (propax) nil nil) ("2" (assert) (("2" (grind 1) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (lemma qs_perm) (("2" (inst -1 "split(car(g),cdr(g))`2") (("2" (lemma perm_commutative) (("2" (inst -1 "qs(split(car(g),cdr(g))`2)" "split(car(g),cdr(g))`2") (("2" (split -1) (("1" (propax) nil nil) ("2" (propax) 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) ((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_length_induction formula-decl nil my_list_induction nil) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (split def-decl "[list[nat], list[nat]]" SPLIT nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (i skolem-const-decl "nat" QS_props nil) (upb_perm formula-decl nil QS_props nil) (nth def-decl "T" list_props nil) (qs_perm formula-decl nil QS_props nil) (perm_commutative formula-decl nil my_list_props nil) (lwb const-decl "bool" SPLIT nil) (upb const-decl "bool" SPLIT nil) (j skolem-const-decl "nat" QS_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) (lwb_perm formula-decl nil QS_props nil) (split_lwb_upb formula-decl nil SPLIT nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (i skolem-const-decl "nat" QS_props nil) (less const-decl "bool" my_list_induction 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (split_length formula-decl nil SPLIT nil) (sorted_append formula-decl nil SORTED nil) (qs def-decl "list[nat]" QS nil) (sorted? const-decl "bool" SORTED nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil)) shostak)))