Quelle replacement.prf
Sprache: Lisp
(replacementnil 3389903609"" (skosimp*)"" (lemma "not_var" )"" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1" )"1" (typepred "p!1" )"1" (assert )"1" "finite_sequences_extras[posnat].seq_first_rest" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil nil ))nil 3389903609"" (skosimp*)"" (typepred "p!1" )"" (expand "positionsOF" )"" (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" (hide -1) (("3" (rewrite "empty_0" ) nil nil )) nil ))nil )"4" (expand "only_empty_seq" )"4" (hide -1) (("4" (rewrite "empty_0" ) nil nil )) nil ))nil )"5" (assert ) nil nil )"6" (replaces -2)"6" (expand * "union" "member" )"6" (prop)"1" (expand "only_empty_seq" )"1" (rewrite "empty_0" ) nil nil )) nil )"2" (expand "IUnion" )"2" (skolem * "j" )"2" (expand "catenate" )"2" (skolem * "p1" )"2" (flatten)"2" (hide -1)"2" "fsepn.seq_first_rest" )"2" "2" assert )"2" replace -1 -2)"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 ))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]" replacement 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 replacement nil )nil replacement nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans 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 )"bool" reals nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"positions" positions nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )"int" integers nil )"(total_order?[real])" nil )"positions" positions nil )nil finite_sequences nil )nil seq_extras "structures/" ))nil ))nil 3389903609"" (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" (lemma "fsepn.first_equal" )"2" "q!1" "y1" "i!1" "i1" )"2" "1" "1" "1" (replaces -3) nil nil ))nil ))nil )"2" "fsepn.seq_first_rest" )"2" "2" (assert ) 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]" replacement 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 replacement nil )nil replacement 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/" )"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 3389903609"" (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]" replacement nil )nil replacement nil )nil replacement nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil seq_extras "structures/" ))nil ))nil 3389903609 ("" (termination-tcc) nil nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil nat_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"positions" positions nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )"[below[length(fs)] -> T]" finite_sequencesnil )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 )"T" seq_extras "structures/" )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"finseq" seq_extras "structures/" )nil term_adt nil )"[symbol -> nat]" replacement nil )nil naturalnumbers nil )nil replacement nil )nil replacement nil )replace const-decl "finseq" seq_extras "structures/" )"posint" nil ))nil ))nil 3389903609 ("" (termination-tcc) nil nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )nil nat_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )"[below[length(fs)] -> T]" finite_sequencesnil )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 )"T" seq_extras "structures/" )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"finseq" seq_extras "structures/" )nil term_adt nil )"[symbol -> nat]" replacement nil )nil naturalnumbers nil )nil replacement nil )nil replacement nil )replace const-decl "finseq" seq_extras "structures/" )"posint" nil ))nil ))nil 3516386077"" (skosimp*)"" (lemma "not_var" )"" (inst -1 "first(p!1)" "p!1" "rest(p!1)" "s!1" )"1" (typepred "p!1" )"1" (assert )"1" (lemma "seq_extras[posnat].seq_first_rest" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"[symbol -> nat]" replacement 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 replacement nil )nil replacement nil )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )nil finite_sequences nil )"boolean" notequal nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil term_adt nil )nil positions nil )"positions" positions nil )"term[variable, symbol, arity]" replacementnil )nil positions nil )"positions?[variable, symbol, arity](s!1)" nil ))nil ))nil 3432995634"" (measure-induct+ "length(p)" "p" )"" (skeep)"" (name-replace "rp" "replaceTerm(s, t, x!1)" :hide? nil )"" (expand "replaceTerm" -1)"" (lift-if)"" (prop)"1" (hide -3)"1" (expand "positionsOF" 1)"1" (lift-if)"1" (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)"3" (expand "only_empty_seq" )"3" (rewrite "empty_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (copy -1)"2" (decompose-equality -1)"2" (hide (-1 -2))"2" (expand "positionsOF" 2)"2" (lift-if)"2" (prop)"1" (assert ) nil nil )"2" (expand "replace" -2)"2" (lift-if)"2" "1" "1" expand "positionsOF" )"1" "1" (prop) nil nil ))nil ))nil ))nil )"2" "2" "2" expand "positionsOF" -4)"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand * "union" "member" )"3" (prop)"3" expand "only_empty_seq" )"3" expand "finseq_appl" )"3" "rest(x!1)" )"3" "args(s)(first(x!1) - 1)" "t" )"1" "1" "1" expand "IUnion" )"1" "first(x!1)" )"1" expand "catenate" )"1" "rest(x!1)" )"1" "1" expand "member" )"1" replace "1" "1" "fset.nth_x" )"1" "args(s)" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))" "first(x!1) - 1" )"1" expand "finseq_appl" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "fsepn.seq_first_rest" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "replace" )"2" "2" "1" expand "positionsOF" )"1" "1" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" "2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" expand *"union" "member" )"2" "2" expand "IUnion" )"2" "i1" )"2" expand "catenate" )"2" "y1" )"2" expand "member" )"2" "2" "2" "i1" )"2" "fsepn.first_equal" )"2" "rest(x!1)" "y1" "first(x!1)" "i1" )"2" assert )"2" "2" "fsepn.seq_first_rest" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" -1)"2" "2" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" nil nil ))nil )"3" expand *"union" "member" )"3" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "IUnion" )"2" "i1" )"2" expand "catenate" )"2" "y1" )"2" expand "member" )"2" "2" "fsepn.first_equal" )"2" "rest(x!1)" "y1" "first(x!1)" "i1" )"2" "1" assert )nil nil )"2" "2" "fsepn.seq_first_rest" )"2" "x!1" )"2" assert )"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 ))nil ))nil )"3" "3" rewrite "length_rest" )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sequences nil )nil seq_extras "structures/" )"positions" positions nil )"set" sets nil )"bool" sets nil )"(total_order?[real])" nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[term -> boolean]" term_adt nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) replace const-decl "finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"position[variable, symbol, arity]" nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" reals nil )"term[variable, symbol, arity]" replacementnil )nil IUnion_extra nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"positions" positions nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"set[T]" indexed_sets nil )"[T, T -> boolean]" equalities nil )"term" replacement nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3432997519"" (measure-induct+ "length(p)" "p" )"" (skeep)"" (expand "positionsOF" -3)"" (lift-if)"" (prop)"1" (hide -3)"1" (expand "only_empty_seq" )"1" (lemma "fsepn.empty_0" )"1" (inst -1 "x!1" )"1" (assert )"1" (expand "replaceTerm" )"1" (replaces -5)"1" (replaces -3)"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (expand "only_empty_seq" )"2" (lemma "fsepn.empty_0" )"2" (inst -1 "x!1" )"2" (assert )"2" (expand "replaceTerm" )"2" (replaces -5)"2" (replaces -3)"2" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand * "union" "member" )"3" (prop)"1" (hide -2)"1" (expand "only_empty_seq" )"1" (lemma "fsepn.empty_0" )"1" (inst -1 "x!1" )"1" (assert )"1" (expand "replaceTerm" )"1" (replaces -5)"1" "1" "1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "rp" "replaceTerm(s, t, x!1)" :hide?nil )"2" (expand "replaceTerm" -1)"2" (lift-if)"2" (prop)"1" (hide (-3 -4))"1" (rewrite "empty_0" )"1" (replaces -1)"1" "1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "IUnion" )"2" (skolem * "i1" )"2" (expand "catenate" )"2" "y1" )"2" expand "member" )"2" "2" "rest(x!1)" )"2" "q" "args(s)(first(x!1) - 1)" "t" )"1" rewrite "length_rest" )"1" assert )"1" "fsepn.seq_first_rest" )"1" "1" assert )"1" replace -1 -4)"1" "fsepn.first_equal" )"1" "rest(x!1)" "y1" "first(x!1)" "i1" )"1" assert )"1" "1" "1" replace "1" replace "1" "1" "1" "1" "1" expand "replace" "1" "1" "1" expand "positionsOF" "1" "1" assert )nil nil )"2" "2" expand *"union" "member" )"2" "2" expand "IUnion" )"2" "first(x!1)" )"1" expand "catenate" )"1" "rest(x!1) o q" )"1" "1" expand "member" )"1" replace "1" "fset.nth_x" )"1" "args(s)" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))" "first(x!1) - 1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "fsepn.add_first_compo" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "2" "i1" )"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 )"2" (assert ) 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 )"[T, T -> boolean]" equalities nil )"set[T]" indexed_sets nil )"positions" positions nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )replace const-decl "finseq" seq_extras "structures/" )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"term[variable, symbol, arity]" replacementnil )nil seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil IUnion_extra nil )"[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 )"position[variable, symbol, arity]" nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"positions" positions nil )"finseq" finite_sequences nil )nil finite_sequences nil )"term" replacement 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]" replacement nil )nil replacement nil )nil replacement 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 3432999380"" (measure-induct+ "length(q)" "q" )"" (skeep)"" (name-replace "rp" "replaceTerm(s, t, p)" :hide? nil )"" (case "first(x!1)=first(p)" )"1" (expand "positionsOF" 1)"1" (lift-if)"1" (prop)"1" (lemma "replace_preserv_pos" )"1" (inst?)"1" (assert )"1" (replaces -4)"1" (hide-all-but (-1 -2 -7))"1" (expand "positionsOF" )"1" (expand "only_empty_seq" )"1" expand "parallel" )"1" expand "<=" )"1" "1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "replace_preserv_pos" )"2" (inst?)"2" (assert )"2" (replaces -4)"2" (hide-all-but (-1 -2 -7))"2" (expand "positionsOF" )"2" (expand "only_empty_seq" )"2" expand "parallel" )"2" expand "<=" )"2" "2" "2" "x!1" )"2" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand * "union" "member" "only_empty_seq" )"3" (prop)"3" (expand "IUnion" )"3" (inst 3 "first(p)" )"1" (expand "catenate" )"1" (inst 3 "rest(x!1)" )"1" (expand "member" )"1" "1" expand "finseq_appl" )"1" expand "replaceTerm" -2)"1" "1" "1" "1" expand * "parallel" "<=" )"1" "1" rewrite "empty_0" )"1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -3 2 rl)"2" "fset.nth_x" )"2" "RT" "replaceTerm(args(s)(first(p) - 1), t, rest(p))" )"1" "args(s)" "RT" "first(p) - 1" )"1" expand "finseq_appl" )"1" "1" expand "RT" )"1" "rest(x!1)" )"1" "rest(p)" "args(s)(first(p) - 1)" "t" )"1" rewrite "length_rest" )"1" "rest_of_positions" )"1" "x!1" "s" )"1" "rest_of_positions" )"1" "p" "s" )"1" "1" expand "finseq_appl" )"1" nil nil ))nil )"2" rewrite "rest_parallel" )"2" "2" "2" rewrite "empty_0" )nil nil ))nil ))nil ))nil )"3" "3" rewrite "empty_0" )nil nil ))nil )"4" "4" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "empty_0" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1 1 rl)"2" "2" rewrite "seq_first_rest" )"2" "2" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 1 rl)"2" (typepred "args(rp)" )"2" (decompose-equality -3)"2" "2" expand "replaceTerm" -3)"2" "2" "1" "1" expand * "parallel" "<=" )"1" "1" rewrite "empty_0" )"1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" nil nil ))nil )"2" expand "only_empty_seq" )"2" nil nil ))nil )"3" expand *"union" "member" "only_empty_seq" )"3" "3" expand "IUnion" )"3" "j" )"3" expand "catenate" )"3" "y" )"3" expand "member" )"3" "3" "j" )"3" "3" "fsepn.seq_first_rest" )"3" "x!1" )"3" "1" "1" "fsepn.first_equal" )"1" "rest(x!1)" "y" "first(x!1)" "j" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "parallel" )"2" (expand "<=" )"2" (prop)"2" (expand "positionsOF" (-3 4))"2" (lift-if)"2" (prop)"1" (hide-all-but (-2 6))"1" (expand "only_empty_seq" )"1" (replaces -1)"1" (inst 1 "p" )"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 7))"2" (expand "only_empty_seq" )"2" (replaces -1)"2" (inst 1 "p" )"2" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil )"3" (lemma "replace_preserv_pos" )"3" (inst?)"3" (assert )"3" (replaces -4)"3" "3" expand "positionsOF" )"3" expand "only_empty_seq" )"3" "3" "x!1" )"3" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (lemma "replace_preserv_pos" )"4" (inst?)"4" (assert )"4" (hide-all-but (-1 -2 6))"4" expand "positionsOF" )"4" expand "only_empty_seq" )"4" "4" "x!1" )"4" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (expand * "union" "member" "only_empty_seq" )"5" (prop)"5" (expand "IUnion" )"5" (skolem * "i1" )"5" "i1" )"1" expand "catenate" )"1" "y" )"1" "y" )"1" expand "member" )"1" "1" "args(rp)(i1 - 1) = args(s)(i1 - 1)" )"1" "1" expand "replaceTerm" )"1" "1" "1" "1" rewrite "empty_0" )"1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "finseq_appl" )"2" replace "2" expand "replace" )"2" "2" "1" expand "finseq_appl" )"1" nil nil ))nil )"2" "2" "fsepn.seq_first_rest" )"2" "x!1" )"2" "1" "1" "fsepn.first_equal" )"1" "rest(x!1)" "y" "first(x!1)" "i1" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil )"3" expand "finseq_appl" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "args(rp)" )"2" "2" "2" expand "replaceTerm" -3)"2" "2" "1" "1" rewrite "empty_0" )"1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-5 1))"3" (expand "parallel" )"3" (expand "<=" )"3" (prop)"3" (rewrite "empty_0" )"3" (replaces -1)"3" (inst 1 "x!1" )"3" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but (-5 1))"4" (expand "parallel" )"4" (expand "<=" )"4" (prop)"4" (rewrite "empty_0" )"4" (replaces -1)"4" (inst 2 "p" )"4" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sequences nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"[(vars?) -> variable]" term_adt nil )"[term -> boolean]" term_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )NOT const-decl "[bool -> bool]" booleans nil )"positions" positions nil )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )replace const-decl "finseq" seq_extras "structures/" )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "int" integers nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil positions nil )nil positions nil )"term[variable, symbol, arity]" replacementnil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )nil IUnion_extra nil )"term[variable, symbol, arity]" replacementnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"position[variable, symbol, arity]" nil )"bool" reals nil )"(total_order?[real])" nil )nil replacement nil )"positions" positions nil )"bool" positions nil )nil seq_extras "structures/" )"upto?[position[variable, symbol, arity]](length(args(s)))" nil )"term[variable, symbol, arity]" replacementnil )"[T, T -> boolean]" equalities nil )"term" replacement nil )nil 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 )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433002525"" (induct "s" )"1" (skeep)"1" (skeep)"1" (expand "positionsOF" (-1 1))"1" (expand "only_empty_seq" )"1" (expand "replaceTerm" )"1" (rewrite "empty_0" )"1" (assert )"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" )"3" (prop)"1" (expand "only_empty_seq" )"1" (propax) nil nil )) nil )"2" (expand "IUnion" )"2" "2" expand "catenate" )"2" "2" expand "member" )"2" expand "finseq_appl" )"2" expand * "parallel" "<=" )"2" "2" "add_first(i!1, x!1)" )"2" "2" "2" rewrite "empty_o_seq" )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" (skeep)"2" (skeep)"2" (expand "positionsOF" 1)"2" (prop)"1" (hide -2)"1" (expand "positionsOF" -2)"1" (assert )"1" (expand "only_empty_seq" )"1" (expand "replaceTerm" )"1" (rewrite "empty_0" )"1" (assert )"1" (expand "positionsOF" )"1" (lift-if)"1" "1" expand "only_empty_seq" )"1" (propax) nil nil ))nil )"2" expand "only_empty_seq" )"2" (propax) nil nil ))nil )"3" expand * "union" "member" )"3" expand "IUnion" )"3" "3" expand "catenate" )"3" "3" expand "member" )"3" expand "finseq_appl" )"3" expand *"parallel" "<=" )"3" "3" "add_first(i!1, x!1)" )"3" "3" "3" rewrite "empty_o_seq" )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" (expand * "union" "member" )"2" (flatten)"2" (expand "IUnion" )"2" (expand "finseq_appl" )"2" (expand "positionsOF" -3)"2" (lift-if)"2" (prop)"2" (expand * "union" "member" )"2" (assert )"2" expand "IUnion" )"2" "2" expand "catenate" )"2" "2" expand "member" )"2" expand "finseq_appl" )"2" expand "positionsOF" -4)"2" expand *"union" "member" )"2" "1" expand *"parallel" "<=" )"1" "1" "1" expand "only_empty_seq" )"1" "add_first(i!1, x!1)" )"1" "1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "IUnion" )"2" "2" expand "catenate" )"2" "2" expand "member" )"2" expand "finseq_appl" )"2" "i!1 = i!2" )"1" "i!2 - 1" )"1" "x!2" "x!1" "t" )"1" assert )"1" "1" "i!2" )"1" "x!1" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "replaceTerm" "2" expand "finseq_appl" )"2" "1" "1" nil nil ))nil )"2" expand "replace" )"2" "fsepn.first_add" )"2" "x!2" "i!2" )"2" replace "2" assert )"2" "fsepn.rest_add_first" )"2" "x!2" "i!2" )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "rest_parallel" )"3" "p" "q" )"3" "3" "fsepn.first_add" )"3" "3" "x!2" "i!2" )"3" "x!1" "i!2" )"3" "fsepn.rest_add_first" )"3" "3" "x!2" "i!2" )"3" "x!1" "i!2" )"3" replace "3" replace "3" assert )"3" "1" "1" expand *"parallel" "<=" )"1" "1" rewrite "empty_0" )"1" "add_first(i!2, x!1)" )"1" "1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "empty_0" )"2" expand "only_empty_seq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"1" "x!1" )"1" assert )"1" "args(replaceTerm(app(app1_var, app2_var), t, p))`seq(i!1 - 1) = app2_var`seq(i!1 - 1)" )"1" "1" expand "replaceTerm" "1" "1" "1" "1" expand *"parallel" "<=" )"1" "1" rewrite "empty_0" )"1" "add_first(i!1, x!1)" )"1" "1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "fsepn.first_add" )"2" "x!2" "i!2" )"2" "fsepn.rest_add_first" )"2" "x!2" "i!2" )"2" replace "2" "2" "2" expand "replace" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" expand "replaceTerm" "2" "2" rewrite "empty_0" )"2" "1" "1" expand *"parallel" "<=" )"1" "1" "add_first(i!1, x!1)" )"1" "1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "replace" )"2" 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 )"posint" nil )"posint" nil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )replace const-decl "finseq" seq_extras "structures/" )nil positions nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"symbol" replacement nil )"{args: finite_sequence[term[variable, symbol, arity]] | " replacement nil) "term[variable, symbol, arity]" replacementnil )"position[variable, symbol, arity]" nil )"upto? " nil )NOT const-decl "[bool -> bool]" booleans nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"positions" positions nil )"bool" 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 )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )nil seq_extras "structures/" )nil finite_sequences nil )"positions" positions nil )nil term_adt nil )nil replacement nil )nil replacement 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]" replacement nil )"bool" positions nil )"term" replacement nil )nil positions nil )"positions" positions nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil ))nil 3433002823"" (skosimp*)"" (lemma "replace_preserv_pos" )"" (inst -1 "p!1" "s!1" "t!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil replacement nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433002825"" (measure-induct+ "length(p)" "p" )"1" (skeep)"1" (expand "subtermOF" 1)"1" (lift-if)"1" (prop)"1" (expand "replaceTerm" 1) (("1" (assert ) nil nil ))nil )"2" (expand "replaceTerm" 2)"2" (lift-if)"2" (prop)"2" (lemma "fset.nth_x" )"2" "args(s)" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))" "first(x!1) - 1" )"1" (replaces -1)"1" (inst -1 "rest(x!1)" )"1" (inst -1 "args(s)(first(x!1) - 1)" "t" )"1" (prop)"1" "1" expand "positionsOF" -1)"1" "1" "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" "1" expand "only_empty_seq" )"1" rewrite "empty_0" )nil nil ))nil )"2" expand "IUnion" )"2" "i1" )"2" expand "catenate" )"2" "y1" )"2" "2" expand "member" )"2" "fsepn.seq_first_rest" )"2" "x!1" )"2" assert )"2" "2" "fsepn.first_equal" )"2" "rest(x!1)" "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 )"2" (rewrite "length_rest" ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-2 -3 2))"2" (lemma "replace_preserv_pos" )"2" (inst -1 "y!1" "s!1" "t!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"3" (hide 2)"3" (lemma "replace_preserv_pos" )"3" (inst -1 "p!1" "s!1" "t!1" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )nil replacement nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil finite_sequences nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"position[variable, symbol, arity]" nil )"[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 )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil seq_extras "structures/" )"positions" positions nil )nil IUnion_extra nil )"bool" reals nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"positions" positions nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"term" subterm nil )"[T, T -> boolean]" equalities nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil positions nil )"term" replacement nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433002925"" (measure-induct+ "length(p)" "p" )"" (skeep)"" (expand "replaceTerm" 1)"" (lift-if)"" (prop)"1" (expand "subtermOF" 1) (("1" (assert ) nil nil )) nil )"2" (decompose-equality 2)"2" (expand "subtermOF" 1)"2" (inst -1 "rest(x!1)" )"2" (inst -1 "args(s)(first(x!1) - 1)" )"2" (lemma "fsepn.length_rest" )"2" (inst?)"2" (lemma "rest_of_positions" )"2" (inst?)"2" (assert )"2" replace -3 1)"2" "fset.replace_nth" )"2" (inst?) 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 )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil finite_sequences nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"position[variable, symbol, arity]" nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[(app?) -> symbol]" term_adt nil )replace const-decl "finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"finseq" seq_extras "structures/" )nil term_adt nil )"[term -> boolean]" term_adt nil )nil seq_extras "structures/" )nil positions nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"term" subterm nil )"term" replacement nil )nil positions nil )"[T, T -> boolean]" equalities nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )nil term_adt nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003094"" (skosimp*)"" (lemma "replace_compose_pos" )"" (inst -1 "p!1" "q!1" "s!1" "t!1" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil replacement nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003095"" (skeep)"" (lemma "pos_subterm" )"" (inst -1 "p" "q" "replaceTerm(s, t, p)" )"" (prop)"1" (lemma "subterm_of_replace" )"1" (inst -1 "p" "s" "t" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (lemma "replace_compose_pos" )"2" (inst -1 "p" "q" "s" "t" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[symbol -> nat]" replacement 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 replacement nil )nil replacement nil )nil subterm nil )nil replacement nil )nil replacement nil )"term" replacement nil )nil positions nil )"positions" positions nil )nil positions nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil 3433003239"" (measure-induct+ "length(p)" "p" )"1" (skeep)"1" (case "length(x!1) = 0" )"1" (hide (-2 -3 -4))"1" (lemma "fsepn.empty_0" )"1" (inst?)"1" (assert )"1" (expand "replaceTerm" 1 (2 3))"1" (replaces -1)"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replaceTerm" 2 1)"2" (lift-if)"2" (prop)"1" (hide-all-but (-1 2))"1" (rewrite "empty_0" -1)"1" (lemma "fsepn.seq_empty" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (rewrite "first_compo" )"2" (rewrite "rest_compo" )"2" (expand "replaceTerm" 2 5)"2" (lift-if)"2" (prop)"2" (decompose-equality 2)"1" (expand "replaceTerm" 1)"1" (propax) nil nil )) nil )"2" (expand "replaceTerm" 1 2)"2" (lemma "fset.nth_x" )"2" "Rtns" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))" )"2" "args(s)" "Rtns" "first(x!1) - 1" )"2" "2" "rest(x!1)" )"2" "q" "r" "args(s)(first(x!1) - 1)" "t" )"2" rewrite "length_rest" )"2" "1" expand "Rtns" )"1" "1" "RTR" "replaceTerm(args(s)(first(x!1) - 1), replaceTerm(t, r, q), rest(x!1))" )"1" expand "replaceTerm" "1" "fset.replace_n2" )"1" "args(s)" "RTR" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1))" )"1" "1" "first(x!1) - 1" )nil nil )"2" "2" expand "positionsOF" )"2" "2" assert )"2" expand "only_empty_seq" )"2" rewrite "empty_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rest_of_positions" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-3 -4 2))"2" (lemma "replace_compose_pos" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (lemma "replace_compose_pos" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )nil replacement nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"(total_order?[real])" nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[(app?) -> symbol]" term_adt nil )replace const-decl "finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"finseq" seq_extras "structures/" )nil term_adt nil )"[term -> boolean]" term_adt nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil positions nil )"term[variable, symbol, arity]" replacementnil )nil seq_extras "structures/" )"positions" positions nil )"int" integers nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )"[T, T -> boolean]" equalities nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil positions nil )"term" replacement nil )nil finite_sequences nil )"finseq" finite_sequences nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003327"" (skosimp*)"" (lemma "replace_preserv_pos" )"" (inst -1 "p!1 o q!1" "s!1" "t!1" )"" (assert )"" (lemma "closed_positions" )"" "p!1" "p!1 o q!1" "replaceTerm(s!1, t!1, o[posnat](p!1, q!1))" )"" (assert )"" (expand "<=" ) (("" (inst 1 "q!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil replacement nil )nil positions nil )"positions" positions nil )nil positions nil )"term" replacement nil )"bool" positions nil )nil positions nil )nil term_adt nil )"finseq" finite_sequences nil )nil finite_sequences nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003327"" (skosimp*)"" (lemma "pos_ax" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil )"[symbol -> nat]" replacement 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 replacement nil )nil replacement nil )nil positions nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3433003327"" (skosimp*)"" (lemma "pos_subterm_ax" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )"[symbol -> nat]" replacement 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 replacement nil )nil replacement nil )nil subterm nil )nil term_adt nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil ))nil ))nil 3433003328"" (measure-induct+ "length(p)" "p" )"1" (skeep)"1" (expand "subtermOF" 1)"1" (lift-if)"1" (prop)"1" (rewrite "empty_0" )"1" (replace -1 1)"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil )"2" (expand "replaceTerm" 2 1)"2" (lift-if)"2" (prop)"1" (hide-all-but (-1 2))"1" (rewrite "empty_0" )"1" (lemma "fsepn.seq_empty" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "fsepn.first_compo" )"2" (inst?)"2" (assert )"2" (replaces -1)"2" (lemma "fsepn.rest_compo" )"2" (inst?)"2" assert )"2" "2" "RT" "replaceTerm(args(s)(first(x!1) - 1), t, rest(x!1) o q)" )"2" "fset.nth_x" )"2" "args(s)" "RT" "first(x!1) - 1" )"2" "2" expand "RT" )"2" "rest(x!1)" )"2" "q" "args(s)(first(x!1) - 1)" "t" )"2" "1" "fsepn.rest_compo" )"1" "x!1" "q" )"1" "1" replace "1" "1" "rest_of_positions" )"1" "x!1 o q" "s" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_rest" )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 1))"2" (rewrite "pos_subterm_ax" ) nil nil )) nil )"3" (hide-all-but (-1 1))"3" (lemma "pos_ax" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (hide-all-but (-1 1))"4" (lemma "replace_preserv_pos" )"4" (inst -1 "y!1 o q!1" "s!1" "t!1" )"4" (assert )"4" (lemma "pos_ax" )"4" "y!1" "q!1" "replaceTerm(s!1, t!1, y!1 o q!1)" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"5" (lemma "pos_subterm_ax" )"5" (inst -1 "p!1" "q!1" "s!1" ) (("5" (assert ) nil nil )) nil ))nil )"6" (lemma "pos_ax" )"6" (inst -1 "p!1" "q!1" "s!1" ) (("6" (assert ) nil nil )) nil ))nil )"7" (hide 2)"7" (lemma "replace_preserv_pos" )"7" (inst -1 "p!1 o q!1" "s!1" "t!1" )"7" (assert )"7" (lemma "pos_ax" )"7" "p!1" "q!1" "replaceTerm(s!1, t!1, p!1 o q!1)" )"7" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil replacement nil )nil positions nil )nil subterm nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil positions nil )nil seq_extras "structures/" )"term[variable, symbol, arity]" replacementnil )"finseq" seq_extras "structures/" )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[(app?) -> symbol]" term_adt nil )nil finite_sequences nil )"[term -> boolean]" term_adt nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )nil seq_extras "structures/" )"int" integers nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities 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 positions nil )"term" replacement nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003587"" (measure-induct+ "length(p)" "p" )"1" (skeep)"1" (expand "replaceTerm" 1)"1" (lift-if)"1" (prop)"1" (hide-all-but (-1 2))"1" (rewrite "empty_0" )"1" (lemma "fsepn.seq_empty" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (decompose-equality 2)"2" (lemma "fsepn.first_compo" )"2" (inst?)"2" (assert )"2" (replace -1 1)"2" (lemma "fsepn.rest_compo" )"2" (inst?)"2" (assert )"2" (replace -1 1)"2" "z" "args(s)(first(x!1) - 1)" )"2" "w" "replaceTerm(z, t, rest(x!1) o q)" )"2" "fset.nth_x" )"2" "args(s)" "w" "first(x!1) - 1" )"2" "2" "fset.replace_n2" )"2" "args(s)" "replaceTerm(w, r, rest(x!1))" "w" )"2" "1" "first(x!1) - 1" )"1" "1" "rest(x!1)" )"1" expand * "w" "z" )"1" "q" "r" "args(s)(first(x!1) - 1)" "t" )"1" "1" assert )nil nil )"2" replace "2" "2" "rest_of_positions" )"2" "x!1 o q" "s" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "fsepn.length_rest" )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" "fsepn.seq_empty" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" expand "only_empty_seq" )"2" "fsepn.seq_empty" )"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 )"2" (hide-all-but (-1 1))"2" (lemma "pos_ax" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (hide (-2 -3 2))"3" (lemma "replace_preserv_pos" )"3" (inst -1 "y!1 o q!1" "s!1" "t!1" )"3" (assert )"3" (lemma "pos_ax" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"4" (lemma "pos_ax" ) (("4" (inst?) (("4" (assert ) nil nil )) nil ))nil )"5" (lemma "replace_preserv_pos" )"5" (inst -1 "p!1 o q!1" "s!1" "t!1" )"5" (assert )"5" (lemma "pos_ax" )"5" (inst?) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil replacement nil )nil positions nil )"(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]" nil )"position[variable, symbol, arity]" nil )nil finite_sequences nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) "[(app?) -> symbol]" term_adt nil )replace const-decl "finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"finseq" seq_extras "structures/" )nil term_adt nil )"[term -> boolean]" term_adt nil )nil seq_extras "structures/" )"term[variable, symbol, arity]" replacementnil )"term[variable, symbol, arity]" replacementnil )nil positions nil )nil seq_extras "structures/" )"positions" positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities 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 positions nil )"term" replacement nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003734"" (skosimp*)"" (lemma "replace_preserv_parallel_pos" )"" (inst -1 "p!1" "q!1" "s!1" "t!1" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil replacement nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003735"" (measure-induct+ "length(q)" "q" )"1" (skeep)"1" (case "first(p)=first(x!1)" )"1" (expand "subtermOF" 1)"1" (lift-if)"1" (prop)"1" (hide-all-but (-1 -6))"1" (expand * "parallel" "<=" )"1" (prop)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (inst 2 "p" )"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replaceTerm" 2)"2" (lift-if)"2" (prop)"1" (hide-all-but (-1 -6))"1" (expand * "parallel" "<=" )"1" (prop)"1" (rewrite "empty_0" )"1" (replaces -1)"1" "x!1" )"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 2)"2" "RT" "replaceTerm(args(s)(first(x!1) - 1), t, rest(p))" )"1" (lemma "fset.nth_x" )"1" "args(s)" "RT" "first(x!1) - 1" )"1" (replaces -1)"1" expand "RT" )"1" "rest(x!1)" )"1" "rest(p)" "args(s)(first(x!1) - 1)" "t" )"1" rewrite "length_rest" )"1" "1" replace -1 1 rl)"1" "rest_of_positions" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "rest_of_positions" )"2" "2" (assert ) nil nil ))nil ))nil )"3" "rest_parallel" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand * "parallel" "<=" )"2" (prop)"2" (expand "subtermOF" )"2" (lift-if)"2" (prop)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (inst 4 "p" )"1" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil )"2" "args(replaceTerm(s, t, p))(first(x!1) - 1) = args(s)(first(x!1) - 1)" )"1" (hide 3)"1" (expand "replaceTerm" )"1" (lift-if)"1" (prop)"1" rewrite "empty_0" )"1" "1" "x!1" )"1" rewrite "empty_o_seq" )nil nil ))nil ))nil ))nil )"2" expand "finseq_appl" )"2" expand "replace" )"2" "2" "1" expand "finseq_appl" )"1" (propax) nil nil ))nil )"2" (assert ) nil nil )"3" expand "finseq_appl" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-4 1))"3" (expand * "parallel" "<=" )"3" (prop)"3" (rewrite "empty_0" )"3" (replaces -1)"3" (inst 2 "p" )"3" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but (-4 1))"4" (expand * "parallel" "<=" )"4" (prop)"4" (rewrite "empty_0" )"4" (replaces -1)"4" (inst 1 "x!1" )"4" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-4 -5 2))"2" (lemma "replace_preserv_parallel_pos" )"2" (inst -1 "p!1" "y!1" "s!1" "t!1" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (hide 2)"3" (lemma "replace_preserv_parallel_pos" )"3" (inst -1 "p!1" "q!1" "s!1" "t!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil )nil replacement nil )replace const-decl "finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"bool" positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil seq_extras "structures/" )nil positions nil )nil positions nil )"term[variable, symbol, arity]" replacementnil )"position[variable, symbol, arity]" nil )"int" integers nil )"[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 )"finseq" seq_extras "structures/" )"(total_order?[real])" nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil finite_sequences nil )"term" subterm nil )"[T, T -> boolean]" equalities nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"bool" positions nil )nil positions nil )"term" replacement nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003908"" (skosimp*)"" (lemma "replace_preserv_parallel_pos" )"" (inst -1 "q!1" "p!1" "s!1" "r!1" )"" (assert ) (("" (rewrite "parallel_comm" ) nil nil )) nil ))nil ))nil ))nil )nil replacement nil )nil positions nil )nil term_adt nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3433003909"" (measure-induct+ "length(q)" "q" )"1" (skeep)"1" (case "first(p)=first(x!1)" )"1" (expand "replaceTerm" 1)"1" (lift-if)"1" (lift-if)"1" (prop)"1" (hide-all-but (-2 -7))"1" (expand * "parallel" "<=" )"1" (prop)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (inst 2 "p" )"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -6))"2" (expand * "parallel" "<=" )"2" (prop)"2" (rewrite "empty_0" )"2" (replaces -1)"2" (inst 2 "p" )"2" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-1 -6))"3" (expand * "parallel" "<=" )"3" (prop)"3" (rewrite "empty_0" )"3" (replaces -1)"3" (inst 1 "x!1" )"3" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (decompose-equality 2)"4" (replace -1 1)"4" "w" "replaceTerm(args(s)(first(x!1) - 1), t, rest(p))" )"4" "w1" "replaceTerm(args(s)(first(x!1) - 1), r, rest(x!1))" )"4" (lemma "fset.nth_x" )"4" "args(s)" "w" "first(x!1) - 1" )"4" (lemma "fset.nth_x" )"4" "args(s)" "w1" "first(x!1) - 1" )"4" case "length(args(s)) /= 0" )"1" assert )"1" "1" "1" "fset.replace_n2" )"1" "args(s)" "replaceTerm(w, r, rest(x!1))" "w" )"1" "fset.replace_n2" )"1" "args(s)" "replaceTerm(w1, t, rest(p))" "w1" )"1" assert )"1" "first(x!1) - 1" )"1" "first(x!1) - 1" )"1" "1" "1" "replaceTerm(w, r, rest(x!1)) = replaceTerm(w1, t, rest(p))" )"1" "1" "rest(x!1)" )"1" expand *"w" "w1" )"1" "rest(p)" "r" "args(s)(first(x!1) - 1)" "t" )"1" "1" "1" replace "1" "rest_of_positions" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "rest_of_positions" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "rest_parallel" )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "fsepn.length_rest" )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "positionsOF" )"2" "2" "1" expand "only_empty_seq" )"1" rewrite "empty_0" )nil nil ))nil )"2" expand "only_empty_seq" )"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 -1)"2" (expand * "parallel" "<=" )"2" (prop)"2" (expand "replaceTerm" )"2" (lift-if)"2" (lift-if)"2" (prop)"1" (rewrite "empty_0" -2)"1" (replaces -2)"1" (inst 4 "p" )"1" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil )"2" (hide (1 2 3))"2" (rewrite "empty_0" )"2" (replaces -1)"2" (inst 2 "p" )"2" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil )"3" (hide (1 2 3))"3" (rewrite "empty_0" )"3" (replaces -1)"3" (inst 1 "x!1" )"3" (rewrite "empty_o_seq" ) nil nil ))nil ))nil ))nil ))nil )"4" (decompose-equality 2)"4" (decompose-equality 1)"1" (expand "replace" )"1" (propax) nil nil )) nil )"2" (decompose-equality 1)"2" (expand "replace" )"2" "2" "2" "2" "1" expand "finseq_appl" )"1" "1" "1" (prop) nil nil ))nil ))nil ))nil )"2" expand "finseq_appl" )"2" "2" (assert ) nil nil ))nil ))nil )"3" expand "finseq_appl" )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil )"4" expand "finseq_appl" )"4" "4" (assert ) nil nil ))nil ))nil )"5" expand "finseq_appl" )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-4 1))"3" (expand * "parallel" "<=" )"3" (prop)"3" (rewrite "empty_0" )"3" (replaces -1)"3" (inst 2 "p" )"3" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but (-4 1))"4" (expand * "parallel" "<=" )"4" (prop)"4" (rewrite "empty_0" )"4" (replaces -1)"4" (inst 1 "x!1" )"4" (rewrite "empty_o_seq" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-4 -5 2))"2" (lemma "replace_preserv_parallel_pos" )"2" (inst -1 "y!1" "p!1" "s!1" "r!1" )"2" (assert ) (("2" (rewrite "parallel_comm" ) nil nil ))nil ))nil ))nil ))nil )"3" (hide (-4 -5 2))"3" (lemma "replace_preserv_parallel_pos" )"3" (inst -1 "p!1" "y!1" "s!1" "t!1" )"3" (assert ) nil nil )) nil ))nil ))nil )"4" (hide 2)"4" (lemma "replace_preserv_parallel_pos" )"4" (inst -1 "q!1" "p!1" "s!1" "r!1" )"4" (assert ) (("4" (rewrite "parallel_comm" ) nil nil ))nil ))nil ))nil ))nil )"5" (hide 2)"5" (lemma "replace_preserv_parallel_pos" )"5" (inst -1 "p!1" "q!1" "s!1" "t!1" )"5" (assert ) nil nil )) nil ))nil ))nil ))nil )nil positions nil )nil replacement nil )"(total_order?[real])" nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"position[variable, symbol, arity]" nil )"position[variable, symbol, arity]" nil )"finseq" seq_extras "structures/" )"[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" nil )"[below[length(fs)] -> T]" finite_sequencesnil )replace const-decl "finseq" seq_extras "structures/" )"[(app?) -> symbol]" term_adt nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " term_adt nil) nil finite_sequences nil )nil term_adt nil )"[term -> boolean]" term_adt nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"term[variable, symbol, arity]" replacementnil )"term[variable, symbol, arity]" replacementnil )nil positions nil )nil positions nil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"positions" positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"bool" positions nil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )nil term_adt nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"bool" positions nil )nil positions nil )"term" replacement nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 3414553266"" (induct "t" )"1" (skosimp*)"1" (expand * "subset?" "member" )"1" (skosimp*)"1" (typepred "p!1" )"1" (expand "positionsOF" -1)"1" (expand * "only_empty_seq" "replaceTerm" )"1" (rewrite "empty_0" )"1" (assert )"1" (typepred "x!1" )"1" (expand "V" )"1" (expand "positionsOF" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand * "subset?" "member" )"2" (skosimp*)"2" (expand "positionsOF" (-2 1))"2" (lift-if)"2" (prop)"1" (expand * "union" "member" ) (("1" (prop) nil nil ))nil )"2" (expand * "union" "member" ) (("2" (prop) nil nil ))nil )"3" (hide (-2 -3))"3" (expand "replaceTerm" 2)"3" (lift-if)"3" (prop)"1" (expand "replaceTerm" 3)"1" (lift-if)"1" (assert )"1" "x!1" )"1" expand "V" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replace" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (expand * "union" "member" )"4" (prop)"4" (expand "IUnion" )"4" (skosimp*)"4" (expand "catenate" )"4" (skosimp*)"4" (expand "member" )"4" expand "finseq_appl" )"4" "i!1" )"1" "x!3" )"1" "1" expand "replaceTerm" -1)"1" "1" "1" expand "replaceTerm" )"1" "1" "1" "x!1" )"1" expand "V" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "finseq_appl" )"2" expand "replace" )"2" "1" expand "finseq_appl" )"1" nil nil ))nil )"2" "i!1 - 1" )"2" "x!1" "rest(p!1)" )"1" "x!3" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "p!1" )"2" expand "positionsOF" "2" assert )"2" expand *"union" "member" )"2" "1" expand "only_empty_seq" )"1" rewrite "empty_0" )nil nil ))nil )"2" expand "IUnion" )"2" "2" expand "catenate" )"2" "2" expand "member" )"2" expand "finseq_appl" )"2" replace "2" rewrite "rest_add_first" )"2" replace "2" rewrite "first_add" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "finseq_appl" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" expand "replaceTerm" )"2" "2" "1" "x!1" )"1" expand "V" )"1" nil nil ))nil ))nil )"2" "2" expand "replace" )"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 )"set[T]" indexed_sets nil )"positions" positions nil )"(total_order?[real])" nil )"upto? " replacement nil) nil IUnion_extra nil )"positions?[variable, symbol, arity](app(app1_var!1, app2_var!1))" nil )"(V)" replacement nil )"{args: finite_sequence[term[variable, symbol, arity]] | " replacement nil) "symbol" replacement nil )"[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> " 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 )"[term -> boolean]" term_adt nil )"bool" reals nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil )replace const-decl "finseq" seq_extras "structures/" )"set" sets nil )nil finite_sequences nil )nil seq_extras "structures/" )"positions" positions nil )"[variable -> (vars?)]" term_adt nil )"[term -> boolean]" term_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil term_adt nil )nil replacement nil )nil replacement 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]" replacement nil )"term" replacement nil )"bool" sets 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 3414515459"" (skolem-typepred)"" (expand "V" )"" (flatten)"" (decompose-equality 2)"" (iff)"" (prop)"1" (expand * "remove" "Pos_var" "extend" )"1" (prop)"1" (lemma "subterm_of_replace" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (expand "member" )"2" (prop)"1" (lemma "subterm_of_replace" )"1" (inst -1 "p!1" "t!1" "y!1" )"1" (assert )"1" (lemma "variable_positions_parallel" )"1" "replaceTerm(t!1, y!1, p!1)" "y!1" "x!1" "p!1" "x!2" )"1" assert )"1" "replace_persistence" )"1" "p!1" "x!2" "t!1" "y!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "pos_replaces_is_subset" )"2" (inst?)"2" (expand * "subset?" "member" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand * "remove" "Pos_var" )"2" (expand "extend" )"2" (prop)"1" (expand "member" )"1" (prop)"1" (lemma "variable_positions" )"1" (inst?)"1" (inst -1 "x!1" )"1" assert )"1" expand * "member" "Pos_var" )"1" expand "extend" )"1" "replace_persistence" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "member" )"2" (prop)"2" (lemma "variable_positions" )"2" (inst?)"2" (inst -1 "x!1" )"2" assert )"2" expand * "member" "Pos_var" )"2" expand "extend" )"2" "replace_preserv_parallel_pos" )"2" "p!1" "x!2" "t!1" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"positions" subterm nil )"term" replacement nil )"set" sets nil )nil replacement nil )nil subterm nil )nil replacement nil )"bool" sets nil )nil replacement nil )"bool" sets nil )"R" extend nil )nil replacement nil )nil 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 )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" replacement 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 replacement nil )nil replacement nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3414642772"" (skosimp*)"" (lemma "sets_lemmas[position].remove_as_difference" )"" (inst -1 "Pos_var(t!1, x!1)" "p!1" )"" (lemma "pos_occ_var_replace" )"" (inst?)"" (assert )"" (replaces -2)"" (expand "difference" ) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"[symbol -> nat]" replacement nil )nil replacement nil )nil replacement 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 sets_lemmas nil )nil replacement nil )"non_empty_finite_set" finite_sets nil )"non_empty_finite_set[position]" replacement nil )"set" sets nil )"(singleton?)" sets nil )"bool" sets nil )"R" extend nil )"posint" nil )nil positions nil )"positions" positions nil )"positions" subterm nil )nil positions nil )"set[term]" variables_term nil )nil term_adt nil ) (set type-eq-decl nil sets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.364 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
