|
(confluence_commute
(RC_RTC_is_RTC 0
(RC_RTC_is_RTC-1 nil 3390042971
("" (lemma "RTC_characterization")
(("" (skeep)
(("" (inst -1 "RTC(R)")
(("" (lemma "RTC_idempotent")
(("" (inst -1 "R")
(("" (prop)
(("1" (expand reflexive_transitive?)
(("1" (flatten)
(("1" (lemma "RC_characterization")
(("1" (inst -1 "RTC(R)") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((RTC_idempotent formula-decl nil relations_closure nil)
(RC_characterization formula-decl nil relations_closure 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(RTC_characterization formula-decl nil relations_closure nil)
(T formal-type-decl nil confluence_commute nil))
shostak))
(RTC_o_RTC_is_RTC 0
(RTC_o_RTC_is_RTC-1 nil 3401787428
("" (skeep)
(("" (expand "RTC")
(("" (expand "IUnion")
(("" (skosimp*)
(("" (inst 1 "i!1 + i!2")
(("" (lemma iterate_add)
(("" (inst -1 "R" "i!1" "i!2")
(("" (assert) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((RTC const-decl "reflexive_transitive" relations_closure nil)
(iterate_add formula-decl nil relation_iterate "orders/")
(T formal-type-decl nil confluence_commute nil)
(O const-decl "bool" relation_props nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(RC_o_RTC_is_RTC 0
(RC_o_RTC_is_RTC-1 nil 3417283391
("" (skeep)
(("" (expand "RTC")
(("" (expand "RC")
(("" (expand "IUnion")
(("" (expand "union")
(("" (prop)
(("1" (expand member)
(("1" (skosimp*)
(("1" (inst 1 "i!1 + 1")
(("1" (lemma iterate_add)
(("1" (inst -1 "R" "1" "i!1")
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(expand o)
(("1"
(assert)
(("1"
(inst 1 y)
(("1"
(assert)
(("1"
(hide -2)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst 1 "0+i!1")
(("2" (lemma iterate_add)
(("2" (inst -1 "R" "0" "i!1")
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand member)
(("2" (replace -1) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((RTC const-decl "reflexive_transitive" relations_closure nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(iterate_add formula-decl nil relation_iterate "orders/")
(T formal-type-decl nil confluence_commute nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(O const-decl "bool" relation_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(member const-decl "bool" sets nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(union const-decl "set" sets nil)
(RC const-decl "reflexive" relations_closure nil))
shostak))
(RTC_converse_RTC_R 0
(RTC_converse_RTC_R-1 nil 3417861331
("" (skolem 1 ("R" "_" "_"))
((""
(case "FORALL (i: nat, x,y : T) : (iterate(R,i)(x,y) <=> iterate(converse(R), i)(y, x))")
(("1" (skeep)
(("1" (inst -1 "_" x y)
(("1" (expand RTC)
(("1" (expand IUnion)
(("1" (prop)
(("1" (skosimp)
(("1" (inst 1 i!1)
(("1" (inst -2 i!1) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp)
(("2" (inst -2 i!1)
(("2" (inst 1 i!1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct i)
(("1" (skeep)
(("1" (expand iterate) (("1" (grind) nil nil)) nil)) nil)
("2" (skeep)
(("2" (skeep)
(("2" (lemma iterate_add)
(("2" (inst -1 R j 1)
(("2" (replace -1 1)
(("2" (expand o)
(("2" (prop)
(("1" (skosimp -1)
(("1" (inst -4 "x" "y!1")
(("1" (hide -3)
(("1"
(prop)
(("1"
(lemma iterate_add)
(("1"
(inst -1 "converse(R)" "1" "j")
(("1"
(decompose-equality -1)
(("1"
(inst -1 "(y,x)")
(("1"
(expand o -1)
(("1"
(replace -1 1)
(("1"
(hide -1)
(("1"
(inst 1 y!1)
(("1"
(assert)
(("1"
(hide -1 -2 -3)
(("1"
(expand iterate)
(("1"
(expand o -1)
(("1"
(skosimp)
(("1"
(expand
iterate
-1)
(("1"
(replace
-1
-2
rl)
(("1"
(hide
-1)
(("1"
(expand
o)
(("1"
(inst
1
y)
(("1"
(assert)
(("1"
(expand
iterate)
(("1"
(expand
converse)
(("1"
(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)
("2" (hide -2)
(("2" (lemma iterate_add)
(("2" (inst -1 "converse(R)" 1 j)
(("2"
(decompose-equality)
(("2"
(inst -1 "(y,x)")
(("2"
(expand o -1)
(("2"
(replace -1 -2)
(("2"
(hide -1)
(("2"
(skosimp -1)
(("2"
(inst -3 x y!1)
(("2"
(assert)
(("2"
(inst 1 y!1)
(("2"
(assert)
(("2"
(hide -2 -3)
(("2"
(expand iterate)
(("2"
(expand o -1)
(("2"
(skosimp)
(("2"
(expand
iterate
-1)
(("2"
(replace
-1
-2
rl)
(("2"
(hide
-1)
(("2"
(expand
iterate)
(("2"
(expand
o)
(("2"
(inst
1
y!1)
(("2"
(expand
converse)
(("2"
(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)
((converse const-decl "pred[[T2, T1]]" relation_defs nil)
(PRED type-eq-decl nil defined_types nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(pred type-eq-decl nil defined_types nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil confluence_commute 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)
(IUnion const-decl "set[T]" indexed_sets nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(nat_induction formula-decl nil naturalnumbers nil)
(O const-decl "bool" relation_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(iterate_add formula-decl nil relation_iterate "orders/"))
shostak))
(semi_comm_implies_comm 0
(semi_comm_implies_comm-1 nil 3386429566
("" (skeep)
(("" (expand commute?)
(("" (skeep)
(("" (expand "RTC" -2)
(("" (expand "IUnion" -2)
(("" (skolem * "i")
((""
(case "FORALL (j: nat, a, b, c: T) : (iterate(R1,j)(a,b) AND RTC(R2)(a,c)) => EXISTS (d: T): RTC(R2)(b, d) & RTC(R1)(c, d)")
(("1" (inst -1 "i" "x" "y" "z")
(("1" (assert) nil nil)) nil)
("2" (induct j)
(("1" (hide 2 -2 -3)
(("1" (assert)
(("1" (skeep)
(("1" (expand iterate)
(("1" (replace -1 -2)
(("1" (inst 1 "c")
(("1"
(assert)
(("1"
(expand "RTC" 1)
(("1"
(expand "IUnion")
(("1"
(inst 1 "0")
(("1"
(assert)
(("1"
(expand iterate)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 -3 2)
(("2" (skeep)
(("2" (skeep)
(("2" (rewrite "iterate_add_one")
(("2" (expand o)
(("2" (skolem * "a1")
(("2"
(expand semi_commute?)
(("2"
(inst -4 "a" "a1" "c")
(("2"
(flatten)
(("2"
(assert)
(("2"
(skolem * "c1")
(("2"
(flatten)
(("2"
(inst -1 "a1" "b" "c1")
(("2"
(assert)
(("2"
(skolem * "d1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(hide
-3
-4
-5
-6)
(("2"
(inst 1 "d1")
(("2"
(assert)
(("2"
(hide -1)
(("2"
(expand
"RTC")
(("2"
(expand
"IUnion")
(("2"
(skolem
*
"n")
(("2"
(skolem
*
"m")
(("2"
(inst
1
"m + n")
(("2"
(lemma
iterate_add)
(("2"
(inst
-1
"R1"
"m"
"n")
(("2"
(assert)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((commute? const-decl "bool" ars_terminology nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(nat_induction formula-decl nil naturalnumbers nil)
(iterate_add_one formula-decl nil relation_iterate "orders/")
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(iterate_add formula-decl nil relation_iterate "orders/")
(semi_commute? const-decl "bool" confluence_commute nil)
(O const-decl "bool" relation_props 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)
(T formal-type-decl nil confluence_commute nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(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)
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(sub_comm_rtc_implies_conf 0
(sub_comm_rtc_implies_conf-1 nil 3390042462
("" (skeep)
(("" (expand confluent?)
(("" (expand sub_commutative?)
(("" (rewrite "RC_RTC_is_RTC")
(("" (expand joinable?) (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((confluent? const-decl "bool" ars_terminology nil)
(RC_RTC_is_RTC formula-decl nil confluence_commute nil)
(T formal-type-decl nil confluence_commute nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(joinable? const-decl "bool" ars_terminology nil)
(sub_commutative? const-decl "bool" confluence_commute nil))
shostak))
(conf_local_request_implies_request 0
(conf_local_request_implies_request-2 ": y" 3390555429
("" (skeep)
(("" (expand request?)
(("" (expand "RTC" 1 2)
(("" (expand "IUnion")
(("" (skeep)
((""
(case "FORALL (n : nat, x,y,z : T) : confluent?(R2) & RTC(R1)(x, y) & iterate(R2, n)(x, z) =>
EXISTS r, s: RTC(R2)(y, r) & RTC(R1)(z, s) & RTC(R2)(s, r)")
(("1" (assert)
(("1" (skosimp* -5)
(("1" (inst -2 "i!1" "x" "y" "z")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct n)
(("1" (skosimp*)
(("1" (hide -4 -6)
(("1" (hide -5)
(("1" (expand iterate)
(("1" (replace -3)
(("1" (inst 1 "y!1" "y!1")
(("1"
(assert)
(("1"
(expand "RTC")
(("1"
(hide -4)
(("1"
(expand "IUnion")
(("1"
(hide-all-but 1)
(("1"
(prop)
(("1"
(inst 1 0)
(("1" (grind) nil nil))
nil)
("2"
(inst 1 0)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skosimp*)
(("2" (hide -5 -6 -7 -8)
(("2" (assert)
(("2" (expand iterate -4)
(("2" (expand o -4)
(("2"
(skosimp* -4)
(("2"
(inst -1 "x!1" "y!1" "y!2")
(("2"
(assert)
(("2"
(skosimp* -1)
(("2"
(reveal -3)
(("2"
(inst -1 "y!2" "s!1" "z!1")
(("2"
(assert)
(("2"
(skosimp* -1)
(("2"
(expand confluent?)
(("2"
(inst
-7
"s!1"
"r!1"
"r!2")
(("2"
(assert)
(("2"
(expand
joinable?)
(("2"
(skosimp* -7)
(("2"
(inst
1
"z!2"
"s!2")
(("2"
(hide-all-but
(-4
-7
-2
-8
-3
1))
(("2"
(assert)
(("2"
(hide
-1)
(("2"
(lemma
"RTC_o_RTC_is_RTC")
(("2"
(copy
-1)
(("2"
(inst
-1
"R2"
"y!1"
"r!1"
"z!2")
(("2"
(assert)
(("2"
(inst
-2
"R2"
"s!2"
"r!2"
"z!2")
(("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)
((request? const-decl "bool" confluence_commute nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(iterate def-decl "pred[[T, T]]" relation_iterate "orders/")
(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)
(confluent? const-decl "bool" ars_terminology nil)
(PRED type-eq-decl nil defined_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil confluence_commute 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(O const-decl "bool" relation_props nil)
(joinable? const-decl "bool" ars_terminology nil)
(RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
(RTC const-decl "reflexive_transitive" relations_closure nil))
shostak)
(conf_local_request_implies_request-1 nil 3390044720
("" (skeep)
(("" (expand request?)
(("" (expand "RTC" 1 2)
(("" (expand "IUnion")
(("" (skeep)
((""
(case "FORALL (n : nat) : confluent?(R2) & RTC(R1)(x, y) & iterate(R2, n)(x, z) =>
EXISTS r, s: RTC(R2)(y, r) & RTC(R1)(z, s) & RTC(R2)(s, r)")
(("1" (assert)
(("1" (inst -3 "x" "y" "z")
(("1" (assert)
(("1" (skosimp* -5)
(("1" (inst -2 "i!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(comp_rtc_req_conf_impl_diamond 0
(comp_rtc_req_conf_impl_diamond-2 "" 3400255840
("" (assert)
(("" (skeep)
(("" (expand diamond_property?)
(("" (skeep)
(("" (expand o -4)
(("" (expand o -5)
(("" (skosimp*)
(("" (inst -3 "x" "y!1" "y!2")
(("" (assert)
(("" (skosimp*)
(("" (expand o -3)
(("" (expand o -4)
(("" (skosimp*)
(("" (hide -7 -9)
((""
(copy -1)
((""
(expand request? -1)
((""
(inst -1 "y!1" "y!3" "y")
((""
(assert)
((""
(skosimp*)
((""
(hide -6 -10)
((""
(expand request?)
((""
(inst -4 "y!2" "y!4" "z")
((""
(assert)
((""
(skosimp*)
((""
(hide -9 -11)
((""
(copy -7)
((""
(copy -1)
((""
(expand
confluent?
-1)
((""
(inst
-1
"y!4"
"r!1"
"r!3")
((""
(assert)
((""
(expand
joinable?)
((""
(skosimp*)
((""
(hide
-7
-12)
((""
(expand
confluent?
-3)
((""
(inst
-3
"y!3"
"r!2"
"r!1")
((""
(assert)
((""
(expand
joinable?)
((""
(skosimp*)
((""
(hide
-5
-11)
((""
(expand
confluent?)
((""
(inst
-9
"r!1"
"z!2"
"z!1")
((""
(assert)
((""
(expand
joinable?)
((""
(skosimp*)
((""
(hide
-1
-4)
((""
(inst
1
"z!3")
((""
(expand
o)
((""
(split)
(("1"
(inst
1
"s!1")
(("1"
(lemma
"RTC_o_RTC_is_RTC")
(("1"
(copy
-1)
(("1"
(inst
-1
"R2"
"s!1"
"r!2"
"z!2")
(("1"
(inst
-2
"R2"
"s!1"
"z!2"
"z!3")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
1
"s!2")
(("2"
(lemma
"RTC_o_RTC_is_RTC")
(("2"
(copy
-1)
(("2"
(inst
-1
"R2"
"s!2"
"r!3"
"z!1")
(("2"
(inst
-2
"R2"
"s!2"
"z!1"
"z!3")
(("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))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil confluence_commute nil)
(request? const-decl "bool" confluence_commute nil)
(confluent? const-decl "bool" ars_terminology nil)
(RTC_o_RTC_is_RTC formula-decl nil confluence_commute nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(joinable? const-decl "bool" ars_terminology nil)
(O const-decl "bool" relation_props nil)
(diamond_property? const-decl "bool" ars_terminology nil))
shostak)
(comp_rtc_req_conf_impl_diamond-1 nil 3400001153
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (expand diamond_property?)
(("" (skeep)
(("" (expand o -4)
(("" (expand o -5)
(("" (skosimp*)
(("" (inst -3 "x" "y!1" "y!2")
(("" (assert)
(("" (skosimp*)
(("" (expand o -3)
(("" (expand o -4)
(("" (skosimp*)
((""
(copy -1)
((""
(expand request? -1)
((""
(inst -1 "y!1" "y!3" "y")
((""
(assert)
((""
(skosimp*)
((""
(expand request?)
((""
(inst -4 "y!2" "y!4" "z")
((""
(assert)
((""
(skosimp*)
((""
(copy -7)
((""
(expand confluent?)
((""
(inst
-1
"y!4"
"r!1"
"r!3")
((""
(assert)
((""
(postpone)
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 shostak))
(union_req_conf_is_confluent 0
(union_req_conf_is_confluent-1 nil 3401714997
("" (skeep)
(("" (assert)
(("" (lemma "comp_rtc_req_conf_impl_diamond")
(("" (inst -1 "R1" "R2")
(("" (assert)
(("" (prop)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.715 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.
|
