Impressum critical_pairs_aux.prf
Sprache: Lisp
(critical_pairs_auxnil 3463227045"" (lemma "var_countable" ) (("" (propax) nil nil )) nil )nil critical_pairs_aux nil )) nil ))nil 3420220323"" (skosimp*)"" (typepred "fstp!1" )"" (expand "SPP?" )"" (flatten)"" (assert )"" (hide -1)"" (expand "SP?" )"" (skosimp*)"" (inst -1 "i!1" )"" (expand "finseq_appl" )"" (rewrite "ext_preserv_pos" ) 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]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil )nil substitution nil )"bool" reals nil )"bool" positions nil ))nil ))nil 3455274769 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil critical_pairs_aux nil )nil critical_pairs_aux 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]" critical_pairs_aux nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution 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" functions nil )"bool" finite_sets nil )"bool" positions nil )"bool" reals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil ))nil ))nil 3420225063"" (measure-induct+ "length(fstp)" ("t" "fstp" ))"1" (skosimp*)"1" (expand "finseq_appl" )"1" (case-replace "length(x!2) = 0" )"1" (hide-all-but (-1 1))"1" (expand "replace_pos" )"1" (lift-if)"1" (assert )"1" (expand "iterate" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "iterate" 2)"2" (prop)"2" (hide 3)"2" (expand "o" )"2" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2,length(x!2) - 1))" )"1" (prop)"1" "x!1" "delete(x!2, length(x!2) - 1)" )"1" (inst -1 "R!1" "x!3" "sg1!1" "sg2!1" )"1" (prop)"1" case "length(delete(x!2, length(x!2) - 1)) = length(x!2) - 1" )"1" (replaces -1) nil nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" (hide-all-but (-1 1 3))"2" "2" "fspos.delete_pos" )"2" "2" assert )"2" "i!1" )"1" "i!1" )"1" expand "finseq_appl" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 3))"3" (rewrite "length_delete" ) nil nil ))nil ))nil ))nil )"2" (hide-all-but (1 3))"2" (typepred "x!2" )"2" (expand "SPP?" )"2" "2" rewrite "delete_of_PP_is_PP" )"2" rewrite "delete_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (1 3))"3" (grind) nil nil )) nil ))nil )"2" (hide -1)"2" (lemma "preserv_unchanged_subterms" )"2" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "last(x!2)" )"1" (prop)"1" "replace_subterm_of_term" )"1" "last(x!2)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1))" )"1" "1" "1" expand "last" )"1" expand "finseq_appl" )"1" "x!2`length - 1" )"1" "subterm_ext_commute" )"1" "x!2`seq(x!2`length - 1)" "x!1" "sg1!1" )"1" "1" "1" "1" expand *"comp_cont?" "RSigma" )"1" "x!3" )"1" assert )"1" "x!2`seq(x!2`length - 1)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1))" )"1" "1" "sg1!1(x!3)" "sg2!1(x!3)" )"1" assert )"1" replace "1" "1" "x!3" )"1" expand "V" )"1" expand "ext" "1" assert )"1" "replace_pos(ext(sg1!1)(x!1), sg2!1(x!3), x!2) = replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1)), sg2!1(x!3), x!2`seq(x!2`length - 1))" )"1" "1" "fspos.add_last_delete" )"1" "1" assert )"1" "RTermTemp" "replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1)), sg2!1(x!3), x!2`seq(x!2`length - 1))" )"1" "1" "1" expand "RTermTemp" )"1" "CP_lemma_aux2a" )"1" "sg2!1(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "last(x!2)" )"1" "1" expand "ext" "1" expand *"last" "finseq_appl" )nil nil ))nil )"2" "2" case "length(x!2) = 1" )"1" nil nil )"2" "2" "x!2" )"2" "2" "fspos.delete_pos" )"2" expand "finseq_appl" )"2" "2" assert )"2" "i!1" )"1" expand "SPP?" )"1" "1" "1" expand *"last" "finseq_appl" )"1" replace "1" expand "PP?" )"1" "i!1" "x!2`length - 1" )"1" expand "finseq_appl" )"1" assert )"1" "1" "i!1" )"1" nil nil ))nil ))nil ))nil ))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 )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" expand *"last" "finseq_appl" )"2" "x!2`length - 1" )"2" rewrite "ext_preserv_pos" )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" "preserv_all_parallel_positions" )"2" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "x!2`seq(x!2`length - 1)" )"1" assert )"1" case "length(delete(x!2, length(x!2) - 1)) = 0" )"1" "1" nil nil ))nil )"2" "2" "2" "x!2" )"2" expand "SPP?" )"2" "2" expand "PP?" )"2" "1" "1" nil nil ))nil )"2" "fspos.delete_pos" )"2" "2" assert )"2" "i!1" )"1" expand "finseq_appl" )"1" "i!1" "x!2`length - 1" )"1" "1" assert )nil nil )"2" "2" "i!1" )"2" 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 )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" "x!2`length - 1" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" "x!2`length - 1" )"1" expand "finseq_appl" )"1" nil nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand * "last" "finseq_appl" )"2" "preserv_all_parallel_positions" )"2" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "x!2`seq(x!2`length - 1)" )"1" assert )"1" case "length(delete(x!2, length(x!2) - 1)) = 0" )"1" "1" nil nil ))nil )"2" "2" "2" "x!2" )"2" expand "SPP?" )"2" "2" expand "PP?" )"2" "1" "1" nil nil ))nil )"2" "fspos.delete_pos" )"2" "2" assert )"2" "i!1" )"1" "i!1" "x!2`length - 1" )"1" "1" expand "finseq_appl" )"1" assert )nil 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 ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" "x!2`length - 1" )"1" expand "finseq_appl" )"1" rewrite "ext_preserv_pos" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand * "last" "finseq_appl" )"2" case "length(delete(x!2, length(x!2) - 1)) = 0" )"1" "1" (grind) nil nil ))nil )"2" "2" "x!2" )"2" expand "SPP?" )"2" "2" expand "PP?" )"2" "1" "1" nil nil ))nil )"2" "fspos.delete_pos" )"2" "2" assert )"2" "i!1" )"1" "i!1" "x!2`length - 1" )"1" "1" expand "finseq_appl" )"1" assert )nil 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 )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 3))"2" "x!2" )"2" expand "SPP?" )"2" "2" "2" expand "SP?" )"2" expand *"last" "finseq_appl" )"2" "x!2`length - 1" )"1" rewrite "ext_preserv_pos" )nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (rewrite "delete_of_PP_is_PP" )"2" "2" expand "SP?" )"2" case "length(delete(x!2, length(x!2) - 1)) = 0" )"1" (grind) nil nil )"2" "2" "fspos.delete_pos" )"2" "2" assert )"2" "i!1" )"1" expand "finseq_appl" )"1" "i!1" )"1" replace -1 2 rl)"1" "1" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) 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 -1 "i!1" )"2" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (hide -1)"3" (expand "SP?" ) (("3" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (hide-all-but 1)"4" (typepred "y!2" )"4" (expand "SPP?" )"4" (flatten)"4" (assert )"4" (hide -1)"4" (expand "SP?" )"4" (skosimp*)"4" (inst -1 "i!1" )"4" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp*)"5" (typepred "y!2" )"5" (expand "SPP?" )"5" (flatten)"5" (hide -1)"5" (expand "SP?" ) (("5" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*)"6" (typepred "x!1`2" )"6" (hide-all-but (-1 1))"6" (expand "SPP?" )"6" (flatten)"6" (assert )"6" (hide -1)"6" (expand "SP?" )"6" (skosimp*)"6" (inst -1 "i!1" )"6" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide-all-but 1)"7" (typepred "y!1`2" )"7" (expand "SPP?" )"7" (flatten)"7" (assert )"7" (hide -1)"7" (expand "SP?" )"7" (skosimp*)"7" (inst -1 "i!1" )"7" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide-all-but 1)"8" (skosimp*)"8" (typepred "y!1`2" )"8" (expand "SPP?" )"8" (flatten)"8" (hide -1)"8" (expand "SP?" ) (("8" (inst?) nil nil )) 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" (hide -1)"9" (expand "SP?" ) (("9" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but 1)"10" (typepred "y!1`2" )"10" (expand "SPP?" )"10" (flatten)"10" (assert )"10" (hide -1)"10" (expand "SP?" )"10" (skosimp*)"10" (inst -1 "i!1" )"10" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (hide-all-but 1)"11" (skosimp*)"11" (typepred "y!1`2" )"11" (expand "SPP?" )"11" (flatten)"11" (hide -1)"11" (expand "SP?" ) (("11" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (hide-all-but 1)"12" (typepred "y!1`2" )"12" (expand "SPP?" )"12" (flatten)"12" (assert )"12" (hide -1)"12" (expand "SP?" )"12" (skosimp*)"12" (inst -1 "i!1" )"12" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (hide-all-but 1)"13" (skosimp*)"13" (typepred "y!1`2" )"13" (expand "SPP?" )"13" (flatten)"13" (hide -1)"13" (expand "SP?" ) (("13" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide-all-but 1)"14" (skosimp*)"14" (typepred "fstp!1" )"14" (expand "SPP?" )"14" (flatten)"14" (hide -1)"14" (expand "SP?" ) (("14" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (hide 2)"15" (typepred "fstp!1" )"15" (expand "SPP?" )"15" (flatten)"15" (assert )"15" (hide -1)"15" (expand "SP?" )"15" (skosimp*)"15" (inst -1 "i!1" )"15" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" relation_props nil )"below " nil )nil positions nil )"bool" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil )nil seq_extras "structures/" )nil seq_extras "structures/" )NOT const-decl "[bool -> bool]" booleans nil )"below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_auxnil )"posint" nil )nil replace_positions nil )"below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_auxnil )nil substitution nil )"nonneg_int" nil )"below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_auxnil )nil replace_positionsnil )"term" replacement nil )nil seq_extras "structures/" )"term[variable, symbol, arity]" nil )"below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_auxnil )"finseq" finite_sequences nil )"bool" positions nil )"bool" positions nil )"even_int" integersnil )nil substitution nil )nil replace_positions nil )nil replacement nil )"below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_auxnil )"T" seq_extras "structures/" )nil seq_extras "structures/" )"boolean" notequal nil )"finseq" seq_extras "structures/" )"Sub[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](x!1)" nil )"term[variable, symbol, arity]" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"pred[[T, T]]" relation_iterate "orders/" )"bool" substitution nil )"bool" compatibility nil )"term" subterm nil )nil positions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term" replace_positions nil )nil positions nil )"positions" positions 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 )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]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3420220323 ("" (subtype-tcc) nil nil )NOT const-decl "[bool -> bool]" booleans nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution 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 )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"bool" finite_sets nil )"bool" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finseq" finite_sequences nil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )"bool" positions nil )"bool" positions nil ))nil ))nil 3420220323"" (skolem-typepred)"" (flatten)"" (hide-all-but 1)"" (expand "SPP?" )"" (split)"1" (grind) nil nil )"2" (expand * "SP?" "nth_seq" "#" "finseq_appl" )"2" (skosimp*)"2" (typepred "q!1" )"2" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" positions nil )nil substitution nil )"posint" nil )"finite_sequence[T]" set2seq "structures/" )"bool" positions nil )"(strict_total_order?[real])" real_props 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 substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3420220323"" (skolem-typepred)"" (skosimp*)"" (expand "SPP?" )"" (flatten)"" (split)"1" (rewrite "add_first_parallel_pos_to_PP_is_PP" )"1" (hide-all-but (-7 1))"1" (skosimp*)"1" (inst?)"1" (expand "finseq_appl" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "add_first_parallel_pos_to_SP_is_SP" )"1" (hide-all-but (1 -6))"1" (rewrite "ext_preserv_pos" ) nil nil )) nil )"2" (hide-all-but (-5 1))"2" (expand "SP?" )"2" (skosimp*)"2" (inst?)"2" (rewrite "ext_preserv_pos" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil positions nil )ext def-decl "term" substitution nil )"bool" positions nil )nil positions nil )nil substitution nil )nil positions nil )"bool" positions nil )nil positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" reals nil )nil positions nil )"positions" positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil finite_sequences nil )nil positions nil )nil integers nil )"bool" reals nil )nil integers nil )nil nat_types nil )nil substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3420227790"" (measure-induct+ "length(fst)" ("t" "fst" ))"1" (skosimp*)"1" (case "length(x!2) = 0" )"1" (hide-all-but (-1 1))"1" (replace -1 1)"1" (rewrite "empty_0" )"1" (replaces -1)"1" (rewrite "add_first_empty_seq" )"1" (expand "iterate" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "finseq_appl" )"2" (inst -1 "x!1" "rest(x!2)" )"1" (inst -1 "R!1" "x!3" "sg1!1" "sg2!1" "q!1" )"1" (rewrite "length_rest" )"1" (prop)"1" "length(rest(x!2)) = length(x!2) -1" "1" (expand "iterate" 2)"1" (assert )"1" (expand "o" )"1" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), add_first(q!1, rest(x!2)))" )"1" (assert )"1" "1" "CP_lemma_aux2a1" )"1" "1" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "x!2" "q!1" )"1" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "q!1" )"1" expand "finseq_appl" )"1" "1" "1" "1" "preserv_unchanged_subterms" )"1" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2(0)" )"1" expand "finseq_appl" )"1" "1" "replace_subterm_of_term" )"1" "x!2(0)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2))" )"1" expand "finseq_appl" )"1" "1" "1" "subterm_ext_commute" )"1" "x!2(0)" "x!1" "sg1!1" )"1" expand "finseq_appl" )"1" "1" "0" )"1" "1" "1" "1" "1" replace "1" "1" "fspos.seq_first_rest" )"1" "1" assert )"1" expand *"first" "finseq_appl" )"1" "RTTemp" "replaceTerm(replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2)), ext(sg1!1)(x!3), x!2`seq(0)), ext(sg2!1)(x!3), q!1)" )"1" replace "1" "1" "CP_lemma_aux2a1" )"1" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2`seq(0)" )"1" "1" "1" expand "RTTemp" )"1" assert )"1" "replace_commutativity" )"1" "1" "repTemp" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2))" )"1" "x!2`seq(0)" "q!1" "ext(sg2!1)(x!3)" "repTemp" "ext(sg1!1)(x!3)" )"1" "x!2`seq(0)" "q!1" "ext(sg2!1)(x!3)" "repTemp" "ext(sg2!1)(x!3)" )"1" "1" "1" "1" "REPLACEtemp" "replaceTerm(repTemp, ext(sg2!1)(x!3), q!1)" )"1" "x!3" )"1" expand *"V" "ext" )"1" assert )"1" expand *"comp_cont?" "RSigma" )"1" "x!2`seq(0)" "REPLACEtemp" )"1" "x!3" )"1" "1" "sg1!1(x!3)" "sg2!1(x!3)" )"1" assert )nil nil ))nil )"2" "2" expand "REPLACEtemp" )"2" expand "repTemp" )"2" "q!1" )"2" "preserv_all_parallel_positions" )"2" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "q!1" )"1" "1" "preserv_all_parallel_positions" )"1" "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2`seq(0)" )"1" "1" "replace_preserv_parallel_pos" )"1" "q!1" "x!2`seq(0)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2))" "ext(sg2!1)(x!3)" )"1" assert )"1" "1" rewrite "parallel_comm" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "rest_parallel_first" )nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "rest_parallel_pos_parallel" )"2" "2" "q!1" )"2" "1" nil nil )"2" "2" "2" expand "finseq_appl" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "repTemp" )"2" rewrite "preserv_all_parallel_positions" )"1" "1" case "length(rest(x!2)) = 0" )"1" "1" nil nil ))nil )"2" "x!2" )"2" expand *"SPP?" "PP?" )"2" "2" "2" "1" nil nil )"2" "2" "i!1 + 1" "0" )"1" assert )"1" "fspos.rest_pos" )"1" "1" assert )"1" "i!1" )"1" expand "finseq_appl" )"1" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "repTemp" )"3" "3" rewrite "preserv_all_parallel_positions" )"1" "1" case "length(rest(x!2)) = 0" )"1" "1" nil nil ))nil )"2" "2" "i!1 + 1" )"1" "fspos.rest_pos" )"1" expand "finseq_appl" )"1" "1" assert )"1" "i!1" )"1" assert )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 ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "repTemp" )"4" rewrite "preserv_all_parallel_positions" )"1" "1" "1" "x!2" )"1" expand "SPP?" )"1" "1" "rest_parallel_first" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" expand "repTemp" )"5" rewrite "preserv_all_parallel_positions" )"1" "1" "1" "rest_parallel_first" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "6" expand "repTemp" )"6" rewrite "preserv_all_parallel_positions" )"1" "1" "1" "rest_parallel_pos_parallel" )"1" "1" "q!1" )"1" "1" nil nil )"2" "2" "2" expand "finseq_appl" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"7" "7" expand "repTemp" )"7" rewrite "preserv_all_parallel_positions" )"1" "1" "x!2" )"1" "1" "rest_parallel_pos_parallel" )"1" "1" "q!1" )"1" "1" nil nil )"2" "2" "2" expand "finseq_appl" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"8" "8" expand "repTemp" )"8" rewrite "preserv_all_parallel_positions" )"1" "1" "x!2" )"1" "1" "1" "rest_parallel_first" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" "9" expand "repTemp" )"9" rewrite "preserv_all_parallel_positions" )"1" "1" "1" "rest_parallel_pos_parallel" )"1" "1" "q!1" )"1" "1" nil nil )"2" "2" "2" expand "finseq_appl" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "rest_parallel_first" )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "ext_parallel_pos" )"3" "3" "x!2" )"3" expand "SPP?" )"3" "3" rewrite "rest_of_PP_is_PP" )"3" rewrite "rest_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "preserv_all_parallel_positions" )"1" "1" "rest_parallel_first" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "rest_parallel_first" )"2" "2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "rest_parallel_pos_parallel" )"2" "2" "q!1" )"2" expand "finseq_appl" )"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "i!1" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" "rest_parallel_pos_parallel" )"4" "4" "q!1" )"4" expand "finseq_appl" )"4" "4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil )"3" "3" rewrite "ext_parallel_pos" )"3" "3" "x!2" )"3" expand "SPP?" )"3" "3" rewrite "rest_of_PP_is_PP" )"3" rewrite "rest_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "q!1" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil )"3" "3" rewrite "ext_parallel_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 2)) (("2" (grind) nil nil ))nil ))nil )"2" (hide-all-but (-1 1 2))"2" (case "length(rest(x!2)) = 0" )"1" (hide -2) (("1" (grind) nil nil )) nil )"2" (skosimp*)"2" (lemma "fspos.rest_pos" )"2" (inst?)"2" (assert )"2" "i!1" )"1" expand "finseq_appl" )"1" "i!1 + 1" )"1" replace -1 2 rl)"1" "1" (assert ) nil nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) 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 )"2" (hide-all-but 1)"2" (typepred "x!2" )"2" (expand "SPP?" )"2" (flatten)"2" (rewrite "rest_of_PP_is_PP" )"2" (rewrite "rest_of_SP_is_SP" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (expand "finseq_appl" )"2" (lemma "add_parallel_pos" )"2" (inst?)"2" (prop)"2" (hide 2)"2" (skosimp*)"2" (inst?)"2" (expand "finseq_appl" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (expand "SPP?" )"3" (split)"1" (expand "PP?" )"1" (prop) (("1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (typepred "q!1" )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp*)"4" (expand "finseq_appl" )"4" (typepred "y!2" )"4" (expand * "SPP?" "SP?" )"4" (flatten)"4" (inst?)"4" (expand "finseq_appl" ) (("4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp*)"5" (hide (-2 -3 -4))"5" (lemma "add_parallel_pos" )"5" (inst?)"5" (prop)"5" (hide 2)"5" (skosimp*)"5" (expand "finseq_appl" )"5" (inst?) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide (-1 2))"6" (skosimp*)"6" (hide-all-but 1)"6" (expand "SPP?" )"6" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide (-1 2))"7" (skosimp*)"7" (hide -1)"7" (expand "finseq_appl" )"7" (typepred "y!2" )"7" (expand * "SPP?" "SP?" )"7" (flatten)"7" (inst?)"7" (expand "finseq_appl" )"7" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" (hide-all-but 1)"8" (skosimp*)"8" (hide (-2 -3 -4))"8" (lemma "add_parallel_pos" )"8" (inst?)"8" (prop)"8" (hide 2)"8" (skosimp*)"8" (expand "finseq_appl" )"8" (inst?) (("8" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" (hide-all-but (-1 1))"9" (lemma "add_parallel_pos" )"9" (inst?)"9" (prop)"9" (hide 2)"9" (skosimp*)"9" (expand "finseq_appl" )"9" (inst?) (("9" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (hide-all-but 1)"10" (expand "SPP?" )"10" (split)"1" (expand "PP?" )"1" (prop) (("1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (hide-all-but 1)"11" (skosimp*)"11" (hide -1)"11" (typepred "y!1`2" )"11" (expand * "SPP?" "SP?" )"11" (flatten) (("11" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (hide-all-but 1)"12" (expand "SPP?" )"12" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (hide-all-but (-1 1))"13" (lemma "add_parallel_pos" )"13" (inst?)"13" (prop)"13" (hide 2)"13" (skosimp*)"13" (expand "finseq_appl" )"13" (inst?) (("13" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"14" (hide-all-but 1)"14" (expand "SPP?" )"14" (split)"1" (expand "PP?" )"1" (prop) (("1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (hide-all-but 1)"15" (skosimp*)"15" (hide -1)"15" (typepred "y!1`2" )"15" (expand * "SPP?" "SP?" )"15" (flatten) (("15" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"16" (expand "finseq_appl" )"16" (hide-all-but 1)"16" (skosimp*)"16" (hide -1)"16" (typepred "x!1`2" )"16" (expand * "SPP?" "SP?" )"16" (flatten)"16" (inst?)"16" (expand "finseq_appl" )"16" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"17" (hide-all-but (-1 1))"17" (lemma "add_parallel_pos" )"17" (inst?)"17" (prop)"17" (hide 2)"17" (skosimp*)"17" (expand "finseq_appl" )"17" (inst?) (("17" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"18" (hide-all-but 1)"18" (expand "SPP?" )"18" (split)"1" (expand "PP?" )"1" (prop) (("1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"19" (hide-all-but 1)"19" (skosimp*)"19" (hide -1)"19" (expand "finseq_appl" )"19" (typepred "y!1`2" )"19" (expand * "SPP?" "SP?" )"19" (flatten)"19" (inst?)"19" (expand "finseq_appl" )"19" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"20" (hide-all-but 1)"20" (skosimp*)"20" (hide (-2 -3 -4))"20" (lemma "add_parallel_pos" )"20" (inst?)"20" (prop)"20" (hide 2)"20" (skosimp*)"20" (expand "finseq_appl" )"20" (inst?) (("20" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"21" (hide-all-but 1)"21" (skosimp*)"21" (hide (-1 -2 -3 -4))"21" (expand "SPP?" )"21" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"22" (hide-all-but 1)"22" (skosimp*)"22" (expand "finseq_appl" )"22" (typepred "y!1`2" )"22" (expand * "SPP?" "SP?" )"22" (flatten)"22" (inst?)"22" (expand "finseq_appl" )"22" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"23" (hide-all-but (-1 1))"23" (lemma "add_parallel_pos" )"23" (inst?)"23" (prop)"23" (hide 2)"23" (skosimp*)"23" (expand "finseq_appl" )"23" (inst?) (("23" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"24" (hide-all-but 1)"24" (expand "SPP?" )"24" (split)"1" (expand "PP?" )"1" (prop) (("1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil )"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (typepred "q!1" )"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"25" (hide-all-but 1)"25" (typepred "fst!1" )"25" (expand * "SPP?" "SP?" )"25" (flatten) (("25" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )nil substitution nil )"bool" relation_props nil )nil replace_positions nil )"Sub[variable, symbol, arity]" nil )"positions?[variable, symbol, arity](x!1)" nil )nil replace_positions nil )nil replacement nil )nil seq_extras "structures/" )"term" replacement nil )NOT const-decl "[bool -> bool]" booleans nil )"term[variable, symbol, arity]" nil )nil substitution nil )"bool" positions nil )nil substitution nil )nil positions nil )nil replacement nil )nil substitution nil )nil replace_positionsnil )"term[variable, symbol, arity]" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"below[length(rest(x!2))]" nil )nil seq_extras "structures/" )"int" integers nil )"bool" positions 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 )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"below[length(rest(x!2))]" nil )nil replacement nil )"term[variable, symbol, arity]" nil )nil substitution nil )nil positions nil )nil positions nil )nil positions nil )nil positions nil )"T" seq_extras "structures/" )nil substitution nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"below[length(rest(x!2))]" nil )nil seq_extras "structures/" )"SPP[variable, symbol, arity](x!1)" nil )"finseq" seq_extras "structures/" )"term[variable, symbol, arity]" nil )nil seq_extras "structures/" )nil seq_extras "structures/" )"term" replace_positions nil )"pred[[T, T]]" relation_iterate "orders/" )"finseq" seq_extras "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"term" subterm nil )"bool" compatibility nil )"bool" substitution nil )ext def-decl "term" substitution nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )nil positions nil )"positions" positions nil )nil positions nil )"[bool, bool -> bool]" booleans nil )"bool" 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]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3420220323"" (skolem-typepred)"" (flatten)"" (skosimp*)"" (hide (-1 -2 -3))"" (expand "SPP?" )"" (flatten)"" (hide -1)"" (expand "SP?" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))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 substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3420220323"" (skolem-typepred)"" (flatten)"" (skosimp*)"" (hide-all-but (-4 2))"" (expand "SPP?" )"" (flatten)"" (split)"1" (hide (-1 -2)) (("1" (grind) nil nil )) nil )"2" (hide -1)"2" (expand * "SP?" "finseq_appl" )"2" (skosimp*)"2" (expand * "#" "finseq_appl" )"2" (inst?)"2" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil substitution nil )"bool" positions nil )"(strict_total_order?[real])" real_props nil )"bool" positions nil )"finite_sequence[T]" set2seq "structures/" )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" 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 substitution nil )"bool" substitution nil )"set[term]" variables_term nil )set type-eq-decl nil sets nil ) (term type-decl nil term_adt nil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3420220323 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"[below[length(fs)] -> T]" finite_sequencesnil )"[symbol -> nat]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )"bool" compatibility nil )"bool" substitution nil )"posint" nil ))nil ))nil 3420228904"" (measure-induct+ "length(fstp)" ("t" "fstp" ))"1" (skolem 1 ("R" "x" "sg1" "sg2" ))"1" (flatten)"1" (skosimp*)"1" (case "length(rest(x!2)) = 0" )"1" (hide-all-but (-1 1 2))"1" (lemma "fspos.length_rest_0" )"1" (inst?)"1" (assert )"1" (replace -1 2)"1" (typepred "i!1" )"1" (replaces -2 (-1 2))"1" (expand "finseq_appl" )"1" (expand "replace_pos" )"1" "1" "1" "1" (grind) nil nil ))nil )"2" case "length(rest( #(x!2`seq(i!1)))) = 0" )"1" expand "replace_pos" )"1" assert )"1" "1" expand *"iterate" "#" "finseq_appl" )"1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "finseq_appl" )"2" (case-replace "i!1 = 0" )"1" (hide -2)"1" (lemma "CP_lemma_aux2c1" )"1" "R" "x!1" "x" "sg1" "sg2" "rest(x!2)" "x!2`seq(0)" )"1" (prop)"1" (lemma "fspos.seq_first_rest" )"1" (inst?)"1" (assert )"1" expand * "first" "finseq_appl" )"1" replace -1 -2 rl)"1" "length(rest(x!2)) = length(x!2) - 1" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (split)"1" (hide-all-but (1 2 3))"1" expand "finseq_appl" )"1" "rest_parallel_first" )"1" "1" assert )"1" "1" expand "finseq_appl" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-2 1 2 3))"2" "fspos.rest_pos" )"2" "x!2" )"2" assert )"2" "i!2" )"1" expand "finseq_appl" )"1" replace -1 1 rl)"1" "i!2 + 1" )"1" (assert ) nil nil )"2" "2" "i!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but (-2 1))"3" (inst -1 "0" ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (typepred "x!2" )"2" (expand * "SPP?" "SP?" )"2" (flatten)"2" "2" expand "finseq_appl" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (typepred "x!2" )"3" (expand "SPP?" )"3" (flatten)"3" rewrite "rest_of_PP_is_PP" )"3" rewrite "rest_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "iterate" 4)"2" (prop)"1" (hide-all-but (-1 3 4))"1" (grind) nil nil )) nil )"2" (expand "o" )"2" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))" )"1" (split)"1" (inst -1 "x!1" "rest(x!2)" )"1" (inst -1 "R" "x" "sg1" "sg2" )"1" rewrite "length_rest" )"1" assert )"1" "1" "i!1 - 1" )"1" "length(rest(x!2)) = length(x!2) - 1" "1" assert )"1" "fspos.rest_pos" )"1" "1" assert )"1" "i!1 - 1" )"1" expand "finseq_appl" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" "i!1" )"2" (grind) nil nil ))nil ))nil ))nil )"2" "2" "2" "fspos.rest_pos" )"2" "2" assert )"2" "i!2" )"1" expand "finseq_appl" )"1" replace -1 1 rl)"1" "1 + i!2" )nil nil ))nil ))nil )"2" "2" "i!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "x!2" )"2" expand "SPP?" )"2" "2" rewrite "rest_of_PP_is_PP" )"2" rewrite "rest_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (lemma "fspos.seq_first_rest" )"2" "2" assert )"2" "RErestTemp" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))" )"2" replace -1 1)"2" expand * "first" "finseq_appl" )"2" "2" "CP_lemma_aux2a1" )"2" "1" "1" "1" expand "RErestTemp" )"1" "preserv_unchanged_subterms" )"1" "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)" )"1" "1" "0" )"1" "subterm_ext_commute" )"1" "x!2`seq(0)" "x!1" "sg1" )"1" "1" "1" "1" "replace_subterm_of_term" )"1" "x!2`seq(0)" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))" )"1" "1" "1" "REPtemp" "replaceTerm(replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2)), ext(sg2)(x), x!2`seq(0))" )"1" replace "1" expand "REPtemp" )"1" "1" expand *"comp_cont?" "RSigma" )"1" "x" )"1" expand "V" )"1" expand "ext" "1" assert )"1" "x!2`seq(0)" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))" )"1" "x" )"1" "1" "1" "sg1(x)" "sg2(x)" )"1" assert )nil nil ))nil ))nil )"2" "2" "preserv_all_parallel_positions" )"2" "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)" )"1" "1" "1" rewrite "rest_parallel_first" )nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )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" "preserv_all_parallel_positions" )"2" "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)" )"1" "1" "1" rewrite "rest_parallel_first" )nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "rest_parallel_first" )nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "rest_parallel_first" )nil nil ))nil ))nil )"2" "2" "x!2" )"2" expand *"SPP?" "SP?" )"2" "2" "2" "0" )"2" expand "finseq_appl" )"2" rewrite "ext_preserv_pos" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!2" )"3" expand "SPP?" )"3" "3" rewrite "rest_of_PP_is_PP" )"3" "3" expand "SP?" )"3" "3" "fspos.rest_pos" )"3" "3" assert )"3" "i!2" )"1" expand "finseq_appl" )"1" replace "1" "1" "1 + i!2" )"1" rewrite "ext_preserv_pos" )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 4 5))"2" (rewrite "ext_parallel_pos" )"2" (hide 2)"2" "x!2" )"2" expand "SPP?" )"2" "2" rewrite "rest_of_PP_is_PP" )"2" rewrite "rest_of_SP_is_SP" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 2)"2" (skosimp*)"2" (typepred "y!2" )"2" (expand * "SPP?" "SP?" )"2" (flatten)"2" (assert )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (hide -1)"2" (rewrite "ext_preserv_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 2)"3" (skosimp*)"3" (typepred "y!2" )"3" (expand "SPP?" )"3" (flatten)"3" (split)"1" (hide (-1 -2))"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 2)"4" (skosimp*)"4" (typepred "y!2" )"4" (expand * "SPP?" "SP?" )"4" (flatten) (("4" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (skosimp*)"5" (hide (-2 -3))"5" (lemma "ext_parallel_pos" ) (("5" (inst?) nil nil ))nil ))nil ))nil ))nil )"6" (hide-all-but 1)"6" (skosimp*)"6" (hide-all-but 2)"6" (typepred "y!2" )"6" (expand "SPP?" )"6" (flatten)"6" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (hide-all-but 1)"7" (skosimp*)"7" (typepred "y!2" )"7" (expand * "SPP?" "SP?" )"7" (flatten) (("7" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"8" (hide-all-but 1)"8" (skosimp*)"8" (hide-all-but 2)"8" (typepred "x!1`2" )"8" (lemma "ext_parallel_pos" ) (("8" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"9" (hide-all-but 2)"9" (skosimp*)"9" (typepred "y!1`2" )"9" (lemma "ext_parallel_pos" ) (("9" (inst?) nil nil ))nil ))nil ))nil ))nil )"10" (hide-all-but 2)"10" (skosimp*)"10" (typepred "y!1`2" )"10" (expand "SPP?" )"10" (flatten)"10" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (hide-all-but 2)"11" (skosimp*)"11" (typepred "y!1`2" )"11" (expand * "SPP?" "SP?" )"11" (flatten) (("11" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"12" (hide-all-but 1)"12" (skosimp*)"12" (hide (-2 -3))"12" (typepred "x!1`2" )"12" (expand "SPP?" )"12" (flatten)"12" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (hide-all-but 2)"13" (skosimp*)"13" (lemma "ext_parallel_pos" ) (("13" (inst?) nil nil ))nil ))nil ))nil )"14" (hide-all-but 2)"14" (skosimp*)"14" (typepred "y!1`2" )"14" (expand "SPP?" )"14" (flatten)"14" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"15" (hide-all-but 2)"15" (skosimp*)"15" (typepred "y!1`2" )"15" (expand * "SPP?" "SP?" )"15" (flatten) (("15" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"16" (hide-all-but 1)"16" (skosimp*)"16" (typepred "x!1`2" )"16" (expand * "SPP?" "SP?" )"16" (flatten) (("16" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"17" (hide-all-but 2)"17" (skosimp*)"17" (lemma "ext_parallel_pos" ) (("17" (inst?) nil nil ))nil ))nil ))nil )"18" (hide-all-but 2)"18" (skosimp*)"18" (typepred "y!1`2" )"18" (expand "SPP?" )"18" (flatten)"18" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"19" (hide-all-but 2)"19" (skosimp*)"19" (typepred "y!1`2" )"19" (expand * "SPP?" "SP?" )"19" (flatten) (("19" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"20" (hide-all-but 1)"20" (skosimp*)"20" (hide-all-but 2)"20" (lemma "ext_parallel_pos" ) (("20" (inst?) nil nil ))nil ))nil ))nil ))nil )"21" (hide-all-but 1)"21" (skosimp*)"21" (hide-all-but 2)"21" (typepred "y!1`2" )"21" (expand "SPP?" )"21" (flatten)"21" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"22" (hide-all-but 1)"22" (skosimp*)"22" (typepred "y!1`2" )"22" (expand * "SPP?" "SP?" )"22" (flatten) (("22" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"23" (hide-all-but 2)"23" (skosimp*)"23" (lemma "ext_parallel_pos" ) (("23" (inst?) nil nil ))nil ))nil ))nil )"24" (hide-all-but 2)"24" (skosimp*)"24" (typepred "fstp!1" )"24" (expand "SPP?" )"24" (flatten)"24" (split)"1" (expand "PP?" )"1" (prop)"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide -1)"2" (expand "SP?" )"2" (skosimp*)"2" (expand "finseq_appl" )"2" (inst?)"2" (lemma "ext_preserv_pos" )"2" (inst?) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"25" (hide-all-but 2)"25" (skosimp*)"25" (typepred "fstp!1" )"25" (expand * "SPP?" "SP?" )"25" (flatten) (("25" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" relation_props nil )nil substitution nil )"below[length(rest(x!2))]" nil )"below[length(x!2)]" critical_pairs_aux nil )"int" integers nil )nil seq_extras "structures/" )nil replace_positions nil )nil substitution nil )nil replace_positionsnil )nil substitution nil )"term[variable, symbol, arity]" nil )"term" replacement nil )nil replacement nil )"term[variable, symbol, arity]" nil )"below[length(rest[position[variable, symbol, arity]](x!2))]" nil )nil replace_positions nil )"Sub[variable, symbol, arity]" nil )"term[variable, symbol, arity]" nil )"SPP[variable, symbol, arity](x!1)" nil )"below[length(rest(x!2))]" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil seq_extras "structures/" )nil substitution nil )nil seq_extras "structures/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"T" seq_extras "structures/" )"bool" positions nil )nil positions nil )nil positions nil )nil positions nil )"bool" positions nil )nil positions nil )nil critical_pairs_aux nil )"posint" nil )"{k: int | k <= i AND k <= j}" nil )"{k: nat | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"finseq" finite_sequences nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil seq_extras "structures/" )"finseq" seq_extras "structures/" )"term" replace_positions nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"pred[[T, T]]" relation_iterate "orders/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil positions nil )"term" subterm nil )"bool" compatibility nil )"bool" substitution nil )ext def-decl "term" substitution nil )nil finite_sequences nil )"finite_sequence[T]" set2seq "structures/" )set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil positions nil )"positions" positions nil )"[below[length(fs)] -> T]" finite_sequencesnil )"int" integers 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]" critical_pairs_aux 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 critical_pairs_aux nil )nil critical_pairs_aux nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))nil 3420220323"" (skosimp*)"" (replaces -1)"" (lemma "Pos_var_is_finite" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )nil subterm nil )nil critical_pairs_aux nil )nil critical_pairs_aux 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]" critical_pairs_aux nil ))nil ))nil 3420220323"" (skosimp*)"" (rewrite "ext_parallel_pos" )"" (hide (-2 -3 2))"" (expand "SPP?" )"" (lemma "pos_occ_var_HAStypePP" )"" (inst?)"" (assert )"" (lemma "pos_occ_var_HAStypeSP" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil substitution nil )nil term_adt nil ) (set type-eq-decl nil sets nil )"set[term]" variables_term nil )"bool" substitution nil )nil substitution 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 finite_sequences nil )nil critical_pairs_aux nil )nil critical_pairs_aux 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]" critical_pairs_aux nil )nil subterm nil )nil subterm nil ))nil ))nil 3565129732"" (measure-induct+ "card(Pos_var(t,x))" ("t" "x" ))"1" (skeep)"1" (name-replace "seqvarsx!2" "set2seq(Pos_var(x!1, x!2))" )"1" (expand "replace_pos" 1)"1" (expand "finseq_appl" )"1" (lift-if)"1" (prop)"1" (hide -2)"1" (lemma "same_term" )"1" (inst?)"1" (assert )"1" (skeep)"1" (hide (-3 2))"1" (expand "RSigma" )"1" "x" )"1" "1" "1" expand "seqvarsx!2" )"1" expand "set2seq" )"1" "1" "1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "positionsOF(x!1)(seqvarsx!2`seq(0))" )"1" (lemma "exists_var" )"1" (inst -1 "Vars(x!1)" "Vars(x!1)" )"1" (skosimp*)"1" (rewrite "union_idempotent" )"1" "replaceTerm(x!1, z!1, seqvarsx!2`seq(0))" "x!2" )"1" "R" "gamma(sg1, sg2, x!2, z!1)" "gamma(sg2, sg2, x!2, z!1)" )"1" "1" "seqvarx2Term" "set2seq(Pos_var(replaceTerm(x!1, z!1, seqvarsx!2`seq(0)), x!2))" )"1" "x!2" "z!1" )"1" expand "V" )"1" expand "ext" -3 2)"1" assert )"1" expand "gamma" -3 2)"1" expand "ext" 3 (2 3))"1" "ext_replace_ext" )"1" "1" "1" "seqvarsx!2`seq(0)" "x!1" "gamma(sg2, sg2, x!2, z!1)" "z!1" )"1" "1" "1" "1" expand "ext" "1" expand "gamma" "1" "gamma_term" )"1" "1" assert )"1" "1" replace "1" "replace_subterm_of_term" )"1" "seqvarsx!2`seq(0)" "ext(sg2)(x!1)" )"1" "1" "subterm_ext_commute" )"1" "seqvarsx!2`seq(0)" "x!1" "sg2" )"1" assert )"1" "subtermOF(x!1, seqvarsx!2`seq(0)) = x!2" "1" "1" expand "ext" "1" "1" replace "1" "CP_lemma_aux2a3" )"1" "sg2(x!2)" "replaceTerm(ext(sg1)(x!1), sg2(x!2), seqvarsx!2`seq(0))" "rest(seqvarsx!2)" "seqvarx2Term" )"1" "1" assert )nil nil )"2" "2" expand "equivalent" )"2" expand "finseq_appl" )"2" "1" expand "seqvarx2Term" )"1" "rest(seqvarsx!2)`length = seqvarsx!2`length -1" "1" "set2seq_length[position]" )"1" "1" "1" "set2seq_length[position]" )"1" expand "seqvarsx!2" "1" "1" "1" "pos_occ_var_replace_as_diff" )"1" "1" "1" "1" "finite_sets[position].card_diff_subset" )"1" "singleton(seqvarsx!2`seq(0))" "Pos_var(x!1, x!2)" )"1" "1" rewrite "card_singleton" )"1" expand "difference" )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand *"subset?" "member" )"2" "2" expand "singleton" )"2" "2" "set2seq_lem[position]" )"2" expand "seqvarsx!2" "2" "2" assert )"2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "set2seq_lem[position]" )"2" expand "seqvarsx!2" "2" "2" assert )"2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand *"member" "Vars" "restrict" )"3" "seqvarsx!2`seq(0)" )"3" "3" "set2seq_lem[position]" )"3" expand "seqvarsx!2" )"3" "3" assert )"3" "0" )"3" expand "finseq_appl" )"3" expand "Pos_var" "3" expand "extend" "3" 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" nil nil ))nil ))nil ))nil )"2" expand "different_elements" )"2" "2" expand "finseq_appl" )"2" "rest_pos[position]" )"2" "seqvarsx!2" )"2" assert )"2" "rest_pos[position]" )"2" "seqvarsx!2" )"2" assert )"2" "i!1" )"1" "j!1" )"1" expand "finseq_appl" )"1" replace "1" replace "1" "1" "set2seq_neq[position]" )"1" expand "seqvarsx!2" )"1" "1" assert )"1" "1 + i!1" "1 + j!1" )"1" assert )"1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil )"2" "2" "j!1" )"2" expand "seqvarsx!2" "2" nil nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" expand "seqvarsx!2" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "different_elements" )"3" "3" expand "finseq_appl" )"3" "set2seq_neq[position]" )"3" expand "seqvarx2Term" )"3" "3" assert )"3" "i!1" "j!1" )"1" assert )"1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil )"2" "2" "j!1" )"2" expand "seqvarx2Term" )"2" rewrite "set2seq_length" )nil nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" expand "seqvarx2Term" )"3" rewrite "set2seq_length" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "rest_pos[position]" )"4" "4" assert )"4" "i!1" )"1" expand "finseq_appl" )"1" replace "1" expand "seqvarsx!2" "1" "set2seq_lem[position]" )"1" "1" assert )"1" "1 + i!1" )"1" expand "finseq_appl" )"1" expand "seqvarx2Term" )"1" case "Pos_var(replaceTerm(x!1, z!1, seqvarsx!2`seq(0)), x!2)(set2seq(Pos_var(x!1, x!2))`seq(1 + i!1))" )"1" "set2seq_exists[position]" )"1" "1" assert )"1" assert )"1" "1" expand "finseq_appl" )"1" assert )"1" "1" assert )nil nil )"2" "ii!1" )"2" expand "seqvarx2Term" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Pos_var_is_finite" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "pos_occ_var_replace_as_diff" )"2" "2" "1" "1" expand "difference" )"1" expand "member" )"1" assert )"1" expand "singleton" )"1" "1" "set2seq_neq[position]" )"1" expand "seqvarsx!2" )"1" "1" assert )"1" "1 + i!1" "0" )"1" expand "finseq_appl" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "seqvarsx!2" )"2" "set2seq_lem[position]" )"2" "2" assert )"2" "0" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand *"member" "Vars" "restrict" )"3" "seqvarsx!2`seq(0)" )"3" "3" "set2seq_lem[position]" )"3" expand "seqvarsx!2" )"3" "3" assert )"3" "0" )"3" expand "finseq_appl" )"3" expand "Pos_var" "3" expand "extend" "3" 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" )"2" expand "seqvarsx!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" nil nil ))nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.1.56Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
