| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 MB |
|
Quelle critical_pairs.prfSprache: Lisp |
|||||||||||||||
|
(critical_pairs (IMP_critical_pairs_aux_TCC1 0 (IMP_critical_pairs_aux_TCC1-1 nil 3420229945 ("" (lemma "var_countable") (("" (propax) nil nil)) nil) ((var_countable formula-decl nil critical_pairs nil)) nil)) (CP?_TCC1 0 (CP?_TCC1-1 nil 3395743409 ("" (skosimp*) (("" (lemma "ext_preserv_pos") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" critical_pairs 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 nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (ext_preserv_pos formula-decl nil substitution nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (positions? type-eq-decl nil positions nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (lhs const-decl "term" rewrite_rules nil) (rewrite_rule type-eq-decl nil rewrite_rules nil) (rewrite_rule? const-decl "bool" rewrite_rules nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (term type-decl nil term_adt 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)) nil)) (CP_lemma_aux1a_TCC1 0 (CP_lemma_aux1a_TCC1-1 nil 3406618276 ("" (skosimp*) (("" (hide-all-but 2) (("" (typepred "alpha!1" "rho!1") (("" (hide -3) (("" (rewrite "subs_o") nil nil)) nil)) nil)) nil)) nil) ((subs_o formula-decl nil substitution 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 nil) (symbol formal-nonempty-type-decl nil critical_pairs 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 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) (Ren? const-decl "bool" substitution nil) (Ren type-eq-decl nil substitution nil)) nil)) (CP_lemma_aux1a 0 (CP_lemma_aux1a-1 nil 3406746822 ("" (skosimp*) (("" (lemma "exists_renaming") (("" (inst -1 "Vars(lhs(e2!1))" "Vars(lhs(e1!1))") (("1" (skosimp*) (("1" (lemma "inverse_renaming") (("1" (inst?) (("1" (skosimp*) (("1" (lemma "inverse_rename_identity") (("1" (inst -1 "rho!1" "rho1!1" "lhs(e2!1)") (("1" (prop) (("1" (inst 2 "comp(sg2!1, rho1!1)" "rho!1") (("1" (split) (("1" (lemma "vars_term_rename") (("1" (inst?) (("1" (assert) (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "restrict[term[variable, symbol, arity], ((V)), boolean](Ran(rho!1))") (("1" (assert) (("1" (hide-all-but 1) (("1" (expand* "subset?" "member") (("1" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-4 2)) (("2" (rewrite "o_ass") (("2" (rewrite "ext_o") (("2" (expand "o") (("2" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "subs_o") nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand* "subset?" "member") (("2" (skosimp*) (("2" (decompose-equality -2) (("2" (inst -1 "x!1") (("2" (iff) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "vars_of_term_finite") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "vars_of_term_finite") nil nil)) nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" critical_pairs 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 nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (exists_renaming formula-decl nil substitution nil) (vars_of_term_finite formula-decl nil subterm nil) (Ren type-eq-decl nil substitution nil) (Ren? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (inverse_rename_identity formula-decl nil substitution nil) (subs_o formula-decl nil substitution nil) (disjoint_subset formula-decl nil IUnion_extra nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (ext def-decl "term" substitution nil) (restrict const-decl "R" restrict nil) (Ran const-decl "set[term]" substitution nil) (vars_term_rename formula-decl nil substitution nil) (o_ass formula-decl nil substitution nil) (O const-decl "T3" function_props nil) (ext_o formula-decl nil substitution nil) (rho1!1 skolem-const-decl "Ren[variable, symbol, arity]" critical_pairs nil) (sg2!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs nil) (comp const-decl "term" substitution nil) (Dom const-decl "set[(V)]" substitution nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse_renaming formula-decl nil substitution nil) (finite_set type-eq-decl nil finite_sets nil) (e1!1 skolem-const-decl "{e1 | member(e1, E!1)}" critical_pairs nil) (term type-decl nil term_adt nil) (set type-eq-decl nil sets nil) (V const-decl "set[term]" variables_term nil) (is_finite const-decl "bool" finite_sets nil) (Vars const-decl "set[(V)]" subterm nil) (rewrite_rule? const-decl "bool" rewrite_rules nil) (rewrite_rule type-eq-decl nil rewrite_rules nil) (lhs const-decl "term" rewrite_rules nil) (member const-decl "bool" sets nil) (E!1 skolem-const-decl "set[rewrite_rule]" critical_pairs nil) (e2!1 skolem-const-decl "{e2 | member(e2, E!1)}" critical_pairs nil)) shostak)) (CP_lemma_aux1_TCC1 0 (CP_lemma_aux1_TCC1-1 nil 3402063728 ("" (skosimp*) (("" (hide-all-but (-1 2)) (("" (rewrite "ext_preserv_pos") nil nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" critical_pairs 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 nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (lhs const-decl "term" rewrite_rules nil) (rewrite_rule type-eq-decl nil rewrite_rules nil) (rewrite_rule? const-decl "bool" rewrite_rules nil) (term type-decl nil term_adt 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) (ext_preserv_pos formula-decl nil substitution nil)) nil)) (CP_lemma_aux1 0 (CP_lemma_aux1-1 nil 3402063736 ("" (skosimp*) (("" (lemma "CP_lemma_aux1a") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (case "ext(union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(V (("1" (lemma "unification") (("1" (inst -1 "subtermOF(lhs(e1!1), p!1)" "ext(rho!1)(lhs(e2!1))") (("1" (prop) (("1" (skosimp*) (("1" (copy -1) (("1" (expand "mgu" -1) (("1" (flatten) (("1" (hide -1) (("1" (inst -1 "union_subs(restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rh (("1" (expand "member" -1) (("1" (expand "U" -1) (("1" (expand "unifier" -1) (("1" (assert) (("1" (expand "<=") (("1" (skosimp*) (("1" (inst 2 "ext(theta!1)(rhs(e1!1))" "replaceTerm(ext(theta!1)(lhs(e1!1)), ext(theta!1)(ext(rho!1)(rhs(e2!1))),p!1)" "tau!1") (("1" (lemma "ext_o") (("1" (inst -1 "tau!1" "theta!1") (("1" (decompose-equality -1) (("1" (split) (("1" (hide -1) (("1" (expand "CP?") (("1" (inst 1 "theta!1" "rho!1" "e1!1" "e2!1" "p!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -1 "rhs(e1!1)") (("2" (expand "o") (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (lemma "restriction_union") (("2" (inst -1 "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "rhs(e1!1)") (("1" (lemma "dom_restriction") (("1" (copy -1) (("1" (inst -1 "Vars(lhs(e1!1))" "sg1!1") (("1" (inst -2 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1") (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (assert) (("1" (prop) (("1" (replace -1 1) (("1" (lemma "restriction_term") (("1" (inst?) (("1" (prop) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "e1!1") (("2" (expand "rewrite_rule?") (("2" (expand* "lhs" "rhs") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 -6 1)) (("2" (lemma "IUnion_extra[(V)].disjoint_subset") (("2" (inst -1 "Vars(rhs(e1!1))" "Vars(rhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("2" (prop) (("1" (hide-all-but 1) (("1" (expand* "subset?" "member") (("1" (skeep) nil nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "IUnion_extra[(V)].disjoint_subset") (("2" (inst -1 "Vars(rhs(e1!1))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))") (("2" (prop) (("1" (hide (-1 2)) (("1" (typepred "e1!1") (("1" (expand* "rewrite_rule?" "lhs" "rhs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "restriction_Subs") nil nil) ("3" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "ext_replace_ext") (("3" (inst?) (("3" (prop) (("1" (replaces -1) (("1" (copy -1) (("1" (inst -1 "ext(rho!1)(rhs(e2!1))") (("1" (inst -2 "lhs(e1!1)") (("1" (expand "o") (("1" (replace -1 1 rl) (("1" (replace -2 1 rl) (("1" (replace -3 1 rl) (("1" (hide (-1 -2 -3)) (("1" (lemma "restriction_union") (("1" (copy -1) (("1" (inst -1 "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "lhs(e1!1)") (("1" (inst -2 "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "restriction(sg1!1)(Vars(lhs(e1!1)))" "ext(rho!1)(rhs(e2!1))") (("1" (lemma "dom_restriction") (("1" (copy -1) (("1" (inst -1 "Vars(lhs(e1!1))" "sg1!1") (("1" (inst -2 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1") (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (assert) (("1" (lemma "IUnion_extra[(V)].disjoint_commute") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))") (("1" (assert) (("1" (prop) (("1" (rewrite "union_commute") (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "restriction_term") (("1" (copy -1) (("1" (inst -1 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" "ext(rho!1)(rhs(e2!1))") (("1" (inst -2 "Vars(lhs(e1!1))" "sg1!1" "lhs(e1!1)") (("1" (prop) (("1" (replace -1 1 rl) (("1" (replace -2 1 rl) (("1" (rewrite "ext_o") (("1" (expand "o") (("1" (case-replace "ext(alpha!1)(ext(rho!1)(rhs(e2!1))) = ext(sg2!1)(rhs(e2!1))") (("1" (hide-all-but (-10 -12 1)) (("1" (replaces -1) (("1" (lemma "ext_o") (("1" (inst -1 "alpha!1" "rho!1") (("1" (copy -1) (("1" (decompose-equality -1) (("1" (decompose-equality -2) (("1" (inst -1 "lhs(e2!1)") (("1" (inst -2 "rhs(e2!1)") (("1" (expand "o") (("1" (replace -1 * rl) (("1" (replace -2 * rl) (("1" (hide (-1 -2)) (("1" (lemma "same_substitution") (("1" (inst -1 "comp(alpha!1, rho!1)" "sg2!1" "lhs(e2!1)") (("1" (assert) (("1" (lemma "same_term") (("1" (inst -1 "comp(alpha!1, rho!1)" "sg2!1" "rhs(e2!1)") (("1" (prop) (("1" (skosimp*) (("1" (hide (-3 2)) (("1" (inst -2 "x!1") (("1" (assert) (("1" (hide 1) (("1" (typepred "e2!1") (("1" (hide -2) (("1" (expand "rewrite_rule?") (("1" (flatten) (("1" (expand* "subset?" "rhs" "lhs") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "e2!1") (("3" (expand "rewrite_rule?") (("3" (flatten) (("3" (lemma "rename_preserv_inclusion") (("3" (expand* "rhs" "lhs") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand* "subset?" "member") (("4" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -8 1)) (("2" (lemma "IUnion_extra[(V)].disjoint_subset") (("2" (case "disjoint?(Vars(lhs(e1!1)), Vars(ext(rho!1)(rhs(e2!1))))") (("1" (inst -2 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(rhs(e2!1)))" "Vars(ext(rho!1)(rhs(e2!1)))") (("1" (prop) (("1" (lemma "IUnion_extra[(V)].disjoint_commute") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(ext(rho!1)(rhs(e2!1)))") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 1)) (("2" (typepred "e2!1") (("2" (expand "rewrite_rule?") (("2" (flatten) (("2" (expand* "lhs" "rhs") (("2" (lemma "rename_preserv_inclusion") (("2" (inst -1 "rho!1" "e2!1`1" "e2!1`2") (("2" (assert) (("2" (inst -4 "Vars(e1!1`1)" "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))" "Vars(ext(rho!1)(e2!1`1))") (("2" (prop) (("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-5 -8 1)) (("3" (lemma "IUnion_extra[(V)].disjoint_subset") (("3" (inst -1 "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("3" (prop) (("3" (hide-all-but 1) (("3" (expand* "subset?" "member") (("3" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-3 -7 1)) (("4" (lemma "IUnion_extra[(V)].disjoint_subset") (("4" (case "disjoint?(Vars(ext(rho!1)(rhs(e2!1))), Vars(lhs(e1!1)))") (("1" (inst -2 "Vars(ext(rho!1)(rhs(e2!1)))" "Vars(ext(rho!1)(rhs(e2!1)))" "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))") (("1" (prop) (("1" (hide-all-but 1) (("1" (expand* "subset?" "member") (("1" (skeep) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 2)) (("2" (typepred "e2!1") (("2" (expand "rewrite_rule?") (("2" (flatten) (("2" (lemma "rename_preserv_inclusion") (("2" (inst -1 "rho!1" "e2!1`1" "e2!1`2") (("2" (assert) (("2" (inst -4 "Vars(e1!1`1)" "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))" "Vars(ext(rho!1)(e2!1`1))") (("2" (prop) (("1" (expand* "rhs" "lhs") (("1" (hide-all-but (-1 2)) (("1" (lemma "IUnion_extra[(V)].disjoint_commute") (("1" (inst -1 "Vars(e1!1`1)" "Vars(ext(rho!1)(e2!1`2))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil) ("3" (expand* "rhs" "lhs") 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) (("2" (rewrite "restriction_Subs") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "restriction_Subs") nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "restriction_Subs") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (rewrite "ext_preserv_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "restriction_Subs") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "unifiable") (("2" (inst 1 "union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(r (("1" (expand "unifier") (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "restriction_Subs") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "restriction_union") (("2" (inst -1 "restriction(sg1!1)(Vars(lhs(e1!1)))" "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "subtermOF(lhs(e1!1), p!1)") (("1" (lemma "dom_restriction") (("1" (inst -1 "Vars(lhs(e1!1))" "sg1!1") (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (lemma "dom_restriction") (("1" (inst -1 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1") (("1" (assert) (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Vars(lhs(e1!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (prop) (("1" (replaces -1) (("1" (lemma "restriction_union") (("1" (inst -1 "restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1))))" "restriction(sg1!1)(Vars(lhs(e1!1)))" "ext(rho!1)(lhs(e2!1))") (("1" (lemma "IUnion_extra[(V)].disjoint_commute") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))") (("1" (assert) (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (assert) (("1" (prop) (("1" (rewrite "union_commute") (("1" (replaces -1) (("1" (lemma "restriction_term") (("1" (inst?) (("1" (prop) (("1" (replace -1 1 rl) (("1" (lemma "restriction_term") (("1" (inst -1 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1" "ext(rho!1)(lhs(e2!1))") (("1" (prop) (("1" (replace -1 1 rl) (("1" (rewrite "ext_o") (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "vars_subterm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (rewrite "IUnion_extra[(V)].disjoint_commute") nil nil)) nil) ("3" (hide-all-but 1) (("3" (expand* "subset?" "member") (("3" (skeep) nil nil)) nil)) nil) ("4" (hide-all-but (-5 -6 1)) (("4" (lemma "IUnion_extra[(V)].disjoint_subset") (("4" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(ext(rho!1)(lhs(e2!1)))") (("4" (assert) (("4" (prop) (("1" (hide (-2 -3)) (("1" (lemma "IUnion_extra[(V)].disjoint_commute") (("1" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (lemma "vars_subterm") (("2" (inst?) (("2" (assert) (("2" (lemma "IUnion_extra[(V)].disjoint_subset") (("2" (inst -1 "Vars(subtermOF(lhs(e1!1), p!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))") (("2" (prop) (("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand* "subset?" "member") (("3" (skeep) nil nil)) nil)) nil) ("4" (hide-all-but (-1 -4 1)) (("4" (lemma "IUnion_extra[(V)].disjoint_subset") (("4" (inst -1 "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))" "Vars(lhs(e1!1))" "Vars(lhs(e1!1))") (("4" (lemma "IUnion_extra[(V)].disjoint_commute") (("4" (inst?) (("4" (assert) (("4" (prop) (("1" (hide (-2 -3 -4)) (("1" (lemma "vars_subterm") (("1" (inst?) (("1" (assert) (("1" (lemma "IUnion_extra[(V)].disjoint_subset") (("1" (inst -1 "Vars(subtermOF(lhs(e1!1), p!1))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))") (("1" (prop) (("1" (hide-all-but 1) (("1" (expand* "subset?" "member") (("1" (skeep) nil nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (lemma "IUnion_extra[(V)].disjoint_commute") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand* "subset?" "member") (("2" (skeep) 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" (rewrite "restriction_Subs") nil nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (rewrite "union_is_sub") (("1" (hide 2) (("1" (rewrite "restriction_Subs") nil nil)) nil) ("2" (hide 2) (("2" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil) ("4" (hide-all-but (-1 1)) (("4" (expand "disjoint_D?") (("4" (lemma "dom_restriction") (("4" (copy -1) (("4" (inst -1 "Vars(lhs(e1!1))" "sg1!1") (("4" (inst -2 "Vars(ext(rho!1)(lhs(e2!1)))" "alpha!1") (("4" (lemma "IUnion_extra[(V)].disjoint_subset") (("4" (inst -1 "Dom(restriction(sg1!1)(Vars(lhs(e1!1))))" "Vars(lhs(e1!1))" "Dom(restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))" "Vars(ext(rho!1)(lhs(e2!1)))") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (rewrite "restriction_Subs") nil nil)) nil) ("6" (hide-all-but 1) (("6" (rewrite "restriction_Subs") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((CP_lemma_aux1a formula-decl nil critical_pairs nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (Ren type-eq-decl nil substitution nil) (Ren? const-decl "bool" substitution nil) (lhs const-decl "term" rewrite_rules nil) (Vars const-decl "set[(V)]" subterm nil) (restriction const-decl "term" substitution nil) (union_subs const-decl "term" substitution nil) (disjoint_D type-eq-decl nil substitution nil) (disjoint_D? const-decl "bool" substitution nil) (ext def-decl "term" substitution nil) (= const-decl "[T, T -> boolean]" equalities nil) (unifiable const-decl "bool" unification nil) (mgu const-decl "bool" unification nil) (unifier const-decl "bool" unification nil) (<= const-decl "bool" unification nil) (theta!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs nil) (p!1 skolem-const-decl "position[variable, symbol, arity]" critical_pairs nil) (replaceTerm def-decl "term" replacement nil) (rhs const-decl "term" rewrite_rules nil) (CP? const-decl "bool" critical_pairs nil) (Dom const-decl "set[(V)]" substitution nil) (restriction_term formula-decl nil substitution nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (disjoint_subset formula-decl nil IUnion_extra nil) (dom_restriction formula-decl nil substitution nil) (restriction_Subs formula-decl nil substitution nil) (restriction_union formula-decl nil substitution nil) (ext_preserv_pos formula-decl nil substitution nil) (disjoint_commute formula-decl nil IUnion_extra nil) (disjoint? const-decl "bool" sets nil) (union_commute formula-decl nil substitution nil) (rename_preserv_inclusion formula-decl nil substitution nil) (same_substitution formula-decl nil substitution nil) (same_term formula-decl nil substitution nil) (ext_replace_ext formula-decl nil substitution nil) (comp const-decl "term" substitution nil) (O const-decl "T3" function_props nil) (ext_o formula-decl nil substitution nil) (U const-decl "set[Sub]" unification nil) (e2!1 skolem-const-decl "{e2 | member(e2, E!1)}" critical_pairs nil) (rho!1 skolem-const-decl "Ren[variable, symbol, arity]" critical_pairs nil) (alpha!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs nil) (e1!1 skolem-const-decl "{e1 | member(e1, E!1)}" critical_pairs nil) (E!1 skolem-const-decl "set[rewrite_rule]" critical_pairs nil) (sg1!1 skolem-const-decl "Sub[variable, symbol, arity]" critical_pairs nil) (unification formula-decl nil unification nil) (vars_subterm formula-decl nil subterm nil) (union_is_sub formula-decl nil substitution nil) (member const-decl "bool" sets 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) (rewrite_rule type-eq-decl nil rewrite_rules nil) (rewrite_rule? const-decl "bool" rewrite_rules 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 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 nil) (variable formal-nonempty-type-decl nil critical_pairs nil)) shostak)) (CP_lemma_aux2_TCC1 0 (CP_lemma_aux2_TCC1-1 nil 3412313494 ("" (skosimp*) (("" (lemma "Pos_var_is_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" critical_pairs 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 nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (Pos_var_is_finite formula-decl nil subterm nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil)) nil)) (CP_lemma_aux2_TCC2 0 (CP_lemma_aux2_TCC2-1 nil 3420229945 ("" (skosimp*) (("" (hide (-2 -3)) (("" (expand "SPP?") (("" (split) (("1" (grind) nil nil) ("2" (expand "SP?") (("2" (skosimp*) (("2" (expand* "#" "finseq_appl") (("2" (rewrite "ext_preserv_pos") (("2" (hide 2) (("2" (lemma "set2seq_lem[position]") (("2" (inst?) (("2" (assert) (("2" (replaces -2) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (expand "Pos_var" -1 1) (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs nil) (symbol formal-nonempty-type-decl nil critical_pairs nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (ext_preserv_pos formula-decl nil substitution nil) (finite_sequence type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals 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) (set2seq_lem formula-decl nil set2seq "structures/") (below type-eq-decl nil naturalnumbers nil) (set2seq def-decl "finite_sequence[T]" set2seq "structures/") (Pos_var const-decl "positions" subterm nil) (extend const-decl "R" extend nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (positions type-eq-decl nil positions nil) (SP? const-decl "bool" positions nil) (SPP? const-decl "bool" positions nil)) nil)) (CP_lemma_aux2 0 (CP_lemma_aux2-2 nil 3565130737 ("" (skolem 1 ("R" "t" "x" "sg1" "sg2")) (("" (skoletin* 1) (("" (flatten) (("" (split) (("1" (case "length(seqv) = 0") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "CP_lemma_aux2c") (("2" (inst -1 "R" "t" "x" "sg1" "sg2" "seqv") (("1" (assert) (("1" (lemma "CP_lemma_aux2d") (("1" (inst -1 "R" "t" "x" "sg1" "sg2") (("1" (assert) (("1" (replace -6 -1 rl) (("1" (replace -5 -1 rl) (("1" (replaces -1) (("1" (prop) (("1" (inst?) (("1" (expand "finseq_appl") (("1" (expand* "RTC" "IUnion") (("1" (inst 2 "length(seqv) - 1") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lemma "set2seq_lem[position]") (("2" (inst -1 "Posv") (("2" (assert) (("2" (inst?) (("1" (expand "finseq_appl") (("1" (replaces -5 -1) (("1" (expand "Pos_var" -1 1) (("1" (expand "extend") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!2") (("2" (replaces -4) (("2" (rewrite "set2seq_length") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "SPP?") (("2" (split) (("1" (lemma "pos_occ_var_HAStypePP") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "pos_occ_var_HAStypeSP") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "CP_lemma_aux2b") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (inst?) (("2" (inst?) (("1" (assert) (("1" (prop) (("1" (lemma "CP_lemma_aux2d") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand* "RTC" "IUnion") (("1" (inst 1 "length(seqv)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "set2seq_lem[position]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("1" (expand "finseq_appl") (("1" (replaces -5) (("1" (expand "Pos_var" -1 1) (("1" (expand "extend") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (replaces -4) (("2" (rewrite "set2seq_length") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "SPP?") (("2" (split) (("1" (lemma "pos_occ_var_HAStypePP") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "pos_occ_var_HAStypeSP") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (variable formal-nonempty-type-decl nil critical_pairs nil) (symbol formal-nonempty-type-decl nil critical_pairs nil) (arity formal-const-decl "[symbol -> nat]" critical_pairs nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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 const-decl "positions" subterm nil) (is_finite const-decl "bool" finite_sets nil) (finite_sequence type-eq-decl nil finite_sequences nil) (pred type-eq-decl nil defined_types nil) (comp_cont? const-decl "bool" compatibility nil) (Sub? const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (RSigma const-decl "bool" substitution nil) (finite_set type-eq-decl nil finite_sets nil) (set2seq def-decl "finite_sequence[T]" set2seq "structures/") (< const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (SPP? const-decl "bool" positions nil) (ext def-decl "term" substitution nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (reflexive_transitive? const-decl "bool" relations_closure nil) (reflexive_transitive type-eq-decl nil relations_closure nil) (RTC const-decl "reflexive_transitive" relations_closure nil) (SPP type-eq-decl nil positions nil) (replace_pos def-decl "term" replace_positions nil) (t skolem-const-decl "term[variable, symbol, arity]" critical_pairs nil) (seqv skolem-const-decl "finite_sequence[position[variable, symbol, arity]]" critical_pairs nil) (CP_lemma_aux2d formula-decl nil critical_pairs_aux nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (i!2 skolem-const-decl "below[length(seqv)]" critical_pairs nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Posv skolem-const-decl "positions[variable, symbol, arity]" critical_pairs nil) (below type-eq-decl nil naturalnumbers nil) (set2seq_length formula-decl nil set2seq "structures/") (extend const-decl "R" extend nil) (set2seq_lem formula-decl nil set2seq "structures/") (pos_occ_var_HAStypeSP formula-decl nil subterm nil) (pos_occ_var_HAStypePP formula-decl nil subterm nil) (CP_lemma_aux2c formula-decl nil critical_pairs_aux nil) (IUnion const-decl "set[T]" indexed_sets nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (i!1 skolem-const-decl "below[length(seqv)]" critical_pairs nil) (CP_lemma_aux2b formula-decl nil critical_pairs_aux nil)) nil) (CP_lemma_aux2-1 nil 3412011699 ("" (skolem 1 ("R" "t" "x" "sg1" "sg2")) (("" (skoletin* 1) (("1" (flatten) (("1" (split) (("1" (case "length(seqv) = 0") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "CP_lemma_aux2c") (("2" (inst -1 "R" "t" "x" "sg1" "sg2" "seqv") (("1" (assert) (("1" (lemma "CP_lemma_aux2d") (("1" (inst -1 "R" "t" "x" "sg1" "sg2") (("1" (assert) (("1" (replace -6 -1 rl) (("1" (replace -3 -1 rl) (("1" (replaces -1) (("1" (prop) (("1" (inst?) (("1" (expand "finseq_appl") (("1" (expand* "RTC" "IUnion") (("1" (inst 2 "length(seqv) - 1") nil nil)) nil)) nil)) nil) ("2" (hide (-2 -3 3)) (("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (lemma "fspos.set2seq_lem") (("2" (inst -1 "Posv") (("2" (assert) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (replaces -3 -1) (("2" (expand "Pos_var" -1 1) (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -3 3)) (("2" (expand "SPP?") (("2" (split) (("1" (lemma "pos_occ_var_HAStypePP") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "pos_occ_var_HAStypeSP") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "CP_lemma_aux2b") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (inst?) (("2" (inst?) (("1" (assert) (("1" (prop) (("1" (lemma "CP_lemma_aux2d") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (replaces -6) (("1" (expand* "RTC" "IUnion") (("1" (inst 1 "length(seqv)") (("1" (replaces -3) (("1" (replaces -1 -2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-3 2)) (("2" (skosimp*) (("2" (lemma "fspos.set2seq_lem") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (replaces -4) (("2" (expand "Pos_var" -1 1) (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -3 2)) (("2" (expand "SPP?") (("2" (split) (("1" (lemma "pos_occ_var_HAStypePP") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "pos_occ_var_HAStypeSP") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "CP_lemma_aux2_TCC2") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "CP_lemma_aux2_TCC2") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "CP_lemma_aux2_TCC1") (("4" (inst?) (("4" (inst?) (("4" (assert) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ext def-decl "term" substitution nil) (replace_pos def-decl "term" replace_positions nil) (SPP type-eq-decl nil positions nil) (SPP? const-decl "bool" positions nil) (RTC const-decl "reflexive_transitive" relations_closure nil) (reflexive_transitive type-eq-decl nil relations_closure nil) (reflexive_transitive? const-decl "bool" relations_closure nil) (RSigma const-decl "bool" substitution nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (comp_cont? const-decl "bool" compatibility nil) (finseq type-eq-decl nil finite_sequences nil) (position type-eq-decl nil positions nil) (positions type-eq-decl nil positions 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 const-decl "positions" subterm nil) (CP_lemma_aux2d formula-decl nil critical_pairs_aux nil) (pos_occ_var_HAStypeSP formula-decl nil subterm nil) (pos_occ_var_HAStypePP formula-decl nil subterm nil) (CP_lemma_aux2c formula-decl nil critical_pairs_aux nil) (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (CP_lemma_aux2b formula-decl nil critical_pairs_aux nil)) shostak)) (CP_Theorem 0 (CP_Theorem-4 nil 3565535039 ("" (skeep) (("" (skoletin* 1) (("" (hide -1) (("" (split) (("1" (flatten) (("1" (skeep) (("1" (expand "CP?") (("1" (skosimp*) (("1" (expand "locally_confluent?") (("1" (inst -1 "ext(sigma!1)(lhs(e1!1))" "t1" "t2") (("1" (assert) (("1" (hide-all-but (-2 -3 -4 1)) (("1" (expand "RRE") (("1" (expand "reduction?") (("1" (split) (("1" (inst 1 "e1!1" "sigma!1" "empty_seq") (("1" (split) (("1" (expand "subtermOF" 1) (("1" (lift-if) (("1" (prop) (("1" (rewrite "empty_0") nil nil)) nil)) nil)) nil) ("2" (expand "replaceTerm" 1) (("2" (lift-if) (("2" (prop) (("2" (rewrite "empty_0") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "positionsOF") (("2" (lift-if) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (inst 1 "e2p!1" "comp(sigma!1, rho!1)" "p!1") (("1" (rewrite "ext_o") (("1" (expand "o") (("1" (expand* "mgu" "member" "U" "unifier") (("1" (flatten) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "p!1" "lhs(e1!1)" "sigma!1") (("1" (typepred "p!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "subs_o") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "locally_confluent?") (("2" (skeep) (("2" (expand "RRE") (("2" (expand "reduction?" (-2 -3)) (("2" (skosimp*) (("2" (case "parallel(p!1, p!2)") (("1" (hide -2) (("1" (expand "joinable?") (("1" (inst 1 "replaceTerm(y, ext(sigma!2)(rhs(e!2)), p!2)") (("1" (expand* "RTC" "IUnion") (("1" (split) (("1" (inst 1 "1") (("1" (rewrite "iterate_1") (("1" (expand "reduction?") (("1" (inst 1 "e!2" "sigma!2" "p!2") (("1" (lemma "replace_persistence") (("1" (inst -1 "p!1" "p!2" "x" "ext(sigma!1)(rhs(e!1))") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "replace_preserv_parallel_pos") (("2" (inst?) (("2" (inst -1 "p!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "1") (("2" (rewrite "iterate_1") (("2" (expand "reduction?") (("2" (inst 1 "e!1" "sigma!1" "p!1") (("1" (split) (("1" (lemma "replace_persistence") (("1" (inst -1 "p!2" "p!1" "x" "ext(sigma!2)(rhs(e!2))") (("1" (assert) (("1" (rewrite "parallel_comm") nil nil)) nil)) nil)) nil) ("2" (lemma "replace_commutativity") (("2" (inst -1 "p!1" "p!2" "ext(sigma!2)(rhs(e!2))" "x" "ext(sigma!1)(rhs(e!1))") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "replace_preserv_parallel_pos") (("2" (inst -1 "p!2" "p!1" "x" "ext(sigma!2)(rhs(e!2))") (("2" (assert) (("2" (rewrite "parallel_comm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "replace_preserv_parallel_pos") (("2" (inst?) (("2" (inst -1 "p!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "parallel") (("2" (expand "<=") (("2" (prop) (("1" (skosimp*) (("1" (lemma "replace_distributivity") (("1" (inst?) (("1" (inst -1 "x" "ext(sigma!2)(rhs(e!2))") (("1" (replace -2 -1 rl) (("1" (typepred "p!2") (("1" (assert) (("1" (replace -8 -2 rl) (("1" (replace -5 -2) (("1" (lemma "pos_subterm") (("1" (inst?) (("1" (inst -1 "x") (("1" (replace -4 -1 rl) (("1" (assert) (("1" (replace -6 -1) (("1" (replace -1 -8) (("1" (lemma "pos_subterm_ax") (("1" (inst -1 "p!1" "p1!1" "x") (("1" (replace -5 -3) (("1" (assert) (("1" (replace -7 -1) (("1" (lemma "positions_of_ext") (("1" (inst -1 "sigma!1" "lhs(e!1)") (("1" (decompose-equality -1) (("1" (inst -1 "p1!1") (("1" (iff) (("1" (flatten) (("1" (hide -2) (("1" (assert) (("1" (expand* "union" "member") (("1" (prop) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "p1!1" "lhs(e!1)" "sigma!1") (("1" (assert) (("1" (replaces -1) (("1" (lemma "CP_lemma_aux1") (("1" (inst -1 "sigma!1" "sigma!2" "E" "p1!1" "(lhs(e!1), rhs(e!1))" "(lhs(e!2), rhs(e!2))") (("1" (expand* "lhs" "rhs") (("1" (assert) (("1" (skosimp*) (("1" (inst -10 "t1!1" "t2!1") (("1" (assert) (("1" (replace -8 -3 rl) (("1" (expand "joinable?") (("1" (skolem -10 "M") (("1" (lemma "reduction_is_subs_op") (("1" (inst?) (("1" (flatten) (("1" (lemma "closure_close_subs") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide (-1 -3 -4)) (("1" (expand "close_subs?") (("1" (copy -1) (("1" (inst -1 "t1!1" "M" "delta!1") (("1" (inst -2 "t2!1" "M" "delta!1") (("1" (assert) (("1" (replaces -5) (("1" (replaces -5) (("1" (lemma "comp_op_iff_comp_cont") (("1" (inst?) (("1" (assert) (("1" (lemma "closure_comp_cont") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide (-1 -3 -4 -7)) (("1" (copy -1) (("1" (expand "comp_cont?") (("1" (inst -1 "p!1" "x") (("1" (assert) (("1" (inst -2 "p!1" "x") (("1" (assert) (("1" (inst -1 "ext(sigma!1)(e!1`2)" "ext(delta!1)(M)") (("1" (inst -2 "subtermOF(z, p!1)" "ext(delta!1)(M)") (("1" (assert) (("1" (lemma "replace_associativity") (("1" (inst -1 "p!1" "p1!1" "ext(sigma!2)(e!2`2)" "x" "ext(sigma!1)(e!1`1)") (("1" (assert) (("1" (replace -12 -1 rl) (("1" (replace -11 -1 rl) (("1" (replace -15 -1 rl) (("1" (rewrite "replace_subterm_of_term") (("1" (replace -18 -1 rl) (("1" (replace -1 -3 rl) (("1" (replace -16 -2 rl) (("1" (hide-all-but (-2 -3 2)) (("1" (inst 1 "replaceTerm(x, ext(delta!1)(M), p!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "e!2") (("2" (hide-all-but (-1 -2 1)) (("2" (expand* "lhs" "rhs" "member" "rewrite_rule?") (("2" (prop) (("2" (hide-all-but (-2 1)) (("2" (case-replace "(e!2) = (e!2`1, e!2`2)" :hide? t) (("1" (assert) nil nil) ("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "e!1") (("3" (hide-all-but (-1 -2 1)) (("3" (expand* "lhs" "rhs" "member" "rewrite_rule?") (("3" (case-replace "(e!1) = (e!1`1, e!1`2)" :hide? t) (("1" (assert) nil nil) ("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name-replace "w" "subtermOF(lhs(e!1), p1!2)" :hide? nil) (("2" (lemma "CP_lemma_aux2") (("2" (inst -1 "reduction?(E)" "lhs(e!1)" "w" "sigma!1" "SigmaP(sigma!1, ext(sigma!2)(rhs(e!2)), w, p2!1)") (("1" (skoletin* -1 :old? t) (("1" (prop) (("1" (hide -2) (("1" (lemma "set2seq_exists[position]") (("1" (inst -1 "Posv" "p1!2") (("1" (replace -3 -1 rl) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (inst -2 "ii!1") (("1" (replace -1 -2) (("1" (hide (-1 -3 -4)) (("1" (lemma "CP_lemma_aux2") (("1" (inst -1 "reduction?(E)" "rhs(e!1)" "w" "sigma!1" "SigmaP(sigma!1, ext(sigma!2)(rhs(e!2)), w, p2!1)") (("1" (lemma "set2seq_exists[position]") (("1" (inst -1 "Posv" "p1!2") (("1" (assert) (("1" (hide -1) (("1" (prop) (("1" (hide -1) (("1" (name-replace "SIGMAp" "SigmaP(sigma!1, ext(sigma!2)(rhs(e!2)), w, p2!1)") (("1" (case "length( #(p1!2)) = 0") (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (expand "replace_pos" -2) (("2" (assert) (("2" (expand "replace_pos" -2) (("2" (case "length(rest( #(p1!2))) = 0") (("1" (assert) (("1" (hide -1) (("1" (expand "SIGMAp" -2 1) (("1" (expand "ext" -2 2) (("1" (expand "SigmaP" -2 1) (("1" (lemma "gen_seq_lem[position]") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (replaces -1) (("1" (expand "ext" -7) (("1" (lemma "ext_preserv_pos") (("1" (inst -1 "p1!2" "lhs(e!1)" "sigma!1") (("1" (assert) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "p1!2" "lhs(e!1)" "sigma!1") (("1" (assert) (("1" (replaces -5 -1) (("1" (expand "ext" -1 2) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "p1!2" "ext(sigma!1)(lhs(e!1))") (("1" (assert) (("1" (replaces -2 -1) (("1" (lemma "replace_associativity") (("1" (inst -1 "p1!2" "p2!1" "ext(sigma!2)(rhs(e!2))" "ext(sigma!1)(lhs(e!1))" "sigma!1(w)") (("1" (assert) (("1" (replaces -2 -1) (("1" (replace -5 -1 rl) (("1" (replace -1 -4 rl) (("1" (hide -1) (("1" (replace -11 -3 rl) (("1" (case "RTC(reduction?(E))(subtermOF(z, p!1), ext(SIGMAp)(rhs(e!1)))") (("1" (hide -4) (("1" (lemma "reduction_is_subs_op") (("1" (inst?) (("1" (flatten) (("1" (lemma "comp_op_iff_comp_cont") (("1" (inst?) (("1" (assert) (("1" (lemma "closure_comp_cont") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide (-1 -3 -4 -5 -6)) (("1" (copy -1) (("1" (expand "comp_cont?") (("1" (inst -1 "p!1" "x") (("1" (assert) (("1" (inst -2 "p!1" "x") (("1" (assert) (("1" (inst -1 "ext(sigma!1)(e!1`2)" "ext(SIGMAp)(rhs(e!1))") (("1" (inst -2 "subtermOF(z, p!1)" "ext(SIGMAp)(rhs(e!1))") (("1" (expand* "rhs" "lhs") (("1" (assert) (("1" (lemma "replace_associativity") (("1" (inst -1 "p!1" "p1!1" "ext(sigma!2)(e!2`2)" "x" "ext(sigma!1)(e!1`1)") (("1" (assert) (("1" (replace -14 -1 rl) (("1" (replace -15 -1 rl) (("1" (replace -17 -1 rl) (("1" (rewrite "replace_subterm_of_term") (("1" (replace -1 -3 rl) (("1" (replace -20 -3 rl) (("1" (replace -18 -2 rl) (("1" (hide-all-but (-2 -3 2)) (("1" (expand "joinable?") (("1" (inst 1 "replaceTerm(x, ext(SIGMAp)(e!1`2), p!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "reduction_is_subs_op") (("2" (inst?) (("2" (flatten) (("2" (hide -2) (("2" (lemma "lhs_reduces_to_rhs") (("2" (inst?) (("2" (expand "close_subs?") (("2" (inst -2 "lhs(e!1)" "rhs(e!1)" "SIGMAp") (("2" (assert) (("2" (expand "RTC") (("2" (expand "IUnion") (("2" (skosimp*) (("2" (inst 1 "i!1 + 1") (("2" (expand "iterate" 1) (("2" (expand "o") (("2" (inst 1 "ext(SIGMAp)(lhs(e!1))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "reduction_is_subs_op") (("2" (inst?) (("2" (flatten) (("2" (lemma "comp_op_iff_comp_cont") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 -3 -4 -5 -6 -7 -8 -9 -11 -15 1)) (("3" (lemma "subterm_of_ext") (("3" (inst -1 "p1!2" "p2!1" "sigma!1" "lhs(e!1)") (("3" (replace -2 -1) (("3" (expand "ext" -1 (1 3)) (("3" (expand "ext" -6) (("3" (assert) (("3" (replace -3 -1 rl) (("3" (replace -11 -1) (("3" (lemma "lhs_reduces_to_rhs") (("3" (inst?) (("3" (lemma "reduction_is_subs_op") (("3" (inst?) (("3" (flatten) (("3" (lemma "comp_op_iff_comp_cont") (("3" (inst?) (("3" (assert) (("3" (expand "close_subs?") (("3" (inst -2 "lhs(e!2)" "rhs(e!2)" "sigma!2") (("3" (assert) (("3" (replaces -5) (("3" (hide (-1 -3 -4)) (("3" (lemma "SigmaP_is_RSigma") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "Posv") (("2" (lemma "Pos_var_is_finite") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -6 -7 1)) (("2" (expand "Posv") (("2" (lemma "no_empty_set_positions") (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "reduction_is_subs_op") (("2" (inst?) (("2" (flatten) (("2" (lemma "comp_op_iff_comp_cont") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 -4 -5 -6 -7 -8 -9 -10 -12 -16 1)) (("3" (lemma "subterm_of_ext") (("3" (inst -1 "p1!2" "p2!1" "sigma!1" "lhs(e!1)") (("3" (replace -2 -1) (("3" (expand "ext" -1 (1 3)) (("3" (expand "ext" -6) (("3" (assert) (("3" (assert) (("3" (replace -3 -1 rl) (("3" (replace -11 -1) (("3" (lemma "lhs_reduces_to_rhs") (("3" (inst?) (("3" (lemma "reduction_is_subs_op") (("3" (inst?) (("3" (flatten) (("3" (lemma "comp_op_iff_comp_cont") (("3" (inst?) (("3" (assert) (("3" (expand "close_subs?") (("3" (inst -2 "lhs(e!2)" "rhs(e!2)" "sigma!2") (("3" (assert) (("3" (replaces -5) (("3" (hide (-1 -3 -4)) (("3" (lemma "SigmaP_is_RSigma") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -4 1)) (("2" (expand "ext" -2) (("2" (assert) (("2" (rewrite "SigmaP_Subs") nil nil)) nil)) nil)) nil) ("3" (hide-all-but (-5 -4 1)) (("3" (expand "ext" -2) (("3" (assert) nil nil)) nil)) nil) ("4" (expand "V") (("4" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "replace_distributivity") (("2" (inst?) (("2" (inst -1 "x" "ext(sigma!1)(rhs(e!1))") (("2" (replace -2 -1 rl) (("2" (typepred "p!1") (("2" (assert) (("2" (replace -6 -2 rl) (("2" (replace -7 -2) (("2" (lemma "pos_subterm") (("2" (inst?) (("2" (inst -1 "x") (("2" (replace -4 -1 rl) (("2" (assert) (("2" (replace -8 -1) (("2" (replace -1 -6) (("2" (lemma "pos_subterm_ax") (("2" (inst -1 "p!2" "p1!1" "x") (("2" (replace -5 -3) (("2" (assert) (("2" (replace -9 -1) (("2" (lemma "positions_of_ext") (("2" (inst -1 "sigma!2" "lhs(e!2)") (("2" (decompose-equality -1) (("2" (inst -1 "p1!1") (("2" (iff) (("2" (flatten) (("2" (hide -2) (("2" (assert) (("2" (expand* "union" "member") (("2" (prop) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "p1!1" "lhs(e!2)" "sigma!2") (("1" (assert) (("1" (replaces -1) (("1" (lemma "CP_lemma_aux1") (("1" (inst -1 "sigma!2" "sigma!1" "E" "p1!1" "(lhs(e!2), rhs(e!2))" "(lhs(e!1), rhs(e!1))") (("1" (expand* "lhs" "rhs") (("1" (assert) (("1" (skosimp*) (("1" (inst -10 "t1!1" "t2!1") (("1" (assert) (("1" (replace -8 -3 rl) (("1" (expand "joinable?") (("1" (skolem -10 "M") (("1" (lemma "reduction_is_subs_op") (("1" (inst?) (("1" (flatten) (("1" (lemma "closure_close_subs") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide (-1 -3 -4)) (("1" (expand "close_subs?") (("1" (copy -1) (("1" (inst -1 "t1!1" "M" "delta!1") (("1" (inst -2 "t2!1" "M" "delta!1") (("1" (assert) (("1" (replaces -5) (("1" (replaces -5) (("1" (lemma "comp_op_iff_comp_cont") (("1" (inst?) (("1" (assert) (("1" (lemma "closure_comp_cont") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (hide (-1 -3 -4 -7)) (("1" (copy -1) (("1" (expand "comp_cont?") (("1" (inst -1 "p!2" "x") (("1" (assert) (("1" (inst -2 "p!2" "x") (("1" (assert) (("1" (inst -1 "ext(sigma!2)(e!2`2)" "ext(delta!1)(M)") (("1" (inst -2 "subtermOF(y, p!2)" "ext(delta!1)(M)") (("1" (assert) (("1" (lemma "replace_associativity") (("1" (inst -1 "p!2" "p1!1" "ext(sigma!1)(e!1`2)" "x" "ext(sigma!2)(e!2`1)") (("1" (assert) (("1" (replace -12 -1 rl) (("1" (replace -11 -1 rl) (("1" (replace -17 -1 rl) (("1" (rewrite "replace_subterm_of_term") (("1" (replace -16 -1 rl) (("1" (replace -1 -3 rl) (("1" (replace -18 -2 rl) (("1" (hide-all-but (-2 -3 2)) (("1" (inst 1 "replaceTerm(x, ext(delta!1)(M), p!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "e!1") (("2" (hide-all-but (-1 -2 1)) (("2" (expand* "lhs" "rhs" "member" "rewrite_rule?") (("2" (prop) (("2" (hide-all-but (-2 1)) (("2" (case-replace "e!1 = (e!1`1, e!1`2)" :hide? t) (("1" (assert) nil nil) ("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "e!2") (("3" (hide-all-but (-1 -2 1)) (("3" (expand* "lhs" "rhs" "member" "rewrite_rule?") (("3" (case-replace "e!2 = (e!2`1, e!2`2)" :hide? t) (("1" (assert) nil nil) ("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name-replace "w" "subtermOF(lhs(e!2), p1!2)" :hide? nil) (("2" (lemma "CP_lemma_aux2") (("2" (inst -1 "reduction?(E)" "lhs(e!2)" "w" "sigma!2" "SigmaP(sigma!2, ext(sigma!1)(rhs(e!1)), w, p2!1)") (("1" (skoletin* -1 :old? t) (("1" (prop) (("1" (hide -2) (("1" (lemma "set2seq_exists[position]") (("1" (inst -1 "Posv" "p1!2") (("1" (replace -3 -1 rl) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (inst -2 "ii!1") (("1" (replace -1 -2) (("1" (hide (-1 -3 -4)) (("1" (lemma "CP_lemma_aux2") (("1" (inst -1 "reduction?(E)" "rhs(e!2)" "w" "sigma!2" "SigmaP(sigma!2, ext(sigma!1)(rhs(e!1)), w, p2!1)") (("1" (lemma "set2seq_exists[position]") (("1" (inst -1 "Posv" "p1!2") (("1" (assert) (("1" (hide -1) (("1" (prop) (("1" (hide -1) (("1" (name-replace "SIGMAp" "SigmaP(sigma!2, ext(sigma!1)(rhs(e!1)), w, p2!1)") (("1" (case "length( #(p1!2)) = 0") (("1" (hide-all-but -1) (("1" (grind) nil nil)) nil) ("2" (expand "replace_pos" -2) (("2" (assert) (("2" (expand "replace_pos" -2) (("2" (case "length(rest( #(p1!2))) = 0") (("1" (assert) (("1" (hide -1) (("1" (expand "SIGMAp" -2 1) (("1" (expand "ext" -2 2) (("1" (expand "SigmaP" -2 1) (("1" (lemma "gen_seq_lem[position]") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (replaces -1) (("1" (expand "ext" -7) (("1" (lemma "ext_preserv_pos") (("1" (inst -1 "p1!2" "lhs(e!2)" "sigma!2") (("1" (assert) (("1" (lemma "subterm_ext_commute") (("1" (inst -1 "p1!2" "lhs(e!2)" "sigma!2") (("1" (assert) (("1" (replaces -5 -1) (("1" (expand "ext" -1 2) (("1" (lemma "replace_subterm_of_term") (("1" (inst -1 "p1!2" "ext(sigma!2)(lhs(e!2))") (("1" (assert) (("1" (replaces -2 -1) (("1" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.464 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26