|
(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)(Vars(ext(rho!1)(lhs(e2!1)))))))(subtermOF(lhs(e1!1), p!1)) = ext(union_subs((restriction(sg1!1)(Vars(lhs(e1!1))), restriction(alpha!1)(Vars(ext(rho!1)(lhs(e2!1)))))))(ext(rho!1)(lhs(e2!1)))")
(("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(rho!1)(lhs(e2!1)))))")
(("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))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.55 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
