|
(results_confluence
(Joinable_implies_Equiv 0
(Joinable_implies_Equiv-1 nil 3374063633
("" (skeep)
(("" (expand "joinable?")
(("" (skolem * "z")
(("" (flatten)
(("" (lemma "RTC_subset_EC")
(("" (inst?)
(("" (expand* "subset?" "member")
(("" (copy -1)
(("" (inst -1 "(x, z)")
(("" (inst -2 "(y, z)")
(("" (assert)
(("" (hide (-3 -4))
(("" (typepred "EC(R)")
(("" (expand "equivalence?")
((""
(flatten)
((""
(hide -1)
((""
(expand "symmetric?")
((""
(expand "transitive?")
((""
(inst -1 "y" "z")
((""
(inst -2 "x" "z" "y")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((joinable? const-decl "bool" ars_terminology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(equivalence? const-decl "bool" relations nil)
(equivalence type-eq-decl nil relations_closure nil)
(EC const-decl "equivalence" relations_closure nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(RTC_subset_EC formula-decl nil relations_closure nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(reduct_transitive 0
(reduct_transitive-1 nil 3374063683
("" (skeep)
(("" (expand "joinable?" -2)
(("" (skolem * "r")
(("" (flatten)
(("" (expand "joinable?")
(("" (inst?)
(("" (prop)
(("" (typepred "RTC(R)")
(("" (expand "reflexive_transitive?")
(("" (flatten)
(("" (lemma "R_subset_RTC")
(("" (inst?)
(("" (expand* "subset?" "member")
(("" (inst -1 "(x, y)")
((""
(assert)
((""
(expand "transitive?")
((""
(inst -3 "x" "y" "r")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((joinable? const-decl "bool" ars_terminology nil)
(T formal-type-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types 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)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(transitive? const-decl "bool" relations nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(R_subset_RTC formula-decl nil relations_closure nil))
shostak))
(semi_and_iterate 0
(semi_and_iterate-1 nil 3374063721
("" (expand "joinable?")
(("" (induct "n")
(("1" (skeep)
(("1" (typepred "RTC(R)")
(("1" (inst 1 "x")
(("1" (expand "reflexive_transitive?")
(("1" (flatten)
(("1" (split)
(("1" (hide-all-but (-1 1))
(("1" (expand "reflexive?") (("1" (inst?) nil nil))
nil))
nil)
("2" (hide-all-but (-4 1))
(("2" (expand "iterate")
(("2" (assert)
(("2" (expand* "RTC" "IUnion")
(("2" (inst? 1 ("i" "0"))
(("2" (expand "iterate")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (rewrite "iterate_add_one")
(("2" (expand "o")
(("2" (skolem * "r")
(("2" (flatten)
(("2" (inst -1 "R" "r" "y")
(("2" (assert)
(("2" (hide -4)
(("2" (expand* "SC" "union" "member")
(("2" (prop)
(("1" (hide -3)
(("1"
(skolem * "z")
(("1"
(inst?)
(("1"
(prop)
(("1"
(lemma "R_subset_RTC")
(("1"
(inst?)
(("1"
(expand* "subset?" "member")
(("1"
(inst -1 "(x, r)")
(("1"
(assert)
(("1"
(typepred "RTC(R)")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(expand
"transitive?")
(("1"
(inst
-2
"x"
"r"
"z")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "converse")
(("2"
(expand "semi_confluent?")
(("2"
(expand "joinable?")
(("2"
(skolem * "z1")
(("2"
(flatten)
(("2"
(inst -4 "r" "x" "z1")
(("2"
(assert)
(("2"
(skolem * "z2")
(("2"
(inst 1 "z2")
(("2"
(prop)
(("2"
(hide-all-but
(-3 -5 1))
(("2"
(typepred "RTC(R)")
(("2"
(expand
"reflexive_transitive?")
(("2"
(flatten)
(("2"
(expand
"transitive?")
(("2"
(inst
-2
"y"
"z1"
"z2")
(("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)
((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)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(semi_confluent? const-decl "bool" ars_terminology nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(symmetric? const-decl "bool" relations nil)
(symmetric type-eq-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure 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)
(nat_induction formula-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(reflexive? const-decl "bool" relations nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(O const-decl "bool" relation_props nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(R_subset_RTC formula-decl nil relations_closure nil)
(subset? const-decl "bool" sets nil)
(transitive? const-decl "bool" relations nil)
(iterate_add_one formula-decl nil relation_iterate "orders/")
(joinable? const-decl "bool" ars_terminology nil))
shostak))
(Confl_implies_Semi 0
(Confl_implies_Semi-1 nil 3374063795
("" (skeep)
(("" (expand "semi_confluent?")
(("" (skeep)
(("" (expand "confluent?")
(("" (inst? -1 ("x" "x" "y" "y" "z" "z"))
(("" (prop)
(("" (hide (-2 2))
(("" (lemma "R_subset_RTC")
(("" (inst?)
(("" (expand* "subset?" "member")
(("" (inst -1 "(x,y)") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((semi_confluent? const-decl "bool" ars_terminology nil)
(confluent? const-decl "bool" ars_terminology nil)
(R_subset_RTC formula-decl nil relations_closure nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(PRED type-eq-decl nil defined_types nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(Semi_implies_CR 0
(Semi_implies_CR-1 nil 3374063856
("" (skeep)
(("" (expand "church_rosser?")
(("" (skeep)
(("" (expand "EC")
(("" (expand "RTC")
(("" (expand "IUnion")
(("" (skolem * "i")
(("" (lemma "semi_and_iterate")
(("" (inst -1 "R" "x" "y" "i")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((church_rosser? const-decl "bool" ars_terminology nil)
(EC const-decl "equivalence" relations_closure nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(semi_and_iterate formula-decl nil results_confluence 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)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil)
(RTC const-decl "reflexive_transitive" relations_closure nil))
shostak))
(CR_iff_Confluent 0
(CR_iff_Confluent-1 nil 3374321725
("" (skeep)
(("" (prop)
(("1" (expand "confluent?")
(("1" (skeep)
(("1" (expand "church_rosser?")
(("1" (inst? -1 ("x" "y" "y" "z"))
(("1" (prop)
(("1" (hide 2)
(("1" (lemma "preorder_closure_is_monotone")
(("1" (inst -1 "R" "SC(R)")
(("1" (rewrite-lemma "change_to_RTC" ("R" "R"))
(("1"
(rewrite-lemma "change_to_RTC" ("R" "SC(R)"))
(("1" (lemma "R_subset_SC")
(("1" (inst?)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(expand* "subset?" "member")
(("1"
(copy -1)
(("1"
(inst? -1 ("x" "(x, y)"))
(("1"
(inst? -2 ("x" "(x, z)"))
(("1"
(assert)
(("1"
(typepred "EC(R)")
(("1"
(expand "EC")
(("1"
(expand
"equivalence?")
(("1"
(flatten)
(("1"
(hide (-1 -6 -7))
(("1"
(expand*
"symmetric?"
"transitive?")
(("1"
(inst?
-1
("x"
"x"
"y"
"y"))
(("1"
(inst?
-2
("x"
"y"
"y"
"x"
"z"
"z"))
(("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)
("2" (lemma "Confl_implies_Semi")
(("2" (inst?)
(("2" (lemma "Semi_implies_CR")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil results_confluence nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric type-eq-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(equivalence? const-decl "bool" relations nil)
(equivalence type-eq-decl nil relations_closure nil)
(EC const-decl "equivalence" relations_closure nil)
(transitive? const-decl "bool" relations nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(R_subset_SC formula-decl nil relations_closure nil)
(change_to_RTC formula-decl nil relations_closure nil)
(preorder_closure_is_monotone formula-decl nil closure_ops
"orders/")
(church_rosser? const-decl "bool" ars_terminology nil)
(confluent? const-decl "bool" ars_terminology nil)
(Semi_implies_CR formula-decl nil results_confluence nil)
(Confl_implies_Semi formula-decl nil results_confluence nil))
shostak))
(strong_and_iterate 0
(strong_and_iterate-1 nil 3374063926
("" (induct "n")
(("1" (skeep)
(("1" (inst 1 "y")
(("1" (prop)
(("1" (assert)
(("1" (expand "RTC")
(("1" (expand "IUnion")
(("1" (inst 1 "0")
(("1" (expand "iterate") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "iterate")
(("2" (expand "RC")
(("2" (expand "union")
(("2" (flatten)
(("2" (expand "member") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (rewrite "iterate_add")
(("2" (rewrite "iterate_1")
(("2" (expand "o")
(("2" (skolem * "xj")
(("2" (inst -1 "R" "x" "y" "xj")
(("2" (prop)
(("2" (skolem * "yj")
(("2" (flatten)
(("2" (expand "RC" -2)
(("2" (expand* "union" "member")
(("2" (split)
(("1"
(hide (-4 -5))
(("1"
(expand "strong_confluent?")
(("1"
(inst -3 "xj" "yj" "z")
(("1"
(assert)
(("1"
(skolem * "r")
(("1"
(inst 1 "r")
(("1"
(prop)
(("1"
(typepred "RTC(R)")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(expand
"transitive?")
(("1"
(inst
-2
"y"
"yj"
"r")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 -2 rl)
(("2"
(hide-all-but (-2 -6 1))
(("2"
(inst 1 "z")
(("2"
(prop)
(("1"
(lemma "R_subset_RTC")
(("1"
(inst?)
(("1"
(expand*
"subset?"
"member")
(("1"
(inst -1 "(xj, z)")
(("1"
(assert)
(("1"
(typepred "RTC(R)")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(expand
"transitive?")
(("1"
(inst
-2
"y"
"xj"
"z")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "RC" "union" "member")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((iterate_add formula-decl nil relation_iterate "orders/")
(O const-decl "bool" relation_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(transitive? const-decl "bool" relations nil)
(subset? const-decl "bool" sets nil)
(R_subset_RTC formula-decl nil relations_closure nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(IUnion const-decl "set[T]" indexed_sets nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(nat_induction formula-decl nil naturalnumbers nil)
(RC const-decl "reflexive" relations_closure nil)
(reflexive type-eq-decl nil relations_closure nil)
(reflexive? const-decl "bool" relations 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)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(strong_confluent? const-decl "bool" ars_terminology nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil results_confluence nil)
(pred type-eq-decl nil defined_types 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))
shostak))
(Str_Confl_implies_Semi_Confl 0
(Str_Confl_implies_Semi_Confl-1 nil 3374064012
("" (skeep)
(("" (expand "semi_confluent?")
(("" (skeep)
(("" (expand* "RTC" "IUnion")
(("" (skolem * "i")
(("" (lemma "strong_and_iterate")
(("" (inst -1 "R" "x" "y" "z" "i")
(("" (assert)
(("" (hide-all-but (-1 1))
(("" (expand "joinable?")
(("" (skolem * "r")
(("" (flatten)
(("" (inst 1 "r")
(("" (prop)
((""
(hide -1)
((""
(expand* "RTC" "IUnion")
((""
(expand* "RC" "union" "member")
((""
(prop)
(("1"
(inst 1 "1")
(("1"
(rewrite "iterate_1")
nil
nil))
nil)
("2"
(inst 1 "0")
(("2"
(expand "iterate")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((semi_confluent? const-decl "bool" ars_terminology nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(strong_and_iterate formula-decl nil results_confluence nil)
(joinable? const-decl "bool" ars_terminology nil)
(pred type-eq-decl nil defined_types nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(RC const-decl "reflexive" relations_closure nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets 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)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(Strong_Confl_implies_Confl 0
(Strong_Confl_implies_Confl-1 nil 3374064199
("" (skeep)
(("" (lemma "Str_Confl_implies_Semi_Confl")
(("" (inst?)
(("" (lemma "Semi_implies_CR")
(("" (inst?)
(("" (lemma "CR_iff_Confluent")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((Str_Confl_implies_Semi_Confl formula-decl nil results_confluence
nil)
(Semi_implies_CR formula-decl nil results_confluence nil)
(CR_iff_Confluent formula-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(DP_implies_StC 0
(DP_implies_StC-1 nil 3374064308
("" (skeep)
(("" (expand "strong_confluent?")
(("" (skeep)
(("" (expand "diamond_property?")
(("" (inst -1 "x" "y" "z")
(("" (assert)
(("" (skolem * "r")
(("" (flatten)
(("" (hide (-3 -4))
(("" (inst 1 "r")
(("" (lemma "R_subset_RTC")
(("" (inst?)
(("" (expand* "subset?" "member")
(("" (inst -1 "(y, r)")
((""
(lemma "R_subset_RC")
((""
(inst?)
((""
(expand* "subset?" "member")
((""
(inst -1 "(z, r)")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((strong_confluent? const-decl "bool" ars_terminology nil)
(diamond_property? const-decl "bool" ars_terminology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(R_subset_RC formula-decl nil relations_closure nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(R_subset_RTC formula-decl nil relations_closure nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(R1_Confl_iff_R2_Confl 0
(R1_Confl_iff_R2_Confl-1 nil 3374321809
("" (skeep)
(("" (decompose-equality -1)
(("" (copy -1)
(("" (copy -1)
(("" (copy -1)
(("" (expand "confluent?")
(("" (prop)
(("1" (skeep)
(("1" (inst -1 "x" "y" "z")
(("1" (inst? -4 ("x" "(x, y)"))
(("1" (inst? -5 ("x" "(x, z)"))
(("1" (replace -4 -1)
(("1" (replace -5 -1)
(("1" (assert)
(("1"
(hide-all-but (-1 -6 -7 1))
(("1"
(expand "joinable?")
(("1"
(skolem * "r")
(("1"
(flatten)
(("1"
(inst? -3 ("x" "(y, r)"))
(("1"
(inst? -4 ("x" "(z, r)"))
(("1"
(inst 1 "r")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (inst -1 "x" "y" "z")
(("2" (inst? -4 ("x" "(x, y)"))
(("2" (inst? -5 ("x" "(x, z)"))
(("2" (replace -4 -1 rl)
(("2" (replace -5 -1 rl)
(("2" (assert)
(("2"
(hide-all-but (-1 -6 -7 1))
(("2"
(expand "joinable?")
(("2"
(skolem * "r")
(("2"
(flatten)
(("2"
(inst? -3 ("x" "(y, r)"))
(("2"
(inst? -4 ("x" "(z, r)"))
(("2"
(inst 1 "r")
(("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)
((T formal-type-decl nil results_confluence nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types 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)
(PRED type-eq-decl nil defined_types nil)
(confluent? const-decl "bool" ars_terminology nil)
(joinable? const-decl "bool" ars_terminology nil))
shostak))
(R1_equal_R2 0
(R1_equal_R2-1 nil 3374064621
("" (skeep)
(("" (lemma "preorder_closure_is_monotone")
(("" (copy -1)
(("" (inst -1 "R1" "R2")
(("" (inst -2 "R2" "RTC(R1)")
(("" (rewrite-lemma "change_to_RTC" ("R" "R1"))
(("" (rewrite-lemma "change_to_RTC" ("R" "R2"))
(("" (rewrite-lemma "change_to_RTC" ("R" "RTC(R1)"))
(("" (assert)
(("" (rewrite "RTC_idempotent")
(("" (hide (-3 -4))
(("" (apply-extensionality :hide? t)
(("" (iff)
(("" (expand* "subset?" "member")
((""
(inst -1 "(x!1, x!2)")
((""
(inst -2 "(x!1, x!2)")
(("" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil results_confluence nil)
(preorder_closure_is_monotone formula-decl nil closure_ops
"orders/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(change_to_RTC formula-decl nil relations_closure nil)
(RTC_idempotent formula-decl nil relations_closure nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas 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))
shostak))
(R2_Str_Confl_implies_R1_Confl 0
(R2_Str_Confl_implies_R1_Confl-1 nil 3374064655
("" (skeep)
(("" (lemma "R1_equal_R2")
(("" (inst -1 "R1" "R2")
(("" (assert)
(("" (hide (-2 -3))
(("" (lemma "Strong_Confl_implies_Confl")
(("" (inst -1 "R2")
(("" (assert)
(("" (hide -3)
(("" (lemma "R1_Confl_iff_R2_Confl")
(("" (inst -1 "R1" "R2") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((R1_equal_R2 formula-decl nil results_confluence nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(Strong_Confl_implies_Confl formula-decl nil results_confluence
nil)
(R1_Confl_iff_R2_Confl formula-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil))
shostak))
(Confluence_Commute 0
(Confluence_Commute-1 nil 3374064705
("" (skeep)
(("" (expand "diamond_property?")
(("" (skeep)
(("" (expand "o" (-4 -5))
(("" (skolem * "y1")
(("" (skolem * "z1")
(("" (expand "confluent?")
(("" (inst -1 "x" "y1" "z1")
(("" (assert)
(("" (prop)
(("" (expand "joinable?" -1)
(("" (skolem * "r1")
(("" (flatten)
(("" (copy -4)
((""
(expand "commute?")
((""
(inst -5 "y1" "r1" "y")
((""
(assert)
((""
(skolem * "r2")
((""
(flatten)
((""
(inst -1 "z1" "r1" "z")
((""
(assert)
((""
(skolem * "r3")
((""
(flatten)
((""
(inst
-5
"r1"
"r2"
"r3")
((""
(assert)
((""
(expand
"joinable?")
((""
(skolem * "r4")
((""
(flatten)
((""
(inst
1
"r4")
((""
(expand
"o")
((""
(split)
(("1"
(inst
1
"r2")
(("1"
(assert)
nil
nil))
nil)
("2"
(inst
1
"r3")
(("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)
((diamond_property? const-decl "bool" ars_terminology nil)
(O const-decl "bool" relation_props nil)
(T formal-type-decl nil results_confluence nil)
(commute? const-decl "bool" ars_terminology nil)
(joinable? const-decl "bool" ars_terminology nil)
(confluent? const-decl "bool" ars_terminology nil))
shostak))
(R1_R2_RTC_R1_R2 0
(R1_R2_RTC_R1_R2-1 nil 3374064758
("" (skeep)
(("" (split)
(("1" (expand* "subset?" "member")
(("1" (skeep)
(("1" (expand* "union" "member")
(("1" (prop)
(("1" (expand "o")
(("1" (inst 1 "x`2")
(("1" (lemma "R_subset_RTC")
(("1" (inst?)
(("1" (expand* "subset?" "member")
(("1" (inst?)
(("1" (assert)
(("1" (hide-all-but 1)
(("1"
(expand* "RTC" "IUnion")
(("1"
(inst 1 "0")
(("1"
(expand "iterate")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o")
(("2" (inst 1 "x`1")
(("2" (lemma "R_subset_RTC")
(("2" (inst -1 "R2")
(("2" (expand* "subset?" "member")
(("2" (inst?)
(("2" (assert)
(("2" (hide-all-but 1)
(("2"
(expand* "RTC" "IUnion")
(("2"
(inst 1 "0")
(("2"
(expand "iterate")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "subset?" "member")
(("2" (skeep)
(("2" (expand "o")
(("2" (skolem * "y")
(("2" (flatten)
(("2" (expand* "RTC" "IUnion")
(("2" (skolem * "i1")
(("2" (skolem * "i2")
(("2" (inst 1 "i1 + i2")
(("2" (rewrite "iterate_add")
(("2" (expand "o")
(("2" (inst 1 "y")
(("2"
(split)
(("1"
(hide -2)
(("1"
(case "subset?(R1, union(R1, R2))")
(("1"
(lemma "iterate_is_monotone")
(("1"
(inst?
-1
("R1"
"R1"
"R2"
"union(R1, R2)"))
(("1"
(assert)
(("1"
(hide -2)
(("1"
(expand*
"subset?"
"member")
(("1"
(inst -1 "(x`1, y)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "subset?" "member")
(("2"
(skosimp*)
(("2"
(expand* "union" "member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(case "subset?(R2, union(R1, R2))")
(("1"
(lemma "iterate_is_monotone")
(("1"
(inst?
-1
("R1"
"R2"
"R2"
"union(R1, R2)"))
(("1"
(assert)
(("1"
(hide -2)
(("1"
(expand*
"subset?"
"member")
(("1"
(inst -1 "(y,x`2)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "subset?" "member")
(("2"
(skosimp*)
(("2"
(expand* "union" "member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans 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)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(RTC const-decl "reflexive_transitive" relations_closure nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(R_subset_RTC formula-decl nil relations_closure nil)
(O const-decl "bool" relation_props nil)
(union const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(iterate_add formula-decl nil relation_iterate "orders/")
(iterate_is_monotone formula-decl nil relation_iterate "orders/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
shostak))
(Commutative_Union_Lemma 0
(Commutative_Union_Lemma-1 nil 3374064822
("" (skeep)
(("" (lemma "Confluence_Commute")
(("" (inst -1 "R1" "R2")
(("" (assert)
(("" (lemma "DP_implies_StC")
(("" (inst -1 "RTC(R1) o RTC(R2)")
(("" (assert)
(("" (lemma "R1_R2_RTC_R1_R2")
(("" (inst -1 "R1" "R2")
(("" (flatten)
(("" (lemma "R2_Str_Confl_implies_R1_Confl")
((""
(inst -1 "union(R1, R2)" "RTC(R1) o RTC(R2)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Confluence_Commute formula-decl nil results_confluence nil)
(pred type-eq-decl nil defined_types nil)
(O const-decl "bool" relation_props 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)
(R1_R2_RTC_R1_R2 formula-decl nil results_confluence nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(R2_Str_Confl_implies_R1_Confl formula-decl nil results_confluence
nil)
(DP_implies_StC formula-decl nil results_confluence nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil results_confluence nil))
shostak)))
¤ Dauer der Verarbeitung: 0.93 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.
|
