Quelle positions.prf
Sprache: Lisp
(positionsnil 3388744728 ("" (subtype-tcc) nil nil ) nil nil ))nil 3389723936 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil nat_types nil )nil positions nil )nil positions nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"[symbol -> nat]" positions nil )nil term_adt nil )nil finite_sequences nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_well_founded?[term])" term_adt nil )"boolean" term_adt nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil IUnion_extra nil )nil positions nil )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3511797058"" (skosimp) (("" (rewrite empty_0) nil nil )) nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3511797058"" (skosimp) (("" (rewrite empty_0) nil nil )) nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3415310384"" (induct "t" )"1" (skosimp*)"1" (expand * "positionsOF" "only_empty_seq" )"1" "{x: position | x = empty_seq} = singleton(empty_seq)" "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" "{x: position | x = empty_seq} = singleton(empty_seq)" "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" "1" "1" "LAMBDA (x: (catenate(i!1, positionsOF(app2_var!1`seq(i!1 - 1))))): f!1(rest(x))" )"1" expand "injective?" )"1" "1" expand "catenate" )"1" "1" expand "member" )"1" "1" "1" rewrite "rest_add_first" )"1" rewrite "rest_add_first" )"1" "x!1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "catenate" )"2" "2" expand "member" )"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" "{x: position | x = empty_seq} = singleton(empty_seq)" "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" integers nil )nil finite_sets nil )"bool" reals nil )nil finite_sequences nil )nil IUnion_extra nil )"set[T]" indexed_sets nil )"positions" positions nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{args: finite_sequence[term[variable, symbol, arity]] | " positions nil) "symbol" positions nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"upto?[position](length(app2_var!1))" nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"bool" sets nil )"bool" functions nil )nil IUnion_extra nil )nil finite_sets nil )"(singleton?)" sets nil )"bool" sets nil )"finseq" finite_sequences nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"non_empty_finite_set[position]" positions nil )nil finite_sets nil )"positions" positions nil )nil term_adt nil )nil positions nil )nil positions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" positions nil )"positions" positions nil )nil positions nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil ))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 )"bool" positions nil )"bool" reals nil )"nonneg_int" nil )"bool" booleans nil )nil defined_types nil )"T" epsilons nil )"bool" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil ))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" "p1" )"2" "rest(p)" "args(t)(i1 - 1)" )"2" "1" "i1" )"1" expand "catenate" )"1" "rest(p)" )"1" expand "member" )"1" assert )"1" "1" "fsepn.seq_first_rest" )"1" "p" )"1" "1" "1" "fsepn.add_first_compo" )"1" "rest(p)" "p1" "first(p)" )"1" "1" "1" "fsepn.first_equal" )"1" "1" assert )"1" "1" "1" "fsepn.seq_first_rest" )"1" "p" )"1" assert )"1" "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" "2" expand "<=" )"2" "p1" )"2" "fsepn.seq_first_rest" )"2" "p" )"2" "1" "1" rewrite "fsepn.add_first_compo" )"1" "1" "fsepn.first_equal" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"(strict_total_order?[real])" real_props nil )nil finite_sequences nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[term -> boolean]" term_adt nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil IUnion_extra nil )"int" integers nil )"(total_order?[real])" nil )nil positions nil )"positions" positions nil )"bool" positions nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3496152694"" (skosimp*) (("" (grind) nil nil )) nil ) nil shostak))nil 3388757591 ("" (skeep) (("" (grind) nil nil )) nil )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"positions" positions nil )"finseq" finite_sequences nil )"positions" positions nil )"posint" nil ))nil 3496151134 ("" (skosimp) (("" (grind) nil nil )) nil )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"positions" positions nil )"finseq" finite_sequences nil )"positions" positions nil )"posint" nil ))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 )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )"finseq" finite_sequences nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )"bool" positions nil )nil positions nil ))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" "2" expand "member" )"2" expand "finseq_appl" )"2" replace -3 -2)"2" "fsepn.first_equal" )"2" "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 )nil positions nil )"int" integers nil )"(total_order?[real])" nil )"positions" positions nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )nil IUnion_extra nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"bool" reals nil )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"positions" positions nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )nil numbers nil )nil booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil nat_types nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )"position" positions nil ))nil ))nil 3411856776"" (skosimp*)"" (expand "positionsOF" ) (("" (grind) nil nil )) nil )) nil )"positions" positions nil )"finseq" finite_sequences nil )"positions" positions nil ))nil ))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" "2" assert )"2" "2" "fsepn.first_equal" )"2" "2" assert )"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 ))nil )"positions" positions nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"positions" positions nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )nil seq_extras "structures/" )"int" integers nil )nil seq_extras "structures/" )nil IUnion_extra nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )"bool" reals nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" ))nil 3495982353 ("" (subtype-tcc) nil nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))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 )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil seq_extras "structures/" )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"bool" reals nil )"finseq" seq_extras "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil positions nil )nil positions nil )"[symbol -> nat]" positions nil )nil term_adt nil )nil positions nil )nil seq_extras "structures/" )nil positions nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil ))nil 3394367640"" (skeep)"" (expand * "parallel" "<=" ) (("" (prop) nil nil )) nil )) nil )"bool" positions nil )"bool" positions nil ))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" "p1!1" )"1" "1" "1" "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" "p1!1" )"2" "p1!1" )"2" "2" "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 )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )"bool" positions nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"bool" positions nil ))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" "2" "j!1" )"2" (grind) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "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 )nil seq_extras "structures/" )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[below[length(fs)] -> T]" finite_sequencesnil )"below[length(rest(fss!1))]" positions nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"PP" positions nil )"below[length(rest(fss!1))]" positions nil )"posint" nil )"int" integers nil )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"term[variable, symbol, arity]" positionsnil )"SP(s!1)" positions nil )"below[length(rest(fss!1))]" positions nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"posint" nil )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil positions nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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" "j!1" )"2" "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" "2" "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" "2" "j!1" )"2" (grind) nil nil ))nil ))nil )"3" "3" "i!2" )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil nat_types nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"below[length(delete(fss, i!1))]" positionsnil )"posint" nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"PP" positions nil )"below[length(fss)]" positions nil )"below[length(delete(fss, i!1))]" positionsnil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil ))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 )nil positions nil )"bool" positions nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil nat_types nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"below[length(delete(fss, i!1))]" positionsnil )"below[length(fss)]" positions nil )"SP(s)" positions nil )"term[variable, symbol, arity]" positions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil ))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" "1" rewrite "parallel_comm" )nil nil ))nil ))nil )"2" (hide-all-but 1)"2" "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" "2" "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" "fss!1" "q!1" "i!1" )"1" "fspos.nth_add_first" )"1" "fss!1" "q!1" "j!1" )"1" (assert ) nil nil )"2" "2" "j!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" "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 )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"below[length(add_first(q!1, fss!1))]" nil )"(total_order?[real])" nil )"int" integers nil )"below[length(add_first(q!1, fss!1))]" nil )"PP" positions nil )"position" positions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil positions nil )nil seq_extras "structures/" )"bool" reals nil ) (PP type-eq-decl nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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 )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"positions?(s!1)" positions nil )"below[length(add_first(q!1, fss!1))]" nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"term[variable, symbol, arity]" positionsnil )"SP(s!1)" positions nil )nil seq_extras "structures/" )"bool" reals nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil positions nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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" "1" rewrite "parallel_comm" )nil nil ))nil ))nil )"2" (hide-all-but 1)"2" "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" "2" "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" "fss!1" "q!1" "i!1" )"1" assert )"1" "fspos.nth_add_last" )"1" "fss!1" "q!1" "j!1" )"1" (assert ) nil nil )"2" "2" "j!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "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 )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"below[length(add_last(fss!1, q!1))]" nil )"below[length(add_last(fss!1, q!1))]" nil )"position" positions nil )"PP" positions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil positions nil )nil seq_extras "structures/" )"bool" reals nil ) (PP type-eq-decl nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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 )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"term[variable, symbol, arity]" positionsnil )"SP(s!1)" positions nil )"positions?(s!1)" positions nil )"below[length(add_last(fss!1, q!1))]" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil seq_extras "structures/" )"bool" reals nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil positions nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))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 )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil positions nil )nil positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set[T]" indexed_sets nil )"bool" sets nil )"set" sets nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )nil finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"positions" positions nil )"positions" positions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil IUnion_extra nil )nil positions nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posint" nil )"(total_order?[real])" nil )"finite_sequence[T]" set2seq "structures/" )"positions" positions nil ))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" "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" "2" "2" "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" "2" "2" "2" rewrite "2" "2" rewrite "2" rewrite "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" "2" (rewrite empty_0 -2) nil nil ))nil ))nil ))nil ))nil )"3" (replace -1 -3)"3" (replace -3 -5)"3" "3" "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" "1" rewrite empty_0)nil nil ))nil ))nil )"2" "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" "2" "2" assert )"2" "2" rewrite empty_0 -2)nil nil ))nil ))nil ))nil ))nil )"3" replace -1 -5)"3" replace -3 -5)"3" "3" "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 "1" assert )nil nil ))nil ))nil ))nil )"2" rewrite first_compo)"1" rewrite first_compo)"1" "1" rewrite empty_0)nil nil ))nil ))nil )"2" "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 )"bool" positions nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil finite_sequences nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"[T, T -> boolean]" equalities nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"bool" reals nil )"bool" positions nil )nil seq_extras "structures/" ))nil ))nil 3512738444"" (skosimp*)"" (expand * "left_without_children" "left_pos" )"" (skosimp*)"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" positions nil )"bool" positions nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )"(strict_total_order?[real])" real_props nil ))nil ))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" "1" "1" "1" assert )"1" rewrite empty_0)nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil ))nil )"2" "2" "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" "1" "1" assert )"1" rewrite empty_0)nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil ))nil )"2" "2" "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" "1" assert )"1" "1" "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" "1" assert )"1" "1" "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 )"bool" positions nil )"[T, T -> boolean]" equalities nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )nil seq_extras "structures/" )nil finite_sequences nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"bool" reals nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )"bool" positions nil ))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 )"positions" positions nil )"(total_order?[real])" nil )"set[T]" indexed_sets nil )"positions" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" sets nil )"set" sets nil )"positions" positions nil )"finseq" finite_sequences nil )nil finite_sequences nil )nil seq_extras "structures/" )nil IUnion_extra nil )nil positions nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil nat_types nil )"[term -> boolean]" term_adt nil )nil term_adt nil )"[symbol -> nat]" positions nil )nil naturalnumbers nil )nil positions nil )nil positions nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil ))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"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" "2" expand "#" )"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 )"positions" positions nil )"positions" positions nil )"finite_sequence[T]" set2seq "structures/" )"finseq" finite_sequences nil )nil positions nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[term -> boolean]" term_adt nil )nil nat_types nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil positions nil )nil IUnion_extra nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil term_adt nil )"[symbol -> nat]" positions nil )nil naturalnumbers nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"set" sets nil )"positions" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" sets nil )"set[T]" indexed_sets nil ))nil ))nil 3513013796"" (skosimp)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil seq_extras "structures/" )"int" integers nil )"(total_order?[real])" nil )nil positions nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil ))nil ))nil 3513013796"" (skosimp)"" (hide -1)"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )nil seq_extras "structures/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3514047307"" (skosimp)"" (assert )"" (flatten)"" "pi" "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1))" 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" "q!1" "delete(p!1, length(p!1) - 1)" )"2" expand o)"2" "1" expand * add_last insert? "#" )nil nil )"2" "1" "1" "q!1" "1 + last(p!1)" "x!1" )"1" expand finseq_appl)"1" "1" "1" "1" assert )nil nil ))nil )"2" "1" expand "#" )"1" nil nil ))nil )"2" "2" "2" expand *"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand *nil nil ))nil ))nil ))nil ))nil )"2" "2" expand * add_last insert? "#" )nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" "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" "1" rewrite o_assoc)"1" replace -2 -6)"1" replace -5 -6)"1" "rest(q1!2)" )"1" assert )"1" "1" "1" "1" "rest(q1!2)" )"1" assert )"1" expand *"#" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand o)"2" "1" expand *"#" )nil nil )"2" "1" "1" expand finseq_appl)"1" "1" "1" "1 + last(p!1)" "1" assert )nil nil )"2" assert )nil nil ))nil )"2" "2" expand "2" expand "2" "1 + last(p!1)" "2" assert )"2" expand "#" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"#" )nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" "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" "#(1 + last(p!1))" q1!2)"1" assert )"1" "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" "2" "2" "2" "2" assert )"2" rewrite add_last_is_o)"2" "2" "delete(p!1, p!1`length - 1)" "#(last(p!1))" "p1!1" )"2" assert )"2" "2" expand *"#" "2" "2" "2" 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" "#(1 + last(p!1))" q1!2)"1" assert )"1" "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" "2" expand *"#" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "1" "1" "1" "1" assert )"1" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" "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" "2" replace -1)"2" "2" "2" "2" "2" "2" assert )"2" rewrite add_last_is_o)"2" "2" "delete(p!1, p!1`length - 1)" "#(last(p!1))" "p1!1" )"2" assert )"2" "2" expand *"#" "2" "2" "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 ))nil ))nil ))nil ))nil )"2" "dp" "delete(p!1, length(p!1) - 1)" 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" "p1!2 o #(1 + last(p!1))" "1" rewrite o_assoc)"1" assert )"1" rewrite first_compo)"1" assert )"1" "1" "1" "1" "#(1 + last(p!1))" )"1" assert )"1" "1" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite empty_0)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" "2" assert )"2" rewrite add_last_is_o)"2" replace -3)"2" replace -2 -1)"2" replace -1 -5)"2" "2" "2" "p1!2 o #(last(p!1))" "2" rewrite "2" assert )"2" "2" replace "2" rewrite "2" "2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "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" "2" "r!1" "p1!1" "dp" "#(last(p!1))" )"2" assert )"2" "1" "1" expand child 2)"1" "1" assert )"1" "1" "1" replace "1" "1" rewrite "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "r!1" "p1!1" "dp" "#(last(p!1))" )"2" assert )"2" "2" "dp" "#(last(p!1))" "r!1" "p1!1" )"2" assert )"2" "2" replace "2" "2" "#(last(p!1))" "seq!1 o p1!1" )"2" rewrite "2" assert )"2" case "seq!1 = empty_seq" )"1" "1" replace "1" "1" rewrite nil nil ))nil ))nil ))nil )"2" "2" expand *"#" "2" "2" "2" "2" "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 ))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" nil )"int" integers nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"bool" reals nil )"finseq" seq_extras "structures/" )nil positions nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )"nonneg_int" nil )"position" positions nil )"finseq[posnat]" positions nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"below[add_last(q!1, 1 + last(p!1))`length]" nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"finseq" finite_sequences nil )"position" positions nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"position" positions nil )"below[add_last(r!1, 1 + last(p!1))`length]" nil )"finseq" seq_extras "structures/" )nil finite_sequences nil )"odd_int" integers nil )nil seq_extras "structures/" )"bool" positions nil )"T" seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" positions nil ))nil )nil 3513524398"" (skosimp)"" (assert )"" (flatten)"" "pi" "add_last(delete(p!1, length(p!1) - 1), 1 + last(p!1))" 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" "q!1" "delete(p!1, length(p!1) - 1)" )"2" (expand o)"2" "1" expand * add_last insert? "#" )nil nil )"2" "1" "1" "q!1" "1 + last(p!1)" "x!1" )"1" expand finseq_appl)"1" "1" "1" "1" (assert ) nil nil ))nil )"2" "1" expand "#" )"1" nil nil ))nil )"2" "2" "2" expand *"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand * add_last insert?)nil nil ))nil ))nil ))nil ))nil )"2" "2" expand * add_last insert? "#" )nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" "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" "1" rewrite o_assoc)"1" replace -2 -5)"1" replace -4 -5)"1" "rest(q1!2)" )"1" assert )"1" "1" "1" expand rest)"1" expand "^" )"1" "1" "1" nil nil )"2" nil nil )"3" 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))nil 3514218201"" (skosimp)"" (assert )"" (lemma empty_0[posnat])"" (inst -1 p!1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"int" integers nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )"boolean" notequal nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3514218201"" (skosimp) (("" (rewrite empty_0) nil nil )) nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil positions nil )"boolean" notequal nil )"finseq" finite_sequences nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil ))nil ))nil 3515010779"" (skosimp)"" (assert )"" (flatten)"" "pi" "add_last(delete(p!1, length(p!1) - 1), " :hide? nil) "1" (expand left_without_children -2)"1" (skosimp)"1" "dp" "delete(p!1, length(p!1) - 1)" 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" "1" expand child 4)"1" "rest(p1!1)" )"1" "1" "1" "1" "1" "1" assert )"1" replace -2)"1" rewrite "1" "1" "1" replace "1" "1" "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" "2" "2" "2" "2" "2" assert )"2" "2" "2" "dp" "#(first(p1!1))" "rest(p1!1)" )"2" replace "2" "2" replace "2" 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" "#(last(p!1))" )"2" assert )"2" "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" "2" "2" "2" "2" "#(1 + last(p!1))" "2" assert )"2" "2" expand "#" )"2" "2" "2" expand *"2" "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" "1" "#(1 + last(p!1))" )"1" assert )"1" "1" replace -1 -3)"1" expand "1" "seq!1 o #(last(p!1))" )"1" rewrite o_assoc)"1" assert )"1" "1" "1" expand *"#" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "1" replace "1" "1" "seq!1 o #(1 + last(p!1))" "1" rewrite "1" assert )"1" replace "1" rewrite "1" "1" "1" rewrite "1" "1" rewrite "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "2" "2" rewrite "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "#(1 + last(p!1))" "2" assert )"2" "2" "2" expand * "#" o)"2" "2" "2" "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" nil )"int" integers nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil nat_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"finseq" seq_extras "structures/" )"bool" reals nil )"finseq" seq_extras "structures/" )nil positions nil )"boolean" notequal nil )"finseq" finite_sequences nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )NOT const-decl "[bool -> bool]" booleans nil )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )"posint" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"finseq" seq_extras "structures/" )nil finite_sequences nil )nil seq_extras "structures/" )"finite_sequence[T]" set2seq "structures/" )nil finite_sequences nil )nil seq_extras "structures/" )"bool" positions nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"nonneg_int" nil )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"bool" positions nil ))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"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" "1" "1" expand * "#" empty_seq)nil nil ))nil )"2" rewrite first_compo)"1" "1" expand "#" 1)"1" expand * first finseq_appl)"1" "1" "s!1" "i!1" )"1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"positions" positions nil )"posint" nil )"positions" positions nil )nil finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil positions nil )"term[variable, symbol, arity]" positionsnil )"posnat" positions nil )"bool" reals nil )"T" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil seq_extras "structures/" )"bool" positions nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )nil positions nil )nil positions nil )nil naturalnumbers nil )"[symbol -> nat]" positions nil )nil term_adt nil )"[term -> boolean]" term_adt nil )nil nat_types nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"[(app?) -> symbol]" term_adt nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil positions nil )nil IUnion_extra nil )"set" sets nil )"positions" positions nil )"bool" sets nil )"[below[length(fs)] -> T]" finite_sequencesnil )"set[T]" indexed_sets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.265 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
