We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if2(true(), b2, b3, x, y) -> 0()
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if3(true(), b3, x, y) -> 0()
, if3(false(), b3, x, y) -> if4(b3, x, y)
, if4(true(), x, y) -> s(0())
, if4(false(), x, y) -> average(s(x), p(p(y)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if2(true(), b2, b3, x, y) -> 0()
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if3(true(), b3, x, y) -> 0()
, if3(false(), b3, x, y) -> if4(b3, x, y)
, if4(true(), x, y) -> s(0())
, if4(false(), x, y) -> average(s(x), p(p(y)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
average(x1, x2) = [1 1] x1 + [1 2] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 1] x5 + [1 1] x6 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [0 0] x1 + [1 0] 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
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, if4(false(), x, y) -> average(s(x), p(p(y)))}
Weak Trs:
{ p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if3(false(), b3, x, y) -> if4(b3, x, y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
average(x1, x2) = [1 1] x1 + [1 1] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 1] x5 + [1 1] x6 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [0 0] x1 + [1 0] 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
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if4(false(), x, y) -> average(s(x), p(p(y)))}
Weak Trs:
{ if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
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(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
average(x1, x2) = [1 1] x1 + [1 2] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 1] x5 + [1 1] x6 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [0]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [0 0] x1 + [1 0] 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
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if4(false(), x, y) -> average(s(x), p(p(y)))}
Weak Trs:
{ if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
true() = [1]
[0]
false() = [0]
[0]
average(x1, x2) = [1 1] x1 + [1 2] x2 + [1]
[0 0] [0 0] [1]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 1] x5 + [1 1] x6 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [2]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [0 0] x1 + [1 0] 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
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))}
Weak Trs:
{ if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if4(false(), x, y) -> average(s(x), p(p(y)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [2]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
true() = [1]
[0]
false() = [1]
[1]
average(x1, x2) = [1 1] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 3] x4 + [1 1] x5 + [1 1] x6 + [0]
[0 0] [0 1] [0 1] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [1 0] x1 + [1 0] x2 + [1 3] x3 + [1 0] x4 + [1 0] x5 + [1]
[0 0] [0 1] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [1 0] x1 + [1 3] x2 + [1 0] x3 + [1 0] x4 + [2]
[0 1] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [1 3] x1 + [1 0] x2 + [1 0] x3 + [3]
[0 0] [0 0] [0 0] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))}
Weak Trs:
{ if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
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(), b1, b2, b3, x, y) -> average(p(x), s(y))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [0]
[0 0] [0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
average(x1, x2) = [1 1] x1 + [1 1] x2 + [0]
[0 0] [0 0] [0]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 1] x5 + [1 1] x6 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [1 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ p(s(x)) -> x
, le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)}
Weak Trs:
{ if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
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(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [1]
[0 1] [0]
s(x1) = [1 0] x1 + [0]
[0 1] [0]
0() = [0]
[0]
le(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [0]
true() = [0]
[0]
false() = [1]
[0]
average(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 0] x5 + [1 0] x6 + [0]
[0 0] [0 0] [0 0] [0 0] [0 0] [0 0] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 0] x5 + [0]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ le(s(x), s(y)) -> le(x, y)
, average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)}
Weak Trs:
{ p(s(x)) -> x
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {le(s(x), s(y)) -> le(x, y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(p) = {1}, Uargs(s) = {}, Uargs(le) = {},
Uargs(average) = {1, 2}, Uargs(if) = {1, 2, 3, 4}, Uargs(if2) = {},
Uargs(if3) = {}, Uargs(if4) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
p(x1) = [1 0] x1 + [0]
[0 1] [1]
s(x1) = [1 0] x1 + [2]
[0 1] [0]
0() = [1]
[0]
le(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [0]
true() = [1]
[0]
false() = [2]
[0]
average(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
if(x1, x2, x3, x4, x5, x6) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 0] x5 + [1 0] x6 + [0]
[0 0] [0 0] [0 0] [0 0] [0 1] [0 1] [1]
if2(x1, x2, x3, x4, x5) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1 0] x5 + [1]
[0 0] [0 0] [0 0] [0 0] [0 0] [1]
if3(x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [1]
[0 0] [0 0] [0 0] [0 0] [1]
if4(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [3]
[0 0] [0 0] [0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs:
{average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak DPs:
{ le^#(s(x), s(y)) -> le^#(x, y)
, p^#(s(x)) -> c_3()
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, p^#(0()) -> c_9()
, le^#(0(), y) -> c_10()
, le^#(s(x), 0()) -> c_11()
, if2^#(true(), b2, b3, x, y) -> c_12()
, if3^#(true(), b3, x, y) -> c_13()
, if4^#(true(), x, y) -> c_14()}
We consider the following Problem:
Strict DPs:
{average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Strict Trs:
{average(x, y) ->
if(le(x, 0()), le(y, 0()), le(y, s(0())), le(y, s(s(0()))), x, y)}
Weak DPs:
{ le^#(s(x), s(y)) -> le^#(x, y)
, p^#(s(x)) -> c_3()
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, p^#(0()) -> c_9()
, le^#(0(), y) -> c_10()
, le^#(s(x), 0()) -> c_11()
, if2^#(true(), b2, b3, x, y) -> c_12()
, if3^#(true(), b3, x, y) -> c_13()
, if4^#(true(), x, y) -> c_14()}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, if(false(), b1, b2, b3, x, y) -> average(p(x), s(y))
, if4(false(), x, y) -> average(s(x), p(p(y)))
, if2(false(), b2, b3, x, y) -> if3(b2, b3, x, y)
, if(true(), b1, b2, b3, x, y) -> if2(b1, b2, b3, x, y)
, if3(false(), b3, x, y) -> if4(b3, x, y)
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, if2(true(), b2, b3, x, y) -> 0()
, if3(true(), b3, x, y) -> 0()
, if4(true(), x, y) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
We consider the following Problem:
Strict DPs:
{average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak DPs:
{ le^#(s(x), s(y)) -> le^#(x, y)
, p^#(s(x)) -> c_3()
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, p^#(0()) -> c_9()
, le^#(0(), y) -> c_10()
, le^#(s(x), 0()) -> c_11()
, if2^#(true(), b2, b3, x, y) -> c_12()
, if3^#(true(), b3, x, y) -> c_13()
, if4^#(true(), x, y) -> c_14()}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs:
{average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak DPs:
{ le^#(s(x), s(y)) -> le^#(x, y)
, p^#(s(x)) -> c_3()
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, p^#(0()) -> c_9()
, le^#(0(), y) -> c_10()
, le^#(s(x), 0()) -> c_11()
, if2^#(true(), b2, b3, x, y) -> c_12()
, if3^#(true(), b3, x, y) -> c_13()
, if4^#(true(), x, y) -> c_14()}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->6:{1,5,8,6,7,4} [ YES(O(1),O(1)) ]
|
|->9:{12} [ YES(O(1),O(1)) ]
|
|->7:{13} [ YES(O(1),O(1)) ]
|
`->8:{14} [ YES(O(1),O(1)) ]
->3:{2} [ subsumed ]
|
|->4:{10} [ YES(O(1),O(1)) ]
|
`->5:{11} [ YES(O(1),O(1)) ]
->2:{3} [ YES(O(1),O(1)) ]
->1:{9} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{1: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
WeakDPs DPs:
{ 2: le^#(s(x), s(y)) -> le^#(x, y)
, 3: p^#(s(x)) -> c_3()
, 4: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, 5: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 6: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 7: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 8: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 9: p^#(0()) -> c_9()
, 10: le^#(0(), y) -> c_10()
, 11: le^#(s(x), 0()) -> c_11()
, 12: if2^#(true(), b2, b3, x, y) -> c_12()
, 13: if3^#(true(), b3, x, y) -> c_13()
, 14: if4^#(true(), x, y) -> c_14()}
* Path 6:{1,5,8,6,7,4}: YES(O(1),O(1))
------------------------------------
We consider the following Problem:
Strict DPs:
{average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{1,5,8,6,7,4}->9:{12}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Weak DPs:
{ if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
-->_1 if4^#(false(), x, y) -> average^#(s(x), p(p(y))) :1
3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
-->_1 if3^#(false(), b3, x, y) -> if4^#(b3, x, y) :2
4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
-->_1 if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y) :3
5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
-->_1 if^#(false(), b1, b2, b3, x, y) ->
average^#(p(x), s(y)) :5
-->_1 if^#(true(), b1, b2, b3, x, y) ->
if2^#(b1, b2, b3, x, y) :4
together with the congruence-graph
->1:{1,2,3,4,6,5} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{1,5,8,6,7,4}->7:{13}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Weak DPs:
{ if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
-->_1 if4^#(false(), x, y) -> average^#(s(x), p(p(y))) :1
3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
-->_1 if3^#(false(), b3, x, y) -> if4^#(b3, x, y) :2
4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
-->_1 if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y) :3
5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
-->_1 if^#(false(), b1, b2, b3, x, y) ->
average^#(p(x), s(y)) :5
-->_1 if^#(true(), b1, b2, b3, x, y) ->
if2^#(b1, b2, b3, x, y) :4
together with the congruence-graph
->1:{1,2,3,4,6,5} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{1,5,8,6,7,4}->8:{14}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Weak DPs:
{ if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
-->_1 if4^#(false(), x, y) -> average^#(s(x), p(p(y))) :1
3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
-->_1 if3^#(false(), b3, x, y) -> if4^#(b3, x, y) :2
4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
-->_1 if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y) :3
5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
-->_1 average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y) :6
6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
-->_1 if^#(false(), b1, b2, b3, x, y) ->
average^#(p(x), s(y)) :5
-->_1 if^#(true(), b1, b2, b3, x, y) ->
if2^#(b1, b2, b3, x, y) :4
together with the congruence-graph
->1:{1,2,3,4,6,5} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: if4^#(false(), x, y) -> average^#(s(x), p(p(y)))
, 2: if3^#(false(), b3, x, y) -> if4^#(b3, x, y)
, 3: if2^#(false(), b2, b3, x, y) -> if3^#(b2, b3, x, y)
, 4: if^#(true(), b1, b2, b3, x, y) -> if2^#(b1, b2, b3, x, y)
, 6: average^#(x, y) ->
if^#(le(x, 0()),
le(y, 0()),
le(y, s(0())),
le(y, s(s(0()))),
x,
y)
, 5: if^#(false(), b1, b2, b3, x, y) -> average^#(p(x), s(y))}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{2}: subsumed
--------------------
This path is subsumed by the proof of paths 3:{2}->5:{11},
3:{2}->4:{10}.
* Path 3:{2}->4:{10}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Weak DPs: {le^#(s(x), s(y)) -> le^#(x, y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: le^#(s(x), s(y)) -> le^#(x, y)
-->_1 le^#(s(x), s(y)) -> le^#(x, y) :1
together with the congruence-graph
->1:{1} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{1: le^#(s(x), s(y)) -> le^#(x, y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: le^#(s(x), s(y)) -> le^#(x, y)}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{2}->5:{11}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Weak DPs: {le^#(s(x), s(y)) -> le^#(x, y)}
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: le^#(s(x), s(y)) -> le^#(x, y)
-->_1 le^#(s(x), s(y)) -> le^#(x, y) :1
together with the congruence-graph
->1:{1} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{1: le^#(s(x), s(y)) -> le^#(x, y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: le^#(s(x), s(y)) -> le^#(x, y)}
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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:{9}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ le(s(x), s(y)) -> le(x, y)
, p(s(x)) -> x
, p(0()) -> 0()
, le(0(), y) -> true()
, le(s(x), 0()) -> false()}
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))