| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 716 kB |
|
Quellcode-Bibliothek critical_pairs_aux.prfSprache: Lisp |
|||||||||||||||
|
(critical_pairs_aux (IMP_rewrite_rules_TCC1 0 (IMP_rewrite_rules_TCC1-1 nil 3463227045 ("" (lemma "var_countable") (("" (propax) nil nil)) nil) ((var_countable formula-decl nil critical_pairs_aux nil)) nil)) (CP_lemma_aux2b_TCC1 0 (CP_lemma_aux2b_TCC1-1 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) ((SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (ext_preserv_pos formula-decl nil substitution nil) (< const-decl "bool" reals nil) (SP? const-decl "bool" positions nil)) nil)) (CP_lemma_aux2b_TCC2 0 (CP_lemma_aux2b_TCC2-1 nil 3455274769 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (SP? const-decl "bool" positions nil) (< const-decl "bool" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (CP_lemma_aux2b 0 (CP_lemma_aux2b-1 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" (inst 2 "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2,length(x!2) - 1))") (("1" (prop) (("1" (inst -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" (hide-all-but (1 3)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (1 3)) (("3" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1 3)) (("2" (skosimp*) (("2" (lemma "fspos.delete_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (inst -2 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "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" (flatten) (("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" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "last(x!2)") (("1" (prop) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "last(x!2)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - 1))") (("1" (prop) (("1" (replaces -2 -1) (("1" (expand "last") (("1" (expand "finseq_appl") (("1" (inst -2 "x!2`length - 1") (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "x!2`seq(x!2`length - 1)" "x!1" "sg1!1") (("1" (prop) (("1" (replaces -1 -2) (("1" (replaces -2 -1) (("1" (expand* "comp_cont?" "RSigma") (("1" (inst -3 "x!3") (("1" (assert) (("1" (inst -2 "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" (prop) (("1" (inst -1 "sg1!1(x!3)" "sg2!1(x!3)") (("1" (assert) (("1" (replace -2 1 rl) (("1" (hide (-2 -3)) (("1" (typepred "x!3") (("1" (expand "V") (("1" (expand "ext" 1 (3 5)) (("1" (assert) (("1" (case-replace "replace_pos(ext(sg1!1)(x!1), sg2!1(x!3), x!2) = replaceTerm(replace_pos(ext(sg1!1)( (("1" (hide-all-but (1 3)) (("1" (lemma "fspos.add_last_delete") (("1" (inst?) (("1" (assert) (("1" (name-replace "RTermTemp" "replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), delete(x!2, length(x!2) - (("1" (hide 2) (("1" (replaces -1) (("1" (expand "RTermTemp") (("1" (lemma "CP_lemma_aux2a") (("1" (inst -1 "sg2!1(x!3)" "ext(sg1!1)(x!1)" "delete(x!2, length(x!2) - 1)" "last(x!2)") (("1" (prop) (("1" (expand "ext" 1 3) (("1" (expand* "last" "finseq_appl") nil nil)) nil) ("2" (hide 2) (("2" (case "length(x!2) = 1") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (typepred "x!2") (("2" (reveal 4) (("2" (lemma "fspos.delete_pos") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (expand "SPP?") (("1" (flatten) (("1" (hide -3) (("1" (expand* "last" "finseq_appl") (("1" (replace -1 3 rl) (("1" (expand "PP?") (("1" (inst -2 "i!1" "x!2`length - 1") (("1" (expand "finseq_appl") (("1" (assert) (("1" (hide (-1 4)) (("1" (typepred "i!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (expand* "last" "finseq_appl") (("2" (inst -1 "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" (hide-all-but (1 3)) (("2" (lemma "preserv_all_parallel_positions") (("2" (inst -1 "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" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (expand "PP?") (("2" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (lemma "fspos.delete_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (inst -2 "i!1" "x!2`length - 1") (("1" (prop) (("1" (assert) nil nil) ("2" (hide-all-but (-1 4)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (inst -1 "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" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (inst -1 "x!2`length - 1") (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (reveal 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (expand* "last" "finseq_appl") (("2" (lemma "preserv_all_parallel_positions") (("2" (inst -1 "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" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (expand "PP?") (("2" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (lemma "fspos.delete_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (inst -2 "i!1" "x!2`length - 1") (("1" (prop) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 4)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (inst -1 "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" (hide-all-but (1 3)) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (expand* "last" "finseq_appl") (("2" (case "length(delete(x!2, length(x!2) - 1)) = 0") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (expand "PP?") (("2" (prop) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (lemma "fspos.delete_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (inst -2 "i!1" "x!2`length - 1") (("1" (prop) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 4)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) 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" (typepred "x!2") (("2" (expand "SPP?") (("2" (flatten) (("2" (hide -1) (("2" (expand "SP?") (("2" (expand* "last" "finseq_appl") (("2" (inst -1 "x!2`length - 1") (("1" (rewrite "ext_preserv_pos") nil nil) ("2" (hide-all-but (1 3)) (("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" (hide -1) (("2" (expand "SP?") (("2" (case "length(delete(x!2, length(x!2) - 1)) = 0") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (lemma "fspos.delete_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (inst -2 "i!1") (("1" (replace -1 2 rl) (("1" (hide -1) (("1" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (typepred "i!1") (("2" (grind) 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) ((O const-decl "bool" relation_props nil) (i!1 skolem-const-decl "below [length (delete[position[variable, symbol, arity]](x!2, length(x!2) - 1))]" critical_pairs_aux nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions nil) (delete_of_PP_is_PP formula-decl nil positions nil) (delete_of_SP_is_SP formula-decl nil positions nil) (SP? const-decl "bool" positions nil) (SP type-eq-decl nil positions nil) (length_delete formula-decl nil seq_extras "structures/") (delete_pos formula-decl nil seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_aux nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (preserv_unchanged_subterms formula-decl nil replace_positions nil) (i!1 skolem-const-decl "below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_aux nil) (subterm_ext_commute formula-decl nil substitution nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (i!1 skolem-const-decl "below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_aux nil) (preserv_all_parallel_positions formula-decl nil replace_positions nil) (replaceTerm def-decl "term" replacement nil) (add_last_delete formula-decl nil seq_extras "structures/") (RTermTemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (i!1 skolem-const-decl "below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_aux nil) (O const-decl "finseq" finite_sequences nil) (<= const-decl "bool" positions nil) (parallel const-decl "bool" positions nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (ext_preserv_pos formula-decl nil substitution nil) (CP_lemma_aux2a formula-decl nil replace_positions nil) (replace_subterm_of_term formula-decl nil replacement nil) (i!1 skolem-const-decl "below[length(delete(x!2, length(x!2) - 1))]" critical_pairs_aux nil) (last const-decl "T" seq_extras "structures/") (not_empty_seq type-eq-decl nil seq_extras "structures/") (/= const-decl "boolean" notequal nil) (delete const-decl "finseq" seq_extras "structures/") (sg1!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs_aux nil) (x!2 skolem-const-decl "SPP[variable, symbol, arity](x!1)" critical_pairs_aux nil) (x!1 skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (iterate def-decl "pred[[T, T]]" relation_iterate "orders/") (RSigma const-decl "bool" substitution nil) (comp_cont? const-decl "bool" compatibility nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (replace_pos def-decl "term" replace_positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (ext def-decl "term" substitution nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (CP_lemma_aux2c1_TCC1 0 (CP_lemma_aux2c1_TCC1-1 nil 3420220323 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (SP? const-decl "bool" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (<= const-decl "bool" positions nil) (parallel const-decl "bool" positions nil)) nil)) (CP_lemma_aux2c1_TCC2 0 (CP_lemma_aux2c1_TCC2-1 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) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (SP? const-decl "bool" positions nil) (ext_preserv_pos formula-decl nil substitution nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (PP? const-decl "bool" positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (CP_lemma_aux2c1_TCC3 0 (CP_lemma_aux2c1_TCC3-1 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) ((add_first_parallel_pos_to_SP_is_SP formula-decl nil positions nil) (ext def-decl "term" substitution nil) (SP? const-decl "bool" positions nil) (SP type-eq-decl nil positions nil) (ext_preserv_pos formula-decl nil substitution nil) (PP type-eq-decl nil positions nil) (PP? const-decl "bool" positions nil) (add_first_parallel_pos_to_PP_is_PP formula-decl nil positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (< const-decl "bool" reals nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (CP_lemma_aux2c1 0 (CP_lemma_aux2c1-1 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" (case-replace "length(rest(x!2)) = length(x!2) -1" :hide? T) (("1" (expand "iterate" 2) (("1" (assert) (("1" (expand "o") (("1" (inst 2 "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), add_first(q!1, rest(x!2)))") (("1" (assert) (("1" (hide -1) (("1" (lemma "CP_lemma_aux2a1") (("1" (copy -1) (("1" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "x!2" "q!1") (("1" (inst -2 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "q!1") (("1" (expand "finseq_appl") (("1" (prop) (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "preserv_unchanged_subterms") (("1" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2(0)") (("1" (expand "finseq_appl") (("1" (prop) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "x!2(0)" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2))") (("1" (expand "finseq_appl") (("1" (prop) (("1" (replaces -2) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "x!2(0)" "x!1" "sg1!1") (("1" (expand "finseq_appl") (("1" (copy -3) (("1" (inst -1 "0") (("1" (flatten) (("1" (prop) (("1" (replaces -3) (("1" (replaces -1) (("1" (replace -2 2 rl) (("1" (hide -2) (("1" (lemma "fspos.seq_first_rest") (("1" (inst?) (("1" (assert) (("1" (expand* "first" "finseq_appl") (("1" (name-replace "RTTemp" "replaceTerm(replaceTerm(replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2)), (("1" (replace -1 2) (("1" (hide -1) (("1" (lemma "CP_lemma_aux2a1") (("1" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2`seq(0)") (("1" (prop) (("1" (replaces -1) (("1" (expand "RTTemp") (("1" (assert) (("1" (lemma "replace_commutativity") (("1" (copy -1) (("1" (name-replace "repTemp" "replace_pos(ext(sg1!1)(x!1), ext(sg2!1)(x!3), rest(x!2))") (("1" (inst -2 "x!2`seq(0)" "q!1" "ext(sg2!1)(x!3)" "repTemp" "ext(sg1!1)(x!3)") (("1" (inst -1 "x!2`seq(0)" "q!1" "ext(sg2!1)(x!3)" "repTemp" "ext(sg2!1)(x!3)") (("1" (prop) (("1" (replaces -1) (("1" (replaces -1) (("1" (name-replace "REPLACEtemp" "replaceTerm(repTemp, ext(sg2!1)(x!3), q!1)") (("1" (typepred "x!3") (("1" (expand* "V" "ext") (("1" (assert) (("1" (expand* "comp_cont?" "RSigma") (("1" (inst -5 "x!2`seq(0)" "REPLACEtemp") (("1" (inst -6 "x!3") (("1" (prop) (("1" (inst -3 "sg1!1(x!3)" "sg2!1(x!3)") (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (expand "REPLACEtemp") (("2" (expand "repTemp") (("2" (typepred "q!1") (("2" (lemma "preserv_all_parallel_positions") (("2" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "q!1") (("1" (prop) (("1" (lemma "preserv_all_parallel_positions") (("1" (inst -1 "ext(sg2!1)(x!3)" "ext(sg1!1)(x!1)" "rest(x!2)" "x!2`seq(0)") (("1" (prop) (("1" (lemma "replace_preserv_parallel_pos") (("1" (inst -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" (hide-all-but (-7 1)) (("1" (rewrite "parallel_comm") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (rewrite "rest_parallel_first") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1 3)) (("2" (skosimp*) (("2" (lemma "rest_parallel_pos_parallel") (("2" (inst?) (("2" (inst -1 "q!1") (("2" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "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" (hide (-1 3)) (("2" (expand "repTemp") (("2" (rewrite "preserv_all_parallel_positions") (("1" (hide-all-but (-2 1)) (("1" (case "length(rest(x!2)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (typepred "x!2") (("2" (expand* "SPP?" "PP?") (("2" (flatten) (("2" (hide (-2 -3)) (("2" (prop) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1" "0") (("1" (assert) (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide (-1 4)) (("2" (typepred "i!1") (("2" (grind) nil nil)) 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)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -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" (hide-all-but (-3 1)) (("3" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (case "length(rest(x!2)) = 0") (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst -1 "i!1 + 1") (("1" (lemma "fspos.rest_pos") (("1" (expand "finseq_appl") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (assert) nil nil) ("2" (hide (-1 3)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide (-1 3)) (("4" (expand "repTemp") (("4" (rewrite "preserv_all_parallel_positions") (("1" (hide-all-but (1 3)) (("1" (skosimp*) (("1" (typepred "x!2") (("1" (expand "SPP?") (("1" (flatten) (("1" (lemma "rest_parallel_first") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but (1 3)) (("5" (expand "repTemp") (("5" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "rest_parallel_first") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide-all-but (-2 1 3)) (("6" (expand "repTemp") (("6" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "rest_parallel_pos_parallel") (("1" (inst?) (("1" (inst -1 "q!1") (("1" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide-all-but (-3 1 2)) (("7" (expand "repTemp") (("7" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (typepred "x!2") (("1" (skosimp*) (("1" (lemma "rest_parallel_pos_parallel") (("1" (inst?) (("1" (inst -1 "q!1") (("1" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil) ("8" (hide-all-but (-2 1 3)) (("8" (expand "repTemp") (("8" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (typepred "x!2") (("1" (hide -2) (("1" (skosimp*) (("1" (lemma "rest_parallel_first") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (hide-all-but (-2 1 3)) (("9" (expand "repTemp") (("9" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "rest_parallel_pos_parallel") (("1" (inst?) (("1" (inst -1 "q!1") (("1" (prop) (("1" (inst?) nil nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (lemma "rest_parallel_first") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "ext_parallel_pos") (("3" (hide 2) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (rewrite "preserv_all_parallel_positions") (("1" (hide 2) (("1" (lemma "rest_parallel_first") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -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" (hide-all-but (1 2)) (("2" (lemma "rest_parallel_first") (("2" (inst?) (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (inst -2 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1 2)) (("2" (lemma "rest_parallel_pos_parallel") (("2" (inst?) (("2" (inst -1 "q!1") (("2" (expand "finseq_appl") (("2" (prop) (("2" (hide 2) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1 2)) (("3" (skosimp*) (("3" (inst -1 "i!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but (-1 1 3)) (("4" (lemma "rest_parallel_pos_parallel") (("4" (inst?) (("4" (inst -1 "q!1") (("4" (expand "finseq_appl") (("4" (prop) (("4" (hide 2) (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil) ("3" (hide-all-but (1 2)) (("3" (rewrite "ext_parallel_pos") (("3" (hide 2) (("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" (hide-all-but 1) (("2" (typepred "q!1") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil) ("3" (hide-all-but 1) (("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" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (inst -2 "i!1 + 1") (("1" (replace -1 2 rl) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide (-1 3)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 3)) (("2" (typepred "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) ((add_parallel_pos formula-decl nil substitution nil) (O const-decl "bool" relation_props nil) (CP_lemma_aux2a1 formula-decl nil replace_positions nil) (sg1!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs_aux nil) (q!1 skolem-const-decl "positions?[variable, symbol, arity](x!1)" critical_pairs_aux nil) (preserv_unchanged_subterms formula-decl nil replace_positions nil) (replace_subterm_of_term formula-decl nil replacement nil) (seq_first_rest formula-decl nil seq_extras "structures/") (replaceTerm def-decl "term" replacement nil) (NOT const-decl "[bool -> bool]" booleans nil) (REPLACEtemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (rest_parallel_pos_parallel formula-decl nil substitution nil) (SP? const-decl "bool" positions nil) (ext_preserv_pos formula-decl nil substitution nil) (parallel_comm formula-decl nil positions nil) (replace_preserv_parallel_pos formula-decl nil replacement nil) (rest_parallel_first formula-decl nil substitution nil) (preserv_all_parallel_positions formula-decl nil replace_positions nil) (repTemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "below[length(rest(x!2))]" critical_pairs_aux nil) (rest_pos formula-decl nil seq_extras "structures/") (int_plus_int_is_int application-judgement "int" integers nil) (PP? const-decl "bool" positions nil) (<= const-decl "bool" positions nil) (O const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!1 skolem-const-decl "below[length(rest(x!2))]" critical_pairs_aux nil) (replace_commutativity formula-decl nil replacement nil) (RTTemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (ext_parallel_pos formula-decl nil substitution nil) (SP type-eq-decl nil positions nil) (rest_of_SP_is_SP formula-decl nil positions nil) (rest_of_PP_is_PP formula-decl nil positions nil) (PP type-eq-decl nil positions nil) (first const-decl "T" seq_extras "structures/") (subterm_ext_commute formula-decl nil substitution nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "below[length(rest(x!2))]" critical_pairs_aux nil) (length_rest formula-decl nil seq_extras "structures/") (x!2 skolem-const-decl "SPP[variable, symbol, arity](x!1)" critical_pairs_aux nil) (rest const-decl "finseq" seq_extras "structures/") (x!1 skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (empty_0 formula-decl nil seq_extras "structures/") (add_first_empty_seq formula-decl nil seq_extras "structures/") (replace_pos def-decl "term" replace_positions nil) (iterate def-decl "pred[[T, T]]" relation_iterate "orders/") (add_first const-decl "finseq" seq_extras "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (subtermOF def-decl "term" subterm nil) (comp_cont? const-decl "bool" compatibility nil) (RSigma const-decl "bool" substitution nil) (ext def-decl "term" substitution nil) (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions? type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (parallel const-decl "bool" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (CP_lemma_aux2c_TCC1 0 (CP_lemma_aux2c_TCC1-1 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) ((SP? const-decl "bool" positions nil) (< const-decl "bool" reals nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (CP_lemma_aux2c_TCC2 0 (CP_lemma_aux2c_TCC2-1 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) ((< const-decl "bool" reals nil) (ext_preserv_pos formula-decl nil substitution nil) (SP? const-decl "bool" positions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (PP? const-decl "bool" positions nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (CP_lemma_aux2c_TCC3 0 (CP_lemma_aux2c_TCC3-1 nil 3420220323 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (comp_cont? const-decl "bool" compatibility nil) (RSigma const-decl "bool" substitution nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (CP_lemma_aux2c 0 (CP_lemma_aux2c-1 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" (lift-if) (("1" (prop) (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (case "length(rest( #(x!2`seq(i!1)))) = 0") (("1" (expand "replace_pos") (("1" (assert) (("1" (hide -1) (("1" (expand* "iterate" "#" "finseq_appl") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("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" (inst -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" (case-replace "length(rest(x!2)) = length(x!2) - 1") (("1" (hide-all-but (1 2 3)) (("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" (lemma "rest_parallel_first") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1 2 3)) (("2" (lemma "fspos.rest_pos") (("2" (inst -1 "x!2") (("2" (assert) (("2" (inst -1 "i!2") (("1" (expand "finseq_appl") (("1" (replace -1 1 rl) (("1" (inst -2 "i!2 + 1") (("1" (assert) nil nil) ("2" (hide (-1 2)) (("2" (typepred "i!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "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" (inst?) (("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" (inst 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" (prop) (("1" (inst -1 "i!1 - 1") (("1" (case-replace "length(rest(x!2)) = length(x!2) - 1" :hide? T) (("1" (assert) (("1" (lemma "fspos.rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1 - 1") (("1" (expand "finseq_appl") (("1" (replace -1 -2 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5 6)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 5)) (("2" (skosimp*) (("2" (lemma "fspos.rest_pos") (("2" (inst?) (("2" (assert) (("2" (inst -1 "i!2") (("1" (expand "finseq_appl") (("1" (replace -1 1 rl) (("1" (inst -2 "1 + i!2") nil nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "i!2") (("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) ("2" (hide -1) (("2" (lemma "fspos.seq_first_rest") (("2" (inst?) (("2" (assert) (("2" (name-replace "RErestTemp" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))") (("2" (replace -1 1) (("2" (expand* "first" "finseq_appl") (("2" (hide -1) (("2" (lemma "CP_lemma_aux2a1") (("2" (inst?) (("1" (prop) (("1" (replaces -1) (("1" (expand "RErestTemp") (("1" (lemma "preserv_unchanged_subterms") (("1" (inst -1 "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)") (("1" (prop) (("1" (inst -2 "0") (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "x!2`seq(0)" "x!1" "sg1") (("1" (prop) (("1" (replaces -3 -1) (("1" (replaces -1) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "x!2`seq(0)" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))") (("1" (prop) (("1" (replaces -2) (("1" (name-replace "REPtemp" "replaceTerm(replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2)), ext(sg2)(x), x!2`se (("1" (replace -1 1 rl) (("1" (expand "REPtemp") (("1" (hide -1) (("1" (expand* "comp_cont?" "RSigma") (("1" (typepred "x") (("1" (expand "V") (("1" (expand "ext" 1 (3 6)) (("1" (assert) (("1" (inst -2 "x!2`seq(0)" "replace_pos(ext(sg1)(x!1), ext(sg2)(x), rest(x!2))") (("1" (inst -3 "x") (("1" (prop) (("1" (hide -1) (("1" (inst -2 "sg1(x)" "sg2(x)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide (-1 -2 -3 2)) (("2" (lemma "preserv_all_parallel_positions") (("2" (inst -1 "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)") (("1" (prop) (("1" (hide-all-but (1 5 6)) (("1" (rewrite "rest_parallel_first") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "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" (hide-all-but (1 5 6)) (("2" (lemma "preserv_all_parallel_positions") (("2" (inst -1 "ext(sg2)(x)" "ext(sg1)(x!1)" "rest(x!2)" "x!2`seq(0)") (("1" (prop) (("1" (hide-all-but 1) (("1" (rewrite "rest_parallel_first") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "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" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "rest_parallel_first") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "rest_parallel_first") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x!2") (("2" (expand* "SPP?" "SP?") (("2" (flatten) (("2" (hide -1) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 5 6)) (("3" (typepred "x!2") (("3" (expand "SPP?") (("3" (flatten) (("3" (rewrite "rest_of_PP_is_PP") (("3" (hide -1) (("3" (expand "SP?") (("3" (skosimp*) (("3" (lemma "fspos.rest_pos") (("3" (inst?) (("3" (assert) (("3" (inst -1 "i!2") (("1" (expand "finseq_appl") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (inst -1 "1 + i!2") (("1" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (typepred "i!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4 5)) (("2" (rewrite "ext_parallel_pos") (("2" (hide 2) (("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)) 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" (inst?) (("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" (inst?) (("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" (inst?) (("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) ((O const-decl "bool" relation_props nil) (ext_parallel_pos formula-decl nil substitution nil) (i!2 skolem-const-decl "below[length(rest(x!2))]" critical_pairs_aux nil) (i!1 skolem-const-decl "below[length(x!2)]" critical_pairs_aux nil) (int_plus_int_is_int application-judgement "int" integers nil) (length_rest formula-decl nil seq_extras "structures/") (preserv_unchanged_subterms formula-decl nil replace_positions nil) (subterm_ext_commute formula-decl nil substitution nil) (preserv_all_parallel_positions formula-decl nil replace_positions nil) (ext_preserv_pos formula-decl nil substitution nil) (REPtemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (replaceTerm def-decl "term" replacement nil) (replace_subterm_of_term formula-decl nil replacement nil) (RErestTemp skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (i!2 skolem-const-decl "below[length(rest[position[variable, symbol, arity]](x!2))]" critical_pairs_aux nil) (CP_lemma_aux2a1 formula-decl nil replace_positions nil) (sg1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs_aux nil) (x!1 skolem-const-decl "term[variable, symbol, arity]" critical_pairs_aux nil) (x!2 skolem-const-decl "SPP[variable, symbol, arity](x!1)" critical_pairs_aux nil) (i!2 skolem-const-decl "below[length(rest(x!2))]" critical_pairs_aux nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rest_pos formula-decl nil seq_extras "structures/") (rest_parallel_first formula-decl nil substitution nil) (seq_first_rest formula-decl nil seq_extras "structures/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (first const-decl "T" seq_extras "structures/") (SP? const-decl "bool" positions nil) (SP type-eq-decl nil positions nil) (rest_of_SP_is_SP formula-decl nil positions nil) (rest_of_PP_is_PP formula-decl nil positions nil) (PP? const-decl "bool" positions nil) (PP type-eq-decl nil positions nil) (CP_lemma_aux2c1 formula-decl nil critical_pairs_aux nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (length_rest_0 formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (replace_pos def-decl "term" replace_positions nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (iterate def-decl "pred[[T, T]]" relation_iterate "orders/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (positions? type-eq-decl nil positions nil) (subtermOF def-decl "term" subterm nil) (comp_cont? const-decl "bool" compatibility nil) (RSigma const-decl "bool" substitution nil) (ext def-decl "term" substitution nil) (finite_sequence type-eq-decl nil finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (positions type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (CP_lemma_aux2d_TCC1 0 (CP_lemma_aux2d_TCC1-1 nil 3420220323 ("" (skosimp*) (("" (replaces -1) (("" (lemma "Pos_var_is_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Pos_var_is_finite formula-decl nil subterm nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil)) nil)) (CP_lemma_aux2d_TCC2 0 (CP_lemma_aux2d_TCC2-1 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) ((ext_parallel_pos formula-decl nil substitution nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (below type-eq-decl nil nat_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (position type-eq-decl nil positions nil) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (SPP type-eq-decl nil positions nil) (finite_sequence type-eq-decl nil finite_sequences nil) (variable formal-nonempty-type-decl nil critical_pairs_aux nil) (symbol formal-nonempty-type-decl nil critical_pairs_aux nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs_aux nil) (pos_occ_var_HAStypeSP formula-decl nil subterm nil) (pos_occ_var_HAStypePP formula-decl nil subterm nil)) nil)) (CP_lemma_aux2d 0 (CP_lemma_aux2d-2 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" (inst -3 "x") (("1" (prop) (("1" (hide (-2 1)) (("1" (expand "seqvarsx!2") (("1" (expand "set2seq") (("1" (lift-if) (("1" (prop) (("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" (inst -2 "replaceTerm(x!1, z!1, seqvarsx!2`seq(0))" "x!2") (("1" (inst -2 "R" "gamma(sg1, sg2, x!2, z!1)" "gamma(sg2, sg2, x!2, z!1)") (("1" (prop) (("1" (name-replace "seqvarx2Term" "set2seq(Pos_var(replaceTerm(x!1, z!1, seqvarsx!2`seq(0)), x!2))") (("1" (typepred "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" (lemma "ext_replace_ext") (("1" (copy -1) (("1" (inst?) (("1" (inst -2 "seqvarsx!2`seq(0)" "x!1" "gamma(sg2, sg2, x!2, z!1)" "z!1") (("1" (prop) (("1" (replaces -1) (("1" (replaces -1) (("1" (expand "ext" -3 (2 4)) (("1" (expand "gamma" -3 (2 4)) (("1" (lemma "gamma_term") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (replace -2 -5) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "seqvarsx!2`seq(0)" "ext(sg2)(x!1)") (("1" (prop) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "seqvarsx!2`seq(0)" "x!1" "sg2") (("1" (assert) (("1" (case-replace "subtermOF(x!1, seqvarsx!2`seq(0)) = x!2" :hide? T) (("1" (replaces -1) (("1" (expand "ext" -1 2) (("1" (replaces -1) (("1" (replace -1 -5) (("1" (lemma "CP_lemma_aux2a3") (("1" (inst -1 "sg2(x!2)" "replaceTerm(ext(sg1)(x!1), sg2(x!2), seqvarsx!2`seq(0))" "rest(seqvarsx!2)" "seqvarx2Term") (("1" (prop) (("1" (assert) nil nil) ("2" (hide (-1 -2 -5 -7 -8 4)) (("2" (expand "equivalent") (("2" (expand "finseq_appl") (("2" (prop) (("1" (expand "seqvarx2Term") (("1" (case-replace "rest(seqvarsx!2)`length = seqvarsx!2`length -1" :hide? T) (("1" (lemma "set2seq_length[position]") (("1" (inst?) (("1" (replaces -1) (("1" (lemma "set2seq_length[position]") (("1" (expand "seqvarsx!2" 1 1) (("1" (inst?) (("1" (replaces -1) (("1" (lemma "pos_occ_var_replace_as_diff") (("1" (inst?) (("1" (prop) (("1" (replaces -1) (("1" (lemma "finite_sets[position].card_diff_subset") (("1" (inst -1 "singleton(seqvarsx!2`seq(0))" "Pos_var(x!1, x!2)") (("1" (prop) (("1" (rewrite "card_singleton") (("1" (expand "difference") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand* "subset?" "member") (("2" (skosimp*) (("2" (expand "singleton") (("2" (replaces -1) (("2" (lemma "set2seq_lem[position]") (("2" (expand "seqvarsx!2" (1 3)) (("2" (inst?) (("2" (assert) (("2" (inst -1 "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" (hide 2) (("2" (lemma "set2seq_lem[position]") (("2" (expand "seqvarsx!2" (1 3)) (("2" (inst?) (("2" (assert) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 1) (("3" (expand* "member" "Vars" "restrict") (("3" (inst 1 "seqvarsx!2`seq(0)") (("3" (replaces -1) (("3" (lemma "set2seq_lem[position]") (("3" (expand "seqvarsx!2") (("3" (inst?) (("3" (assert) (("3" (inst -1 "0") (("3" (expand "finseq_appl") (("3" (expand "Pos_var" -1 1) (("3" (expand "extend" -1 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "different_elements") (("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lemma "rest_pos[position]") (("2" (inst -1 "seqvarsx!2") (("2" (assert) (("2" (lemma "rest_pos[position]") (("2" (inst -1 "seqvarsx!2") (("2" (assert) (("2" (inst -1 "i!1") (("1" (inst -2 "j!1") (("1" (expand "finseq_appl") (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (hide (-1 -2)) (("1" (lemma "set2seq_neq[position]") (("1" (expand "seqvarsx!2") (("1" (inst?) (("1" (assert) (("1" (inst -1 "1 + i!1" "1 + j!1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil) ("2" (hide (-1 -4)) (("2" (typepred "j!1") (("2" (expand "seqvarsx!2" -1) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide (-1 -4)) (("3" (typepred "i!1") (("3" (expand "seqvarsx!2" -1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "different_elements") (("3" (skosimp*) (("3" (expand "finseq_appl") (("3" (lemma "set2seq_neq[position]") (("3" (expand "seqvarx2Term") (("3" (inst?) (("3" (assert) (("3" (inst -1 "i!1" "j!1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil) ("2" (hide (-1 -4)) (("2" (typepred "j!1") (("2" (expand "seqvarx2Term") (("2" (rewrite "set2seq_length") nil nil)) nil)) nil)) nil) ("3" (hide (-1 -4)) (("3" (typepred "i!1") (("3" (expand "seqvarx2Term") (("3" (rewrite "set2seq_length") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "rest_pos[position]") (("4" (inst?) (("4" (assert) (("4" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (replace -1 1 rl) (("1" (expand "seqvarsx!2" (1 3)) (("1" (lemma "set2seq_lem[position]") (("1" (inst?) (("1" (assert) (("1" (inst -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))`s (("1" (lemma "set2seq_exists[position]") (("1" (inst?) (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "ii!1") (("2" (expand "seqvarx2Term") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "Pos_var_is_finite") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "pos_occ_var_replace_as_diff") (("2" (inst?) (("2" (prop) (("1" (replaces -1) (("1" (expand "difference") (("1" (expand "member") (("1" (assert) (("1" (expand "singleton") (("1" (hide-all-but (-1 2)) (("1" (lemma "set2seq_neq[position]") (("1" (expand "seqvarsx!2") (("1" (inst?) (("1" (assert) (("1" (inst -1 "1 + i!1" "0") (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1 4)) (("2" (expand "seqvarsx!2") (("2" (lemma "set2seq_lem[position]") (("2" (inst?) (("2" (assert) (("2" (inst -1 "0") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-2 -3 1)) (("3" (expand* "member" "Vars" "restrict") (("3" (inst 1 "seqvarsx!2`seq(0)") (("3" (replaces -1) (("3" (lemma "set2seq_lem[position]") (("3" (expand "seqvarsx!2") (("3" (inst?) (("3" (assert) (("3" (inst -1 "0") (("3" (expand "finseq_appl") (("3" (expand "Pos_var" -1 1) (("3" (expand "extend" -1 1) (("3" (propax) 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)) (("2" (typepred "i!1") (("2" (expand "seqvarsx!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.689Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26