Impressum subterm.prf
Sprache: Lisp
(subtermnil 3388757677"" (skosimp*)"" (typepred "p!1" )"" (expand "positionsOF" )"" (assert )"" (expand "only_empty_seq" )"" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil nil ))nil 3388757677"" (skosimp*)"" (typepred "p!1" )"" (expand "positionsOF" )"" (lift-if) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" subterm 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 subterm nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" 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 )"T" seq_extras "structures/" )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"bool" sets nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"bool" reals nil )"[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 IUnion_extra nil )"finseq" finite_sequences nil )"positions" positions nil )"posint" nil ))nil ))nil 3388757677"" (skosimp*)"" (typepred "p!1" )"" (expand "positionsOF" -1)"" (lift-if)"" (prop)"1" (expand "only_empty_seq" )"1" (rewrite "empty_0" ) nil nil )) nil )"2" (expand "only_empty_seq" )"2" (rewrite "empty_0" ) nil nil )) nil )"3" (expand * "union" "member" )"3" (prop)"1" (expand "only_empty_seq" )"1" (rewrite "empty_0" ) nil nil )) nil )"2" (expand "IUnion" )"2" (skolem * "i1" )"2" (expand "catenate" )"2" (skolem * "y1" )"2" (expand "member" )"2" (flatten)"2" (replace -3 -1 rl)"2" "i1" )"2" "fsepn.first_equal" )"2" "q!1" "y1" "i!1" "i1" )"2" "1" (assert ) nil nil )"2" "fsepn.seq_first_rest" )"2" "p!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" subterm 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 subterm nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil seq_extras "structures/" )"bool" reals nil )"[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 IUnion_extra nil )"positions" positions nil )nil finite_sequences nil )nil seq_extras "structures/" ))nil ))nil 3388757677"" (skosimp*)"" (replaces -3) (("" (rewrite "length_rest" ) 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 positions nil )"positions" positions nil )nil positions nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil seq_extras "structures/" ))nil ))nil 3388757677"" (skosimp*)"" (typepred "p!1" )"" (expand "positionsOF" )"" (assert )"" (expand "only_empty_seq" )"" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" subterm 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 subterm nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil ))nil ))nil 3411906619"" (skosimp*)"" (skoletin* 1)"" (expand * subset? member)"" (skosimp*)"" (expand "Posv" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans 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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" sets nil )"positions" positions nil )"posint" nil )"R" extend nil )"positions[variable, symbol, arity]" nil )"bool" sets nil ))nil 3414630433"" (skosimp*)"" (skoletin* 1)"" (replaces -1)"" (lemma "pos_vars_subset_pos" )"" (inst?)"" (assert )"" (lemma "positions_of_terms_finite" )"" (inst?)"" (lemma "finite_sets[position].finite_subset" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans 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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" finite_sets nil )nil subterm nil )"(partial_order?[set[T]])" nil )"positions" positions nil )"term[variable, symbol, arity]" subterm nil )nil finite_sets nil )nil finite_sets nil )nil positions nil ))nil 3402241169"" (skeep)"" (decompose-equality)"" (expand "Vars" )"" (expand "restrict" )"" (iff)"" (prop)"1" (skosimp*)"1" (typepred "p!1" )"1" (expand "positionsOF" )"1" (expand * "only_empty_seq" "subtermOF" )"1" (lift-if)"1" (rewrite "empty_0" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (inst 1 "empty_seq" )"1" (expand "subtermOF" )"1" (rewrite "empty_0" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "positionsOF" )"2" (expand "only_empty_seq" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[(V)]" subterm nil )"[T, T -> boolean]" equalities nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" subterm nil )nil naturalnumbers 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 subterm nil )nil subterm nil )"finseq" finite_sequences nil )"term[variable, symbol, arity]" subterm nil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil )"term" subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil ))nil 3415054747"" (skosimp*)"" (lift-if)"" (prop)"1" (decompose-equality 1)"1" (expand "restrict" )"1" (lemma "Vars_is_var" )"1" (inst?)"1" (assert )"1" (replaces -1)"1" (expand "singleton" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 2)"2" (iff)"2" (prop)"1" (expand "finseq_appl" )"1" (expand "IUnion" )"1" (expand "Vars" )"1" (skosimp*)"1" (expand "subtermOF" -1)"1" (lift-if)"1" (prop)"1" (typepred "x!1" )"1" expand "V" )"1" (assert ) nil nil ))nil ))nil )"2" (expand "finseq_appl" )"2" "first(p!1) - 1" )"1" (inst 2 "rest(p!1)" ) nil nil )"2" "first[posnat](p!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "finseq_appl" )"2" (expand "IUnion" )"2" (skosimp*)"2" (expand "Vars" )"2" (skosimp*)"2" (inst 1 "add_first(i!1 + 1, p!1)" )"1" (expand "subtermOF" 1)"1" (lift-if)"1" "1" "1" (grind) nil nil ))nil )"2" expand "finseq_appl" )"2" rewrite "rest_add_first" )"2" rewrite "first_add" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (typepred "p!1" )"2" expand "positionsOF" 1)"2" expand * "union" "member" )"2" "2" "2" expand "IUnion" )"2" expand "finseq_appl" )"2" "i!1 + 1" )"2" expand "catenate" )"2" expand "member" )"2" "p!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"term[variable, symbol, arity]" subtermnil )"[term -> boolean]" term_adt 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 )"bool" reals nil )"set[T]" indexed_sets nil )nil finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"finseq" seq_extras "structures/" )"positions?[variable, symbol, arity](t1!1)" nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"term" subterm nil )"posint" nil )"positions?[variable, symbol, arity](args(t1!1)`seq(i!1))" subtermnil )"below[length(args(t1!1))]" subterm nil )"[numfield, numfield -> numfield]" number_fields nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"bool" sets nil )"set" sets nil )"positions" positions nil )"bool" reals nil )nil IUnion_extra nil )"(total_order?[real])" nil )"non_empty_finite_set[term[variable, symbol, arity]]" subterm nil )"finite_set[S]" nil )"set[(V)]" subterm nil )"[term -> boolean]" term_adt nil )"[variable -> (vars?)]" term_adt nil )"[(vars?) -> variable]" term_adt nil )"R" restrict nil )"bool" sets nil )"(singleton?)" sets nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" subterm nil )nil naturalnumbers 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 subterm nil )nil subterm nil )nil subterm nil ))nil 3415056088"" (induct "t" )"1" (skosimp*)"1" (lemma "vars_term_is_union" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (skosimp*)"2" (case "length(app2_var!1) = 0" )"1" (hide -2)"1" "Vars(app(app1_var!1, app2_var!1)) = emptyset" :hide? T)"1" (rewrite "finite_emptyset" ) nil nil )"2" (hide 2)"2" (decompose-equality 1)"2" (iff)"2" (prop)"1" (expand "Vars" )"1" (skosimp*)"1" (typepred "p!1" )"1" (expand "positionsOF" )"1" (expand "only_empty_seq" )"1" "1" expand "subtermOF" )"1" rewrite "empty_0" )"1" "x!1" )"1" expand "V" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "vars_term_is_union" )"2" (inst?)"2" (assert )"2" (replaces -1 2)"2" (expand "finseq_appl" )"2" "IUnion_extra[(V)].IUnion_of_finite_is_finite1" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil IUnion_extra nil )"posint" nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )"positions" positions nil )"term" subterm nil )nil seq_extras "structures/" )nil finite_sequences nil )"finseq" finite_sequences nil )nil finite_sets nil )"set" sets nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[term -> boolean]" term_adt nil )"finite_set" finite_sets nil )nil finite_sequences nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )"[variable -> (vars?)]" term_adt nil )"[term -> boolean]" term_adt nil )"finite_set[S]" nil )"non_empty_finite_set[term[variable, symbol, arity]]" subterm nil )nil subterm nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"set[(V)]" subterm nil )"bool" finite_sets nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil 3388757677"" (skosimp*)"" (lemma "closed_positions" )"" (inst -1 "p!1" "p!1 o q!1" "t!1" )"" (assert )"" (expand "<=" ) (("" (inst 1 "q!1" ) nil nil )) nil )) nil ))nil ))nil ))nil )"[symbol -> nat]" subterm nil )nil naturalnumbers 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 subterm nil )nil subterm nil )nil positions nil )"bool" positions nil )nil term_adt nil )"finseq" finite_sequences nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3388757678"" (measure-induct+ "length(p)" "p" )"1" (skeep)"1" (expand "subtermOF" 1)"1" (prop)"1" (hide -2)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil )"2" (inst -1 "rest(x!1)" "q" "args(t)(first(x!1) - 1)" )"1" (rewrite "length_rest" )"1" (prop)"1" (hide 3)"1" (expand "positionsOF" -1)"1" (lift-if)"1" (prop)"1" (expand "only_empty_seq" )"1" (lemma "fsepn.seq_empty" )"1" (inst -1 "x!1" "q" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "only_empty_seq" )"2" (lemma "fsepn.seq_empty" )"2" (inst -1 "x!1" "q" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (expand * "union" "member" )"3" (prop)"1" (expand "only_empty_seq" )"1" "fsepn.seq_empty" )"1" "x!1" "q" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "IUnion" )"2" "i1" )"2" expand "catenate" )"2" "y1" )"2" expand "member" )"2" "2" "fsepn.seq_first_rest" )"2" "x!1" )"2" assert )"2" "2" "fsepn.add_first_compo" )"2" "rest(x!1)" "q" "first(x!1)" )"2" "2" "fsepn.first_equal" )"2" "rest(x!1) o q" "y1" "first(x!1)" "i1" )"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 ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide (-2 -3 2))"2" (lemma "pos_ax" )"2" (inst -1 "y!1" "q!1" "t!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (hide 2)"3" (lemma "pos_ax" )"3" (inst -1 "p!1" "q!1" "t!1" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )nil positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil IUnion_extra nil )"bool" reals nil )nil seq_extras "structures/" )"positions" positions nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"position[variable, symbol, arity]" subtermnil )"[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 )"[below[length(fs)] -> T]" finite_sequencesnil )AND const-decl "[bool, bool -> bool]" booleans nil )"term" subterm nil )nil positions nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 3388757677"" (skosimp*)"" (lemma "pos_subterm_ax" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil subterm nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 ))nil 3388769744"" (measure-induct+ "length(p)" ("p" ))"1" (skeep)"1" (lemma "fsepn.seq_first_rest" )"1" (inst -1 "x!1" )"1" (case "x!1`length /= 0" )"1" (assert )"1" (name-replace "subtemp" "subtermOF(t, x!1)" )"1" (replace -2 1)"1" (rewrite "add_first_compo" )"1" (expand "subtermOF" 1 1)"1" (lift-if)"1" (prop)"1" (lemma "fsepn.empty_0" )"1" "add_first(first(x!1), rest(x!1) o q)" )"1" assert )"1" "1" "fsepn.add_first_compo" )"1" "rest(x!1)" "q" "first(x!1)" )"1" replace -1 -2 rl)"1" "1" replace -2 -1 rl)"1" "1" "fsepn.seq_empty" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "first(add_first(first(x!1), rest(x!1) o q)) = first(x!1)" "1" (rewrite "fsepn.rest_add_first" )"1" expand "subtemp" )"1" "rest(x!1)" "q" "args(t)(first(x!1) - 1)" )"1" rewrite "length_rest" )"1" "1" "1" "subtermOF(t, x!1) = subtermOF(args(t)(first(x!1) - 1), rest(x!1))" )"1" "1" expand "subtermOF" 1 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" -2)"2" "2" "1" expand "only_empty_seq" )"1" "1" "fsepn.seq_empty" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "only_empty_seq" )"2" "fsepn.seq_empty" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand *"union" "member" )"3" "1" "1" expand "only_empty_seq" )"1" "fsepn.seq_empty" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "IUnion" )"2" "i1" )"2" expand "catenate" )"2" "y1" )"2" expand "member" )"2" "2" replace "2" rewrite "fsepn.add_first_compo" )"2" "2" "fsepn.first_equal" )"2" "rest(x!1) o q" "y1" "first(x!1)" "i1" )"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 ))nil ))nil ))nil )"2" (hide-all-but (1 4))"2" (rewrite "first_add" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (prop)"1" (hide-all-but (-2 1))"1" (expand "subtermOF" 1 3)"1" (lift-if)"1" (prop)"1" (hide -2)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "subtermOF" 1 3)"2" (lift-if)"2" (prop)"2" (hide -2)"2" (rewrite "empty_0" )"2" (replaces -1)"2" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (lemma "pos_subterm_ax" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide-all-but (-1 1))"3" (lemma "pos_ax" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (hide 2)"4" (lemma "pos_subterm_ax" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil )"5" (hide 2)"5" (lemma "pos_ax" )"5" (inst?) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil )nil positions nil )nil subterm nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[term -> boolean]" term_adt nil )nil finite_sequences 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 )"int" integers nil )"(total_order?[real])" nil )"positions" positions nil )nil seq_extras "structures/" )"bool" reals nil )nil IUnion_extra nil )"positions" positions nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )nil seq_extras "structures/" )"term[variable, symbol, arity]" subtermnil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )"boolean" notequal nil )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil positions nil )"term" subterm nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 3399644897"" (measure-induct+ "length(p)" "p" )"" (skeep)"" (expand "positionsOF" -2)"" (lift-if)"" (prop)"1" (expand "only_empty_seq" )"1" (hide -3)"1" (replaces -2)"1" (expand "subtermOF" )"1" (rewrite "empty_0" )"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (expand "only_empty_seq" )"2" (replaces -2)"2" (expand "subtermOF" )"2" (rewrite "fsepn.empty_0" )"2" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (expand * "union" "member" )"3" (prop)"1" (expand "only_empty_seq" )"1" (hide -2)"1" (replaces -1)"1" (expand "subtermOF" )"1" (rewrite "empty_0" )"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "IUnion" )"2" (skosimp*)"2" (expand "catenate" )"2" (skosimp*)"2" (expand "member" )"2" (expand "positionsOF" 3)"2" (lift-if)"2" "2" expand * "union" "member" )"2" "2" expand "IUnion" )"2" "i!1" )"2" expand "catenate" )"2" case "x!1`length /= 0" )"1" "rest(x!1) o q" )"1" expand "member" )"1" "rest(x!1)" )"1" "q" "args(t)(i!1 - 1)" )"1" "fsepn.rest_add_first" )"1" "x!2" "first(x!1)" )"1" rewrite "length_rest" )"1" replace "1" rewrite "first_add" )"1" replace "1" replace "1" "fsepn.add_first_compo" )"1" "rest(x!1)" "q" "first(x!1)" )"1" "first(x!1) = i!1" )"1" replace "1" replace "1" expand "subtermOF" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "first_add" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"posint" nil )"posint" nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"T" seq_extras "structures/" )"position[variable, symbol, arity]" subtermnil )"[below[length(fs)] -> T]" finite_sequencesnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil )"bool" reals nil )"[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 IUnion_extra nil )"positions" positions nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil finite_sequences nil )"term" subterm nil )nil 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 )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 3497114104 ("" (subtype-tcc) nil nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3497114104"" (skosimp*) (("" (rewrite "delete_is_position" ) nil nil )) nil )nil positions nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil ))nil ))nil 3497114230"" (skosimp*)"" (lemma "pos_subterm_ax" )"" "delete(p!1, length(p!1) - 1)" "#(last(p!1))" "s!1" )"1" (prop)"1" (lemma "fsepn.add_first_empty_seq" )"1" (inst -1 "last(p!1)" )"1" (lemma "not_var" )"1" "last(p!1)" "#(last(p!1))" "empty_seq" "subtermOF(s!1, delete(p!1, length(p!1) - 1))" )"1" (assert ) nil nil )"2" (hide (-1 -2 -3 3))"2" (typepred "length(p!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "fsepn.add_last_delete_is_o" )"2" (inst?)"2" (assert )"2" (lemma "fsepn.add_last_delete" )"2" (inst?)"2" (assert )"2" (replace -1 -2 rl)"2" (expand "finseq_appl" )"2" (expand "last" 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (hide (-1 3))"3" (typepred "length(p!1)" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil subterm nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"finseq" finite_sequences nil )NOT const-decl "[bool -> bool]" booleans nil )nil positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )nil term_adt nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"finite_sequence[T]" set2seq "structures/" )nil finite_sequences nil )"finseq" seq_extras "structures/" )"bool" reals nil )nil finite_sequences nil )"boolean" notequal nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil nat_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )"position[variable, symbol, arity]" subtermnil )"int" integers nil )"(total_order?[real])" nil ))nil 3402782187"" (skeep)"" (expand * "subset?" "member" )"" (skeep)"" (expand "Vars" )"" (expand "restrict" )"" (skosimp*)"" (typepred "p!1" )"" (inst 1 "p o p!1" )"1" (rewrite "pos_subterm" )"1" (rewrite "pos_o_term" ) nil nil )) nil )"2" (rewrite "pos_o_term" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"set[(V)]" subterm nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" subterm 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 subterm nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil subterm nil )nil subterm nil )"term[variable, symbol, arity]" subterm nil )nil finite_sequences nil )"finseq" finite_sequences nil )"position[variable, symbol, arity]" subtermnil )"positions?[variable, symbol, arity](subtermOF(t, p))" subtermnil ))nil 3402066026"" (skeep)"" (lemma "vars_subterm" )"" (inst?)"" (assert )"" (lemma "IUnion_extra[(V)].disjoint_subset" )"" (hide -3)"" "Vars(subtermOF(t, p))" "Vars(t)" "Vars(s)" "Vars(s)" )"" (assert )"" (hide-all-but 1)"" (expand * "subset?" "member" )"" (skeep) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subterm nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil positions nil )"set[(V)]" subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil )nil IUnion_extra nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 3414510689"" (induct "t" )"1" (skeep)"1" (skolem-typepred)"1" (flatten)"1" (expand "V" )"1" (expand "positionsOF" )"1" (expand "only_empty_seq" )"1" (replaces -3)"1" (replaces -3)"1" (expand "subtermOF" )"1" (rewrite "empty_0" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skolem-typepred)"2" (flatten)"2" (expand "V" )"2" (expand "positionsOF" )"2" (prop)"1" (expand "only_empty_seq" )"1" (replaces -2)"1" (replaces -3)"1" (hide-all-but (-6 -7 1))"1" (expand "subtermOF" )"1" (rewrite "empty_0" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "union" "member" )"2" (prop)"1" (expand "only_empty_seq" )"1" (replaces -1)"1" (replaces -1)"1" (hide-all-but (-4 -5 3))"1" (expand "subtermOF" )"1" rewrite "empty_0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -5))"2" (expand "only_empty_seq" )"2" (expand * "parallel" "<=" )"2" (prop)"1" (skosimp*)"1" "1" "fsepn.seq_empty" )"1" "1" assert )"1" "1" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" "2" expand "subtermOF" -4)"2" rewrite "empty_0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-2 -5))"3" (expand "only_empty_seq" )"3" (replaces -1)"3" (expand "subtermOF" -3)"3" (rewrite "empty_0" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (expand "IUnion" )"4" (skosimp*)"4" (expand "catenate" )"4" (skosimp*)"4" (expand "member" )"4" expand "finseq_appl" )"4" expand "subtermOF" (-8 -9))"4" "4" "1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil )"4" expand "finseq_appl" )"4" "fsepn.first_add" )"4" "4" "x!2" "i!1" )"4" "x!3" "i!2" )"4" "fsepn.rest_add_first" )"4" "4" "x!2" "i!1" )"4" "x!3" "i!2" )"4" replace "4" replace "4" "4" "4" "4" "4" "i!2 = i!1" )"1" "i!1 - 1" )"1" "x!1" "y!1" "x!2" "x!3" )"1" assert )"1" "1" expand *"parallel" "<=" )"1" "1" "1" "1" "1" rewrite "add_first_compo" )"1" "fsepn.first_equal" )"1" "1" assert )"1" "p1!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "add_first_compo" )"2" "fsepn.first_equal" )"2" "2" assert )"2" "p1!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand *"parallel" "<=" )"2" "1" "1" "1" "1" rewrite "add_first_compo" )"1" "fsepn.first_equal" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "add_first_compo" )"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 ))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 )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"posint" nil )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil IUnion_extra nil )"bool" reals nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"finseq" finite_sequences nil )nil seq_extras "structures/" )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" positions nil )nil seq_extras "structures/" )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil seq_extras "structures/" )nil finite_sequences nil )"finseq" finite_sequences nil )"positions" positions nil )NOT const-decl "[bool -> bool]" booleans nil )"[term -> boolean]" term_adt nil )"[variable -> (vars?)]" term_adt nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"bool" positions nil )"boolean" notequal nil )"term" subterm nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil 3411906851"" (skosimp*)"" (skoletin 1)"" (flatten)"" (replaces -3)"" (expand * "member" "Pos_var" "parallel" "<=" )"" (expand "extend" )"" (prop)"1" (skosimp*)"1" (replace -1 -3)"1" (rewrite "pos_subterm" )"1" (replace -2 -3)"1" (typepred "q!1" )"1" (replace -2 -1)"1" (lemma "pos_subterm_ax" )"1" "1" assert )"1" replace -4 -1)"1" "1" "x!1" )"1" expand "V" )"1" expand "positionsOF" )"1" assert )"1" expand "only_empty_seq" )"1" "1" rewrite "seq_o_empty" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (replace -1 -2)"2" (rewrite "pos_subterm" )"2" (replace -3 -2)"2" (typepred "p!1" )"2" (replace -2 -1)"2" (lemma "pos_subterm_ax" )"2" "2" assert )"2" replace -5 -1)"2" "2" "x!1" )"2" expand "V" )"2" expand "positionsOF" )"2" assert )"2" expand "only_empty_seq" )"2" "2" rewrite "seq_o_empty" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans 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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" positions nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"R" extend nil )nil subterm nil )NOT const-decl "[bool -> bool]" booleans nil )nil subterm nil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil )"bool" positions nil ))nil 3412415465"" (skosimp*)"" (replaces -1)"" (lemma "Pos_var_is_finite" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil subterm nil )nil subterm 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]" subterm nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )nil subterm nil ))nil ))nil 3411907203"" (skosimp*)"" (skoletin* 1)"" (expand "PP?" )"" (prop)"" (skosimp*)"" (lemma "variable_positions" )"" (expand "finseq_appl" )"" "t!1" "x!1" "seqv`seq(i!1)" "seqv`seq(j!1)" )"1" (assert )"1" (prop)"1" (lemma "set2seq_neq[position]" )"1" (inst -1 "Posv" )"1" (assert )"1" (inst -1 "i!1" "j!1" )"1" (grind) nil nil )"2" "j!1" )"2" replace -3)"2" rewrite "set2seq_length[position]" )nil nil ))nil ))nil )"3" "i!1" )"3" "3" rewrite "set2seq_length[position]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "set2seq_lem[position]" )"2" (inst -1 "Posv" )"2" (assert )"2" (inst -1 "i!1" )"1" expand "finseq_appl" )"1" expand "member" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" rewrite "set2seq_length[position]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "set2seq_lem[position]" )"3" (inst -1 "Posv" )"3" (assert )"3" (inst -1 "j!1" )"1" expand "finseq_appl" )"1" expand "member" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "j!1" )"2" "2" rewrite "set2seq_length[position]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "set2seq_lem[position]" )"2" (inst -1 "Posv" )"2" (assert )"2" (inst -1 "j!1" )"1" (replaces -3)"1" (expand "finseq_appl" )"1" expand "Pos_var" -1 1)"1" expand "extend" -1 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (typepred "j!1" )"2" (replaces -2)"2" rewrite "set2seq_length[position]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "set2seq_lem[position]" )"3" (inst -1 "Posv" )"3" (assert )"3" (inst -1 "i!1" )"1" (expand "finseq_appl" )"1" (replaces -3)"1" expand "Pos_var" -1 1)"1" expand "extend" -1 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (typepred "i!1" )"2" (replaces -2)"2" rewrite "set2seq_length[position]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil naturalnumbers nil )nil nat_types nil )nil numbers 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 )nil integers nil )"bool" reals nil )nil integers nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" finite_sets nil )"[bool, bool -> bool]" booleans nil )nil finite_sequences nil )nil finite_sequences nil )"bool" positions nil )nil finite_sets nil )"finite_sequence[T]" set2seq "structures/" )nil subterm nil )"positions" positions nil )"term[variable, symbol, arity]" subterm nil )"finite_sequence[position[variable, symbol, arity]]" subterm nil )"bool" reals nil )"below[length(seqv)]" subterm nil )"below[length(seqv)]" subterm nil )nil positions nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"positions[variable, symbol, arity]" nil )nil naturalnumbers nil )nil set2seq "structures/" )"boolean" notequal nil )"bool" sets nil )"bool" sets nil )"posint" nil )nil set2seq "structures/" )nil set2seq "structures/" )"(strict_total_order?[real])" real_props nil )"R" extend nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil 3411907585"" (skosimp*)"" (skoletin* 1)"" (expand "SP?" )"" (skosimp*)"" (expand "finseq_appl" )"" (lemma "set2seq_lem[position]" )"" (inst -1 "Posv" )"" (assert )"" (inst -1 "i!1" )"1" (expand "finseq_appl" )"1" (replaces -3)"1" (expand "Pos_var" -1 1)"1" (expand "extend" -1 1)"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "i!1" )"2" (replaces -2)"2" (rewrite "set2seq_length[position]" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil naturalnumbers nil )nil nat_types nil )nil numbers 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 )nil integers nil )"bool" reals nil )nil integers nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" finite_sets nil )"[bool, bool -> bool]" booleans nil )nil finite_sequences nil )nil finite_sequences nil )"bool" positions nil )nil finite_sets nil )"finite_sequence[T]" set2seq "structures/" )nil set2seq "structures/" )"R" extend nil )nil set2seq "structures/" )nil naturalnumbers nil )"positions[variable, symbol, arity]" nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"below[length(seqv)]" subterm nil )"finite_sequence[position[variable, symbol, arity]]" subterm nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil 3412318789"" (skosimp*)"" (skoletin* 1)"" (flatten)"" (replaces -)"" (expand "Pos_var" )"" (expand "extend" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans 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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"term" subterm nil )nil positions nil )"positions" positions nil )"[bool, bool -> bool]" booleans nil )"R" extend nil ))nil 3412318971"" (skosimp*)"" (skoletin* 1)"1" (lemma "no_empty_set_positions" )"1" (inst?)"1" (assert )"1" (case "card(Posv) > 0" )"1" (lemma "fspos.set2seq_length" )"1" (inst?) (("1" (grind) nil nil )) nil )) nil )"2" (lemma "finite_sets[position].nonempty_card" )"2" (inst?)"2" (prop)"2" (hide (1 3))"2" (expand "nonempty?" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (replaces -1)"2" (replaces -1)"2" (lemma "Pos_var_is_finite" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil naturalnumbers nil )nil nat_types nil )nil numbers 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 )nil integers nil )"bool" reals nil )nil integers nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"positions" subterm nil )"bool" finite_sets nil )"[bool, bool -> bool]" booleans nil )"finite_sequence[T]" set2seq "structures/" )nil finite_sets nil )"term" subterm nil )nil positions nil )"positions" positions nil )nil finite_sequences nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"R" extend nil )nil set2seq "structures/" )"posint" nil )"bool" sets nil )nil finite_sets nil )nil subterm nil ))nil 3512737910"" (skosimp)"" (expand positionsOF)"" (lift-if)"" (expand * only_empty_seq union member) nil nil )) nil ))nil ))nil )"positions" positions nil )"positions" positions nil )"set" sets nil )"bool" sets nil ))nil ))nil 3513090436"" (skosimp)"" (expand subtermOF) (("" (rewrite empty_0) nil nil )) nil )) nil )"term" subterm 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 )"finseq" finite_sequences nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil seq_extras "structures/" ))nil 3512737910"" (skosimp)"" (prop)"1" (inst -1 empty_seq)"1" (expand subtermOF) (("1" (rewrite empty_0) nil nil )) nil )"2" (hide 2)"2" (split)"1" (expand positionsOF)"1" (lift-if)"1" (expand * only_empty_seq union member) nil nil ))nil ))nil )"2" (expand positionsOF)"2" (lift-if)"2" (expand * only_empty_seq union member) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil )"positions" positions nil )"set" sets nil )"bool" sets nil )"term" subterm nil )nil seq_extras "structures/" )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil subterm nil )nil subterm nil )nil numbers 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 )nil naturalnumbers nil )"[symbol -> nat]" subterm nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil positions nil )"positions" positions nil )"term[variable, symbol, arity]" subterm nil )nil finite_sequences nil )"finseq" finite_sequences nil )"term[variable, symbol, arity]" subtermnil ))nil ))nil 3455281835"" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil subterm nil )nil subterm nil )nil naturalnumbers nil )"[symbol -> nat]" subterm nil )nil term_adt nil )nil nat_types nil )nil positions nil )nil positions nil )"positions" positions nil )nil finite_sequences nil )"(strict_total_order?[real])" real_props 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 )"finite_sequence[T]" set2seq "structures/" ))nil ))nil 3455281853"" (skeep)"" (replace -1 1)"" (expand "subtermOF" )"" (lift-if)"" (lift-if)"" (prop)"1" (expand "finseq_appl" )"1" (rewrite "first_add" )"1" (rewrite "rest_add_first" )"1" (rewrite "empty_0" -2)"1" (replace -2 2) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "finseq_appl" )"2" (expand "#" ) (("2" (grind) nil nil )) nil )) nil )"3" (expand "finseq_appl" )"3" (rewrite "first_add" )"3" (rewrite "rest_add_first" )"3" (rewrite "empty_0" -1)"3" (replace -1 2) (("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "finseq_appl" )"4" (expand "rest" )"4" (assert )"4" (expand "first" )"4" (expand "finseq_appl" )"4" (assert ) (("4" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "finseq_appl" )"5" (rewrite "first_add" )"5" (rewrite "rest_add_first" )"5" (assert ) (("5" (grind) nil nil )) nil )) nil ))nil ))nil )"6" (expand "finseq_appl" ) (("6" (grind) nil nil )) nil )"7" (expand "finseq_appl" )"7" (rewrite "first_add" )"7" (rewrite "rest_add_first" )"7" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil seq_extras "structures/" )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )"finseq" seq_extras "structures/" )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil term_adt nil )nil positions nil )nil positions nil )"positions" positions nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )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 )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"{k: nat | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"T" seq_extras "structures/" )"posint" nil )"[below[length(fs)] -> T]" finite_sequencesnil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"term" subterm nil ))nil 3455281944"" (induct "t" )"1" (skeep)"1" (skeep)"1" (inst 1 "empty_seq" )"1" (expand "subtermOF" )"1" (rewrite "empty_0" )"1" (expand "subterm" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "positionsOF" )"2" (expand "only_empty_seq" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "subterm" -2)"2" (split)"1" (inst 1 "empty_seq" )"1" (expand "subtermOF" 1)"1" (rewrite "empty_0" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide -) (("2" (grind) nil nil )) nil ))nil )"2" (skosimp)"2" (inst -2 "z!1" )"2" (inst -2 "s!1" )"2" (assert )"2" (skosimp)"2" case "seq(app2_var!1)(z!1) = ") "1" (replace -1 -3)"1" "t!1" "app(app1_var!1, app2_var!1)" )"1" (lemma "subt_of_subt_is_subt_of_term" )"1" (inst 1 "add_first( z!1 + 1, p!1)" )"1" "1" "x!1" "add_first(z!1 + 1, p!1)" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "z!1" )"2" "t!1" )"2" "2" "positions_of_arg" )"2" "t!1" "z!1" )"1" (assert ) nil nil )"2" replace -1 1 rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" )"2" expand "union" )"2" "2" "2" expand "IUnion" )"2" expand "member" )"2" "2" assert )"2" expand "catenate" )"2" "2" "p!1" )"2" expand "member" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "subtermOF" )"2" (lift-if)"2" (prop)"1" "1" (grind) nil nil ))nil )"2" "2" expand "finseq_appl" )"2" expand "first" )"2" expand "rest" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (typepred "z!1" )"3" (lemma "positions_of_arg" )"3" "app(app1_var!1, app2_var!1)" "z!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"finseq" seq_extras "structures/" )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" sets nil )"posint" nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "symbol" subterm nil )"{args: finite_sequence[term[variable, symbol, arity]] | " subterm nil) "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finite_sequence[T]" set2seq "structures/" )"posint" nil )"below[app2_var!1`length]" subterm nil )"{p: position | positionsOF(app2_var!1`seq(z!1))(p)}" subterm nil )nil positions nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(app?)" subterm nil )"(total_order?[real])" nil )nil IUnion_extra nil )"bool" reals nil )"int" integers nil )nil subterm nil )"finseq" seq_extras "structures/" )"{k: int | k <= i AND k <= j}" nil )"{k: nat | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"finseq" finite_sequences nil )"T" seq_extras "structures/" )"[term -> boolean]" term_adt nil )"[variable -> (vars?)]" term_adt nil )"variable" subterm nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )"positions" positions nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"term" subterm nil )nil positions nil )"[T, T -> boolean]" equalities nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"boolean" term_adt nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil ))nil 3455282276"" (induct "t" )"1" (skosimp*)"1" (expand "subtermOF" )"1" (expand "subterm" )"1" (lift-if)"1" (prop)"1" (assert ) nil nil )"2" (hide -1 2)"2" (typepred "p!1" )"2" (expand "positionsOF" )"2" (expand "only_empty_seq" )"2" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (skosimp)"2" (expand "subtermOF" -2)"2" (lift-if)"2" (prop)"1" (replace -2 1)"1" (expand "subterm" ) (("1" (propax) nil nil )) nil ))nil )"2" (expand "finseq_appl" )"2" (inst -2 "first(p!1) -1" "s!1" "rest(p!1)" )"1" (assert )"1" (expand "subterm" 2)"1" (flatten)"1" (inst 3 "first(p!1) - 1" ) nil nil )) nil ))nil ))nil )"2" (hide -1 3)"2" (typepred "p!1" )"2" (expand * "first" "finseq_appl" )"2" (expand "positionsOF" )"2" (prop)"1" (hide -1 1)"1" expand "only_empty_seq" )"1" (rewrite "empty_0" ) nil nil ))nil ))nil )"2" (expand "union" )"2" "1" "1" rewrite "empty_0" )"1" expand *"member" "only_empty_seq" )nil nil ))nil ))nil )"2" "2" expand "member" )"2" expand "IUnion" )"2" "2" expand "catenate" )"2" "2" "2" replace -1 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )"{p: position | positionsOF(app(app1_var!1, app2_var!1))(p)}" nil )"{args: finite_sequence[term[variable, symbol, arity]] | " subterm nil) "symbol" subterm nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[term -> boolean]" term_adt nil )nil finite_sequences nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"finseq" seq_extras "structures/" )"bool" reals nil ) (union const-decl "set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"bool" sets nil )"[below[length(fs)] -> T]" finite_sequencesnil )NOT const-decl "[bool -> bool]" booleans nil )"[term -> boolean]" term_adt nil )"[variable -> (vars?)]" term_adt nil )"positions" positions nil )nil seq_extras "structures/" )nil finite_sequences nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"boolean" term_adt nil )"term" subterm nil )nil positions nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"positions" positions nil )nil positions nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil ))nil 3455282320"" (induct "t" )"1" (skosimp*)"1" (expand "subterm" )"1" (prop)"1" (assert ) nil nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "subterm" -3)"2" (prop)"1" (inst -2 "empty_seq" "s!1" "r!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil )"2" (skosimp)"2" (inst -2 "z!1" "s!1" "r!1" )"2" (assert )"2" (expand "subterm" 1)"2" (flatten) (("2" (inst 2 "z!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )"T" finite_sequences nil )nil finite_sequences nil )"symbol" subterm nil )"{args: finite_sequence[term[variable, symbol, arity]] | " subterm nil) "finseq" finite_sequences nil )nil finite_sequences nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"boolean" term_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil ))nil 3457112583 ("" (subtype-tcc) nil 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 )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3457112583 ("" (termination-tcc) nil nil ) nil nil ))nil 3457201283"" (skosimp*)"" (typepred "q!1" )"" (expand "set_of_seq_pos" -1)"" (expand "IUnion" )"" (skosimp*)"" (expand "singleton" ) (("" (inst 2 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[position]" subterm nil )set type-eq-decl nil sets nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 )"set[T]" indexed_sets nil )"(singleton?)" sets nil ))nil 3457192341"" (induct n)"1" (skeep)"1" (expand comp_of_pos)"1" (assert ) (("1" (rewrite empty_0) nil nil )) nil )) nil ))nil )"2" (skeep)"2" (skeep)"2" (inst -1 p)"2" (expand comp_of_pos 1)"2" (expand o 1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"finseq" finite_sequences nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil seq_extras "structures/" )nil finite_sequences nil )"finseq" finite_sequences nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"position" subterm nil )"[T, T -> boolean]" equalities nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil defined_types nil )nil naturalnumbers 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 3457190961"" (skeep)"" (lemma length_comp_p)"" (copy -1)"" (inst?)"" (inst -2 m p)"" (assert )"" (replace -3 -1)"" (replace -1 -2)"" (lemma empty_0[posnat])"" (inst -1 p)"" (hide -2 -4)"" (assert )"" (rewrite both_sides_times1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil subterm 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 )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil finite_sequences nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil seq_extras "structures/" ))nil 3457205512"" (subtype-tcc) nil nil )"(total_order?[real])" nil )nil naturalnumbers 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 )"finseq" finite_sequences nil )"set[position]" subterm nil )"position" subterm nil )"(singleton?)" sets nil )"set[T]" indexed_sets nil ))nil ))nil 3457205513"" (skeep)"" (expand "injective?" )"" (skeep 2)"" (expand "function_inj" )"" (lemma "length_comp_p" )"" (copy -1)"" (inst -1 "x1" "p" )"" (inst -2 "x2" "p" )"" (replace -3 -1)"" (replaces -1 -2)"" (rewrite "both_sides_times1" )"" (hide-all-but (1 2))"" (prop)"" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )"position" subterm nil )nil finite_sequences nil )nil seq_extras "structures/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil reals nil )"boolean" notequal nil )nil real_props nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil naturalnumbers 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 subterm nil ))nil 3457117766"" (skeep)"" (lemma "infinite_def[position]" )"" (inst?)"" (assert )"" (inst 1 "function_inj(p)" )"" (prop)"1" (hide -1)"1" (skeep)"1" (expand "set_of_seq_pos" )"1" (expand "IUnion" )"1" (expand "function_inj" )"1" (inst 1 "x1" )"1" (expand "singleton" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (lemma "is_injective_function_inj" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 infinite_nat_def "sets_aux/" )"set[T]" indexed_sets nil )"(singleton?)" sets nil )nil subterm nil )AND const-decl "[bool, bool -> bool]" booleans nil )"position[variable, symbol, arity]" subtermnil )"position" subterm nil )"bool" functions nil )"set[position]" subterm nil )set type-eq-decl nil sets nil ))nil 3457168775"" (induct "n" )"1" (skosimp*)"1" (expand "comp_of_pos" )"1" (hide (-1 -2))"1" (expand "positionsOF" )"1" (lift-if)"1" (prop)"1" (expand "only_empty_seq" )"1" (propax) nil nil )) nil )"2" (expand "only_empty_seq" )"2" (propax) nil nil )) nil )"3" (expand * "union" "member" "only_empty_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "comp_of_pos" 1)"2" (inst -1 "p!1" "s!1" )"2" (assert )"2" (replace -3 -1 rl)"2" (rewrite "pos_o_term" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil subterm nil )"set" sets nil )"bool" sets nil )"positions" positions nil )nil naturalnumbers nil )"position" subterm nil )"term" subterm nil )nil positions nil )"[T, T -> boolean]" equalities nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil defined_types nil )nil naturalnumbers 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 3457130014"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (expand "member" )"" (expand "set_of_seq_pos" )"" (expand "IUnion" )"" (skosimp*)"" (expand "singleton" )"" (lemma "comp_of_pos_is_pos" )"" (inst -1 "p!1" "s!1" "i!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"set[T]" indexed_sets nil )"(singleton?)" sets 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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil term_adt nil )nil subterm nil )"set[position]" subterm nil ))nil 3457105607"" (skeep)"" (case "p /= empty_seq" )"1" (hide 1)"1" (case "subset?(set_of_seq_pos(p), positionsOF(s))" )"1" (lemma infinite_set_of_seq_pos)"1" (inst?)"1" (assert )"1" (lemma finite_subset[position])"1" (inst?)"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (rewrite positions_of_terms_finite) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite subset_of_seq_pos) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"finseq" finite_sequences nil )nil finite_sequences nil )"boolean" notequal nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 )"positions" positions nil )nil positions nil )nil term_adt nil )"set[position]" subterm nil )"bool" sets nil )set type-eq-decl nil sets nil )nil finite_sets nil )nil positions nil )nil finite_sets nil )"term[variable, symbol, arity]" subterm nil )"bool" finite_sets nil )"(partial_order?[set[T]])" nil )nil subterm nil )nil subterm nil ))nil 3513089267"" (expand child)"" (skosimp*)"" (lemma seq_first_rest[posnat])"" (inst -1 p1!1)"" (lemma empty_0[posnat])"" (inst -1 p1!1)"" (assert )"" (lemma pos_subterm_ax)"" (inst -1 q!1 p1!1 s!1)"" (assert )"" (lemma not_var)"" "first(p1!1)" "p1!1" "rest(p1!1)" "subtermOF(s!1, q!1)" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )nil subterm nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil positions nil )"positions" positions nil )nil positions nil )"term" subterm nil )nil positions nil )nil term_adt nil )nil seq_extras "structures/" )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 )"bool" positions nil ))nil 3514739012"" (measure-induct+ "length(q)" ("q" ))"" (skosimp)"" (case "x!1 = empty_seq" )"1" (hide-all-but (-1 3 4))"1" (replaces -1)"1" (expand child)"1" (inst 1 p!1)"1" (rewrite empty_o_seq)"1" (flatten)"1" (replaces -1)"1" (inst 1 empty_seq)"1" (rewrite empty_o_seq)"1" (rewrite subterm_empty_seq)"1" (expand positionsOF)"1" "1" expand * only_empty_seq union member)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -1 "delete(x!1, length(x!1) - 1)" )"1" (inst -1 t!1 p!1)"1" case "length(delete(x!1, length(x!1) - 1)) < length(x!1)" )"1" (assert )"1" (hide -1)"1" (rewrite delete_is_position)"1" (prop)"1" (hide-all-but (-1 -2 1 2))"1" "dp" "delete(x!1, length(x!1) - 1)" :hide? nil )"1" (lemma add_last_delete[posnat])"1" (inst -1 x!1)"1" assert )"1" replace -2)"1" rewrite add_last_is_o)"1" expand "left_without_children" )"1" "1" replace -3 -1)"1" "q1!1 o #(last(x!1))" )"1" rewrite o_assoc)"1" rewrite first_compo)"1" assert )"1" "1" expand *"#" "1" "1" "1" assert )nil nil ))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 ))nil ))nil )"2" (hide-all-but (-1 1 3))"2" "dp" "delete(x!1, length(x!1) - 1)" :hide? nil )"2" (lemma add_last_delete[posnat])"2" (inst -1 x!1)"2" assert )"2" replace -2)"2" rewrite add_last_is_o)"2" expand "left_without_children" )"2" "2" replace -4 -1)"2" "p1!1 o #(last(x!1))" "2" rewrite o_assoc)"2" rewrite first_compo)"1" assert )"1" "1" expand *"#" "1" "1" "1" assert )nil nil ))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 ))nil ))nil )"3" "dp" "delete(x!1, length(x!1) - 1)" :hide? nil )"3" (expand child -2)"3" (skosimp)"3" (lemma add_last_delete[posnat])"3" "3" assert )"3" replace -2)"3" rewrite add_last_is_o)"3" case "last(x!1) < first(p1!1)" )"1" "1" expand "left_without_children" )"1" "#(last(x!1))" "1" assert )"1" "1" "1" expand *"#" nil nil ))nil )"2" expand first 1 1)"2" expand "2" expand "#" 1)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "last(x!1) > first(p1!1)" )"1" "1" expand "left_without_children" )"1" "#(last(x!1))" )"1" assert )"1" "1" "1" expand *"#" nil nil ))nil )"2" expand "2" expand "2" expand "#" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "p1!1 = #(last(x!1))" )"1" "1" "1" rewrite seq_o_empty)"1" assert )"1" "1" expand "1" "1" expand *nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "last(x!1) = first(p1!1)" )"1" "1" "1" "1" "1" assert )"1" replace "1" rewrite "1" replace "1" replace "1" expand "1" "rest(p1!1)" )"1" assert )"1" "1" "1" "1" rewrite "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" rewrite empty_0)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2 3 4)"4" (skosimp)"4" (lemma add_last_delete[posnat])"4" (inst -1 x!1)"4" assert )"4" replace -3)"4" rewrite add_last_is_o)"4" "q1!1 o #(last(x!1))" )"4" rewrite o_assoc)"4" assert )"4" "4" "p!1" "q1!1 o #(last(x!1))" "t!1" )"4" assert )"4" rewrite o_assoc)"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (expand delete)"2" (rewrite empty_0) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (hide-all-but (1 2))"3" (lemma empty_0[posnat])"3" (inst -1 x!1) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (lemma empty_0[posnat])"2" (inst -1 x!1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"position[variable, symbol, arity]" subtermnil )"finseq" seq_extras "structures/" )nil finite_sequences nil )nil seq_extras "structures/" )"posint" nil )nil seq_extras "structures/" )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"T" seq_extras "structures/" )nil subterm nil )nil positions nil )nil seq_extras "structures/" )"positions" positions nil )"set" sets nil )"bool" sets nil )nil subterm nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )"term" subterm nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" positions nil )"bool" positions nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"positions" positions nil )nil positions nil )nil term_adt nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" subterm nil )nil subterm nil )nil subterm 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 3516190832"" (skosimp)"" (case "s!1 = app(f(s!1), args(s!1))" )"1" (case "t!1 = app(f(t!1), args(t!1))" )"1" (replace -1 1)"1" (replace -2 1) (("1" (decompose-equality 1) nil nil ))nil ))nil )"2" (decompose-equality 1) nil nil ))nil )"2" (decompose-equality 1) nil nil ))nil ))nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[term -> boolean]" term_adt nil )nil finite_sequences nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil term_adt nil )"[symbol -> nat]" subterm nil )nil naturalnumbers 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 subterm nil )nil subterm nil )nil term_adt nil ))nil 3516237359"" (skosimp*)"" (hide -1 -2)"" (lemma app_term)"" (inst -1 p!1 p1!1 s!1) (("" (assert ) nil nil )) nil )) nil ))nil ))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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )nil subterm nil ))nil ))nil 3516237359"" (skosimp*)"" (hide -1 -2)"" (lemma app_term)"" (inst -1 p!1 p1!1 t!1) (("" (assert ) nil nil )) nil )) nil ))nil ))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 subterm nil )nil subterm nil )"[symbol -> nat]" subterm nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil term_adt nil )nil positions nil )"positions" positions nil )nil subterm nil ))nil ))nil 3516237359"" (induct s)"1" (skosimp*)"1" (typepred p!1)"1" (hide-all-but (-1 1))"1" (expand positionsOF)"1" (expand only_empty_seq) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "s!1" "app(app1_var!1, app2_var!1)" :hide? nil )"2" (case "app?(t!1)" )"1" (lemma equal_app_term)"1" (inst -1 s!1 t!1)"1" (assert )"1" (prop)"1" (hide-all-but (-6 1 2))"1" (inst -1 empty_seq)"1" (rewrite subterm_empty_seq)"1" (rewrite subterm_empty_seq)"1" (assert )"1" (hide 1)"1" expand child)"1" "1" rewrite empty_o_seq)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 3)"2" (split)"1" (expand positionsOF)"1" (expand * only_empty_seq union member)nil nil ))nil )"2" (expand positionsOF)"2" (expand * only_empty_seq union member)nil nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 1)"1" (hide-all-but (-2 -6 1 2))"1" (inst -2 empty_seq)"1" (rewrite subterm_empty_seq)"1" (rewrite subterm_empty_seq)"1" (assert )"1" "1" expand child)"1" "1" assert )"1" rewrite empty_o_seq)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 3)"2" (replaces -1)"2" (split)"1" expand *nil nil )"2" expand *nil nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 1)"2" (lemma positions_of_arg)"2" (inst-cp -1 s!1 x!1)"2" (inst -1 t!1 x!1)"2" case "subtermOF(s!1, #(x!1 + 1)) = args(s!1)`seq(x!1)" )"1" case "subtermOF(t!1, #(x!1 + 1)) = args(t!1)`seq(x!1)" )"1" replace -1 1 rl)"1" replace -2 1 rl)"1" case "left_without_children(p!1, #(x!1 + 1))" )"1" "1" "#(x!1 + 1)" )"1" (assert ) nil nil )"2" replace -5)"2" (assert ) nil nil ))nil ))nil ))nil )"2" case "left_without_children( #(x!1 + 1), p!1)" )"1" "1" "#(x!1 + 1)" )"1" (assert ) nil nil )"2" replace -5)"2" (assert ) nil nil ))nil ))nil ))nil )"2" case "EXISTS(q1 : position) : positionsOF(subtermOF(s!1, p!1))(q1) AND #(x!1 + 1) = p!1 o q1") "1" "1" "1" case "q1!1 = empty_seq" )"1" "1" rewrite "1" assert )nil nil ))nil ))nil )"2" "2" expand * "#" o)"2" "2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "child(p!1, #(x!1 + 1))" )"1" "1" expand child -1)"1" "1" "subtermOF(t!1, #(x!1 + 1))" "1" assert )"1" "1" "1" case "subtermOF(s!1, #(1 + x!1)) = app2_var!1`seq(x!1)" )"1" assert )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "subtermOF(s!1, #(1 + x!1)) = app2_var!1`seq(x!1)" )"1" replace "1" "#(1 + x!1) o q!1" )"1" "1" "1" "1" replace "1" "1" rewrite "1" rewrite "1" "1" rewrite nil nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" "2" "#(1 + x!1) o r!1" "p1!2" "q1!1" )"2" assert )"2" replace "2" rewrite "2" assert )"2" "2" "2" "#(1 + x!1)" "r!1" "q1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))" )"1" "1" "1" rewrite "1" rewrite nil nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))" )"1" replace "1" "#(1 + x!1) o q!1" )"1" "1" "1" "1" "1" rewrite "1" rewrite "1" "1" rewrite nil nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" "2" replace "2" rewrite "2" "#(1 + x!1) o r!1" "p1!2" "q1!1" )"2" assert )"2" "2" "2" "#(1 + x!1)" "r!1" "p1!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" replace "2" "2" rewrite "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))" )"1" replace "1" "#(1 + x!1) o p1!2" )"1" "1" "1" "1" "1" rewrite "1" rewrite "1" "1" rewrite nil nil ))nil ))nil )"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "2" "2" "2" replace "2" rewrite "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" "2" rewrite "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"5" case "app2_var!1`seq(x!1) = subtermOF(s!1, #(1 + x!1))" )"1" replace "1" "1" replace "1" rewrite "1" rewrite nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "app2_var!1`seq(x!1) = subtermOF(s!1, #(x!1 + 1))" )"1" replace -1)"1" "1" rewrite "1" rewrite nil nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "#(x!1 + 1)" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand subtermOF)"2" "2" "1" expand "#" )"1" (assert ) nil nil ))nil )"2" expand finseq_appl)"2" case "rest( #(1 + x!1)) = empty_seq" )"1" "1" rewrite "1" expand *"1" expand "#" 2)"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "#(1 + x!1)" )"2" expand "#" -1 3)"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"2" "2" expand subtermOF)"2" "2" "1" expand "#" )"1" (assert ) nil nil ))nil )"2" expand finseq_appl)"2" case "rest( #(1 + x!1)) = empty_seq" )"1" "1" rewrite "1" expand *"1" expand "#" 2)"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "#(1 + x!1)" )"2" expand "#" -1 3)"2" "2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred p!1)"2" (hide-all-but (-2 1 2))"2" (expand positionsOF)"2" (assert )"2" (expand only_empty_seq)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (hide -1 -2)"3" (lemma app_term)"3" (inst -1 p!1 p1!1 t!1) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (hide -1 -2)"4" (lemma app_term)"4" (inst -1 p!1 p1!1 s!2) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil subterm nil )"symbol" subterm nil )"{args: finite_sequence[term[variable, symbol, arity]] | " subterm nil) "term[variable, symbol, arity]" subterm nil )nil seq_extras "structures/" )nil subterm nil )"set" sets nil )"bool" sets nil )"posint" nil )"finite_sequence[T]" set2seq "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"(total_order?[real])" nil )"finseq" seq_extras "structures/" )"(app?)" subterm nil )"below[args(s!1)`length]" subterm nil )"posint" nil )"finseq" finite_sequences nil )nil seq_extras "structures/" )"nonneg_int" nil )nil seq_extras "structures/" )nil subterm nil )"(strict_total_order?[real])" real_props nil )nil subterm nil )"{p: position | AND " subterm nil) "{p: position | AND " subterm nil) nil subterm nil )nil subterm nil )nil finite_sequences nil )"{p: position | AND " subterm nil) "position[variable, symbol, arity]" subtermnil )nil positions nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil subterm nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "positions" positions nil )"[variable -> (vars?)]" term_adt nil )"[term -> boolean]" term_adt nil )nil term_adt nil )nil subterm nil )nil subterm 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]" subterm nil )"finseq" finite_sequences nil )nil finite_sequences nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[(app?) -> symbol]" term_adt nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"[bool, bool -> bool]" booleans nil )"bool" positions nil )"[T, T -> boolean]" equalities nil )nil positions nil )"term" subterm nil )"bool" positions nil )"[term -> boolean]" term_adt nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.342Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
