We consider the following Problem:
Strict Trs:
{ nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, p(s(x)) -> x
, id_inc(x) -> x
, id_inc(x) -> s(x)
, random(x) -> rand(x, 0())
, rand(x, y) -> if(nonZero(x), x, y)
, if(false(), x, y) -> y
, if(true(), x, y) -> rand(p(x), id_inc(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, p(s(x)) -> x
, id_inc(x) -> x
, id_inc(x) -> s(x)
, random(x) -> rand(x, 0())
, rand(x, y) -> if(nonZero(x), x, y)
, if(false(), x, y) -> y
, if(true(), x, y) -> rand(p(x), id_inc(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [1]
[0 0] [1]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
p(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [1 0] x1 + [1]
[0 0] [0]
random(x1) = [1 1] x1 + [0]
[0 0] [0]
rand(x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, random(x) -> rand(x, 0())
, rand(x, y) -> if(nonZero(x), x, y)
, if(false(), x, y) -> y
, if(true(), x, y) -> rand(p(x), id_inc(y))}
Weak Trs:
{ nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {random(x) -> rand(x, 0())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [0]
[0 0] [1]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
p(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [1 0] x1 + [0]
[0 0] [0]
random(x1) = [1 1] x1 + [2]
[0 0] [2]
rand(x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, rand(x, y) -> if(nonZero(x), x, y)
, if(false(), x, y) -> y
, if(true(), x, y) -> rand(p(x), id_inc(y))}
Weak Trs:
{ random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if(false(), x, y) -> y}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [0]
[0 0] [1]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
p(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [1 0] x1 + [1]
[0 0] [0]
random(x1) = [1 1] x1 + [0]
[0 0] [2]
rand(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, rand(x, y) -> if(nonZero(x), x, y)
, if(true(), x, y) -> rand(p(x), id_inc(y))}
Weak Trs:
{ if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if(true(), x, y) -> rand(p(x), id_inc(y))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
p(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [1 0] x1 + [0]
[0 0] [0]
random(x1) = [1 1] x1 + [0]
[0 0] [2]
rand(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [3]
[0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, rand(x, y) -> if(nonZero(x), x, y)}
Weak Trs:
{ if(true(), x, y) -> rand(p(x), id_inc(y))
, if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {id_inc(x) -> x}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [0]
[0 0] [2]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[2]
p(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [1 0] x1 + [2]
[0 1] [0]
random(x1) = [1 1] x1 + [0]
[0 0] [2]
rand(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 1] x1 + [1 1] x2 + [1 0] x3 + [2]
[0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, rand(x, y) -> if(nonZero(x), x, y)}
Weak Trs:
{ id_inc(x) -> x
, if(true(), x, y) -> rand(p(x), id_inc(y))
, if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {p(s(x)) -> x}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(nonZero) = {}, Uargs(s) = {}, Uargs(p) = {},
Uargs(id_inc) = {}, Uargs(random) = {}, Uargs(rand) = {1, 2},
Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
nonZero(x1) = [0 0] x1 + [0]
[0 1] [3]
0() = [0]
[0]
false() = [0]
[0]
s(x1) = [1 0] x1 + [1]
[0 1] [1]
true() = [0]
[0]
p(x1) = [1 0] x1 + [0]
[0 1] [0]
id_inc(x1) = [1 0] x1 + [1]
[0 1] [2]
random(x1) = [1 0] x1 + [0]
[0 0] [2]
rand(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 1] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {rand(x, y) -> if(nonZero(x), x, y)}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, if(true(), x, y) -> rand(p(x), id_inc(y))
, if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {rand(x, y) -> if(nonZero(x), x, y)}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, if(true(), x, y) -> rand(p(x), id_inc(y))
, if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs: {rand^#(x, y) -> if^#(nonZero(x), x, y)}
Weak DPs:
{ p^#(s(x)) -> c_2()
, id_inc^#(x) -> c_3()
, if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, if^#(false(), x, y) -> c_5()
, random^#(x) -> rand^#(x, 0())
, nonZero^#(0()) -> c_7()
, nonZero^#(s(x)) -> c_8()
, p^#(0()) -> c_9()
, id_inc^#(x) -> c_10()}
We consider the following Problem:
Strict DPs: {rand^#(x, y) -> if^#(nonZero(x), x, y)}
Strict Trs: {rand(x, y) -> if(nonZero(x), x, y)}
Weak DPs:
{ p^#(s(x)) -> c_2()
, id_inc^#(x) -> c_3()
, if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, if^#(false(), x, y) -> c_5()
, random^#(x) -> rand^#(x, 0())
, nonZero^#(0()) -> c_7()
, nonZero^#(s(x)) -> c_8()
, p^#(0()) -> c_9()
, id_inc^#(x) -> c_10()}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, if(true(), x, y) -> rand(p(x), id_inc(y))
, if(false(), x, y) -> y
, random(x) -> rand(x, 0())
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
We consider the following Problem:
Strict DPs: {rand^#(x, y) -> if^#(nonZero(x), x, y)}
Weak DPs:
{ p^#(s(x)) -> c_2()
, id_inc^#(x) -> c_3()
, if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, if^#(false(), x, y) -> c_5()
, random^#(x) -> rand^#(x, 0())
, nonZero^#(0()) -> c_7()
, nonZero^#(s(x)) -> c_8()
, p^#(0()) -> c_9()
, id_inc^#(x) -> c_10()}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {rand^#(x, y) -> if^#(nonZero(x), x, y)}
Weak DPs:
{ p^#(s(x)) -> c_2()
, id_inc^#(x) -> c_3()
, if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, if^#(false(), x, y) -> c_5()
, random^#(x) -> rand^#(x, 0())
, nonZero^#(0()) -> c_7()
, nonZero^#(s(x)) -> c_8()
, p^#(0()) -> c_9()
, id_inc^#(x) -> c_10()}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->7:{2} [ YES(O(1),O(1)) ]
->6:{3} [ YES(O(1),O(1)) ]
->5:{6} [ subsumed ]
|
`->8:{1,4} [ YES(O(1),O(1)) ]
|
`->9:{5} [ YES(O(1),O(1)) ]
->4:{7} [ YES(O(1),O(1)) ]
->3:{8} [ YES(O(1),O(1)) ]
->2:{9} [ YES(O(1),O(1)) ]
->1:{10} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{1: rand^#(x, y) -> if^#(nonZero(x), x, y)}
WeakDPs DPs:
{ 2: p^#(s(x)) -> c_2()
, 3: id_inc^#(x) -> c_3()
, 4: if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, 5: if^#(false(), x, y) -> c_5()
, 6: random^#(x) -> rand^#(x, 0())
, 7: nonZero^#(0()) -> c_7()
, 8: nonZero^#(s(x)) -> c_8()
, 9: p^#(0()) -> c_9()
, 10: id_inc^#(x) -> c_10()}
* Path 7:{2}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 6:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 5:{6}: subsumed
--------------------
This path is subsumed by the proof of paths 5:{6}->8:{1,4}.
* Path 5:{6}->8:{1,4}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict DPs: {rand^#(x, y) -> if^#(nonZero(x), x, y)}
Weak DPs: {random^#(x) -> rand^#(x, 0())}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: rand^#(x, y) -> if^#(nonZero(x), x, y)
2: random^#(x) -> rand^#(x, 0())
-->_1 rand^#(x, y) -> if^#(nonZero(x), x, y) :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: rand^#(x, y) -> if^#(nonZero(x), x, y)}
WeakDPs DPs:
{2: random^#(x) -> rand^#(x, 0())}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: random^#(x) -> rand^#(x, 0())
, 1: rand^#(x, y) -> if^#(nonZero(x), x, y)}
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 5:{6}->8:{1,4}->9:{5}: YES(O(1),O(1))
------------------------------------------
We consider the following Problem:
Weak DPs:
{ random^#(x) -> rand^#(x, 0())
, if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, rand^#(x, y) -> if^#(nonZero(x), x, y)}
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: random^#(x) -> rand^#(x, 0())
-->_1 rand^#(x, y) -> if^#(nonZero(x), x, y) :3
2: if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
-->_1 rand^#(x, y) -> if^#(nonZero(x), x, y) :3
3: rand^#(x, y) -> if^#(nonZero(x), x, y)
-->_1 if^#(true(), x, y) -> rand^#(p(x), id_inc(y)) :2
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{3,2} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: random^#(x) -> rand^#(x, 0())
, 2: if^#(true(), x, y) -> rand^#(p(x), id_inc(y))
, 3: rand^#(x, y) -> if^#(nonZero(x), x, y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: random^#(x) -> rand^#(x, 0())
, 3: rand^#(x, y) -> if^#(nonZero(x), x, y)
, 2: if^#(true(), x, y) -> rand^#(p(x), id_inc(y))}
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 4:{7}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 3:{8}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{9}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 1:{10}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ p(s(x)) -> x
, id_inc(x) -> x
, nonZero(0()) -> false()
, nonZero(s(x)) -> true()
, p(0()) -> 0()
, id_inc(x) -> s(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))