| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 250 kB |
|
Quellcode-Bibliothek positions.prfSprache: Lisp |
|||||||||||||||
|
(positions (positionsOF_TCC1 0 (positionsOF_TCC1-1 nil 3388744728 ("" (subtype-tcc) nil nil) nil nil)) (positionsOF_TCC2 0 (positionsOF_TCC2-1 nil 3389723936 ("" (grind) 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) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions 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) (arity formal-const-decl "[symbol -> nat]" positions nil) (term type-decl nil term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< adt-def-decl "(strict_well_founded?[term])" term_adt nil) (subterm adt-def-decl "boolean" term_adt nil) (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) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (position type-eq-decl nil positions nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (left_without_children_TCC1 0 (left_without_children_TCC1-1 nil 3511797058 ("" (skosimp) (("" (rewrite empty_0) 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) (position 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)) nil)) (left_without_children_TCC2 0 (left_without_children_TCC2-1 nil 3511797058 ("" (skosimp) (("" (rewrite empty_0) 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) (position 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)) nil)) (positions_of_terms_finite 0 (positions_of_terms_finite-1 nil 3415310384 ("" (induct "t") (("1" (skosimp*) (("1" (expand* "positionsOF" "only_empty_seq") (("1" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide 2) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "positionsOF" 1) (("2" (prop) (("1" (expand "only_empty_seq") (("1" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide (-1 -2 2)) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_sets[position].finite_union") (("2" (inst?) (("1" (hide 3) (("1" (expand "finseq_appl") (("1" (lemma "IUnion_of_finite_is_finite") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (inst -1 "i!1 - 1") (("1" (expand "is_finite") (("1" (skolem-typepred) (("1" (inst?) (("1" (inst 1 "LAMBDA (x: (catenate(i!1, positionsOF(app2_var!1`seq(i!1 - 1))))): f!1(rest(x))") (("1" (expand "injective?") (("1" (skolem-typepred) (("1" (expand "catenate") (("1" (skosimp*) (("1" (expand "member") (("1" (replaces -2) (("1" (replaces -3) (("1" (rewrite "rest_add_first") (("1" (rewrite "rest_add_first") (("1" (inst -5 "x!1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "catenate") (("2" (skosimp*) (("2" (expand "member") (("2" (replaces -2) (("2" (rewrite "rest_add_first") 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 (-1 2 3)) (("2" (expand "only_empty_seq") (("2" (case-replace "{x: position | x = empty_seq} = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide 2) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (finite_set type-eq-decl nil finite_sets nil) (<= const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (IUnion const-decl "set[T]" indexed_sets nil) (catenate const-decl "positions" positions nil) (< const-decl "bool" reals 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) (app2_var!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(app1_var!1)}" positions nil) (app1_var!1 skolem-const-decl "symbol" positions 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) (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "upto?[position](length(app2_var!1))" positions nil) (rest const-decl "finseq" seq_extras "structures/") (rest_add_first formula-decl nil seq_extras "structures/") (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (IUnion_of_finite_is_finite formula-decl nil IUnion_extra nil) (finite_union judgement-tcc nil finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[position]" positions nil) (finite_singleton judgement-tcc nil finite_sets nil) (only_empty_seq const-decl "positions" positions nil) (term_induction formula-decl nil term_adt nil) (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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)) (empty_pos 0 (empty_pos-1 nil 3390055503 ("" (skeep) (("" (expand "<=") (("" (skolem * "p1") (("" (replaces -1) (("" (expand* "o" "empty_seq") (("" (flatten) (("" (apply-extensionality) (("" (hide 2) (("" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" positions nil) (< const-decl "bool" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (FALSE const-decl "bool" booleans nil) (pred type-eq-decl nil defined_types nil) (epsilon const-decl "T" epsilons nil) (TRUE const-decl "bool" booleans 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) (>= 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) (O const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil)) shostak)) (closed_positions 0 (closed_positions-1 nil 3388746243 ("" (measure-induct+ "length(q)" "q") (("" (skeep) (("" (expand "positionsOF" (-2 1)) (("" (lift-if) (("" (prop) (("1" (hide (-1 -2 -4)) (("1" (expand "only_empty_seq") (("1" (lemma "empty_pos") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 -4 2 3)) (("2" (expand "only_empty_seq") (("2" (lemma "empty_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand* "union" "member" "only_empty_seq") (("3" (prop) (("1" (hide-all-but (-1 -3 2)) (("1" (lemma "empty_pos") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "IUnion") (("2" (skolem * "i1") (("2" (expand "catenate" -1) (("2" (skolem * "q1") (("2" (flatten) (("2" (expand "member") (("2" (inst -3 "q1") (("2" (expand "<=" -4) (("2" (skolem * "p1") (("2" (inst -3 "rest(p)" "args(t)(i1 - 1)") (("2" (prop) (("1" (inst 3 "i1") (("1" (expand "catenate") (("1" (inst 3 "rest(p)") (("1" (expand "member") (("1" (assert) (("1" (hide-all-but (-3 -4 2 3)) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst -1 "p") (("1" (prop) (("1" (replaces -1 -3) (("1" (lemma "fsepn.add_first_compo") (("1" (inst -1 "rest(p)" "p1" "first(p)") (("1" (replaces -1 -3) (("1" (replaces -1) (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (replaces -1) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst -1 "p") (("1" (assert) (("1" (prop) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") (("2" (hide-all-but (-2 -3 1 3)) (("2" (expand "<=") (("2" (inst 1 "p1") (("2" (lemma "fsepn.seq_first_rest") (("2" (inst -1 "p") (("2" (prop) (("1" (replaces -1 -3) (("1" (rewrite "fsepn.add_first_compo") (("1" (replaces -1 -2) (("1" (lemma "fsepn.first_equal") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 -3 1 3)) (("3" (grind) 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) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (O const-decl "finseq" finite_sequences nil) (empty_0 formula-decl nil seq_extras "structures/") (first_equal formula-decl nil seq_extras "structures/") (add_first_compo formula-decl nil seq_extras "structures/") (seq_first_rest formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (insert? const-decl "finseq" seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq type-eq-decl nil finite_sequences nil) (rest const-decl "finseq" 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) (= 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty_pos formula-decl nil positions nil) (only_empty_seq const-decl "positions" positions nil) (<= const-decl "bool" 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) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions 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) (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_symbol_equal_length_arg 0 (equal_symbol_equal_length_arg-1 nil 3496152694 ("" (skosimp*) (("" (grind) nil nil)) nil) nil shostak)) (not_var 0 (not_var-1 nil 3388757591 ("" (skeep) (("" (grind) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (positionsOF def-decl "positions" positions 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)) shostak)) (not_var1 0 (not_var1-1 nil 3496151134 ("" (skosimp) (("" (grind) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (add_last const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (positionsOF def-decl "positions" positions 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)) shostak)) (pos_ax 0 (pos_ax-1 nil 3388757621 ("" (lemma "closed_positions") (("" (assert) (("" (expand "<=") (("" (skosimp) (("" (inst -1 p!1 "p!1 o q!1" t!1) (("" (assert) (("" (inst 1 q!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions 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) (>= 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) (<= const-decl "bool" positions nil) (closed_positions formula-decl nil positions nil)) shostak)) (rest_of_positions_TCC1 0 (rest_of_positions_TCC1-1 nil 3411856776 ("" (skosimp*) (("" (lemma "not_var") (("" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1") (("1" (assert) (("1" (lemma "fsepn.seq_first_rest") (("1" (inst?) (("1" (assert) (("1" (expand "positionsOF") (("1" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "only_empty_seq") (("1" (rewrite "empty_0") nil nil)) nil) ("2" (expand "IUnion") (("2" (skosimp*) (("2" (expand "catenate") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "finseq_appl") (("2" (replace -3 -2) (("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) ("2" (assert) nil nil)) nil)) nil)) nil) ((not_var formula-decl nil positions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (positionsOF def-decl "positions" positions 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) (upto? nonempty-type-eq-decl nil IUnion_extra 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) (<= const-decl "bool" reals nil) (first_equal formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil) (empty_0 formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (seq_first_rest formula-decl nil seq_extras "structures/") (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (rest const-decl "finseq" seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (position type-eq-decl nil positions nil) (p!1 skolem-const-decl "position" positions nil)) nil)) (rest_of_positions_TCC2 0 (rest_of_positions_TCC2-1 nil 3411856776 ("" (skosimp*) (("" (expand "positionsOF") (("" (grind) nil nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (only_empty_seq const-decl "positions" positions nil)) nil)) (rest_of_positions 0 (rest_of_positions-1 nil 3411856777 ("" (skeep) (("" (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 "only_empty_seq") (("3" (expand* "union" "member") (("3" (prop) (("1" (rewrite "empty_0") 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?) (("2" (assert) (("2" (replaces -1 -3) (("2" (lemma "fsepn.first_equal") (("2" (inst?) (("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) ((positionsOF def-decl "positions" positions 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) (position 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) (only_empty_seq const-decl "positions" positions 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) (seq_first_rest formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (first_equal formula-decl nil seq_extras "structures/") (upto? nonempty-type-eq-decl nil IUnion_extra 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) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (<= const-decl "bool" reals nil) (first const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (rest const-decl "finseq" seq_extras "structures/")) shostak)) (delete_is_position_TCC1 0 (delete_is_position_TCC1-1 nil 3495982353 ("" (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)) (delete_is_position 0 (delete_is_position-1 nil 3495982633 ("" (skosimp*) (("" (lemma "fsepn.add_last_delete") (("" (inst?) (("" (assert) (("" (lemma "fsepn.add_last_delete_is_o") (("" (inst?) (("" (assert) (("" (expand "finseq_appl") (("" (replaces -1 -2) (("" (replaces -1 -2) (("" (lemma "pos_ax") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (add_last_delete formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (term type-decl nil term_adt nil) (pos_ax formula-decl nil positions nil) (add_last_delete_is_o formula-decl nil seq_extras "structures/") (position type-eq-decl nil positions 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)) shostak)) (parallel_comm 0 (parallel_comm-1 nil 3394367640 ("" (skeep) (("" (expand* "parallel" "<=") (("" (prop) nil nil)) nil)) nil) ((<= const-decl "bool" positions nil) (parallel const-decl "bool" positions nil)) shostak)) (rest_parallel 0 (rest_parallel-1 nil 3394301450 ("" (skeep) (("" (lemma "fsepn.seq_first_rest") (("" (copy -1) (("" (inst -1 "p") (("" (inst -2 "q") (("" (assert) (("" (expand "parallel") (("" (expand "<=") (("" (skosimp*) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (replace -2 3) (("1" (replace -3 3) (("1" (inst 3 "p1!1") (("1" (replaces -1) (("1" (replaces -4) (("1" (replaces -3) (("1" (rewrite "add_first_compo") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -2 4) (("2" (replace -3 4) (("2" (inst 3 "p1!1") (("2" (inst 4 "p1!1") (("2" (replaces -4) (("2" (replaces -1) (("2" (rewrite "add_first_compo") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (seq_first_rest 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) (position type-eq-decl nil positions nil) (<= const-decl "bool" positions nil) (add_first_compo formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (/= const-decl "boolean" notequal nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (parallel const-decl "bool" positions nil)) shostak)) (rest_of_PP_is_PP 0 (rest_of_PP_is_PP-1 nil 3411908006 ("" (skolem-typepred) (("" (expand "PP?") (("" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1" "j!1 + 1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (inst -2 "j!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "i!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rest_pos formula-decl nil seq_extras "structures/") (int_min application-judgement "{k: int | 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) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (j!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (fss!1 skolem-const-decl "PP" positions nil) (i!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (empty_seq const-decl "finseq" finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions 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) (>= 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)) shostak)) (rest_of_SP_is_SP 0 (rest_of_SP_is_SP-1 nil 3411908172 ("" (skolem-typepred) (("" (expand "SP?") (("" (case "length(rest(fss!1)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1") (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (prop) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (rest_pos formula-decl nil seq_extras "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" positions nil) (fss!1 skolem-const-decl "SP(s!1)" positions nil) (i!1 skolem-const-decl "below[length(rest(fss!1))]" positions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (rest const-decl "finseq" seq_extras "structures/") (SP type-eq-decl nil positions nil) (SP? const-decl "bool" positions 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) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions 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 positions nil) (variable formal-nonempty-type-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (delete_of_PP_is_PP 0 (delete_of_PP_is_PP-1 nil 3411908236 ("" (skolem 1 ("fss" "_")) (("" (case "length(fss) = 0") (("1" (grind) nil nil) ("2" (skolem-typepred) (("2" (typepred "fss") (("2" (expand "PP?") (("2" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (case "i!2 < i!1") (("1" (case "j!1 < i!1") (("1" (expand "delete" 3) (("1" (assert) (("1" (expand "finseq_appl") (("1" (inst -3 "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "delete" 4) (("2" (assert) (("2" (expand "finseq_appl") (("2" (inst -2 "i!2" "j!1 + 1") (("1" (assert) nil nil) ("2" (typepred "j!1") (("2" (hide (3 5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 < i!1") (("1" (expand "delete" 4) (("1" (assert) (("1" (expand "finseq_appl") (("1" (inst -2 "i!2 + 1" "j!1") (("1" (assert) nil nil) ("2" (hide (3 5)) (("2" (typepred "i!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "delete" 5) (("2" (assert) (("2" (expand "finseq_appl") (("2" (inst -1 "i!2 + 1" "j!1 + 1") (("1" (assert) nil nil) ("2" (hide (4 6)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide (4 6)) (("3" (typepred "i!2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions 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) (>= 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (delete const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!2 skolem-const-decl "below[length(delete(fss, i!1))]" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (fss skolem-const-decl "PP" positions nil) (i!1 skolem-const-decl "below[length(fss)]" positions nil) (j!1 skolem-const-decl "below[length(delete(fss, i!1))]" positions nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (delete_of_SP_is_SP 0 (delete_of_SP_is_SP-1 nil 3411908310 ("" (skolem 1 ("s" "fss" "_")) (("" (case "length(fss) = 0") (("1" (grind) nil nil) ("2" (skolem-typepred) (("2" (typepred "fss") (("2" (expand "SP?") (("2" (case "length(delete(fss, i!1)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (case "i!2 < i!1") (("1" (expand* "delete" "finseq_appl") (("1" (assert) (("1" (inst -2 "i!2") nil nil)) nil)) nil) ("2" (expand* "delete" "finseq_appl") (("2" (assert) (("2" (inst -1 "i!2 + 1") (("1" (assert) nil nil) ("2" (hide 5) (("2" (typepred "i!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((SP type-eq-decl nil positions nil) (SP? const-decl "bool" positions nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions 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) (>= 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (delete const-decl "finseq" seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!2 skolem-const-decl "below[length(delete(fss, i!1))]" positions nil) (i!1 skolem-const-decl "below[length(fss)]" positions nil) (fss skolem-const-decl "SP(s)" positions nil) (s skolem-const-decl "term[variable, symbol, arity]" positions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (add_first_parallel_pos_to_PP_is_PP 0 (add_first_parallel_pos_to_PP_is_PP-1 nil 3411908488 ("" (skolem-typepred) (("" (case "length(fss!1) = 0") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "PP?" 2) (("2" (prop) (("2" (skosimp*) (("2" (case-replace "i!1 = 0") (("1" (inst -3 "j!1 - 1") (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "0") (("1" (replaces -1) (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "j!1") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "parallel_comm") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide (-2 4)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (case-replace "j!1 = 0") (("1" (inst -3 "i!1 - 1") (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "0") (("1" (replaces -1) (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide (-2 5)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "PP?") (("2" (prop) (("1" (typepred "i!1" "j!1") (("1" (hide 5) (("1" (grind) nil nil)) nil)) nil) ("2" (inst -1 "i!1 - 1" "j!1 - 1") (("1" (assert) (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "j!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but (1 4)) (("3" (typepred "i!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (insert? const-decl "finseq" seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!1 skolem-const-decl "below[length(add_first(q!1, fss!1))]" positions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (j!1 skolem-const-decl "below[length(add_first(q!1, fss!1))]" positions nil) (fss!1 skolem-const-decl "PP" positions nil) (q!1 skolem-const-decl "position" positions nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (parallel_comm formula-decl nil positions nil) (nth_add_first formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions 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) (>= 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)) shostak)) (add_first_parallel_pos_to_SP_is_SP 0 (add_first_parallel_pos_to_SP_is_SP-1 nil 3411908749 ("" (skolem-typepred) (("" (case "length(fss!1) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (expand "SP?" 2) (("2" (skosimp*) (("2" (case-replace "i!1 = 0") (("1" (hide -2) (("1" (lemma "fspos.nth_add_first") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "SP?") (("2" (inst -1 "i!1 - 1") (("1" (lemma "fspos.nth_add_first") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (insert? const-decl "finseq" seq_extras "structures/") (add_first const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (q!1 skolem-const-decl "positions?(s!1)" positions nil) (i!1 skolem-const-decl "below[length(add_first(q!1, fss!1))]" positions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" positions nil) (fss!1 skolem-const-decl "SP(s!1)" positions nil) (nth_add_first formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (SP type-eq-decl nil positions nil) (SP? const-decl "bool" positions 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) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions 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 positions nil) (variable formal-nonempty-type-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (add_last_parallel_pos_to_PP_is_PP 0 (add_last_parallel_pos_to_PP_is_PP-1 nil 3411908815 ("" (skolem-typepred) (("" (case "length(fss!1) = 0") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "PP?" 2) (("2" (prop) (("2" (skosimp*) (("2" (case-replace "i!1 = length(fss!1)") (("1" (inst -3 "j!1") (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "length(fss!1)") (("1" (replaces -1) (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "j!1") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "parallel_comm") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3 5)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (case-replace "j!1 = length(fss!1)") (("1" (inst -3 "i!1") (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "length(fss!1)") (("1" (replaces -1) (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (2 1 6)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "PP?") (("2" (prop) (("1" (typepred "i!1" "j!1") (("1" (hide 5) (("1" (grind) nil nil)) nil)) nil) ("2" (inst -1 "i!1" "j!1") (("1" (assert) (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (assert) (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "j!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but (1 4)) (("3" (typepred "i!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (insert? const-decl "finseq" seq_extras "structures/") (add_last const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!1 skolem-const-decl "below[length(add_last(fss!1, q!1))]" positions nil) (j!1 skolem-const-decl "below[length(add_last(fss!1, q!1))]" positions nil) (q!1 skolem-const-decl "position" positions nil) (fss!1 skolem-const-decl "PP" positions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (parallel_comm formula-decl nil positions nil) (nth_add_last formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions 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) (>= 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)) shostak)) (add_last_parallel_pos_to_SP_is_SP 0 (add_last_parallel_pos_to_SP_is_SP-1 nil 3411908915 ("" (skolem-typepred) (("" (case "length(fss!1) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (expand "SP?" 2) (("2" (skosimp*) (("2" (case-replace "i!1 = length(fss!1)") (("1" (hide -2) (("1" (lemma "fspos.nth_add_last") (("1" (inst?) (("1" (replaces -1) nil nil)) nil)) nil)) nil) ("2" (expand "SP?") (("2" (inst -1 "i!1") (("1" (lemma "fspos.nth_add_last") (("1" (inst -1 "fss!1" "q!1" "i!1") (("1" (assert) nil nil) ("2" (hide-all-but (1 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (insert? const-decl "finseq" seq_extras "structures/") (add_last const-decl "finseq" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" positions nil) (fss!1 skolem-const-decl "SP(s!1)" positions nil) (q!1 skolem-const-decl "positions?(s!1)" positions nil) (i!1 skolem-const-decl "below[length(add_last(fss!1, q!1))]" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nth_add_last formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (SP type-eq-decl nil positions nil) (SP? const-decl "bool" positions 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) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions 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 positions nil) (variable formal-nonempty-type-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (positions_of_arg 0 (positions_of_arg-1 nil 3455282168 ("" (skeep) (("" (typepred "k") (("" (expand* "#" "positionsOF") (("" (expand* "union" "IUnion" "member") (("" (flatten) (("" (hide 1) (("" (inst 1 "k + 1") (("" (assert) (("" (expand "catenate") (("" (inst 1 "empty_seq") (("" (split) (("1" (expand* "member" "finseq_appl" "positionsOF") (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (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) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (only_empty_seq const-decl "positions" positions nil) (catenate const-decl "positions" positions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (position type-eq-decl nil positions nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (positionsOF def-decl "positions" positions nil)) shostak)) (left_pos_transitive 0 (left_pos_transitive-1 nil 3512738380 ("" (skosimp) (("" (expand "left_pos") (("" (skosimp*) (("" (prop) (("1" (replace -3 -4 rl) (("1" (replace -2 -4) (("1" (hide -2 -3) (("1" (inst 3 r!2 "p1!2 o p1!1" empty_seq) (("1" (assert) (("1" (prop) (("1" (hide -2 -3) (("1" (lemma seq_empty[posnat]) (("1" (inst?) (("1" (assert) (("1" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -1 2 3) (("2" (rewrite o_assoc) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 -5 rl) (("2" (replace -2 -5) (("2" (hide -2 -4) (("2" (inst 4 r!2 "p1!2 o p1!1" q1!3) (("2" (flatten) (("2" (hide 4) (("2" (prop) (("1" (rewrite o_assoc) nil nil) ("2" (lemma seq_empty[posnat]) (("2" (inst?) (("2" (assert) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil) ("3" (rewrite first_compo) (("3" (flatten) (("3" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "r!2 <= r!1") (("1" (expand <=) (("1" (skosimp) (("1" (replace -1 -5) (("1" (hide -1 -3 -4 -6) (("1" (inst 4 r!2 "p1!3 o p1!1" empty_seq) (("1" (assert) (("1" (prop) (("1" (lemma seq_empty[posnat]) (("1" (inst?) (("1" (assert) (("1" (rewrite empty_0) (("1" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite o_assoc) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "r!1 <= r!2") (("1" (expand <= -1) (("1" (skosimp) (("1" (replace -1 -2) (("1" (inst 5 r!1 p1!1 p1!3) (("1" (flatten) (("1" (hide 5) (("1" (prop) (("1" (expand <=) (("1" (inst 1 empty_seq) (("1" (replace -1 -2) (("1" (rewrite seq_o_empty) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 -3) (("2" (replace -3 -4) (("2" (hide -1 -2 -3 -5) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 r!1 "p1!3 o p1!2" q1!2) (("2" (rewrite o_assoc) (("2" (assert) (("2" (replace -1 -3 rl) (("2" (rewrite first_compo) (("2" (expand <=) (("2" (inst 3 empty_seq) (("2" (reveal -2) (("2" (flatten) (("2" (rewrite empty_0) (("2" (replaces -2) (("2" (rewrite seq_o_empty) (("2" (rewrite seq_o_empty) (("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 (-2 -3 1 2)) (("2" (expand <=) (("2" (replaces -1) (("2" (case "length(r!2) = length(r!1)") (("1" (lemma o_equals_o[posnat]) (("1" (inst?) (("1" (assert) (("1" (inst 1 empty_seq) (("1" (rewrite seq_o_empty) nil nil)) nil)) nil)) nil)) nil) ("2" (case " length(r!2) < length(r!1)") (("1" (lemma o_length_o[posnat]) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma o_length_o[posnat]) (("2" (inst -1 r!1 q1!2 r!2 p1!2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (case "r!1 <= r!2") (("1" (expand <=) (("1" (skosimp) (("1" (replace -1 -2) (("1" (inst 5 r!1 p1!1 "p1!3 o q1!3") (("1" (flatten) (("1" (hide 5) (("1" (prop) (("1" (rewrite o_assoc) nil nil) ("2" (lemma seq_empty[posnat]) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (rewrite empty_0 -2) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -1 -3) (("3" (replace -3 -5) (("3" (lemma equal_prefix[posnat]) (("3" (inst -1 r!1 "p1!3 o p1!2" q1!2) (("3" (rewrite o_assoc) (("3" (assert) (("3" (replace -1 -8 rl) (("3" (case "p1!3 = empty_seq") (("1" (replace -1) (("1" (rewrite empty_o_seq) (("1" (rewrite empty_o_seq) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite first_compo) (("1" (rewrite first_compo) (("1" (flatten) (("1" (rewrite empty_0) nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "r!2 <= r!1") (("1" (hide 1) (("1" (expand <=) (("1" (skosimp) (("1" (replace -1 -6) (("1" (inst 5 r!2 "p1!3 o p1!1" q1!3) (("1" (flatten) (("1" (hide 5) (("1" (prop) (("1" (rewrite o_assoc) nil nil) ("2" (lemma seq_empty[posnat]) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (rewrite empty_0 -2) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -1 -5) (("3" (replace -3 -5) (("3" (lemma equal_prefix[posnat]) (("3" (inst -1 r!2 p1!2 "p1!3 o q1!2") (("3" (rewrite o_assoc) (("3" (assert) (("3" (replace -1 -5) (("3" (case "p1!3 = empty_seq") (("1" (replace -1) (("1" (rewrite empty_o_seq) (("1" (rewrite empty_o_seq) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite first_compo) (("1" (rewrite first_compo) (("1" (flatten) (("1" (rewrite empty_0) nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -4 1 2)) (("2" (replaces -1) (("2" (expand <=) (("2" (case "length(r!2) = length(r!1)") (("1" (lemma o_equals_o[posnat]) (("1" (inst?) (("1" (assert) (("1" (inst 1 empty_seq) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case " length(r!2) < length(r!1)") (("1" (lemma o_length_o[posnat]) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma o_length_o[posnat]) (("2" (inst -1 r!1 q1!2 r!2 p1!2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((left_pos const-decl "bool" positions 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) (position type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (seq_empty formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (o_assoc formula-decl nil finite_sequences nil) (first_compo formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (equal_prefix formula-decl nil seq_extras "structures/") (seq_o_empty formula-decl nil seq_extras "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (o_equals_o formula-decl nil seq_extras "structures/") (o_length_o formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (<= const-decl "bool" positions nil) (empty_o_seq formula-decl nil seq_extras "structures/")) nil)) (lwc_is_left_pos 0 (lwc_is_left_pos-1 nil 3512738444 ("" (skosimp*) (("" (expand* "left_without_children" "left_pos") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((left_pos const-decl "bool" positions nil) (left_without_children const-decl "bool" positions 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) (position type-eq-decl nil positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (lwc_transitive 0 (lwc_transitive-1 nil 3512738520 ("" (skosimp) (("" (expand left_without_children) (("" (skosimp*) (("" (case "r!1 = r!2") (("1" (replaces -1) (("1" (inst 5 r!2 p1!1 q1!3) (("1" (assert) (("1" (lemma equal_prefix[posnat]) (("1" (inst -1 r!2 q1!2 p1!2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "child(r!2, r!1)") (("1" (expand child) (("1" (skosimp) (("1" (inst 7 r!1 p1!1 "p1!3 o q1!3") (("1" (rewrite o_assoc) (("1" (assert) (("1" (lemma equal_prefix[posnat]) (("1" (inst -1 r!1 q1!2 "p1!3 o p1!2") (("1" (rewrite o_assoc) (("1" (assert) (("1" (replace -1 -5) (("1" (rewrite first_compo) (("1" (rewrite first_compo) (("1" (assert) (("1" (flatten) (("1" (lemma seq_empty[posnat]) (("1" (inst -1 p1!3 q1!3) (("1" (assert) (("1" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (rewrite empty_0) 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) ("2" (case "child(r!1, r!2)") (("1" (expand child -1) (("1" (skosimp) (("1" (inst 8 r!2 "p1!3 o p1!1" q1!3) (("1" (rewrite o_assoc) (("1" (assert) (("1" (lemma equal_prefix[posnat]) (("1" (inst -1 r!2 "p1!3 o q1!2" p1!2) (("1" (rewrite o_assoc) (("1" (assert) (("1" (replace -1 -8 rl) (("1" (rewrite first_compo) (("1" (rewrite first_compo) (("1" (assert) (("1" (lemma seq_empty[posnat]) (("1" (inst -1 p1!3 p1!1) (("1" (assert) (("1" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (rewrite empty_0) 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) ("2" (hide-all-but (-1 -5 1 2 3 4 7)) (("2" (replaces -1) (("2" (case "length(r!1) < length(r!2)") (("1" (lemma o_length_o[posnat]) (("1" (inst -1 r!1 q1!2 r!2 p1!2) (("1" (assert) (("1" (skosimp) (("1" (expand child 2) (("1" (inst 2 seq!1) (("1" (assert) (("1" (flatten) (("1" (replaces -3) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "length(r!1) > length(r!2)") (("1" (lemma o_length_o[posnat]) (("1" (inst -1 r!2 p1!2 r!1 q1!2) (("1" (assert) (("1" (skosimp) (("1" (expand child 2) (("1" (inst 2 seq!1) (("1" (assert) (("1" (flatten) (("1" (replaces -3) (("1" (rewrite seq_o_empty) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma o_equals_o[posnat]) (("2" (inst -1 r!1 q1!2 r!2 p1!2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((left_without_children const-decl "bool" positions nil) (= const-decl "[T, T -> boolean]" equalities 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) (>= 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) (equal_prefix formula-decl nil seq_extras "structures/") (finseq type-eq-decl nil finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (o_equals_o formula-decl nil seq_extras "structures/") (o_length_o formula-decl nil seq_extras "structures/") (seq_o_empty formula-decl nil seq_extras "structures/") (< const-decl "bool" reals nil) (O const-decl "finseq" finite_sequences nil) (first_compo formula-decl nil seq_extras "structures/") (seq_empty formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (o_assoc formula-decl nil finite_sequences nil) (child const-decl "bool" positions nil)) shostak)) (subterm_if_le_arity 0 (subterm_if_le_arity-1 nil 3513100939 ("" (skosimp) (("" (expand positionsOF) (("" (lift-if) (("" (assert) (("" (prop) (("1" (assert) nil nil) ("2" (expand* union IUnion member only_empty_seq finseq_appl) (("2" (flatten) (("2" (expand* catenate member) (("2" (inst 3 i!1) (("2" (inst 3 empty_seq) (("2" (prop) (("1" (hide-all-but 1) (("1" (expand positionsOF) (("1" (lift-if) (("1" (expand* union member only_empty_seq) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite add_first_empty_seq) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IUnion const-decl "set[T]" indexed_sets nil) (only_empty_seq const-decl "positions" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (catenate const-decl "positions" positions nil) (empty_seq const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (add_first_empty_seq formula-decl nil seq_extras "structures/") (upto? nonempty-type-eq-decl nil IUnion_extra nil) (position type-eq-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) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-decl nil positions nil) (<= const-decl "bool" reals 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (subterms_acc_arity 0 (subterms_acc_arity-1 nil 3513101734 ("" (skosimp) (("" (expand positionsOF -1) (("" (lift-if) (("" (prop) (("1" (hide-all-but -2) (("1" (expand* only_empty_seq "#" empty_seq) nil nil)) nil) ("2" (hide-all-but -2) (("2" (expand* only_empty_seq "#" empty_seq) nil nil)) nil) ("3" (expand* union IUnion catenate member only_empty_seq finseq_appl) (("3" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (skosimp*) (("2" (lemma subterm_if_le_arity) (("2" (inst -1 j!1 s!1) (("2" (assert) (("2" (hide -1 4) (("2" (typepred i!2) (("2" (case "i!1 = i!2") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (expand* add_first insert? finseq_appl) (("2" (decompose-equality) (("2" (expand "#") (("2" (decompose-equality -2) (("2" (inst -1 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (only_empty_seq const-decl "positions" positions nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (subterm_if_le_arity formula-decl nil positions nil) (real_ge_is_total_order name-judgement "(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) (NOT const-decl "[bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (below type-eq-decl nil nat_types 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) (position type-eq-decl nil positions nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add_first const-decl "finseq" seq_extras "structures/") (insert? const-decl "finseq" seq_extras "structures/") (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (symbol formal-nonempty-type-decl nil positions nil) (variable formal-nonempty-type-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) (>= 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) (union const-decl "set" sets nil) (catenate const-decl "positions" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (member const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil)) nil)) (lwc_add_last_delete_TCC1 0 (lwc_add_last_delete_TCC1-1 nil 3513013796 ("" (skosimp) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) nil 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) (empty_0 formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (position type-eq-decl nil positions 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)) nil)) (lwc_add_last_delete_TCC2 0 (lwc_add_last_delete_TCC2-1 nil 3513013796 ("" (skosimp) (("" (hide -1) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) 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) (position type-eq-decl nil positions nil) (empty_0 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)) nil)) (lwc_add_last_delete 0 (lwc_add_last_delete-2 nil 3514047307 ("" (skosimp) (("" (assert) (("" (flatten) (("" (name-replace "pi" "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1))" :hide? nil) (("1" (expand left_without_children -2) (("1" (skosimp) (("1" (case "r!1 = delete(p!1, length(p!1) - 1)") (("1" (case "q1!2 = #(1 + last(p!1))") (("1" (case "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1)) = r!1 o q1!2") (("1" (assert) nil nil) ("2" (hide-all-but (-1 -2 1)) (("2" (replace -1) (("2" (replace -2) (("2" (hide -) (("2" (name-replace "q!1" "delete(p!1, length(p!1) - 1)") (("2" (expand o) (("2" (decompose-equality 1) (("1" (expand* add_last insert? "#") nil nil) ("2" (decompose-equality 1) (("1" (lemma nth_add_last[posnat]) (("1" (inst -1 "q!1" "1 + last(p!1)" "x!1") (("1" (expand finseq_appl) (("1" (lift-if 1) (("1" (split 1) (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (expand "#") (("1" (propax) nil nil)) nil) ("2" (typepred x!1) (("2" (hide -2 3) (("2" (expand* add_last insert?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred x!1) (("2" (expand* add_last insert?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand* add_last insert? "#") nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "first(q1!2) = 1 + last(p!1) AND length(q1!2) > 1") (("1" (flatten) (("1" (expand child) (("1" (lemma seq_first_rest_1[posnat]) (("1" (inst -1 q1!2) (("1" (assert) (("1" (replace -1 -6) (("1" (replace -4 -5 rl) (("1" (case "add_last(r!1, 1 + last(p!1)) = r!1 o #(1 + last(p!1))") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite o_assoc) (("1" (replace -2 -6) (("1" (replace -5 -6) (("1" (inst 6 "rest(q1!2)") (("1" (assert) (("1" (flatten) (("1" (hide-all-but (-1 -3 -9 3)) (("1" (lemma empty_0[posnat]) (("1" (inst -1 "rest(q1!2)") (("1" (assert) (("1" (expand* o "#") (("1" (decompose-equality -2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (expand o) (("2" (decompose-equality 1) (("1" (expand* add_last insert? "#") nil nil) ("2" (decompose-equality 1) (("1" (lemma nth_add_last[posnat]) (("1" (expand finseq_appl) (("1" (lift-if) (("1" (prop) (("1" (inst -2 r!1 "1 + last(p!1)" x!1) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (typepred x!1) (("2" (expand add_last -1) (("2" (expand insert? -1) (("2" (inst -2 r!1 "1 + last(p!1)" x!1) (("2" (assert) (("2" (expand "#") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand* add_last insert? "#") nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (case "last(p!1) = first(p1!1)") (("1" (replace -1 1) (("1" (expand left_without_children 6) (("1" (rewrite add_last_is_o) (("1" (replace -2 -3 rl) (("1" (inst 6 r!1 "#(1 + last(p!1))" q1!2) (("1" (assert) (("1" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (replace -1) (("2" (expand first 1 1) (("2" (expand finseq_appl) (("2" (expand "#" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 1 4 6)) (("2" (replace -1) (("2" (hide -1) (("2" (lemma add_last_delete[posnat]) (("2" (inst -1 p!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) (("2" (rewrite add_last_is_o) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 "delete(p!1, p!1`length - 1)" "#(last(p!1))" "p1!1") (("2" (assert) (("2" (hide -2 -3) (("2" (expand* last first "#" finseq_appl) (("2" (decompose-equality -1) (("2" (decompose-equality -2) (("2" (inst -1 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite add_last_is_o) (("2" (case "q1!2 = #(1 + last(p!1))") (("1" (propax) nil nil) ("2" (replace -1 -2 rl) (("2" (case "first(p1!1) = last(p!1)") (("1" (expand left_without_children) (("1" (inst 7 r!1 "#(1 + last(p!1))" q1!2) (("1" (assert) (("1" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (case "first(q1!2) = 1 + last(p!1)") (("1" (case "q1!2 = #(1 + last(p!1))") (("1" (propax) nil nil) ("2" (hide-all-but (-1 1 4 6 7)) (("2" (expand* first last "#" finseq_appl) (("2" (decompose-equality 1) (("1" (lemma empty_0[posnat]) (("1" (inst -1 q1!2) (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("1" (skosimp) (("1" (lemma empty_0[posnat]) (("1" (inst -1 q1!2) (("1" (assert) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma empty_0[posnat]) (("3" (inst -1 p!1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (replace -1 2 rl) (("2" (expand first 2 1) (("2" (expand finseq_appl) (("2" (expand "#" 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 1 5 7)) (("2" (replace -1) (("2" (hide -1) (("2" (lemma add_last_delete[posnat]) (("2" (inst -1 p!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) (("2" (rewrite add_last_is_o) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 "delete(p!1, p!1`length - 1)" "#(last(p!1))" "p1!1") (("2" (assert) (("2" (hide -2 -3) (("2" (expand* last first "#" finseq_appl) (("2" (decompose-equality -1) (("2" (decompose-equality -2) (("2" (inst -1 0) (("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" (name-replace "dp" "delete(p!1, length(p!1) - 1)" :hide? nil) (("2" (rewrite add_last_is_o) (("2" (case "child(dp, r!1)") (("1" (expand child -1) (("1" (skosimp) (("1" (replace -1 -3) (("1" (case "first(p1!1) = first(p1!2)") (("1" (expand left_without_children) (("1" (inst 6 r!1 "p1!2 o #(1 + last(p!1))" q1!2) (("1" (rewrite o_assoc) (("1" (assert) (("1" (rewrite first_compo) (("1" (assert) (("1" (hide-all-but (1 6)) (("1" (flatten) (("1" (lemma seq_empty[posnat]) (("1" (inst -1 p1!2 "#(1 + last(p!1))") (("1" (assert) (("1" (flatten) (("1" (rewrite empty_0 -1) nil nil)) 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) ("2" (hide-all-but (-1 -2 -3 -5 1 2 4 6)) (("2" (lemma add_last_delete[posnat]) (("2" (inst -1 p!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) (("2" (rewrite add_last_is_o) (("2" (replace -3) (("2" (replace -2 -1) (("2" (replace -1 -5) (("2" (hide-all-but (-5 2 3 5)) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 r!1 "p1!2 o #(last(p!1))" p1!1) (("2" (rewrite o_assoc) (("2" (assert) (("2" (hide -2) (("2" (replace -1 1 rl) (("2" (rewrite first_compo) (("2" (hide -1 2 4) (("2" (flatten) (("2" (rewrite empty_0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) ("2" (lemma add_last_delete[posnat]) (("2" (inst -1 p!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) (("2" (replace -2) (("2" (rewrite add_last_is_o) (("2" (replace -1 -5) (("2" (lemma o_length_o[posnat]) (("2" (inst -1 "r!1" "p1!1" "dp" "#(last(p!1))") (("2" (assert) (("2" (split) (("1" (skosimp) (("1" (expand child 2) (("1" (inst 2 seq!1) (("1" (assert) (("1" (hide-all-but (-1 2 3)) (("1" (flatten) (("1" (replace -2) (("1" (hide -2) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma o_equals_o[posnat]) (("2" (inst -1 "r!1" "p1!1" "dp" "#(last(p!1))") (("2" (assert) (("2" (lemma o_length_o[posnat]) (("2" (inst -1 "dp" "#(last(p!1))" "r!1" "p1!1") (("2" (assert) (("2" (skosimp) (("2" (replace -1 -6) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 dp "#(last(p!1))" "seq!1 o p1!1") (("2" (rewrite o_assoc) (("2" (assert) (("2" (case "seq!1 = empty_seq") (("1" (hide-all-but (-1 -3 5)) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite seq_o_empty) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 4 7 9)) (("2" (expand* "#" o) (("2" (flatten) (("2" (hide -2) (("2" (lemma empty_0[posnat]) (("2" (inst-cp -1 seq!1) (("2" (inst -1 p1!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 2)) (("3" (lemma empty_0[posnat]) (("3" (inst -1 p!1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (add_last const-decl "finseq" seq_extras "structures/") (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (position type-eq-decl nil positions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" 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/") (last const-decl "T" seq_extras "structures/") (seq_empty formula-decl nil seq_extras "structures/") (first_compo formula-decl nil seq_extras "structures/") (seq_o_empty formula-decl nil seq_extras "structures/") (o_equals_o formula-decl nil seq_extras "structures/") (o_length_o formula-decl nil seq_extras "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (p!1 skolem-const-decl "position" positions nil) (q!1 skolem-const-decl "finseq[posnat]" positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (insert? const-decl "finseq" seq_extras "structures/") (nth_add_last formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (x!1 skolem-const-decl "below[add_last(q!1, 1 + last(p!1))`length]" positions nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "finseq" finite_sequences nil) (equal_prefix formula-decl nil seq_extras "structures/") (add_last_delete formula-decl nil seq_extras "structures/") (add_last_is_o formula-decl nil seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (q1!2 skolem-const-decl "position" positions nil) (seq_first_rest_1 formula-decl nil seq_extras "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (r!1 skolem-const-decl "position" positions nil) (x!1 skolem-const-decl "below[add_last(r!1, 1 + last(p!1))`length]" positions nil) (rest const-decl "finseq" seq_extras "structures/") (o_assoc formula-decl nil finite_sequences nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (empty_0 formula-decl nil seq_extras "structures/") (child const-decl "bool" positions nil) (first const-decl "T" seq_extras "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (left_without_children const-decl "bool" positions nil)) nil) (lwc_add_last_delete-1 nil 3513524398 ("" (skosimp) (("" (assert) (("" (flatten) (("" (name-replace "pi" "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1))" :hide? nil) (("1" (expand left_without_children -2) (("1" (skosimp) (("1" (case "r!1 = delete(p!1, length(p!1) - 1)") (("1" (case "q1!2 = #(1 + last(p!1))") (("1" (case "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1)) = r!1 o q1!2") (("1" (assert) nil nil) ("2" (hide-all-but (-1 -2 1)) (("2" (replaces -1) (("2" (replaces -1) (("2" (name-replace "q!1" "delete(p!1, length(p!1) - 1)") (("2" (expand o) (("2" (decompose-equality 1) (("1" (expand* add_last insert? "#") nil nil) ("2" (decompose-equality 1) (("1" (lemma nth_add_last[posnat]) (("1" (inst -1 "q!1" "1 + last(p!1)" "x!1") (("1" (expand finseq_appl) (("1" (lift-if 1) (("1" (split 1) (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (expand "#") (("1" (propax) nil nil)) nil) ("2" (typepred x!1) (("2" (hide -2 3) (("2" (expand* add_last insert?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred x!1) (("2" (expand* add_last insert?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand* add_last insert? "#") nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "first(q1!2) = 1 + last(p!1)") (("1" (expand child) (("1" (lemma seq_first_rest_1[posnat]) (("1" (inst -1 q1!2) (("1" (lemma empty_0[posnat]) (("1" (inst -1 q1!2) (("1" (assert) (("1" (replace -1 -5) (("1" (replace -3 -4 rl) (("1" (case "add_last(r!1, 1 + last(p!1)) = r!1 o #(1 + last(p!1))") (("1" (replaces -1) (("1" (rewrite o_assoc) (("1" (replace -2 -5) (("1" (replace -4 -5) (("1" (inst 7 "rest(q1!2)") (("1" (assert) (("1" (flatten) (("1" (hide-all-but (-8 1 4)) (("1" (expand rest) (("1" (expand "^") (("1" (lift-if) (("1" (prop) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) nil shostak)) (lwc_add_last_delete1_TCC1 0 (lwc_add_last_delete1_TCC1-1 nil 3514218201 ("" (skosimp) (("" (assert) (("" (lemma empty_0[posnat]) (("" (inst -1 p!1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (empty_seq const-decl "finseq" finite_sequences nil) (empty_0 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)) nil)) (lwc_add_last_delete1_TCC2 0 (lwc_add_last_delete1_TCC2-1 nil 3514218201 ("" (skosimp) (("" (rewrite empty_0) 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) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (empty_seq const-decl "finseq" finite_sequences 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)) nil)) (lwc_add_last_delete1 0 (lwc_add_last_delete1-1 nil 3515010779 ("" (skosimp) (("" (assert) (("" (flatten) (("" (name-replace "pi" "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1))" :hide? nil) (("1" (expand left_without_children -2) (("1" (skosimp) (("1" (name-replace "dp" "delete(p!1, length(p!1) - 1)" :hide? nil) (("1" (rewrite add_last_is_o) (("1" (lemma add_last_delete[posnat]) (("1" (inst -1 p!1) (("1" (lemma empty_0[posnat]) (("1" (inst -1 p!1) (("1" (assert) (("1" (replace -2) (("1" (rewrite add_last_is_o) (("1" (case "r!1 = dp") (("1" (case "first(p1!1) = last(p!1)") (("1" (hide 4) (("1" (expand child 4) (("1" (inst 4 "rest(p1!1)") (("1" (prop) (("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 -2) (("1" (rewrite seq_o_empty) (("1" (hide-all-but (-1 -3 -4 -5 -9 5)) (("1" (replaces -2) (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (replaces -1) (("1" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3 1) (("2" (replace -1 1 rl) (("2" (replace -7 1) (("2" (replace -2 1) (("2" (hide-all-but (1 4)) (("2" (lemma seq_first_rest_1[posnat]) (("2" (inst -1 p1!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p1!1) (("2" (assert) (("2" (hide 1 3) (("2" (lemma o_assoc[posnat]) (("2" (inst -1 "dp" "#(first(p1!1))" "rest(p1!1)") (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (replace -1 1 rl) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand left_without_children) (("2" (inst 5 dp p1!1 "#(last(p!1))") (("2" (assert) (("2" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (case "first(q1!2) = 1 + last(p!1)") (("1" (expand first 1 2) (("1" (expand finseq_appl) (("1" (expand "#" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 -5 1 5)) (("2" (replaces -1) (("2" (replaces -2) (("2" (lemma equal_prefix[posnat]) (("2" (inst -1 dp "#(1 + last(p!1))" q1!2) (("2" (assert) (("2" (hide -2) (("2" (expand "#") (("2" (decompose-equality -1) (("2" (decompose-equality -2) (("2" (expand* first finseq_appl) (("2" (inst -1 0) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "length(r!1) < length(dp)") (("1" (replace -5 -4) (("1" (lemma o_length_o[posnat]) (("1" (inst -1 r!1 q1!2 dp "#(1 + last(p!1))") (("1" (assert) (("1" (skosimp) (("1" (replace -1 -3) (("1" (expand left_without_children) (("1" (inst 5 r!1 p1!1 "seq!1 o #(last(p!1))") (("1" (rewrite o_assoc) (("1" (assert) (("1" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" o empty_seq) (("1" (flatten) (("1" (hide -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite first_compo) (("1" (replace -1 -5) (("1" (lemma equal_prefix[posnat]) (("1" (inst -1 r!1 "seq!1 o #(1 + last(p!1))" q1!2) (("1" (rewrite o_assoc) (("1" (assert) (("1" (replace -1 -9 rl) (("1" (rewrite first_compo) (("1" (hide-all-but (-2 1 3)) (("1" (flatten) (("1" (rewrite empty_0) (("1" (replaces -1) (("1" (rewrite seq_o_empty) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 3)) (("2" (flatten) (("2" (rewrite empty_0) (("2" (replaces -1) (("2" (rewrite seq_o_empty) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma o_equals_o[posnat]) (("2" (inst -1 dp "#(1 + last(p!1))" r!1 q1!2) (("2" (assert) (("2" (hide-all-but (-3 -4 1 2 5)) (("2" (replaces -2) (("2" (expand* "#" o) (("2" (flatten) (("2" (hide -2) (("2" (lemma empty_0[posnat]) (("2" (inst -1 q1!2) (("2" (assert) 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) (("2" (typepred p!1) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred p!1) (("2" (hide-all-but (-1 1)) (("2" (lemma empty_0[posnat]) (("2" (inst -1 p!1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (add_last const-decl "finseq" seq_extras "structures/") (< const-decl "bool" reals nil) (delete const-decl "finseq" seq_extras "structures/") (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (empty_seq const-decl "finseq" finite_sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (not_empty_seq type-eq-decl nil seq_extras "structures/") (last const-decl "T" seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (add_last_is_o formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (equal_prefix formula-decl nil seq_extras "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (rest const-decl "finseq" seq_extras "structures/") (o_assoc formula-decl nil finite_sequences nil) (seq_first_rest_1 formula-decl nil seq_extras "structures/") (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (seq_o_empty formula-decl nil seq_extras "structures/") (child const-decl "bool" positions nil) (first const-decl "T" seq_extras "structures/") (o_equals_o formula-decl nil seq_extras "structures/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (first_compo formula-decl nil seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (o_length_o formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_0 formula-decl nil seq_extras "structures/") (add_last_delete formula-decl nil seq_extras "structures/") (left_without_children const-decl "bool" positions nil)) shostak)) (leftmost_pos 0 (leftmost_pos-1 nil 3514292411 ("" (skosimp) (("" (expand positionsOF -2) (("" (lift-if) (("" (ground) (("1" (hide-all-but (-2 2)) (("1" (expand only_empty_seq) (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but (-2 3)) (("2" (expand only_empty_seq) (("2" (propax) nil nil)) nil)) nil) ("3" (expand* union IUnion catenate only_empty_seq member finseq_appl) (("3" (skosimp*) (("3" (typepred i!2) (("3" (rewrite add_first_is_o) (("3" (case "i!2 = i!1") (("1" (case "x!1 = empty_seq") (("1" (hide-all-but (-1 -2 -6 6)) (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite seq_o_empty) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (hide-all-but (-4 1 6)) (("2" (expand left_pos) (("2" (inst 2 "#(i!1)" x!1 empty_seq) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand left_pos) (("2" (inst 6 empty_seq "#(i!2) o x!1" "#(i!1)") (("2" (flatten) (("2" (hide 6) (("2" (rewrite empty_o_seq) (("2" (rewrite empty_o_seq) (("2" (assert) (("2" (prop) (("1" (hide-all-but -1) (("1" (expand* "#" empty_seq) nil nil)) nil) ("2" (rewrite first_compo) (("1" (hide-all-but (-1 -2 1 2 5)) (("1" (expand "#" 1) (("1" (expand* first finseq_appl) (("1" (lemma positions_of_arg) (("1" (inst -1 "s!1" "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "#") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((positionsOF def-decl "positions" positions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (only_empty_seq const-decl "positions" positions nil) (finseq type-eq-decl nil finite_sequences nil) (add_first_is_o formula-decl nil seq_extras "structures/") (empty_o_seq formula-decl nil seq_extras "structures/") (int_minus_int_is_int application-judgement "int" integers nil) (real_le_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) (first_compo formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions_of_arg formula-decl nil positions nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" positions nil) (i!1 skolem-const-decl "posnat" positions nil) (< const-decl "bool" reals nil) (first const-decl "T" seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (seq_o_empty formula-decl nil seq_extras "structures/") (left_pos const-decl "bool" positions 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (variable formal-nonempty-type-decl nil positions nil) (symbol formal-nonempty-type-decl nil positions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" positions nil) (term type-decl nil term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (below type-eq-decl nil nat_types 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) (position type-eq-decl nil positions nil) (upto? nonempty-type-eq-decl nil IUnion_extra nil) (union const-decl "set" 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) (IUnion const-decl "set[T]" indexed_sets nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.223Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26