SSL replace_positions.prf
Interaktion und
(replace_positionsnil 3455272043"" (lemma "var_countable" ) (("" (propax) nil nil )) nil )nil replace_positions nil )) nil ))nil 3455272043 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil replace_positions nil )nil replace_positions 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]" replace_positions nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil finite_sequences nil )"bool" positions nil )nil positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" positions nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3455272043 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil replace_positions nil )nil replace_positions 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]" replace_positions nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil finite_sequences nil )"bool" positions nil )nil positions nil )"(strict_total_order?[real])" real_props nil )"bool" positions nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3455272043"" (skosimp*)"" (typepred "fssp!1" )"" (expand "SPP?" )"" (flatten)"" (split)"1" (rewrite "rest_of_PP_is_PP" ) nil nil )"2" (expand "SP?" )"2" (expand "PP?" )"2" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (lemma "fspos.rest_pos" )"2" (inst?)"2" (assert )"2" (expand "finseq_appl" )"2" (inst -1 "i!1" )"1" replace -1 2 rl)"1" "1" "1" "0" )"1" "1 + i!1" )"1" "0" "1 + i!1" )"1" assert )"1" "replace_preserv_parallel_pos" )"1" "fssp!1`seq(0)" "fssp!1`seq(1 + i!1)" "s!1" "t!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" positions nil )"bool" reals nil )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil seq_extras "structures/" )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"below[length(rest[position[variable, symbol, arity]](fssp!1))]" nil )"SPP[variable, symbol, arity](s!1)" nil )"term[variable, symbol, arity]" nil )nil replacement nil )"[numfield, numfield -> numfield]" number_fields nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil positions nil )"bool" positions nil )nil positions nil ))nil ))nil 3455272043 ("" (termination-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil term_adt nil )nil finite_sequences nil )"bool" positions nil )nil positions nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )"bool" positions nil )"bool" positions nil )"bool" positions nil )"bool" positions nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )nil positions nil )"[symbol -> nat]" replace_positions nil )nil replace_positions nil )nil replace_positions nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )"finseq" seq_extras "structures/" )"posint" nil ))nil ))nil 3455272043"" (skosimp*)"" (typepred "fss!1" )"" (expand "SPP?" )"" (flatten)"" (assert )"" (hide -1)"" (expand "SP?" )"" (skosimp*)"" (inst?)"" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil substitution nil )"[below[length(fs)] -> T]" finite_sequencesnil )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )"bool" reals nil )"bool" positions nil ))nil ))nil 3455272189"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide -2)"1" (expand "replace_pos" ) (("1" (assert ) nil nil )) nil ))nil )"2" (expand "replace_pos" 2 1)"2" (assert )"2" (inst -1 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)" )"2" (inst -1 "t!1" "sig!1" )"2" (rewrite "length_rest" )"2" (replaces -1)"2" (rewrite "ext_replace_ext" )"1" (expand "replace_pos" 2 2)"1" (propax) nil nil )) nil )"2" (hide (2 3))"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" "2" expand "SP?" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (assert )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (inst?)"2" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skosimp*)"3" (rewrite "replace_pos_is_stable_TCC1" ) nil nil )) nil ))nil )"4" (hide (-1 2))"4" (skosimp*)"4" (rewrite "replace_pos_is_stable_TCC1" ) nil nil )) nil ))nil )"5" (hide-all-but 1)"5" (rewrite "replace_pos_is_stable_TCC1" ) nil nil )) nil )"6" (hide (-1 2))"6" (skosimp*)"6" (rewrite "replace_pos_is_stable_TCC1" ) nil nil )) nil ))nil )"7" (hide 2)"7" (rewrite "replace_pos_is_stable_TCC1" ) nil nil )) nil ))nil )nil replace_positions nil )nil substitution nil )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"term" replacement nil )nil positions nil )"positions" positions nil )nil positions nil )nil seq_extras "structures/" )nil substitution nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" positions nil )"[bool, bool -> bool]" booleans nil )"term" replace_positions nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )ext def-decl "term" substitution nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455272043"" (skolem-typepred)"" (skosimp*)"" (expand "SPP?" )"" (flatten)"" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" ) nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3455272317"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (expand "replace_pos" 1)"1" (prop)"1" (hide-all-but -1)"1" (expand * "add_first" "insert?" )"1" (assert ) nil nil )) nil ))nil )"2" (lemma "fspos.rest_add_first" )"2" (inst -1 "x!2" "q!1" )"2" (replaces -1)"2" (lemma "fspos.nth_add_first" )"2" (inst -1 "x!2" "q!1" "0" )"1" (replace -1)"1" (case "length(x!2) = 0" )"1" (hide -3)"1" (expand "replace_pos" )"1" (prop)"1" "1" "replace_preserv_pos" )"1" "q!1" "x!1" "t!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replace_pos" 3)"2" (prop)"2" (lemma "replace_commutativity" )"2" "q!1" "x!2(0)" "t!1" "x!1" "t!1" )"2" "q!1" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" -4)"2" "0" )"2" "2" "0" )"2" assert )"2" rewrite "parallel_comm" )"2" replace -6 2)"2" case "length(rest(x!2)) = 0" )"1" "1" expand "replace_pos" )"1" "1" "replace_preserv_parallel_pos" )"1" "x!2(0)" "q!1" "x!1" "t!1" )"1" expand "SP?" )"1" "0" )"1" assert )"1" "replace_preserv_pos" )"1" "q!1" "replaceTerm(x!1, t!1, x!2(0))" "t!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)" )"1" "t!1" "q!1" )"1" "1" expand "finseq_appl" )"1" expand "replace_pos" "1" "1" "1" nil nil ))nil )"2" "fspos.nth_add_first" )"2" "rest(x!2)" "q!1" "0" )"1" "1" rewrite "rest_add_first" )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1 + 1" )"1" "fspos.rest_pos" )"1" expand "finseq_appl" )"1" "x!2" )"1" assert )"1" "i!1" )"1" assert )nil nil )"2" "i!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "length_rest" )nil nil ))nil ))nil ))nil )"2" "2" expand "SPP?" )"2" "1" rewrite "rest_of_PP_is_PP" )nil nil )"2" "2" expand "SP?" )"2" "2" expand "finseq_appl" )"2" "i!1 + 1" )"1" "fspos.rest_pos" )"1" "1" assert )"1" "i!1" )"1" expand "PP?" )"1" "1" "1" nil nil ))nil )"2" expand "finseq_appl" )"2" replace "2" "0" "1 + i!1" )"2" assert )"2" "replace_preserv_parallel_pos" )"2" "x!2`seq(0)" "x!2`seq(1 + i!1)" "x!1" "t!1" )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"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 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" ) nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1 2)"3" (skosimp*)"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" )nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide -1 2)"4" (skosimp*)"4" (typepred "x!1`2" )"4" (expand "SPP?" )"4" (flatten)"4" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" )nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but (-1 1))"5" (typepred "y!1`2" )"5" (expand "SPP?" )"5" (flatten)"5" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" ) nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (hide -1 2)"6" (skosimp*)"6" (typepred "y!1`2" )"6" (expand "SPP?" )"6" (flatten)"6" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" )nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide 2)"7" (typepred "fss!1" )"7" (expand "SPP?" )"7" (flatten)"7" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" ) nil nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )nil positions nil )nil positions nil )"finseq" seq_extras "structures/" )"posint" nil )nil seq_extras "structures/" )nil replacement nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" positions nil )"term[variable, symbol, arity]" nil )"int" integers nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )nil seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_int" nil )"bool" positions nil )"finseq" finite_sequences nil )"below[length(rest(x!2))]" replace_positionsnil )nil seq_extras "structures/" )"below[length(rest[position[variable, symbol, arity]](x!2))]" nil )OR const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )nil positions nil )"bool" positions nil )nil positions nil )"term" replacement nil )nil replacement nil )"finseq" seq_extras "structures/" )nil positions nil )nil replacement nil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term" replace_positions nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"bool" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455272446"" (measure-induct+ "length(fss)" ("s" "fss" ))"" (skosimp*)"" (case "length(x!2) = 0" )"1" (hide (-2 -3))"1" (typepred "q!1" )"1" (expand "replace_pos" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "replace_pos" 2)"2" (assert )"2" (inst -1 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)" )"2" (inst -1 "t!1" "q!1" )"1" (rewrite "length_rest" )"1" (assert )"1" (hide 3)"1" (case "length(rest(x!2)) = 0" )"1" (hide -2) (("1" (grind) nil nil )) nil )"2" (skosimp*)"2" (lemma "fspos.rest_pos" )"2" (expand "finseq_appl" )"2" "2" assert )"2" "i!1" )"1" "i!1 + 1" )"1" (assert ) nil nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (inst -1 "0" )"2" (typepred "q!1" )"2" (lemma "replace_preserv_parallel_pos" )"2" (inst -1 "x!2(0)" "q!1" "x!1" "t!1" )"2" (assert )"2" (hide-all-but 1)"2" "x!2" )"2" expand "SPP?" )"2" "2" expand "SP?" )"2" (inst -2 "0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"finseq" seq_extras "structures/" )"term" replacement nil )"bool" positions nil )nil replacement nil )nil seq_extras "structures/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"below[length(rest(x!2))]" replace_positionsnil )nil seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )"bool" positions nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"positions?[variable, symbol, arity](x!1)" nil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term" replace_positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" positions nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )nil positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455272537"" (measure-induct+ "length(fssp)" ("s" "fssp" ))"" (skolem 1 ("t" "_" ))"" (case "length(x!2) = 0" )"1" (hide -2) (("1" (grind) nil nil )) nil )"2" (skosimp*)"2" (case-replace "i!1 = 0" )"1" (hide -2)"1" (lemma "preserv_first_position" )"1" (inst -1 "t" "x!1" "rest(x!2)" "first(x!2)" )"1" (prop)"1" (lemma "fspos.seq_first_rest" )"1" (inst?)"1" (assert )"1" (replace -1 -2 rl)"1" (expand "first" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide (-2 -3 3))"2" (expand "PP?" )"2" "1" (grind) nil nil )"2" "2" "i!2 + 1" "0" )"1" assert )"1" "fspos.rest_pos" )"1" "1" assert )"1" "i!2" )"1" assert )"1" expand *"first" "finseq_appl" )"1" assert )nil nil ))nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide (-1 -3 3))"2" (expand "SP?" )"2" (inst -1 "0" )"2" expand "first" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 3))"3" (typepred "x!2" )"3" (expand "SPP?" )"3" (flatten)"3" (split)"1" (rewrite "rest_of_PP_is_PP" ) nil nil )"2" (rewrite "rest_of_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -1 "replaceTerm(x!1, t, x!2(0))" "rest(x!2)" )"1" (inst -1 "t" "i!1 - 1" )"1" (rewrite "length_rest" )"1" (case "rest(x!2)`length /= 0" )"1" (assert )"1" (expand "replace_pos" 3)"1" (lemma "fspos.rest_pos" )"1" (inst?)"1" (assert )"1" "i!1 - 1" )"1" expand "finseq_appl" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (prop)"2" (expand "replace_pos" )"2" (expand "replace_pos" )"2" (prop)"2" "x!2" )"2" expand "SPP?" )"2" "2" expand "PP?" )"2" "1" "1" (grind) nil nil ))nil )"2" "0" "i!1" )"2" assert )"2" "replace_preserv_parallel_pos" )"2" "x!2(0)" "x!2(i!1)" "x!1" "t" )"2" assert )"2" "2" expand "SP?" )"2" "2" "0" )"2" "i!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 )"2" (typepred "i!1" ) (("2" (grind) nil nil )) nil ))nil )"2" (hide 4)"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (split)"1" (rewrite "rest_of_PP_is_PP" ) nil nil )"2" (expand "SP?" )"2" (skosimp*)"2" (lemma "fspos.rest_pos" )"2" "2" assert )"2" "i!2" )"1" expand "finseq_appl" )"1" replace -1 1 rl)"1" "1" "1" "i!2 + 1" )"1" "0" )"1" "replace_preserv_parallel_pos" )"1" "x!2`seq(0)" "x!2`seq(i!2 + 1)" "x!1" "t" )"1" assert )"1" "1" expand "PP?" )"1" "0" "i!2 + 1" )"1" expand "finseq_appl" )"1" nil nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "x!2" )"3" (expand * "SPP?" "SP?" )"3" (flatten) (("3" (inst -2 "0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"term" replacement nil )"term[variable, symbol, arity]" nil )nil seq_extras "structures/" )nil replacement nil )"below[x!2`length]" replace_positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"below[length(rest[position[variable, symbol, arity]](x!2))]" nil )"term[variable, symbol, arity]" nil )"finseq" seq_extras "structures/" )"SPP[variable, symbol, arity](x!1)" nil )"boolean" notequal nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )nil positions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" positions nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil seq_extras "structures/" )"below[length(rest(x!2))]" replace_positionsnil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"bool" positions nil )"bool" positions nil )nil seq_extras "structures/" )"bool" positions nil )nil positions nil )nil positions nil )nil positions nil )nil positions nil )nil replace_positions nil )"posint" nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[below[length(fs)] -> T]" finite_sequencesnil )"term" replace_positions nil )"positions" positions nil )nil positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455272043"" (skosimp*)"" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )nil replace_positionsnil )nil replace_positions nil )nil replace_positions nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[symbol -> nat]" replace_positions nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil finite_sequences nil )"bool" positions nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil ))nil ))nil 3455272651"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide (-2 -3))"1" (expand "replace_pos" ) (("1" (assert ) nil nil )) nil ))nil )"2" (expand "replace_pos" 2)"2" (assert )"2" (inst -1 "replaceTerm(x!1, t!1, x!2(0))" "rest(x!2)" )"2" (inst -1 "t!1" "q!1" )"1" (rewrite "length_rest" )"1" (prop)"1" (replaces -1)"1" (lemma "replace_persistence" )"1" (inst -1 "x!2(0)" "q!1" "x!1" "t!1" )"1" (assert )"1" (hide 3)"1" "x!2" )"1" expand "SPP?" )"1" "1" expand "SP?" )"1" "0" )"1" "0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (case "length(rest(x!2)) = 0" )"1" (hide -2) (("1" (grind) nil nil )) nil )"2" (skosimp*)"2" (lemma "fspos.rest_pos" )"2" (expand "finseq_appl" )"2" "2" assert )"2" "i!1" )"1" "i!1 + 1" )"1" (assert ) nil nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide -1)"2" (expand "SP?" )"2" (inst -1 "0" )"2" "0" )"2" "q!1" )"2" "replace_preserv_parallel_pos" )"2" "x!2(0)" "q!1" "x!1" "t!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-2 -3 2))"2" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"3" (hide (-1 2))"3" (skosimp*)"3" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"4" (hide (-1 2))"4" (skosimp*)"4" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"5" (hide-all-but (-1 1))"5" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"6" (hide (-1 2))"6" (skosimp*)"6" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"7" (hide 2)"7" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil ))nil )nil replace_positionsnil )"finseq" seq_extras "structures/" )"term" replacement nil )nil replacement nil )nil seq_extras "structures/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"below[length(rest(x!2))]" replace_positionsnil )nil seq_extras "structures/" )"bool" positions nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"bool" positions nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil replacement nil )"positions?[variable, symbol, arity](x!1)" nil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"term" subterm nil )"[T, T -> boolean]" equalities nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"bool" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"term" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3457522914"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil replace_positions nil )nil replace_positions 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]" replace_positions nil )nil term_adt nil )nil nat_types nil )nil integers nil )"bool" reals nil )nil integers nil )nil positions nil )nil finite_sequences nil )"bool" positions nil )nil positions nil )"bool" reals nil )"bool" positions nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3457522958"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide (-2 -3))"1" (expand "replace_pos" )"1" (lift-if) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (expand "replace_pos" 2)"2" (lift-if)"2" (assert )"2" (expand "finseq_appl" )"2" "replaceTerm(x!1, t!1, x!2`seq(0))" "rest(x!2)" )"2" (inst -1 "t!1" )"2" (prop)"1" (inst -2 "0" )"1" case "replaceTerm(x!1, t!1, x!2`seq(0)) = x!1" )"1" (replaces -1) nil nil )"2" (hide (-1 3))"2" (replace -1 1 rl)"2" rewrite "replace_subterm_of_term" )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" expand "SP?" )"2" "0" )"2" expand "finseq_appl" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (skosimp*)"2" (copy -1)"2" (inst -1 "0" )"2" case "replaceTerm(x!1, t!1, x!2`seq(0)) = x!1" )"1" "1" "1" "rest_pos[position]" )"1" "1" "1" "1" expand "finseq_appl" )"1" replace -1 1 rl)"1" "i!1 + 1" )"1" assert )nil nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil )"2" "2" expand "subtermOF" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1 1 rl)"2" rewrite "replace_subterm_of_term" )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" expand "SP?" )"2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 3))"3" (rewrite "length_rest" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (expand "SP?" )"2" (inst -2 "i!1" )"2" (expand "finseq_appl" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (expand "SP?" ) (("3" (inst -2 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide (-1 2))"4" (skosimp*)"4" (typepred "x!1`2" )"4" (expand "SPP?" )"4" (flatten)"4" (expand "SP?" ) (("4" (inst -2 "i1!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide (-1 2 3))"5" (skosimp*)"5" (typepred "y!1`2" )"5" (expand "SPP?" )"5" (flatten)"5" (expand "SP?" ) (("5" (inst -2 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide 2)"6" (skosimp*)"6" (typepred "y!1`2" )"6" (expand "SPP?" )"6" (flatten)"6" (expand "SP?" ) (("6" (inst -2 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide 2)"7" (typepred "fss!1" )"7" (expand "SPP?" )"7" (flatten)"7" (expand "SP?" ) (("7" (inst -2 "i!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"finseq" seq_extras "structures/" )"term" replacement nil )"bool" positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil replacement nil )nil seq_extras "structures/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"below[length(rest(x!2))]" replace_positionsnil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"int" integers nil )"odd_int" integersnil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )nil seq_extras "structures/" )"term" replace_positions nil )"term" subterm nil )nil positions nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil positions nil )"positions" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3456672662"" (skosimp*)"" (lemma "Pos_var_is_finite" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil ))nil 3456672662"" (skosimp*)"" (expand "SPP?" )"" (split)"1" (lemma "pos_occ_var_HAStypePP" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (lemma "pos_occ_var_HAStypeSP" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" positions nil )nil subterm nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil subterm nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil ))nil ))nil 3456672663"" (skosimp*)"" (name-replace "fss" "set2seq(Pos_var(s!1, x!1))" :hide? nil )"" (lemma "replace_pos_subterm_to_term" )"" (inst -1 "x!1" "s!1" "fss" )"" (assert )"" (hide 2)"" (skosimp*)"" (expand "finseq_appl" )"" (lemma "set2seq_lem[position]" )"" (inst?)"" (assert )"" (inst -1 "i!1" )"1" (expand "finseq_appl" )"1" (replaces -2)"1" expand "Pos_var" )"1" expand "extend" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (typepred "i!1" )"2" (replaces -2 :dir rl)"2" rewrite "set2seq_length" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 replace_positions nil )nil replace_positions nil )"[symbol -> nat]" replace_positions nil )nil positions nil )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"finite_sequence[T]" set2seq "structures/" )nil term_adt nil )"set[term]" variables_term nil )nil positions nil )"positions" subterm nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"finite_sequence[position[variable, symbol, arity]]" nil )"below[length(fss)]" replace_positions nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"term[variable, symbol, arity]" nil )"(V)" replace_positions nil )nil naturalnumbers nil )nil set2seq "structures/" )"R" extend nil )NOT const-decl "[bool -> bool]" booleans nil )nil set2seq "structures/" )nil replace_positionsnil ))nil 3455272825"" (skosimp*)"" (typepred "fss!1" )"" (expand "SPP?" )"" (flatten)"" (split)"1" (rewrite "add_last_parallel_pos_to_PP_is_PP" ) nil nil )"2" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"positions" positions nil )nil positions nil ))nil ))nil 3455272867"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide (-2 -3))"1" (expand "replace_pos" )"1" (lift-if)"1" (lift-if)"1" (prop)"1" (hide 1) (("1" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replace_pos" 2 1)"2" (lift-if)"2" (prop)"1" (hide-all-but (-1 2)) (("1" (grind) nil nil )) nil )"2" (lemma "fspos.rest_add_last" )"2" (inst?)"2" (assert )"2" (replaces -1)"2" "replaceTerm(x!1, t!1, add_last(x!2, q!1)(0))" "rest(x!2)" )"1" (inst -1 "t!1" "q!1" )"1" (rewrite "length_rest" )"1" (prop)"1" "RTq" "replaceTerm(x!1, t!1, add_last(x!2, q!1)(0))" )"1" "1" expand "RTq" )"1" "fspos.nth_add_last" )"1" "x!2" "q!1" "0" )"1" assert )"1" "1" expand "replace_pos" "1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "length(rest(x!2)) = 0" )"1" "1" (grind) nil nil ))nil )"2" "2" expand "finseq_appl" )"2" "fspos.rest_pos" )"2" "2" assert )"2" "i!1" )"1" expand "finseq_appl" )"1" "i!1 + 1" )"1" assert )nil nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "finseq_appl" )"2" (hide-all-but (-1 1 4))"2" "fspos.nth_add_last" )"2" "x!2" "q!1" "0" )"2" assert )"2" expand "finseq_appl" )"2" "2" "0" )"2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" "0" )"2" "q!1" )"2" "replace_preserv_parallel_pos" )"2" "x!2(0)" "q!1" "x!1" "t!1" )"2" expand "finseq_appl" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2 3))"2" (lemma "fspos.nth_add_last" )"2" (inst -1 "x!2" "q!1" "0" )"2" assert )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" "1" rewrite "rest_of_PP_is_PP" )nil nil )"2" expand * "PP?" "SP?" )"2" assert )"2" "1" (grind) nil nil )"2" "fspos.rest_pos" )"2" "2" "1" "1" "i!1" )"1" "0" "i!1 + 1" )"1" assert )"1" "1" "0" )"1" "i!1 + 1" )"1" expand "finseq_appl" )"1" replace "1" "1" "replace_preserv_parallel_pos" )"1" "x!2`seq(0)" "x!2`seq(1 + i!1)" "x!1" "t!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "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 )"2" (hide-all-but (-1 1))"2" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"3" (hide-all-but (-1 1))"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"3" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp*)"4" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp*)"5" (typepred "y!2" )"5" (expand "SPP?" )"5" (flatten)"5" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"5" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*)"6" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"7" (hide-all-but (-1 1))"7" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"8" (hide-all-but (-1 1))"8" (typepred "y!1`2" )"8" (expand "SPP?" )"8" (flatten)"8" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"8" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"9" (hide-all-but 1)"9" (skosimp*)"9" (typepred "x!1`2" )"9" (expand "SPP?" )"9" (flatten)"9" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"9" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but (-1 1))"10" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"11" (hide-all-but (-1 1))"11" (typepred "y!1`2" )"11" (expand "SPP?" )"11" (flatten)"11" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"11" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"13" (hide-all-but 1)"13" (skosimp*)"13" (typepred "y!1`2" )"13" (expand "SPP?" )"13" (flatten)"13" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"13" (rewrite "add_last_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide-all-but (-1 1))"14" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"15" (hide 2)"15" (typepred "fss!1" )"15" (expand "SPP?" )"15" (flatten)"15" (rewrite "add_last_parallel_pos_to_PP_is_PP" )"15" (rewrite "add_last_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )nil positions nil )nil positions nil )nil replace_positionsnil )nil positions nil )"bool" positions nil )nil positions nil )"below[length(rest[position[variable, symbol, arity]](x!2))]" nil )nil seq_extras "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"term[variable, symbol, arity]" nil )"int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"bool" positions nil )"{k: nat | k <= i AND k <= j}" nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"below[length(rest(x!2))]" replace_positionsnil )"[numfield, numfield -> numfield]" number_fields nil )nil seq_extras "structures/" )nil seq_extras "structures/" )nil replacement nil )"bool" positions nil )"positions?[variable, symbol, arity](x!1)" nil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )nil seq_extras "structures/" )"posint" nil )"posint" nil )"finseq" seq_extras "structures/" )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"finseq" seq_extras "structures/" )"finseq" finite_sequences nil )"finseq" finite_sequences nil )AND const-decl "[bool, bool -> bool]" booleans nil )"term" replacement nil )"[T, T -> boolean]" equalities nil )"term" replace_positions nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"bool" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455273040"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide (-2 -3))"1" (expand "replace_pos" )"1" (lift-if)"1" (lift-if)"1" (prop)"1" (hide 1) (("1" (grind) nil nil )) nil )"2" (lemma "fspos.nth_add_first" )"2" (inst?)"1" (replaces -1)"1" (rewrite "rest_add_first" )"1" (expand "replace_pos" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replace_pos" 2 1)"2" (lift-if)"2" (prop)"1" (hide-all-but (-1 2)) (("1" (grind) nil nil )) nil )"2" (rewrite "rest_add_first" )"2" (lemma "fspos.nth_add_first" )"2" (inst?)"1" (replaces -1)"1" (expand "replace_pos" 2 1)"1" (lift-if)"1" (assert )"1" (expand "finseq_appl" )"1" "replace_commutativity" )"1" "q!1" "x!2`seq(0)" "t!1" "x!1" "t!1" )"1" "1" "1" "replaceTerm(x!1, t!1, x!2`seq(0))" "rest(x!2)" )"1" "t!1" "q!1" )"1" rewrite "length_rest" )"1" "1" expand "replace_pos" "1" "1" "1" "1" nil nil ))nil )"2" rewrite "rest_add_first" )"2" "fspos.nth_add_first" )"2" "1" "1" "1" expand "replace_pos" "1" expand "finseq_appl" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "length(rest(x!2)) = 0" )"1" "1" nil nil ))nil )"2" "2" "fspos.rest_pos" )"2" "2" assert )"2" "i!1" )"1" expand "finseq_appl" )"1" "i!1 + 1" )"1" assert )nil nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" rewrite "rest_of_PP_is_PP" )"2" expand *"PP?" "SP?" )"2" "1" nil nil )"2" "fspos.rest_pos" )"2" "2" "1" "1" "i!1" )"1" "0" "i!1 + 1" )"1" assert )"1" "1" "0" )"1" "i!1 + 1" )"1" expand "finseq_appl" )"1" replace "1" "1" "replace_preserv_parallel_pos" )"1" "x!2`seq(0)" "x!2`seq(1 + i!1)" "x!1" "t!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "q!1" )"2" (propax) nil nil ))nil )"3" "3" "x!2" )"3" expand "SPP?" )"3" "3" "3" expand "SP?" )"3" "0" )"3" expand "finseq_appl" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "0" )"4" rewrite "parallel_comm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"3" (hide-all-but (-1 1))"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"3" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp*)"4" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp*)"5" (typepred "y!2" )"5" (expand "SPP?" )"5" (flatten)"5" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"5" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*)"6" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"7" (hide-all-but (-1 1))"7" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"8" (hide-all-but (-1 1))"8" (typepred "y!1`2" )"8" (expand "SPP?" )"8" (flatten)"8" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"8" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"9" (hide-all-but 1)"9" (skosimp*)"9" (typepred "x!1`2" )"9" (expand "SPP?" )"9" (flatten)"9" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"9" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but (-1 1))"10" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"11" (hide-all-but (-1 1))"11" (typepred "y!1`2" )"11" (expand "SPP?" )"11" (flatten)"11" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"11" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (rewrite "preserv_all_parallel_positions" ) nil nil ))nil ))nil )"13" (hide-all-but 1)"13" (skosimp*)"13" (typepred "y!1`2" )"13" (expand "SPP?" )"13" (flatten)"13" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"13" (rewrite "add_first_parallel_pos_to_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide-all-but (-1 1))"14" (rewrite "preserv_all_parallel_positions" ) nil nil )) nil )"15" (hide 2)"15" (typepred "fss!1" )"15" (expand "SPP?" )"15" (flatten)"15" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"15" (rewrite "add_first_parallel_pos_to_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )nil positions nil )nil positions nil )nil replace_positionsnil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil )nil replacement nil )"below[length(rest[position[variable, symbol, arity]](x!2))]" nil )"bool" positions nil )"int" integers nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"finseq" finite_sequences nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"finseq" finite_sequences nil )"bool" positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil seq_extras "structures/" )"[numfield, numfield -> numfield]" number_fields nil )"below[length(rest(x!2))]" replace_positionsnil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"term[variable, symbol, arity]" nil )nil replacement nil )"posint" nil )"posint" nil )"finseq" seq_extras "structures/" )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"term[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](x!1)" nil )nil seq_extras "structures/" )nil seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"term" replacement nil )"[T, T -> boolean]" equalities nil )"term" replace_positions nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"bool" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455272825"" (skolem-typepred)"" (expand "SPP?" )"" (flatten)"" (rewrite "delete_of_PP_is_PP" )"" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil ) (< const-decl "bool" reals nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3455272825"" (skolem-typepred)"" (expand "finseq_appl" )"" (expand "SPP?" )"" (flatten)"" (expand * "PP?" "SP?" )"" (rewrite "preserv_all_parallel_positions" )"1" (hide (-2 2))"1" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand * "delete" "finseq_appl" )"2" (lift-if)"2" (prop)"1" (inst -2 "i!2" "i!1" )"1" (assert ) nil nil )) nil )"2" (inst -1 "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" (typepred "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (inst -1 "i!1" )"2" (expand "finseq_appl" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil replace_positionsnil )"finseq" seq_extras "structures/" )nil positions nil )"positions" positions nil )nil positions nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" positions nil )"bool" positions nil )"finseq" finite_sequences nil )"posint" nil )"below[length(delete[position[variable, symbol, arity]](fss!1, i!1))]" nil )"below[length(fss!1)]" replace_positionsnil )"SPP[variable, symbol, arity](s!1)" nil )"term[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"bool" positions nil )"bool" positions nil )"bool" reals nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil replace_positions nil )nil replace_positions nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3455273190"" (measure-induct+ "length(fss)" ("s" "fss" ))"1" (case "length(x!2) = 0" )"1" (hide -2)"1" (skolem 1 ("t" "_" )) (("1" (grind) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand * "finseq_appl" )"2" (case-replace "i!1 = 0" )"1" (hide -2)"1" (lemma "fspos.delete_rest" )"1" (inst?)"1" (assert )"1" (replaces -1)"1" (lemma "CP_lemma_aux2a1" )"1" (inst?)"1" (prop)"1" (lemma "fspos.seq_first_rest" )"1" "1" assert )"1" expand * "first" "finseq_appl" )"1" replace -1 -2 rl)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" expand "finseq_appl" )"2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "PP?" )"2" "1" (grind) nil nil )"2" "2" "i!2 + 1" "0" )"1" assert )"1" expand "finseq_appl" )"1" "fspos.rest_pos" )"1" "1" "1" "i!2" )"1" expand "finseq_appl" )"1" assert )nil nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (typepred "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" "0" )"2" expand "finseq_appl" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "replace_pos" 3 1)"2" (expand "finseq_appl" )"2" "replaceTerm(x!1, t!1, x!2`seq(0))" "rest(x!2)" )"2" (inst -1 "t!1" "i!1 - 1" )"1" (rewrite "length_rest" )"1" (lemma "fspos.rest_pos" )"1" (inst?)"1" (prop)"1" (inst -1 "i!1 - 1" )"1" expand "finseq_appl" )"1" replace -1 -2 rl)"1" "1" "fspos.delete_rest" )"1" "1" assert )"1" "1" expand "replace_pos" "1" "1" "1" "1" nil nil ))nil )"2" expand "finseq_appl" )"2" expand "delete" "2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide (-2 3)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" (typepred "i!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (rewrite "preserv_all_parallel_positions" )"1" (hide 2)"1" (case "length(delete(y!2, i!1)) = 0" )"1" (grind) nil nil )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide -2)"2" (expand "PP?" )"2" (prop)"1" (grind) nil nil )"2" (case "i!2 < i!1" )"1" expand * "delete" "finseq_appl" )"1" assert )"1" "i!2" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand * "delete" "finseq_appl" )"2" assert )"2" "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide (-1 2))"2" (expand "SP?" ) (("2" (inst -1 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (rewrite "delete_of_PP_is_PP" )"3" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp*)"4" (rewrite "preserv_all_parallel_positions" )"1" (hide 2)"1" (case "length(delete(y!2, i!1)) = 0" )"1" (grind) nil nil )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide -2)"2" (expand "PP?" )"2" (prop)"1" (grind) nil nil )"2" case "i!2 < i!1" )"1" expand * "delete" "finseq_appl" )"1" assert )"1" "i!2" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand * "delete" "finseq_appl" )"2" assert )"2" "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "y!2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide (-1 2))"2" (expand "SP?" ) (("2" (inst -1 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "finseq_appl" )"5" (hide-all-but 1)"5" (skosimp*)"5" (typepred "y!2" )"5" (expand "SPP?" )"5" (flatten)"5" (rewrite "delete_of_PP_is_PP" )"5" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*)"6" (rewrite "preserv_all_parallel_positions" )"1" (hide 2)"1" (case "length(delete(x!1`2, i1!1)) = 0" )"1" (grind) nil nil )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "x!1`2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide -2)"2" (expand "PP?" )"2" (prop)"1" (grind) nil nil )"2" expand * "delete" "finseq_appl" )"2" "2" "1" "i!1" "i1!1" )"1" (assert ) nil nil ))nil )"2" "i!1 + 1" "i1!1" )"1" (assert ) nil nil )"2" "i!1" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "x!1`2" )"2" (expand "SPP?" )"2" (flatten)"2" (hide -1)"2" (expand "SP?" )"2" (inst -1 "i1!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "finseq_appl" )"7" (hide-all-but 1)"7" (typepred "y!1`2" )"7" (expand "SPP?" )"7" (flatten)"7" (expand * "PP?" "SP?" )"7" (rewrite "preserv_all_parallel_positions" )"1" (hide (-2 2))"1" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand * "delete" "finseq_appl" )"2" (lift-if)"2" (prop)"1" "i!2" "i!1" )"1" (assert ) nil nil ))nil )"2" "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (inst -1 "i!1" )"2" (expand "finseq_appl" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide-all-but 1)"8" (typepred "y!1`2" )"8" (expand "SPP?" )"8" (flatten)"8" (rewrite "delete_of_PP_is_PP" )"8" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil )"9" (hide-all-but 1)"9" (skosimp*)"9" (typepred "x!1`2" )"9" (expand "SPP?" )"9" (flatten)"9" (rewrite "delete_of_PP_is_PP" )"9" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but 1)"10" (typepred "y!1`2" )"10" (expand "SPP?" )"10" (flatten)"10" (expand * "PP?" "SP?" )"10" (rewrite "preserv_all_parallel_positions" )"1" (hide (-2 2))"1" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand * "delete" "finseq_appl" )"2" (lift-if)"2" (prop)"1" (inst -2 "i!2" "i!1" )"1" (assert ) nil nil )) nil )"2" (inst -1 "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2)) (("2" (inst -1 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (expand "finseq_appl" )"11" (hide-all-but 1)"11" (typepred "y!1`2" )"11" (expand "SPP?" )"11" (flatten)"11" (rewrite "delete_of_PP_is_PP" )"11" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (typepred "y!1`2" )"12" (expand "SPP?" )"12" (flatten)"12" (expand * "PP?" "SP?" )"12" (rewrite "preserv_all_parallel_positions" )"1" (hide (-2 2))"1" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand * "delete" "finseq_appl" )"2" (lift-if)"2" (prop)"1" "i!2" "i!1" )"1" (assert ) nil nil ))nil )"2" "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2)) (("2" (inst -1 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (expand "finseq_appl" )"13" (hide-all-but 1)"13" (skosimp*)"13" (typepred "y!1`2" )"13" (expand "SPP?" )"13" (flatten)"13" (rewrite "delete_of_PP_is_PP" )"13" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide-all-but 1)"14" (typepred "fss!1" )"14" (expand "SPP?" )"14" (flatten)"14" (expand * "PP?" "SP?" )"14" (rewrite "preserv_all_parallel_positions" )"1" (hide (-2 2))"1" (prop)"1" (grind) nil nil )"2" (skosimp*)"2" (expand * "delete" "finseq_appl" )"2" (lift-if)"2" (prop)"1" (inst -2 "i!2" "i!1" )"1" (assert ) nil nil )) nil )"2" (inst -1 "i!2 + 1" "i!1" )"1" (assert ) nil nil )"2" "i!2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2)) (("2" (inst -1 "i!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (expand "finseq_appl" )"15" (hide-all-but 1)"15" (typepred "fss!1" )"15" (expand "SPP?" )"15" (flatten)"15" (rewrite "delete_of_PP_is_PP" )"15" (rewrite "delete_of_SP_is_SP" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"term[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](s!1)" nil )"below[length(fss!1)]" replace_positionsnil )"below[length(delete[position[variable, symbol, arity]](fss!1, i!1))]" nil )"below[length(delete[position[variable, symbol, arity]](y!1`2, i!1))]" nil )"below[length(y!1`2)]" replace_positionsnil )"[s: term[variable, symbol, arity], SPP[variable, symbol, arity](s)]" nil )"[s: term[variable, symbol, arity], SPP[variable, symbol, arity](s)]" nil )"below[length(y!1`2)]" replace_positionsnil )"below[length(delete[position[variable, symbol, arity]](y!1`2, i!1))]" nil )"below[length(delete[position[variable, symbol, arity]](y!1`2, i!1))]" nil )"below[length(y!1`2)]" replace_positionsnil )"[s: term[variable, symbol, arity], SPP[variable, symbol, arity](s)]" nil )"[s: term[variable, symbol, arity], SPP[variable, symbol, arity](s)]" nil )"below[length(x!1`2)]" replace_positionsnil )"below[length(delete[position[variable, symbol, arity]](x!1`2, i1!1))]" nil )"term[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](y!1)" nil )"below[length(y!2)]" replace_positions nil )"below[length(delete[position[variable, symbol, arity]](y!2, i!1))]" nil )nil positions nil )nil positions nil )nil positions nil )nil positions nil )"below[length(delete[position[variable, symbol, arity]](y!2, i!1))]" nil )"below[length(y!2)]" replace_positions nil )"SPP[variable, symbol, arity](y!1)" nil )"term[variable, symbol, arity]" nil )nil replace_positionsnil )"posint" nil )nil seq_extras "structures/" )"below[length(x!2)]" replace_positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"term[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](x!1)" nil )"finseq" seq_extras "structures/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" positions nil )nil seq_extras "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: int | k <= i AND k <= j}" nil )"[numfield, numfield -> numfield]" number_fields nil )"below[length(rest(x!2))]" replace_positionsnil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"bool" positions nil )"bool" positions nil )"int" integers nil )nil seq_extras "structures/" )"T" seq_extras "structures/" )"bool" positions nil )nil replace_positions nil )nil seq_extras "structures/" )"[bool, bool -> bool]" booleans nil )"term" replacement nil )nil positions nil )"[T, T -> boolean]" equalities nil )nil positions nil )"positions" positions nil )"term" replace_positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" seq_extras "structures/" )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3455273398"" (measure-induct+ "fss1`length" ("s" "fss1" ))"" (skosimp*)"" (copy -2)"" (expand "equivalent" -3)"" (flatten)"" (case-replace "length(x!2) = 0" )"1" (hide-all-but (-1 -2 -4 1))"1" (expand "replace_pos" ) (("1" (assert ) nil nil ))nil ))nil )"2" (lemma "CP_lemma_aux2a2" )"2" (copy -1)"2" (inst -1 "t!1" "x!1" "x!2" "0" )"1" (replaces -1)"1" (inst -7 "0" )"1" (skosimp*)"1" (expand "finseq_appl" )"1" (inst -1 "t!1" "x!1" "fss2!1" "j!1" )"1" "1" replace -6 2)"1" "x!1" "delete(x!2, 0)" )"1" "t!1" "delete(fss2!1, j!1)" )"1" "1" (assert ) nil nil )"2" "2" expand "equivalent" )"2" "1" "1" expand "delete" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "different_elements" )"2" "2" expand "delete" )"2" assert )"2" expand "finseq_appl" )"2" "1 + i!1" "1 + j!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "different_elements" )"3" "3" expand "delete" )"3" expand "finseq_appl" )"3" "3" "3" "1" "i!1" "j!2" )"1" assert )nil nil ))nil )"2" "i!1" "1 + j!2" )"2" assert )nil nil ))nil )"3" "3" "1" "1 + i!1" "j!2" )"1" assert )nil nil ))nil )"2" "1 + i!1" "1 + j!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "finseq_appl" )"4" "4" "fspos.delete_equivalent" )"4" "x!2" "fss2!1" "0" "j!1" )"4" expand "finseq_appl" )"4" "1" expand "equivalent" )"1" expand "finseq_appl" )"1" "1" "i!1" )nil nil ))nil ))nil ))nil )"2" expand "equivalent" )"2" assert )"2" "2" expand "finseq_appl" )"2" "i!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"bool" seq_extras "structures/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"(strict_total_order?[real])" real_props nil )nil replace_positions nil )"term" replace_positions nil )"[T, T -> boolean]" equalities nil )"bool" seq_extras "structures/" )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil term_adt nil )"[symbol -> nat]" replace_positions 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 replace_positions nil )nil replace_positions nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.404Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
