| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 316 kB |
|
Impressum subterm.prfSprache: Lisp |
|||||||||||||||
|
(subterm (subtermOF_TCC1 0 (subtermOF_TCC1-1 nil 3388757677 ("" (skosimp*) (("" (typepred "p!1") (("" (expand "positionsOF") (("" (assert) (("" (expand "only_empty_seq") (("" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (subtermOF_TCC2 0 (subtermOF_TCC2-1 nil 3388757677 ("" (skosimp*) (("" (typepred "p!1") (("" (expand "positionsOF") (("" (lift-if) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (first const-decl "T" seq_extras "structures/") (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (subtermOF_TCC3 0 (subtermOF_TCC3-1 nil 3388757677 ("" (skosimp*) (("" (typepred "p!1") (("" (expand "positionsOF" -1) (("" (lift-if) (("" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand "only_empty_seq") (("2" (rewrite "empty_0") nil nil)) nil) ("3" (expand* "union" "member") (("3" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate") (("2" (skolem * "y1") (("2" (expand "member") (("2" (flatten) (("2" (replace -3 -1 rl) (("2" (typepred "i1") (("2" (lemma "fsepn.first_equal") (("2" (inst -1 "q!1" "y1" "i!1" "i1") (("2" (prop) (("1" (assert) nil nil) ("2" (lemma "fsepn.seq_first_rest") (("2" (inst -1 "p!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (first_equal formula-decl nil seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (seq_first_rest formula-decl nil seq_extras "structures/") (<= const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (only_empty_seq const-decl "positions" positions nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/")) nil)) (subtermOF_TCC4 0 (subtermOF_TCC4-1 nil 3388757677 ("" (skosimp*) (("" (replaces -3) (("" (rewrite "length_rest") nil nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length_rest formula-decl nil seq_extras "structures/")) nil)) (subtermOF_TCC5 0 (subtermOF_TCC5-1 nil 3388757677 ("" (skosimp*) (("" (typepred "p!1") (("" (expand "positionsOF") (("" (assert) (("" (expand "only_empty_seq") (("" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (only_empty_seq const-decl "positions" positions nil)) nil)) (pos_vars_subset_pos 0 (pos_vars_subset_pos-1 nil 3411906619 ("" (skosimp*) (("" (skoletin* 1) (("" (expand* subset? member) (("" (skosimp*) (("" (expand "Posv") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (subset? const-decl "bool" sets nil) (positionsOF def-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (extend const-decl "R" extend nil) (Posv skolem-const-decl "positions[variable, symbol, arity]" subterm nil) (member const-decl "bool" sets nil)) shostak)) (Pos_var_is_finite 0 (Pos_var_is_finite-1 nil 3414630433 ("" (skosimp*) (("" (skoletin* 1) (("" (replaces -1) (("" (lemma "pos_vars_subset_pos") (("" (inst?) (("" (assert) (("" (lemma "positions_of_terms_finite") (("" (inst?) (("" (lemma "finite_sets[position].finite_subset") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (is_finite const-decl "bool" finite_sets nil) (pos_vars_subset_pos formula-decl nil subterm nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (positionsOF def-decl "positions" positions nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil) (finite_set type-eq-decl nil finite_sets nil) (finite_subset formula-decl nil finite_sets nil) (positions_of_terms_finite formula-decl nil positions nil)) shostak)) (Vars_is_var 0 (Vars_is_var-1 nil 3402241169 ("" (skeep) (("" (decompose-equality) (("" (expand "Vars") (("" (expand "restrict") (("" (iff) (("" (prop) (("1" (skosimp*) (("1" (typepred "p!1") (("1" (expand "positionsOF") (("1" (expand* "only_empty_seq" "subtermOF") (("1" (lift-if) (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "empty_seq") (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "positionsOF") (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vars const-decl "set[(V)]" subterm nil) (= const-decl "[T, T -> boolean]" equalities nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm 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) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (empty_seq const-decl "finseq" finite_sequences nil) (t skolem-const-decl "term[variable, symbol, arity]" subterm nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (subtermOF def-decl "term" subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil)) shostak)) (vars_term_is_union 0 (vars_term_is_union-1 nil 3415054747 ("" (skosimp*) (("" (lift-if) (("" (prop) (("1" (decompose-equality 1) (("1" (expand "restrict") (("1" (lemma "Vars_is_var") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 2) (("2" (iff) (("2" (prop) (("1" (expand "finseq_appl") (("1" (expand "IUnion") (("1" (expand "Vars") (("1" (skosimp*) (("1" (expand "subtermOF" -1) (("1" (lift-if) (("1" (prop) (("1" (typepred "x!1") (("1" (expand "V") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (inst 2 "first(p!1) - 1") (("1" (inst 2 "rest(p!1)") nil nil) ("2" (typepred "first[posnat](p!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (expand "IUnion") (("2" (skosimp*) (("2" (expand "Vars") (("2" (skosimp*) (("2" (inst 1 "add_first(i!1 + 1, p!1)") (("1" (expand "subtermOF" 1) (("1" (lift-if) (("1" (prop) (("1" (hide (-2 1 2)) (("1" (grind) nil nil)) nil) ("2" (expand "finseq_appl") (("2" (rewrite "rest_add_first") (("2" (rewrite "first_add") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (typepred "p!1") (("2" (expand "positionsOF" 1) (("2" (expand* "union" "member") (("2" (prop) (("2" (hide 1) (("2" (expand "IUnion") (("2" (expand "finseq_appl") (("2" (inst 1 "i!1 + 1") (("2" (expand "catenate") (("2" (expand "member") (("2" (inst 1 "p!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) ((t1!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (IUnion const-decl "set[T]" indexed_sets nil) (finseq type-eq-decl nil finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rest const-decl "finseq" seq_extras "structures/") (p!1 skolem-const-decl "positions?[variable, symbol, arity](t1!1)" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (NOT const-decl "[bool -> bool]" booleans nil) (subtermOF def-decl "term" subterm nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (p!1 skolem-const-decl "positions?[variable, symbol, arity](args(t1!1)`seq(i!1))" subterm nil) (i!1 skolem-const-decl "below[length(args(t1!1))]" subterm nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (add_first const-decl "finseq" seq_extras "structures/") (first_add formula-decl nil seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (catenate const-decl "positions" positions nil) (<= const-decl "bool" reals nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[term[variable, symbol, arity]]" subterm nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (Vars const-decl "set[(V)]" subterm nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (v adt-accessor-decl "[(vars?) -> variable]" term_adt nil) (restrict const-decl "R" restrict nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm 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) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (Vars_is_var formula-decl nil subterm nil)) shostak)) (vars_of_term_finite 0 (vars_of_term_finite-1 nil 3415056088 ("" (induct "t") (("1" (skosimp*) (("1" (lemma "vars_term_is_union") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "length(app2_var!1) = 0") (("1" (hide -2) (("1" (case-replace "Vars(app(app1_var!1, app2_var!1)) = emptyset" :hide? T) (("1" (rewrite "finite_emptyset") nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "Vars") (("1" (skosimp*) (("1" (typepred "p!1") (("1" (expand "positionsOF") (("1" (expand "only_empty_seq") (("1" (replaces -1) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (typepred "x!1") (("1" (expand "V") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "vars_term_is_union") (("2" (inst?) (("2" (assert) (("2" (replaces -1 2) (("2" (expand "finseq_appl") (("2" (lemma "IUnion_extra[(V)].IUnion_of_finite_is_finite1") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (IUnion_of_finite_is_finite1 formula-decl nil IUnion_extra nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (only_empty_seq const-decl "positions" positions nil) (subtermOF def-decl "term" subterm nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (finite_emptyset judgement-tcc nil finite_sets nil) (emptyset const-decl "set" sets nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[term[variable, symbol, arity]]" subterm nil) (vars_term_is_union formula-decl nil subterm nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (Vars const-decl "set[(V)]" subterm nil) (is_finite const-decl "bool" finite_sets nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)) shostak)) (pos_subterm_ax_TCC1 0 (pos_subterm_ax_TCC1-1 nil 3388757677 ("" (skosimp*) (("" (lemma "closed_positions") (("" (inst -1 "p!1" "p!1 o q!1" "t!1") (("" (assert) (("" (expand "<=") (("" (inst 1 "q!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" subterm 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) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (closed_positions formula-decl nil positions nil) (<= const-decl "bool" positions nil) (term type-decl nil term_adt nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil)) nil)) (pos_subterm_ax 0 (pos_subterm_ax-1 nil 3388757678 ("" (measure-induct+ "length(p)" "p") (("1" (skeep) (("1" (expand "subtermOF" 1) (("1" (prop) (("1" (hide -2) (("1" (rewrite "empty_0") (("1" (replaces -1) (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil) ("2" (inst -1 "rest(x!1)" "q" "args(t)(first(x!1) - 1)") (("1" (rewrite "length_rest") (("1" (prop) (("1" (hide 3) (("1" (expand "positionsOF" -1) (("1" (lift-if) (("1" (prop) (("1" (expand "only_empty_seq") (("1" (lemma "fsepn.seq_empty") (("1" (inst -1 "x!1" "q") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "only_empty_seq") (("2" (lemma "fsepn.seq_empty") (("2" (inst -1 "x!1" "q") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand* "union" "member") (("3" (prop) (("1" (expand "only_empty_seq") (("1" (lemma "fsepn.seq_empty") (("1" (inst -1 "x!1" "q") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate") (("2" (skolem * "y1") (("2" (expand "member") (("2" (flatten) (("2" (lemma "fsepn.seq_first_rest") (("2" (inst -1 "x!1") (("2" (assert) (("2" (replaces -1 -3) (("2" (lemma "fsepn.add_first_compo") (("2" (inst -1 "rest(x!1)" "q" "first(x!1)") (("2" (replaces -1 -3) (("2" (lemma "fsepn.first_equal") (("2" (inst -1 "rest(x!1) o q" "y1" "first(x!1)" "i1") (("2" (assert) (("2" (flatten) (("2" (assert) 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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -3 2)) (("2" (lemma "pos_ax") (("2" (inst -1 "y!1" "q!1" "t!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "pos_ax") (("3" (inst -1 "p!1" "q!1" "t!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((pos_ax formula-decl nil positions nil) (empty_0 formula-decl nil seq_extras "structures/") (empty_o_seq formula-decl nil seq_extras "structures/") (length_rest formula-decl nil seq_extras "structures/") (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (seq_first_rest formula-decl nil seq_extras "structures/") (add_first_compo formula-decl nil seq_extras "structures/") (upto? nonempty-type-eq-decl nil IUnion_extra nil) (<= const-decl "bool" reals nil) (first_equal formula-decl nil seq_extras "structures/") (only_empty_seq const-decl "positions" positions nil) (seq_empty formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (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) (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (x!1 skolem-const-decl "position[variable, symbol, arity]" subterm nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finseq type-eq-decl nil finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (pos_subterm_TCC1 0 (pos_subterm_TCC1-1 nil 3388757677 ("" (skosimp*) (("" (lemma "pos_subterm_ax") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((pos_subterm_ax formula-decl nil subterm nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (pos_subterm 0 (pos_subterm-1 nil 3388769744 ("" (measure-induct+ "length(p)" ("p")) (("1" (skeep) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst -1 "x!1") (("1" (case "x!1`length /= 0") (("1" (assert) (("1" (name-replace "subtemp" "subtermOF(t, x!1)") (("1" (replace -2 1) (("1" (rewrite "add_first_compo") (("1" (expand "subtermOF" 1 1) (("1" (lift-if) (("1" (prop) (("1" (lemma "fsepn.empty_0") (("1" (inst -1 "add_first(first(x!1), rest(x!1) o q)") (("1" (assert) (("1" (hide-all-but (-1 -3 2)) (("1" (lemma "fsepn.add_first_compo") (("1" (inst -1 "rest(x!1)" "q" "first(x!1)") (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (replace -2 -1 rl) (("1" (hide -2) (("1" (lemma "fsepn.seq_empty") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "first(add_first(first(x!1), rest(x!1) o q)) = first(x!1)" :hide? t) (("1" (rewrite "fsepn.rest_add_first") (("1" (expand "subtemp") (("1" (inst -2 "rest(x!1)" "q" "args(t)(first(x!1) - 1)") (("1" (rewrite "length_rest") (("1" (prop) (("1" (replaces -1) (("1" (case-replace "subtermOF(t, x!1) = subtermOF(args(t)(first(x!1) - 1), rest(x!1))") (("1" (hide-all-but 1) (("1" (expand "subtermOF" 1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (expand "positionsOF" -2) (("2" (lift-if) (("2" (prop) (("1" (expand "only_empty_seq") (("1" (hide (-1 -3 1)) (("1" (lemma "fsepn.seq_empty") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3 1 2)) (("2" (expand "only_empty_seq") (("2" (lemma "fsepn.seq_empty") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand* "union" "member") (("3" (prop) (("1" (hide (-2 1 2 3)) (("1" (expand "only_empty_seq") (("1" (lemma "fsepn.seq_empty") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate") (("2" (skolem * "y1") (("2" (expand "member") (("2" (flatten) (("2" (replace -3 -2) (("2" (rewrite "fsepn.add_first_compo") (("2" (hide (-3 1 2)) (("2" (lemma "fsepn.first_equal") (("2" (inst -1 "rest(x!1) o q" "y1" "first(x!1)" "i1") (("2" (assert) (("2" (flatten) (("2" (assert) 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) ("2" (hide-all-but (1 4)) (("2" (rewrite "first_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (hide-all-but (-2 1)) (("1" (expand "subtermOF" 1 3) (("1" (lift-if) (("1" (prop) (("1" (hide -2) (("1" (rewrite "empty_0") (("1" (replaces -1) (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "subtermOF" 1 3) (("2" (lift-if) (("2" (prop) (("2" (hide -2) (("2" (rewrite "empty_0") (("2" (replaces -1) (("2" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (lemma "pos_subterm_ax") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 1)) (("3" (lemma "pos_ax") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "pos_subterm_ax") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (lemma "pos_ax") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ((pos_ax formula-decl nil positions nil) (pos_subterm_ax formula-decl nil subterm nil) (empty_o_seq formula-decl nil seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (seq_empty formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (first_add formula-decl nil seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt 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) (only_empty_seq const-decl "positions" positions nil) (first_equal formula-decl nil seq_extras "structures/") (<= const-decl "bool" reals nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (catenate const-decl "positions" positions nil) (IUnion const-decl "set[T]" indexed_sets nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (length_rest formula-decl nil seq_extras "structures/") (subtemp skolem-const-decl "term[variable, symbol, arity]" subterm nil) (add_first_compo formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (/= const-decl "boolean" notequal nil) (seq_first_rest formula-decl nil seq_extras "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (term type-decl nil term_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finseq type-eq-decl nil finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (pos_o_term 0 (pos_o_term-1 nil 3399644897 ("" (measure-induct+ "length(p)" "p") (("" (skeep) (("" (expand "positionsOF" -2) (("" (lift-if) (("" (prop) (("1" (expand "only_empty_seq") (("1" (hide -3) (("1" (replaces -2) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3) (("2" (expand "only_empty_seq") (("2" (replaces -2) (("2" (expand "subtermOF") (("2" (rewrite "fsepn.empty_0") (("2" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand* "union" "member") (("3" (prop) (("1" (expand "only_empty_seq") (("1" (hide -2) (("1" (replaces -1) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "IUnion") (("2" (skosimp*) (("2" (expand "catenate") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "positionsOF" 3) (("2" (lift-if) (("2" (prop) (("2" (expand* "union" "member") (("2" (prop) (("2" (expand "IUnion") (("2" (inst 3 "i!1") (("2" (expand "catenate") (("2" (case "x!1`length /= 0") (("1" (inst 3 "rest(x!1) o q") (("1" (expand "member") (("1" (inst -4 "rest(x!1)") (("1" (inst -4 "q" "args(t)(i!1 - 1)") (("1" (lemma "fsepn.rest_add_first") (("1" (inst -1 "x!2" "first(x!1)") (("1" (rewrite "length_rest") (("1" (replace -4 -1) (("1" (rewrite "first_add") (("1" (replace -4 -1 rl) (("1" (replace -1 * rl) (("1" (lemma "fsepn.add_first_compo") (("1" (inst -1 "rest(x!1)" "q" "first(x!1)") (("1" (case-replace "first(x!1) = i!1") (("1" (replace -6 * rl) (("1" (replace -2 * rl) (("1" (expand "subtermOF" -8) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -5 1)) (("2" (replaces -2) (("2" (rewrite "first_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rest const-decl "finseq" seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (length_rest formula-decl nil seq_extras "structures/") (first_add formula-decl nil seq_extras "structures/") (add_first_compo formula-decl nil seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (x!1 skolem-const-decl "position[variable, symbol, arity]" subterm nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (only_empty_seq const-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (empty_o_seq formula-decl nil seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (subterm_is_app_TCC1 0 (subterm_is_app_TCC1-1 nil 3497114104 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (subterm_is_app_TCC2 0 (subterm_is_app_TCC2-1 nil 3497114104 ("" (skosimp*) (("" (rewrite "delete_is_position") nil nil)) nil) ((delete_is_position formula-decl nil positions nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil)) nil)) (subterm_is_app 0 (subterm_is_app-1 nil 3497114230 ("" (skosimp*) (("" (lemma "pos_subterm_ax") (("" (inst -1 "delete(p!1, length(p!1) - 1)" "#(last(p!1))" "s!1") (("1" (prop) (("1" (lemma "fsepn.add_first_empty_seq") (("1" (inst -1 "last(p!1)") (("1" (lemma "not_var") (("1" (inst -1 "last(p!1)" "#(last(p!1))" "empty_seq" "subtermOF(s!1, delete(p!1, length(p!1) - 1))") (("1" (assert) nil nil) ("2" (hide (-1 -2 -3 3)) (("2" (typepred "length(p!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "fsepn.add_last_delete_is_o") (("2" (inst?) (("2" (assert) (("2" (lemma "fsepn.add_last_delete") (("2" (inst?) (("2" (assert) (("2" (replace -1 -2 rl) (("2" (expand "finseq_appl") (("2" (expand "last" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide (-1 3)) (("3" (typepred "length(p!1)") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((pos_subterm_ax formula-decl nil subterm nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil) (not_var formula-decl nil positions nil) (add_first_empty_seq formula-decl nil seq_extras "structures/") (add_last_delete formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (add_last_delete_is_o formula-decl nil seq_extras "structures/") (term type-decl nil term_adt nil) (last const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (delete const-decl "finseq" seq_extras "structures/") (< const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (/= const-decl "boolean" notequal 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (p!1 skolem-const-decl "position[variable, symbol, arity]" subterm nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (vars_subterm 0 (vars_subterm-1 nil 3402782187 ("" (skeep) (("" (expand* "subset?" "member") (("" (skeep) (("" (expand "Vars") (("" (expand "restrict") (("" (skosimp*) (("" (typepred "p!1") (("" (inst 1 "p o p!1") (("1" (rewrite "pos_subterm") (("1" (rewrite "pos_o_term") nil nil)) nil) ("2" (rewrite "pos_o_term") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (Vars const-decl "set[(V)]" subterm nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pos_subterm formula-decl nil subterm nil) (pos_o_term formula-decl nil subterm nil) (t skolem-const-decl "term[variable, symbol, arity]" subterm nil) (finseq type-eq-decl nil finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (p skolem-const-decl "position[variable, symbol, arity]" subterm nil) (p!1 skolem-const-decl "positions?[variable, symbol, arity](subtermOF(t, p))" subterm nil)) shostak)) (disjoint_subterm 0 (disjoint_subterm-1 nil 3402066026 ("" (skeep) (("" (lemma "vars_subterm") (("" (inst?) (("" (assert) (("" (lemma "IUnion_extra[(V)].disjoint_subset") (("" (hide -3) (("" (inst -1 "Vars(subtermOF(t, p))" "Vars(t)" "Vars(s)" "Vars(s)") (("" (assert) (("" (hide-all-but 1) (("" (expand* "subset?" "member") (("" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((vars_subterm formula-decl nil subterm nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (Vars const-decl "set[(V)]" subterm nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (disjoint_subset formula-decl nil IUnion_extra nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (variable_positions_parallel 0 (variable_positions_parallel-1 nil 3414510689 ("" (induct "t") (("1" (skeep) (("1" (skolem-typepred) (("1" (flatten) (("1" (expand "V") (("1" (expand "positionsOF") (("1" (expand "only_empty_seq") (("1" (replaces -3) (("1" (replaces -3) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skolem-typepred) (("2" (flatten) (("2" (expand "V") (("2" (expand "positionsOF") (("2" (prop) (("1" (expand "only_empty_seq") (("1" (replaces -2) (("1" (replaces -3) (("1" (hide-all-but (-6 -7 1)) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "only_empty_seq") (("1" (replaces -1) (("1" (replaces -1) (("1" (hide-all-but (-4 -5 3)) (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -5)) (("2" (expand "only_empty_seq") (("2" (expand* "parallel" "<=") (("2" (prop) (("1" (skosimp*) (("1" (replaces -1) (("1" (lemma "fsepn.seq_empty") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (replaces -1) (("2" (expand "subtermOF" -4) (("2" (rewrite "empty_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-2 -5)) (("3" (expand "only_empty_seq") (("3" (replaces -1) (("3" (expand "subtermOF" -3) (("3" (rewrite "empty_0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "IUnion") (("4" (skosimp*) (("4" (expand "catenate") (("4" (skosimp*) (("4" (expand "member") (("4" (expand "finseq_appl") (("4" (expand "subtermOF" (-8 -9)) (("4" (lift-if) (("4" (prop) (("1" (hide-all-but (-1 -8)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 -5)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-1 -7)) (("3" (grind) nil nil)) nil) ("4" (expand "finseq_appl") (("4" (lemma "fsepn.first_add") (("4" (copy -1) (("4" (inst -1 "x!2" "i!1") (("4" (inst -2 "x!3" "i!2") (("4" (lemma "fsepn.rest_add_first") (("4" (copy -1) (("4" (inst -1 "x!2" "i!1") (("4" (inst -2 "x!3" "i!2") (("4" (replace -8 (-1 -3) rl) (("4" (replace -10 (-2 -4) rl) (("4" (replaces -1) (("4" (replaces -1) (("4" (replaces -1) (("4" (replaces -1) (("4" (case-replace "i!2 = i!1") (("1" (inst -10 "i!1 - 1") (("1" (inst -10 "x!1" "y!1" "x!2" "x!3") (("1" (assert) (("1" (hide-all-but (-1 -5 -7 -10 6)) (("1" (expand* "parallel" "<=") (("1" (prop) (("1" (skosimp*) (("1" (replaces -3) (("1" (replaces -3) (("1" (rewrite "add_first_compo") (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) (("1" (inst 1 "p1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replaces -3) (("2" (replaces -3) (("2" (rewrite "add_first_compo") (("2" (lemma "fsepn.first_equal") (("2" (inst?) (("2" (assert) (("2" (inst 2 "p1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -6 1 7)) (("2" (expand* "parallel" "<=") (("2" (prop) (("1" (skosimp*) (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite "add_first_compo") (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replaces -1) (("2" (replaces -2) (("2" (rewrite "add_first_compo") (("2" (lemma "fsepn.first_equal") (("2" (inst?) (("2" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (first_add formula-decl nil seq_extras "structures/") (upto? nonempty-type-eq-decl nil IUnion_extra nil) (<= const-decl "bool" reals nil) (rest_add_first formula-decl nil seq_extras "structures/") (add_first_compo formula-decl nil seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (first_equal formula-decl nil seq_extras "structures/") (< const-decl "bool" reals 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (<= const-decl "bool" positions nil) (seq_empty formula-decl nil seq_extras "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (parallel const-decl "bool" positions nil) (/= const-decl "boolean" notequal nil) (subtermOF def-decl "term" subterm nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)) shostak)) (variable_positions 0 (variable_positions-1 nil 3411906851 ("" (skosimp*) (("" (skoletin 1) (("" (flatten) (("" (replaces -3) (("" (expand* "member" "Pos_var" "parallel" "<=") (("" (expand "extend") (("" (prop) (("1" (skosimp*) (("1" (replace -1 -3) (("1" (rewrite "pos_subterm") (("1" (replace -2 -3) (("1" (typepred "q!1") (("1" (replace -2 -1) (("1" (lemma "pos_subterm_ax") (("1" (inst?) (("1" (assert) (("1" (replace -4 -1) (("1" (hide-all-but (-1 -3 1)) (("1" (typepred "x!1") (("1" (expand "V") (("1" (expand "positionsOF") (("1" (assert) (("1" (expand "only_empty_seq") (("1" (replaces -2) (("1" (rewrite "seq_o_empty") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1 -2) (("2" (rewrite "pos_subterm") (("2" (replace -3 -2) (("2" (typepred "p!1") (("2" (replace -2 -1) (("2" (lemma "pos_subterm_ax") (("2" (inst?) (("2" (assert) (("2" (replace -5 -1) (("2" (hide-all-but (-1 -3 1)) (("2" (typepred "x!1") (("2" (expand "V") (("2" (expand "positionsOF") (("2" (assert) (("2" (expand "only_empty_seq") (("2" (replaces -2) (("2" (rewrite "seq_o_empty") 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) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (parallel const-decl "bool" positions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (member const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (extend const-decl "R" extend nil) (pos_subterm formula-decl nil subterm nil) (NOT const-decl "[bool -> bool]" booleans nil) (pos_subterm_ax formula-decl nil subterm nil) (seq_o_empty formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (<= const-decl "bool" positions nil)) shostak)) (pos_occ_var_HAStypePP_TCC1 0 (pos_occ_var_HAStypePP_TCC1-1 nil 3412415465 ("" (skosimp*) (("" (replaces -1) (("" (lemma "Pos_var_is_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var_is_finite formula-decl nil subterm nil)) nil)) (pos_occ_var_HAStypePP 0 (pos_occ_var_HAStypePP-1 nil 3411907203 ("" (skosimp*) (("" (skoletin* 1) (("" (expand "PP?") (("" (prop) (("" (skosimp*) (("" (lemma "variable_positions") (("" (expand "finseq_appl") (("" (inst -1 "t!1" "x!1" "seqv`seq(i!1)" "seqv`seq(j!1)") (("1" (assert) (("1" (prop) (("1" (lemma "set2seq_neq[position]") (("1" (inst -1 "Posv") (("1" (assert) (("1" (inst -1 "i!1" "j!1") (("1" (grind) nil nil) ("2" (typepred "j!1") (("2" (replace -3) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil) ("3" (typepred "i!1") (("3" (replaces -3) (("3" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "set2seq_lem[position]") (("2" (inst -1 "Posv") (("2" (assert) (("2" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (expand "member") (("1" (hide 4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (replaces -2) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "set2seq_lem[position]") (("3" (inst -1 "Posv") (("3" (assert) (("3" (inst -1 "j!1") (("1" (expand "finseq_appl") (("1" (expand "member") (("1" (hide 4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "j!1") (("2" (replaces -2) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "set2seq_lem[position]") (("2" (inst -1 "Posv") (("2" (assert) (("2" (inst -1 "j!1") (("1" (replaces -3) (("1" (expand "finseq_appl") (("1" (expand "Pos_var" -1 1) (("1" (expand "extend" -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "j!1") (("2" (replaces -2) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "set2seq_lem[position]") (("3" (inst -1 "Posv") (("3" (assert) (("3" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (replaces -3) (("1" (expand "Pos_var" -1 1) (("1" (expand "extend" -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (replaces -2) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (is_finite const-decl "bool" finite_sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (finite_sequence type-eq-decl nil finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (PP? const-decl "bool" positions nil) (finite_set type-eq-decl nil finite_sets nil) (set2seq def-decl "finite_sequence[T]" set2seq "structures/") (variable_positions formula-decl nil subterm nil) (positionsOF def-decl "positions" positions nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil) (seqv skolem-const-decl "finite_sequence[position[variable, symbol, arity]]" subterm nil) (< const-decl "bool" reals nil) (i!1 skolem-const-decl "below[length(seqv)]" subterm nil) (j!1 skolem-const-decl "below[length(seqv)]" subterm nil) (positions? type-eq-decl nil positions nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Posv skolem-const-decl "positions[variable, symbol, arity]" subterm nil) (below type-eq-decl nil naturalnumbers nil) (set2seq_length formula-decl nil set2seq "structures/") (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (set2seq_neq formula-decl nil set2seq "structures/") (set2seq_lem formula-decl nil set2seq "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (extend const-decl "R" extend nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) shostak)) (pos_occ_var_HAStypeSP 0 (pos_occ_var_HAStypeSP-1 nil 3411907585 ("" (skosimp*) (("" (skoletin* 1) (("" (expand "SP?") (("" (skosimp*) (("" (expand "finseq_appl") (("" (lemma "set2seq_lem[position]") (("" (inst -1 "Posv") (("" (assert) (("" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (replaces -3) (("1" (expand "Pos_var" -1 1) (("1" (expand "extend" -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (replaces -2) (("2" (rewrite "set2seq_length[position]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (is_finite const-decl "bool" finite_sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (finite_sequence type-eq-decl nil finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (SP? const-decl "bool" positions nil) (finite_set type-eq-decl nil finite_sets nil) (set2seq def-decl "finite_sequence[T]" set2seq "structures/") (set2seq_lem formula-decl nil set2seq "structures/") (extend const-decl "R" extend nil) (set2seq_length formula-decl nil set2seq "structures/") (below type-eq-decl nil naturalnumbers nil) (Posv skolem-const-decl "positions[variable, symbol, arity]" subterm nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (i!1 skolem-const-decl "below[length(seqv)]" subterm nil) (seqv skolem-const-decl "finite_sequence[position[variable, symbol, arity]]" subterm nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) shostak)) (no_empty_set_positions 0 (no_empty_set_positions-1 nil 3412318789 ("" (skosimp*) (("" (skoletin* 1) (("" (flatten) (("" (replaces -) (("" (expand "Pos_var") (("" (expand "extend") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (extend const-decl "R" extend nil)) shostak)) (length_seq_var_g0 0 (length_seq_var_g0-1 nil 3412318971 ("" (skosimp*) (("" (skoletin* 1) (("1" (lemma "no_empty_set_positions") (("1" (inst?) (("1" (assert) (("1" (case "card(Posv) > 0") (("1" (lemma "fspos.set2seq_length") (("1" (inst?) (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "finite_sets[position].nonempty_card") (("2" (inst?) (("2" (prop) (("2" (hide (1 3)) (("2" (expand "nonempty?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replaces -1) (("2" (replaces -1) (("2" (lemma "Pos_var_is_finite") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var const-decl "positions" subterm nil) (is_finite const-decl "bool" finite_sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (set2seq def-decl "finite_sequence[T]" set2seq "structures/") (finite_set type-eq-decl nil finite_sets nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finite_sequence type-eq-decl nil finite_sequences nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (set2seq_length formula-decl nil set2seq "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (no_empty_set_positions formula-decl nil subterm nil)) shostak)) (subterm_empty_seq_TCC1 0 (subterm_empty_seq_TCC1-1 nil 3512737910 ("" (skosimp) (("" (expand positionsOF) (("" (lift-if) (("" (expand* only_empty_seq union member) nil nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (only_empty_seq const-decl "positions" positions nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil)) nil)) (subterm_empty_seq 0 (subterm_empty_seq-1 nil 3513090436 ("" (skosimp) (("" (expand subtermOF) (("" (rewrite empty_0) nil nil)) nil)) nil) ((subtermOF def-decl "term" subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (empty_0 formula-decl nil seq_extras "structures/")) shostak)) (equal_subterms_equal_term 0 (equal_subterms_equal_term-1 nil 3512737910 ("" (skosimp) (("" (prop) (("1" (inst -1 empty_seq) (("1" (expand subtermOF) (("1" (rewrite empty_0) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand positionsOF) (("1" (lift-if) (("1" (expand* only_empty_seq union member) nil nil)) nil)) nil) ("2" (expand positionsOF) (("2" (lift-if) (("2" (expand* only_empty_seq union member) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ((only_empty_seq const-decl "positions" positions nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (subtermOF def-decl "term" subterm nil) (empty_0 formula-decl nil seq_extras "structures/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (term type-decl nil term_adt nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil) (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil)) nil)) (subt_of_subt_is_subt_of_term_TCC1 0 (subt_of_subt_is_subt_of_term_TCC1-1 nil 3455281835 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (term type-decl nil term_adt nil) (below type-eq-decl nil nat_types nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finite_sequence type-eq-decl nil finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (|#| const-decl "finite_sequence[T]" set2seq "structures/")) nil)) (subt_of_subt_is_subt_of_term 0 (subt_of_subt_is_subt_of_term-1 nil 3455281853 ("" (skeep) (("" (replace -1 1) (("" (expand "subtermOF") (("" (lift-if) (("" (lift-if) (("" (prop) (("1" (expand "finseq_appl") (("1" (rewrite "first_add") (("1" (rewrite "rest_add_first") (("1" (rewrite "empty_0" -2) (("1" (replace -2 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (expand "#") (("2" (grind) nil nil)) nil)) nil) ("3" (expand "finseq_appl") (("3" (rewrite "first_add") (("3" (rewrite "rest_add_first") (("3" (rewrite "empty_0" -1) (("3" (replace -1 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "finseq_appl") (("4" (expand "rest") (("4" (assert) (("4" (expand "first") (("4" (expand "finseq_appl") (("4" (assert) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "finseq_appl") (("5" (rewrite "first_add") (("5" (rewrite "rest_add_first") (("5" (assert) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("6" (expand "finseq_appl") (("6" (grind) nil nil)) nil) ("7" (expand "finseq_appl") (("7" (rewrite "first_add") (("7" (rewrite "rest_add_first") (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty_0 formula-decl nil seq_extras "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (add_first const-decl "finseq" seq_extras "structures/") (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (positions? type-eq-decl nil positions 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (subtermOF def-decl "term" subterm nil)) shostak)) (subterm_to_subtermOF 0 (subterm_to_subtermOF-1 nil 3455281944 ("" (induct "t") (("1" (skeep) (("1" (skeep) (("1" (inst 1 "empty_seq") (("1" (expand "subtermOF") (("1" (rewrite "empty_0") (("1" (expand "subterm") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "positionsOF") (("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subterm" -2) (("2" (split) (("1" (inst 1 "empty_seq") (("1" (expand "subtermOF" 1) (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "z!1") (("2" (inst -2 "s!1") (("2" (assert) (("2" (skosimp) (("2" (case "seq(app2_var!1)(z!1) = subtermOF(app(app1_var!1, app2_var!1), #(z!1 + 1))") (("1" (replace -1 -3) (("1" (name-replace "t!1" "app(app1_var!1, app2_var!1)") (("1" (lemma "subt_of_subt_is_subt_of_term") (("1" (inst 1 "add_first( z!1 + 1, p!1)") (("1" (inst?) (("1" (name-replace "x!1" "add_first(z!1 + 1, p!1)") (("1" (inst -1 "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "z!1") (("2" (typepred "t!1") (("2" (reveal -5) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "z!1") (("1" (assert) nil nil) ("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "positionsOF") (("2" (expand "union") (("2" (flatten) (("2" (hide 1) (("2" (expand "IUnion") (("2" (expand "member") (("2" (inst?) (("2" (assert) (("2" (expand "catenate") (("2" (inst?) (("2" (typepred "p!1") (("2" (expand "member") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subtermOF") (("2" (lift-if) (("2" (prop) (("1" (hide 1) (("1" (grind) nil nil)) nil) ("2" (hide 1) (("2" (expand "finseq_appl") (("2" (expand "first") (("2" (expand "rest") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "z!1") (("3" (lemma "positions_of_arg") (("3" (inst -1 "app(app1_var!1, app2_var!1)" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (member const-decl "bool" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app1_var!1 skolem-const-decl "symbol" subterm nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" subterm nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (z!1 skolem-const-decl "below[app2_var!1`length]" subterm nil) (p!1 skolem-const-decl "{p: position | positionsOF(app2_var!1`seq(z!1))(p)}" subterm nil) (positions_of_arg formula-decl nil positions nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (t!1 skolem-const-decl "(app?)" subterm nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (subt_of_subt_is_subt_of_term formula-decl nil subterm nil) (rest const-decl "finseq" seq_extras "structures/") (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_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) (^ const-decl "finseq" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (vars1_var skolem-const-decl "variable" subterm nil) (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (only_empty_seq const-decl "positions" positions nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (subterm adt-def-decl "boolean" term_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil)) shostak)) (subtermOF_to_subterm 0 (subtermOF_to_subterm-1 nil 3455282276 ("" (induct "t") (("1" (skosimp*) (("1" (expand "subtermOF") (("1" (expand "subterm") (("1" (lift-if) (("1" (prop) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (typepred "p!1") (("2" (expand "positionsOF") (("2" (expand "only_empty_seq") (("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (expand "subtermOF" -2) (("2" (lift-if) (("2" (prop) (("1" (replace -2 1) (("1" (expand "subterm") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (inst -2 "first(p!1) -1" "s!1" "rest(p!1)") (("1" (assert) (("1" (expand "subterm" 2) (("1" (flatten) (("1" (inst 3 "first(p!1) - 1") nil nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (typepred "p!1") (("2" (expand* "first" "finseq_appl") (("2" (expand "positionsOF") (("2" (prop) (("1" (hide -1 1) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil)) nil) ("2" (expand "union") (("2" (prop) (("1" (hide 1 2) (("1" (rewrite "empty_0") (("1" (expand* "member" "only_empty_seq") nil nil)) nil)) nil) ("2" (hide 1 3) (("2" (expand "member") (("2" (expand "IUnion") (("2" (skeep -1) (("2" (expand "catenate") (("2" (skeep -1) (("2" (hide -1) (("2" (replace -1 1) (("2" (assert) 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) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (p!1 skolem-const-decl "{p: position | positionsOF(app(app1_var!1, app2_var!1))(p)}" subterm nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" subterm nil) (app1_var!1 skolem-const-decl "symbol" subterm nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (rest const-decl "finseq" seq_extras "structures/") (< const-decl "bool" reals nil) (union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (only_empty_seq const-decl "positions" positions nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (subterm adt-def-decl "boolean" term_adt nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil)) shostak)) (subterm_to_subterm 0 (subterm_to_subterm-1 nil 3455282320 ("" (induct "t") (("1" (skosimp*) (("1" (expand "subterm") (("1" (prop) (("1" (assert) nil nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subterm" -3) (("2" (prop) (("1" (inst -2 "empty_seq" "s!1" "r!1") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (skosimp) (("2" (inst -2 "z!1" "s!1" "r!1") (("2" (assert) (("2" (expand "subterm" 1) (("2" (flatten) (("2" (inst 2 "z!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (extract1 const-decl "T" finite_sequences nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app1_var!1 skolem-const-decl "symbol" subterm nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" subterm nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (subterm adt-def-decl "boolean" term_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil)) shostak)) (comp_of_pos_TCC1 0 (comp_of_pos_TCC1-1 nil 3457112583 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (comp_of_pos_TCC2 0 (comp_of_pos_TCC2-1 nil 3457112583 ("" (termination-tcc) nil nil) nil nil)) (n_for_a_pstart 0 (n_for_a_pstart-1 nil 3457201283 ("" (skosimp*) (("" (typepred "q!1") (("" (expand "set_of_seq_pos" -1) (("" (expand "IUnion") (("" (skosimp*) (("" (expand "singleton") (("" (inst 2 "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((set_of_seq_pos const-decl "set[position]" subterm nil) (set type-eq-decl nil sets nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (IUnion const-decl "set[T]" indexed_sets nil) (singleton const-decl "(singleton?)" sets nil)) shostak)) (length_comp_p 0 (length_comp_p-1 nil 3457192341 ("" (induct n) (("1" (skeep) (("1" (expand comp_of_pos) (("1" (assert) (("1" (rewrite empty_0) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst -1 p) (("2" (expand comp_of_pos 1) (("2" (expand o 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((O const-decl "finseq" finite_sequences nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (empty_0 formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (comp_of_pos def-decl "position" subterm nil) (= const-decl "[T, T -> boolean]" equalities nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (m_neq_n 0 (m_neq_n-1 nil 3457190961 ("" (skeep) (("" (lemma length_comp_p) (("" (copy -1) (("" (inst?) (("" (inst -2 m p) (("" (assert) (("" (replace -3 -1) (("" (replace -1 -2) (("" (lemma empty_0[posnat]) (("" (inst -1 p) (("" (hide -2 -4) (("" (assert) (("" (rewrite both_sides_times1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length_comp_p formula-decl nil subterm 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) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (both_sides_times1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (empty_0 formula-decl nil seq_extras "structures/")) shostak)) (is_injective_function_inj_TCC1 0 (is_injective_function_inj_TCC1-1 nil 3457205512 ("" (subtype-tcc) nil 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) (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) (empty_seq const-decl "finseq" finite_sequences nil) (set_of_seq_pos const-decl "set[position]" subterm nil) (function_inj const-decl "position" subterm nil) (singleton const-decl "(singleton?)" sets nil) (IUnion const-decl "set[T]" indexed_sets nil)) nil)) (is_injective_function_inj 0 (is_injective_function_inj-1 nil 3457205513 ("" (skeep) (("" (expand "injective?") (("" (skeep 2) (("" (expand "function_inj") (("" (lemma "length_comp_p") (("" (copy -1) (("" (inst -1 "x1" "p") (("" (inst -2 "x2" "p") (("" (replace -3 -1) (("" (replaces -1 -2) (("" (rewrite "both_sides_times1") (("" (hide-all-but (1 2)) (("" (prop) (("" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((injective? const-decl "bool" functions nil) (function_inj const-decl "position" subterm nil) (finseq type-eq-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (both_sides_times1 formula-decl nil real_props nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_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) (length_comp_p formula-decl nil subterm nil)) shostak)) (infinite_set_of_seq_pos 0 (infinite_set_of_seq_pos-1 nil 3457117766 ("" (skeep) (("" (lemma "infinite_def[position]") (("" (inst?) (("" (assert) (("" (inst 1 "function_inj(p)") (("" (prop) (("1" (hide -1) (("1" (skeep) (("1" (expand "set_of_seq_pos") (("1" (expand "IUnion") (("1" (expand "function_inj") (("1" (inst 1 "x1") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "is_injective_function_inj") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (infinite_def formula-decl nil infinite_nat_def "sets_aux/") (IUnion const-decl "set[T]" indexed_sets nil) (singleton const-decl "(singleton?)" sets nil) (is_injective_function_inj formula-decl nil subterm nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (p skolem-const-decl "position[variable, symbol, arity]" subterm nil) (function_inj const-decl "position" subterm nil) (injective? const-decl "bool" functions nil) (set_of_seq_pos const-decl "set[position]" subterm nil) (set type-eq-decl nil sets nil)) shostak)) (comp_of_pos_is_pos 0 (comp_of_pos_is_pos-1 nil 3457168775 ("" (induct "n") (("1" (skosimp*) (("1" (expand "comp_of_pos") (("1" (hide (-1 -2)) (("1" (expand "positionsOF") (("1" (lift-if) (("1" (prop) (("1" (expand "only_empty_seq") (("1" (propax) nil nil)) nil) ("2" (expand "only_empty_seq") (("2" (propax) nil nil)) nil) ("3" (expand* "union" "member" "only_empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "comp_of_pos" 1) (("2" (inst -1 "p!1" "s!1") (("2" (assert) (("2" (replace -3 -1 rl) (("2" (rewrite "pos_o_term") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pos_o_term formula-decl nil subterm nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (only_empty_seq const-decl "positions" positions nil) (nat_induction formula-decl nil naturalnumbers nil) (comp_of_pos def-decl "position" subterm nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (subset_of_seq_pos 0 (subset_of_seq_pos-1 nil 3457130014 ("" (skosimp*) (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (expand "set_of_seq_pos") (("" (expand "IUnion") (("" (skosimp*) (("" (expand "singleton") (("" (lemma "comp_of_pos_is_pos") (("" (inst -1 "p!1" "s!1" "i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (singleton const-decl "(singleton?)" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (comp_of_pos_is_pos formula-decl nil subterm nil) (set_of_seq_pos const-decl "set[position]" subterm nil)) shostak)) (term_eq_subterm 0 (term_eq_subterm-1 nil 3457105607 ("" (skeep) (("" (case "p /= empty_seq") (("1" (hide 1) (("1" (case "subset?(set_of_seq_pos(p), positionsOF(s))") (("1" (lemma infinite_set_of_seq_pos) (("1" (inst?) (("1" (assert) (("1" (lemma finite_subset[position]) (("1" (inst?) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (rewrite positions_of_terms_finite) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite subset_of_seq_pos) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (/= const-decl "boolean" notequal nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (set_of_seq_pos const-decl "set[position]" subterm nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (finite_subset formula-decl nil finite_sets nil) (positions_of_terms_finite formula-decl nil positions nil) (finite_set type-eq-decl nil finite_sets nil) (s skolem-const-decl "term[variable, symbol, arity]" subterm nil) (is_finite const-decl "bool" finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (infinite_set_of_seq_pos formula-decl nil subterm nil) (subset_of_seq_pos formula-decl nil subterm nil)) shostak)) (app_term 0 (app_term-1 nil 3513089267 ("" (expand child) (("" (skosimp*) (("" (lemma seq_first_rest[posnat]) (("" (inst -1 p1!1) (("" (lemma empty_0[posnat]) (("" (inst -1 p1!1) (("" (assert) (("" (lemma pos_subterm_ax) (("" (inst -1 q!1 p1!1 s!1) (("" (assert) (("" (lemma not_var) (("" (inst -1 "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(s!1, q!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (pos_subterm_ax formula-decl nil subterm nil) (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (not_var formula-decl nil positions nil) (term type-decl nil term_adt nil) (empty_0 formula-decl nil seq_extras "structures/") (seq_first_rest formula-decl nil seq_extras "structures/") (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (child const-decl "bool" positions nil)) shostak)) (positions_of_a_term 0 (positions_of_a_term-1 nil 3514739012 ("" (measure-induct+ "length(q)" ("q")) (("" (skosimp) (("" (case "x!1 = empty_seq") (("1" (hide-all-but (-1 3 4)) (("1" (replaces -1) (("1" (expand child) (("1" (inst 1 p!1) (("1" (rewrite empty_o_seq) (("1" (flatten) (("1" (replaces -1) (("1" (inst 1 empty_seq) (("1" (rewrite empty_o_seq) (("1" (rewrite subterm_empty_seq) (("1" (expand positionsOF) (("1" (lift-if) (("1" (expand* only_empty_seq union member) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "delete(x!1, length(x!1) - 1)") (("1" (inst -1 t!1 p!1) (("1" (case "length(delete(x!1, length(x!1) - 1)) < length(x!1)") (("1" (assert) (("1" (hide -1) (("1" (rewrite delete_is_position) (("1" (prop) (("1" (hide-all-but (-1 -2 1 2)) (("1" (name-replace "dp" "delete(x!1, length(x!1) - 1)" :hide? nil) (("1" (lemma add_last_delete[posnat]) (("1" (inst -1 x!1) (("1" (assert) (("1" (replace -2) (("1" (rewrite add_last_is_o) (("1" (expand "left_without_children") (("1" (skosimp) (("1" (replace -3 -1) (("1" (inst 4 r!1 p1!1 "q1!1 o #(last(x!1))") (("1" (rewrite o_assoc) (("1" (rewrite first_compo) (("1" (assert) (("1" (hide-all-but 4) (("1" (expand* "#" o empty_seq) (("1" (flatten) (("1" (hide -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 3)) (("2" (name-replace "dp" "delete(x!1, length(x!1) - 1)" :hide? nil) (("2" (lemma add_last_delete[posnat]) (("2" (inst -1 x!1) (("2" (assert) (("2" (replace -2) (("2" (rewrite add_last_is_o) (("2" (expand "left_without_children") (("2" (skosimp) (("2" (replace -4 -1) (("2" (inst 4 r!1 "p1!1 o #(last(x!1))" q1!1) (("2" (rewrite o_assoc) (("2" (rewrite first_compo) (("1" (assert) (("1" (hide-all-but 4) (("1" (expand* "#" o empty_seq) (("1" (flatten) (("1" (hide -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (flatten) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (name-replace "dp" "delete(x!1, length(x!1) - 1)" :hide? nil) (("3" (expand child -2) (("3" (skosimp) (("3" (lemma add_last_delete[posnat]) (("3" (inst -1 x!1) (("3" (assert) (("3" (replace -2) (("3" (rewrite add_last_is_o) (("3" (case "last(x!1) < first(p1!1)") (("1" (hide 3 5 6) (("1" (expand "left_without_children") (("1" (inst 3 dp "#(last(x!1))" p1!1) (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (expand first 1 1) (("2" (expand finseq_appl) (("2" (expand "#" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "last(x!1) > first(p1!1)") (("1" (hide 5 6 7) (("1" (expand "left_without_children") (("1" (inst 4 dp p1!1 "#(last(x!1))") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (expand first 1 2) (("2" (expand finseq_appl) (("2" (expand "#" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "p1!1 = #(last(x!1))") (("1" (hide 5 6 7) (("1" (inst 5 empty_seq) (("1" (rewrite seq_o_empty) (("1" (assert) (("1" (hide-all-but 5) (("1" (expand positionsOF) (("1" (lift-if) (("1" (expand* only_empty_seq union member) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6 7 9) (("2" (case "last(x!1) = first(p1!1)") (("1" (lemma seq_first_rest_1[posnat]) (("1" (inst -1 p1!1) (("1" (lemma empty_0[posnat]) (("1" (inst -1 p1!1) (("1" (assert) (("1" (replace -1 -5) (("1" (rewrite o_assoc) (("1" (replace -2 -5 rl) (("1" (replace -3 -5 rl) (("1" (expand child) (("1" (inst 7 "rest(p1!1)") (("1" (assert) (("1" (hide-all-but (-1 -2 2 7)) (("1" (flatten) (("1" (replaces -3) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3 4)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 2)) (("3" (flatten) (("3" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2 3 4) (("4" (skosimp) (("4" (lemma add_last_delete[posnat]) (("4" (inst -1 x!1) (("4" (assert) (("4" (replace -3) (("4" (rewrite add_last_is_o) (("4" (inst 2 "q1!1 o #(last(x!1))") (("4" (rewrite o_assoc) (("4" (assert) (("4" (lemma pos_subterm_ax) (("4" (inst -1 "p!1" "q1!1 o #(last(x!1))" "t!1") (("4" (assert) (("4" (rewrite o_assoc) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (expand delete) (("2" (rewrite empty_0) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but (1 2)) (("3" (lemma empty_0[posnat]) (("3" (inst -1 x!1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (lemma empty_0[posnat]) (("2" (inst -1 x!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (x!1 skolem-const-decl "position[variable, symbol, arity]" subterm nil) (delete const-decl "finseq" seq_extras "structures/") (o_assoc formula-decl nil finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (first_compo formula-decl nil seq_extras "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (add_last_is_o formula-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (last const-decl "T" seq_extras "structures/") (add_last_delete formula-decl nil seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (seq_first_rest_1 formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (seq_o_empty formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (pos_subterm_ax formula-decl nil subterm nil) (delete_is_position formula-decl nil positions nil) (empty_o_seq formula-decl nil seq_extras "structures/") (only_empty_seq const-decl "positions" positions nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (subterm_empty_seq formula-decl nil subterm nil) (empty_seq const-decl "finseq" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (child const-decl "bool" positions nil) (left_without_children const-decl "bool" positions nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (equal_app_term 0 (equal_app_term-1 nil 3516190832 ("" (skosimp) (("" (case "s!1 = app(f(s!1), args(s!1))") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (replace -1 1) (("1" (replace -2 1) (("1" (decompose-equality 1) nil nil)) nil)) nil) ("2" (decompose-equality 1) nil nil)) nil) ("2" (decompose-equality 1) nil nil)) nil)) nil) ((args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" subterm 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) (symbol formal-nonempty-type-decl nil subterm nil) (variable formal-nonempty-type-decl nil subterm nil) (term_app_extensionality formula-decl nil term_adt nil)) shostak)) (equal_term_TCC1 0 (equal_term_TCC1-1 nil 3516237359 ("" (skosimp*) (("" (hide -1 -2) (("" (lemma app_term) (("" (inst -1 p!1 p1!1 s!1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (app_term formula-decl nil subterm nil)) nil)) (equal_term_TCC2 0 (equal_term_TCC2-1 nil 3516237359 ("" (skosimp*) (("" (hide -1 -2) (("" (lemma app_term) (("" (inst -1 p!1 p1!1 t!1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm nil) (arity formal-const-decl "[symbol -> nat]" subterm nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (app_term formula-decl nil subterm nil)) nil)) (equal_term 0 (equal_term-1 nil 3516237359 ("" (induct s) (("1" (skosimp*) (("1" (typepred p!1) (("1" (hide-all-but (-1 1)) (("1" (expand positionsOF) (("1" (expand only_empty_seq) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name-replace "s!1" "app(app1_var!1, app2_var!1)" :hide? nil) (("2" (case "app?(t!1)") (("1" (lemma equal_app_term) (("1" (inst -1 s!1 t!1) (("1" (assert) (("1" (prop) (("1" (hide-all-but (-6 1 2)) (("1" (inst -1 empty_seq) (("1" (rewrite subterm_empty_seq) (("1" (rewrite subterm_empty_seq) (("1" (assert) (("1" (hide 1) (("1" (expand child) (("1" (inst 1 p!1) (("1" (rewrite empty_o_seq) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (split) (("1" (expand positionsOF) (("1" (expand* only_empty_seq union member) nil nil)) nil) ("2" (expand positionsOF) (("2" (expand* only_empty_seq union member) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("1" (hide-all-but (-2 -6 1 2)) (("1" (inst -2 empty_seq) (("1" (rewrite subterm_empty_seq) (("1" (rewrite subterm_empty_seq) (("1" (assert) (("1" (hide 1) (("1" (expand child) (("1" (inst 1 p!1) (("1" (assert) (("1" (rewrite empty_o_seq) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (replaces -1) (("2" (split) (("1" (expand* positionsOF only_empty_seq union member) nil nil) ("2" (expand* positionsOF only_empty_seq union member) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (lemma positions_of_arg) (("2" (inst-cp -1 s!1 x!1) (("2" (inst -1 t!1 x!1) (("2" (case "subtermOF(s!1, #(x!1 + 1)) = args(s!1)`seq(x!1)") (("1" (case "subtermOF(t!1, #(x!1 + 1)) = args(t!1)`seq(x!1)") (("1" (replace -1 1 rl) (("1" (replace -2 1 rl) (("1" (case "left_without_children(p!1, #(x!1 + 1))") (("1" (hide-all-but (-1 -4 -5 -6 -7 -9 1)) (("1" (inst -6 "#(x!1 + 1)") (("1" (assert) nil nil) ("2" (replace -5) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "left_without_children( #(x!1 + 1), p!1)") (("1" (hide-all-but (-1 -4 -5 -6 -7 -10 2)) (("1" (inst -6 "#(x!1 + 1)") (("1" (assert) nil nil) ("2" (replace -5) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "EXISTS(q1 : position) : positionsOF(subtermOF(s!1, p!1))(q1) AND #(x!1 + 1) = p!1 o q1") (("1" (hide -8 -9 -10 -11) (("1" (skosimp) (("1" (case "q1!1 = empty_seq") (("1" (replaces -1) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-2 1 5)) (("2" (expand* "#" o) (("2" (flatten) (("2" (hide -2) (("2" (lemma empty_0[posnat]) (("2" (inst-cp -1 q1!1) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "child(p!1, #(x!1 + 1))") (("1" (inst -8 x!1) (("1" (expand child -1) (("1" (skosimp) (("1" (inst -8 "subtermOF(t!1, #(x!1 + 1))" p1!1) (("1" (assert) (("1" (split) (("1" (hide-all-but (-1 -3 -4 -7 -8 5)) (("1" (case "subtermOF(s!1, #(1 + x!1)) = app2_var!1`seq(x!1)") (("1" (assert) nil nil) ("2" (hide-all-but (-3 -5 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case "subtermOF(s!1, #(1 + x!1)) = app2_var!1`seq(x!1)") (("1" (replace -1 1 rl) (("1" (inst -10 "#(1 + x!1) o q!1") (("1" (split) (("1" (hide-all-but (-1 -2 1)) (("1" (typepred q!1) (("1" (replace -4 -1 rl) (("1" (hide -4) (("1" (rewrite pos_subterm) (("1" (rewrite pos_subterm) (("1" (hide -1 -3 2) (("1" (rewrite pos_o_term) nil nil)) nil)) nil) ("2" (hide -2 -3 2) (("2" (rewrite pos_o_term) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1 3 8)) (("2" (expand left_without_children) (("2" (skosimp) (("2" (inst 1 "#(1 + x!1) o r!1" "p1!2" "q1!1") (("2" (assert) (("2" (replace -2 -4) (("2" (rewrite o_assoc) (("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (lemma o_assoc[posnat]) (("2" (inst -1 "#(1 + x!1)" "r!1" "q1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9) (("2" (hide-all-but (-5 -6 -7 -9 1)) (("2" (typepred q!1) (("2" (case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))") (("1" (replaces -1) (("1" (hide -3 -6) (("1" (rewrite pos_o_term) (("1" (rewrite pos_o_term) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -6 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -8 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))") (("1" (replace -1 1) (("1" (inst -11 "#(1 + x!1) o q!1") (("1" (split) (("1" (typepred q!1) (("1" (hide-all-but (-1 -2 -3 -4 -9 -10 1)) (("1" (replaces -4) (("1" (rewrite pos_subterm) (("1" (rewrite pos_subterm) (("1" (hide -3 2) (("1" (rewrite pos_o_term) nil nil)) nil)) nil) ("2" (hide -3 2) (("2" (rewrite pos_o_term) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1 3 8)) (("2" (expand left_without_children) (("2" (skosimp) (("2" (replace -1 -4) (("2" (rewrite o_assoc) (("2" (inst 1 "#(1 + x!1) o r!1" "p1!2" "q1!1") (("2" (assert) (("2" (hide-all-but (-2 1)) (("2" (lemma o_assoc[posnat]) (("2" (inst -1 "#(1 + x!1)" "r!1" "p1!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9) (("2" (typepred q!1) (("2" (replace -3) (("2" (hide-all-but (-1 -2 -8 -9 1)) (("2" (rewrite pos_o_term) (("2" (rewrite pos_o_term) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -8 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))") (("1" (replace -1) (("1" (inst -12 "#(1 + x!1) o p1!2") (("1" (split) (("1" (typepred p1!2) (("1" (hide-all-but (-1 -2 -3 -4 -9 -10 1)) (("1" (replaces -4) (("1" (rewrite pos_subterm) (("1" (rewrite pos_subterm) (("1" (hide -3 2) (("1" (rewrite pos_o_term) nil nil)) nil)) nil) ("2" (hide -3 2) (("2" (rewrite pos_o_term) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1 3 8)) (("2" (expand child) (("2" (skosimp) (("2" (inst 1 p1!3) (("2" (replace -1 -2) (("2" (rewrite o_assoc) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9) (("2" (typepred p1!2) (("2" (hide-all-but (-1 -2 -3 -8 -9 1)) (("2" (replaces -3) (("2" (rewrite pos_o_term) (("2" (rewrite pos_o_term) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -8 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))") (("1" (replace -1) (("1" (hide-all-but (-2 -12 1)) (("1" (replace -1) (("1" (rewrite pos_subterm) (("1" (rewrite pos_subterm) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -7 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "app2_var!1`seq(x!1) = subtermOF(s!1, #(x!1 + 1))") (("1" (replace -1) (("1" (hide-all-but (-2 1)) (("1" (rewrite pos_subterm_ax) (("1" (rewrite pos_subterm_ax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -7 1)) (("2" (replaces -1) (("2" (decompose-equality -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred x!1) (("3" (hide-all-but (-1 -8 1)) (("3" (decompose-equality -2) (("3" (hide -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred x!1) (("2" (hide-all-but (-1 -8 1)) (("2" (decompose-equality -2) (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1 2 3 4)) (("2" (lemma positions_of_a_term) (("2" (inst -1 "#(x!1 + 1)" s!1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand subtermOF) (("2" (lift-if) (("2" (prop) (("1" (expand "#") (("1" (assert) nil nil)) nil) ("2" (expand finseq_appl) (("2" (case "rest( #(1 + x!1)) = empty_seq") (("1" (replaces -1) (("1" (rewrite subterm_empty_seq) (("1" (expand* first finseq_appl) (("1" (expand "#" 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma length_rest_0[posnat]) (("2" (inst -1 "#(1 + x!1)") (("2" (expand "#" -1 3) (("2" (flatten) (("2" (rewrite empty_0 -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand subtermOF) (("2" (lift-if) (("2" (prop) (("1" (expand "#") (("1" (assert) nil nil)) nil) ("2" (expand finseq_appl) (("2" (case "rest( #(1 + x!1)) = empty_seq") (("1" (replaces -1) (("1" (rewrite subterm_empty_seq) (("1" (expand* first finseq_appl) (("1" (expand "#" 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma length_rest_0[posnat]) (("2" (inst -1 "#(1 + x!1)") (("2" (expand "#" -1 3) (("2" (flatten) (("2" (rewrite empty_0 -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred p!1) (("2" (hide-all-but (-2 1 2)) (("2" (expand positionsOF) (("2" (assert) (("2" (expand only_empty_seq) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (hide -1 -2) (("3" (lemma app_term) (("3" (inst -1 p!1 p1!1 t!1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (hide -1 -2) (("4" (lemma app_term) (("4" (inst -1 p!1 p1!1 s!2) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((app_term formula-decl nil subterm nil) (app1_var!1 skolem-const-decl "symbol" subterm nil) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" subterm nil) (t!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil) (empty_o_seq formula-decl nil seq_extras "structures/") (subterm_empty_seq formula-decl nil subterm nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (length_rest_0 formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rest const-decl "finseq" seq_extras "structures/") (s!1 skolem-const-decl "(app?)" subterm nil) (x!1 skolem-const-decl "below[args(s!1)`length]" subterm nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (O const-decl "finseq" finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (seq_o_empty formula-decl nil seq_extras "structures/") (positions_of_a_term formula-decl nil subterm nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pos_subterm_ax formula-decl nil subterm nil) (p1!2 skolem-const-decl "{p: position | positionsOF(app2_var!1`seq(x!1))(p) AND positionsOF(subtermOF(t!1, #(1 + x!1)))(p)}" subterm nil) (q!1 skolem-const-decl "{p: position | positionsOF(app2_var!1`seq(x!1))(p) AND positionsOF(subtermOF(t!1, #(1 + x!1)))(p)}" subterm nil) (pos_o_term formula-decl nil subterm nil) (pos_subterm formula-decl nil subterm nil) (o_assoc formula-decl nil finite_sequences nil) (q!1 skolem-const-decl "{p: position | positionsOF(app2_var!1`seq(x!1))(p) AND positionsOF(subtermOF(t!1, #(1 + x!1)))(p)}" subterm nil) (p1!1 skolem-const-decl "position[variable, symbol, arity]" subterm nil) (positions_of_arg formula-decl nil positions nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (equal_app_term formula-decl nil subterm nil) (finite_sequence type-eq-decl nil finite_sequences nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (only_empty_seq const-decl "positions" positions nil) (vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil subterm nil) (symbol formal-nonempty-type-decl nil subterm 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) (arity formal-const-decl "[symbol -> nat]" subterm nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (term type-decl nil term_adt nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (left_without_children const-decl "bool" positions nil) (= const-decl "[T, T -> boolean]" equalities nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (child const-decl "bool" positions nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil)) nil)))
¤ Dauer der Verarbeitung: 0.337 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26