|
(modulo_equivalence
(van_oostrom94 0
(van_oostrom94-1 nil 3383390315
("" (skeep)
(("" (expand* "diamond_property?" "confluent_m?")
(("" (skeep)
(("" (copy -1)
(("" (inst -1 "x" "y" "z")
(("" (typepred "Eq")
(("" (expand "equivalence?")
(("" (flatten)
(("" (prop)
(("1" (skolem * "u1")
(("1" (flatten)
(("1" (expand "o" (-1 -2))
(("1" (skolem * "u2")
(("1" (skolem * "u")
(("1"
(flatten)
(("1"
(copy -7)
(("1"
(expand "transitive?" -1)
(("1"
(copy -7)
(("1"
(expand "symmetric?" -1)
(("1"
(inst -1 "u" "u1")
(("1"
(inst -2 "u2" "u1" "u")
(("1"
(assert)
(("1"
(hide (-1 -4 -6))
(("1"
(inst -7 "y" "u" "w")
(("1"
(prop)
(("1"
(skolem * "v2")
(("1"
(flatten)
(("1"
(expand "o")
(("1"
(skolem
*
"v1")
(("1"
(skolem
*
"v")
(("1"
(flatten)
(("1"
(copy
-10)
(("1"
(expand
"transitive?"
-1)
(("1"
(copy
-10)
(("1"
(expand
"symmetric?"
-1)
(("1"
(inst
-1
"v"
"v2")
(("1"
(inst
-2
"v1"
"v2"
"v")
(("1"
(assert)
(("1"
(typepred
"RTC(R)")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(expand
"transitive?"
-2)
(("1"
(inst
-2
"z"
"u"
"v1")
(("1"
(assert)
(("1"
(hide-all-but
(-2
-4
-7
1))
(("1"
(expand
"joinable_m?")
(("1"
(inst
1
"v1"
"v")
(("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)
("2"
(expand "o")
(("2"
(inst 1 "u2")
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(expand "o")
(("3"
(inst 1 "w")
(("3"
(expand
"reflexive?")
(("3"
(inst
-4
"w")
(("3"
(assert)
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 (-6 1))
(("2" (expand "o" 1)
(("2" (inst 1 "x")
(("2" (typepred "RTC(R)")
(("2" (expand "reflexive_transitive?")
(("2"
(flatten)
(("2"
(expand "reflexive?")
(("2"
(inst -1 "x")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but (-1 -5 1))
(("3" (expand "o" 1)
(("3" (inst 1 "z")
(("3" (expand "reflexive?")
(("3" (inst -1 "z")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((confluent_m? const-decl "bool" modulo_equivalence nil)
(diamond_property? const-decl "bool" ars_terminology nil)
(equivalence type-eq-decl nil relations_closure nil)
(equivalence? const-decl "bool" relations 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)
(O const-decl "bool" relation_props nil)
(reflexive? const-decl "bool" relations nil)
(joinable_m? const-decl "bool" modulo_equivalence 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)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(T formal-type-decl nil modulo_equivalence nil))
shostak))
(newman_lemma_general 0
(newman_lemma_general-1 nil 3383388017
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (lemma "van_oostrom94")
(("1" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "noetherian_induction")
(("1" (inst?)
(("1" (expand "diamond_property?")
(("1" (skeep)
(("1"
(inst -1
"(LAMBDA (a: T): (FORALL (b, c: T):(RTC(R) o Eq)(a, b) AND (RTC(R) o Eq)(a, c) IMPLIES joinable_m?(R, Eq)(c, b)))")
(("1" (split)
(("1" (inst -1 "x" "y" "z")
(("1"
(assert)
(("1"
(expand "joinable_m?")
(("1"
(skolem -1 ("u" "v"))
(("1"
(flatten)
(("1"
(inst 1 "u")
(("1"
(split)
(("1"
(expand "o" 1)
(("1"
(inst 1 "v")
(("1"
(typepred "Eq")
(("1"
(expand*
"equivalence?"
"symmetric?")
(("1"
(flatten)
(("1"
(inst -2 "u" "v")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "o" 1)
(("2"
(inst 1 "u")
(("2"
(typepred "Eq")
(("2"
(expand*
"equivalence?"
"reflexive?")
(("2"
(flatten)
(("2"
(inst -1 "u")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(skolem 1 "a")
(("2"
(flatten)
(("2"
(skeep)
(("2"
(hide (-4 -5))
(("2"
(expand "o" (-2 -3))
(("2"
(skolem * "b2")
(("2"
(skolem * "c2")
(("2"
(flatten)
(("2"
(expand "RTC" (-2 -4))
(("2"
(expand
"IUnion"
(-2 -4))
(("2"
(skolem * "i")
(("2"
(skolem * "j")
(("2"
(case-replace
"i = 0"
:hide?
t)
(("1"
(case-replace
"j = 0"
:hide?
t)
(("1"
(expand
"iterate")
(("1"
(replace
-2
-3
rl)
(("1"
(replace
-4
-5
rl)
(("1"
(hide-all-but
(-3
-5
1))
(("1"
(expand
"joinable_m?")
(("1"
(inst
1
"c"
"b")
(("1"
(typepred
"RTC(R)")
(("1"
(typepred
"Eq")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(hide
-3)
(("1"
(expand*
"equivalence?"
"transitive?"
"reflexive?"
"symmetric?")
(("1"
(flatten)
(("1"
(inst
-2
"a"
"c")
(("1"
(inst
-3
"c"
"a"
"b")
(("1"
(copy
-4)
(("1"
(inst
-1
"c")
(("1"
(inst
-5
"b")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"iterate"
-2)
(("2"
(replace
-2
-3
rl)
(("2"
(hide
-2)
(("2"
(lemma
iterate_add_one)
(("2"
(inst?
-1
("R"
"R"
"n"
"j - 1"))
(("1"
(assert)
(("1"
(decompose-equality)
(("1"
(inst
-1
"(a, c2)")
(("1"
(replaces
-1)
(("1"
(expand
"o"
-3)
(("1"
(skolem
-3
"c1")
(("1"
(flatten)
(("1"
(lemma
"iterate_RTC")
(("1"
(inst
-1
"R"
"j - 1")
(("1"
(expand*
"subset?"
"member")
(("1"
(inst
-1
"(c1, c2)")
(("1"
(expand
"locally_coherent?")
(("1"
(typepred
"Eq")
(("1"
(expand
"equivalence?")
(("1"
(flatten)
(("1"
(inst
-12
"a"
"c1"
"b")
(("1"
(assert)
(("1"
(hide
(-8
-11))
(("1"
(expand
"joinable_m?")
(("1"
(skolem
-10
("d1"
"d2"))
(("1"
(flatten)
(("1"
(inst
-5
"c1")
(("1"
(lemma
"R_subset_TC")
(("1"
(inst?)
(("1"
(expand*
"subset?"
"member")
(("1"
(inst
-1
"(a, c1)")
(("1"
(assert)
(("1"
(inst
-6
"d2"
"c")
(("1"
(prop)
(("1"
(skolem
*
("r1"
"r2"))
(("1"
(flatten)
(("1"
(typepred
"RTC(R)")
(("1"
(expand
"reflexive_transitive?")
(("1"
(flatten)
(("1"
(expand
"transitive?"
-2)
(("1"
(inst
-2
"b"
"d2"
"r2")
(("1"
(inst
2
"r1"
"r2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"o"
1)
(("2"
(inst
1
"d1")
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(expand
"o"
1)
(("3"
(inst
1
"c2")
(("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))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
iterate_add_one)
(("2"
(inst?
-1
("R"
"R"
"n"
"i - 1"))
(("1"
(decompose-equality)
(("1"
(inst
-1
"(a, b2)")
(("1"
(replaces
-1)
(("1"
(expand
"o"
-2)
(("1"
(skolem
-2
"b3")
(("1"
(flatten)
(("1"
(lemma
"iterate_RTC")
(("1"
(inst
-1
"R"
"i - 1")
(("1"
(expand*
"subset?"
"member")
(("1"
(inst
-1
"(b3, b2)")
(("1"
(assert)
(("1"
(hide
-4)
(("1"
(case-replace
"j = 0"
:hide?
t)
(("1"
(expand
"iterate")
(("1"
(replace
-5
-6
rl)
(("1"
(expand
"locally_coherent?")
(("1"
(typepred
"Eq")
(("1"
(expand
"equivalence?")
(("1"
(flatten)
(("1"
(inst
-12
"a"
"b3"
"c")
(("1"
(assert)
(("1"
(hide
(-8
-11))
(("1"
(expand
"joinable_m?")
(("1"
(skolem
-10
("d1"
"d2"))
(("1"
(flatten)
(("1"
(inst
-5
"b3")
(("1"
(lemma
"R_subset_TC")
(("1"
(inst?)
(("1"
(expand*
"subset?"
"member")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 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.
|
