|
(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.40Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
