MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
if(false(),b,l) -> if2(b,l)
if(true(),b,l) -> s(0())
if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
if2(true(),l) -> car(l)
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr,car,cddr,if,if2,ifplus,iftimes,isZero,p,plus,prod
,shorter,times} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(false(),b,l) -> c_6(if2#(b,l))
if#(true(),b,l) -> c_7()
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
if2#(true(),l) -> c_9(car#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
ifplus#(true(),x,y) -> c_11()
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),0()) -> c_20()
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
shorter#(nil(),y) -> c_22()
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(false(),b,l) -> c_6(if2#(b,l))
if#(true(),b,l) -> c_7()
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
if2#(true(),l) -> c_9(car#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
ifplus#(true(),x,y) -> c_11()
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),0()) -> c_20()
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
shorter#(nil(),y) -> c_22()
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
if(false(),b,l) -> if2(b,l)
if(true(),b,l) -> s(0())
if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
if2(true(),l) -> car(l)
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/1,c_10/2,c_11/0,c_12/3
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/2,c_19/3,c_20/0,c_21/1,c_22/0,c_23/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(false(),b,l) -> c_6(if2#(b,l))
if#(true(),b,l) -> c_7()
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
if2#(true(),l) -> c_9(car#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
ifplus#(true(),x,y) -> c_11()
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),0()) -> c_20()
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
shorter#(nil(),y) -> c_22()
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(false(),b,l) -> c_6(if2#(b,l))
if#(true(),b,l) -> c_7()
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
if2#(true(),l) -> c_9(car#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
ifplus#(true(),x,y) -> c_11()
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),0()) -> c_20()
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
shorter#(nil(),y) -> c_22()
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/1,c_10/2,c_11/0,c_12/3
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/2,c_19/3,c_20/0,c_21/1,c_22/0,c_23/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,3,4,5,7,11,13,14,15,16,17,20,22}
by application of
Pre({1,2,3,4,5,7,11,13,14,15,16,17,20,22}) = {8,9,10,12,18,19,21,23}.
Here rules are labelled as follows:
1: cadr#(cons(x,cons(y,l))) -> c_1()
2: car#(cons(x,l)) -> c_2()
3: cddr#(cons(x,cons(y,l))) -> c_3()
4: cddr#(cons(x,nil())) -> c_4()
5: cddr#(nil()) -> c_5()
6: if#(false(),b,l) -> c_6(if2#(b,l))
7: if#(true(),b,l) -> c_7()
8: if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
9: if2#(true(),l) -> c_9(car#(l))
10: ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
11: ifplus#(true(),x,y) -> c_11()
12: iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
13: iftimes#(true(),x,y) -> c_13()
14: isZero#(0()) -> c_14()
15: isZero#(s(x)) -> c_15()
16: p#(0()) -> c_16()
17: p#(s(x)) -> c_17()
18: plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
19: prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
20: shorter#(cons(x,l),0()) -> c_20()
21: shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
22: shorter#(nil(),y) -> c_22()
23: times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
if#(false(),b,l) -> c_6(if2#(b,l))
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
if2#(true(),l) -> c_9(car#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
- Weak DPs:
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(true(),b,l) -> c_7()
ifplus#(true(),x,y) -> c_11()
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
shorter#(cons(x,l),0()) -> c_20()
shorter#(nil(),y) -> c_22()
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/1,c_10/2,c_11/0,c_12/3
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/2,c_19/3,c_20/0,c_21/1,c_22/0,c_23/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{3}
by application of
Pre({3}) = {1}.
Here rules are labelled as follows:
1: if#(false(),b,l) -> c_6(if2#(b,l))
2: if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
3: if2#(true(),l) -> c_9(car#(l))
4: ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
5: iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
6: plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
7: prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
8: shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
9: times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
10: cadr#(cons(x,cons(y,l))) -> c_1()
11: car#(cons(x,l)) -> c_2()
12: cddr#(cons(x,cons(y,l))) -> c_3()
13: cddr#(cons(x,nil())) -> c_4()
14: cddr#(nil()) -> c_5()
15: if#(true(),b,l) -> c_7()
16: ifplus#(true(),x,y) -> c_11()
17: iftimes#(true(),x,y) -> c_13()
18: isZero#(0()) -> c_14()
19: isZero#(s(x)) -> c_15()
20: p#(0()) -> c_16()
21: p#(s(x)) -> c_17()
22: shorter#(cons(x,l),0()) -> c_20()
23: shorter#(nil(),y) -> c_22()
* Step 5: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
if#(false(),b,l) -> c_6(if2#(b,l))
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
- Weak DPs:
cadr#(cons(x,cons(y,l))) -> c_1()
car#(cons(x,l)) -> c_2()
cddr#(cons(x,cons(y,l))) -> c_3()
cddr#(cons(x,nil())) -> c_4()
cddr#(nil()) -> c_5()
if#(true(),b,l) -> c_7()
if2#(true(),l) -> c_9(car#(l))
ifplus#(true(),x,y) -> c_11()
iftimes#(true(),x,y) -> c_13()
isZero#(0()) -> c_14()
isZero#(s(x)) -> c_15()
p#(0()) -> c_16()
p#(s(x)) -> c_17()
shorter#(cons(x,l),0()) -> c_20()
shorter#(nil(),y) -> c_22()
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/1,c_10/2,c_11/0,c_12/3
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/2,c_19/3,c_20/0,c_21/1,c_22/0,c_23/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:if#(false(),b,l) -> c_6(if2#(b,l))
-->_1 if2#(true(),l) -> c_9(car#(l)):15
-->_1 if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l)):2
2:S:if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
-->_2 times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x)):8
-->_1 prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0()))):6
-->_5 cddr#(nil()) -> c_5():13
-->_5 cddr#(cons(x,nil())) -> c_4():12
-->_5 cddr#(cons(x,cons(y,l))) -> c_3():11
-->_3 car#(cons(x,l)) -> c_2():10
-->_4 cadr#(cons(x,cons(y,l))) -> c_1():9
3:S:ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
-->_1 plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x)):5
-->_2 p#(s(x)) -> c_17():21
-->_2 p#(0()) -> c_16():20
4:S:iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
-->_2 times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x)):8
-->_1 plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x)):5
-->_3 p#(s(x)) -> c_17():21
-->_3 p#(0()) -> c_16():20
5:S:plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
-->_2 isZero#(s(x)) -> c_15():19
-->_2 isZero#(0()) -> c_14():18
-->_1 ifplus#(true(),x,y) -> c_11():16
-->_1 ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x)):3
6:S:prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
-->_3 shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y)):7
-->_3 shorter#(nil(),y) -> c_22():23
-->_2 shorter#(nil(),y) -> c_22():23
-->_2 shorter#(cons(x,l),0()) -> c_20():22
-->_1 if#(true(),b,l) -> c_7():14
-->_1 if#(false(),b,l) -> c_6(if2#(b,l)):1
7:S:shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
-->_1 shorter#(nil(),y) -> c_22():23
-->_1 shorter#(cons(x,l),0()) -> c_20():22
-->_1 shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y)):7
8:S:times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
-->_2 isZero#(s(x)) -> c_15():19
-->_2 isZero#(0()) -> c_14():18
-->_1 iftimes#(true(),x,y) -> c_13():17
-->_1 iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x)):4
9:W:cadr#(cons(x,cons(y,l))) -> c_1()
10:W:car#(cons(x,l)) -> c_2()
11:W:cddr#(cons(x,cons(y,l))) -> c_3()
12:W:cddr#(cons(x,nil())) -> c_4()
13:W:cddr#(nil()) -> c_5()
14:W:if#(true(),b,l) -> c_7()
15:W:if2#(true(),l) -> c_9(car#(l))
-->_1 car#(cons(x,l)) -> c_2():10
16:W:ifplus#(true(),x,y) -> c_11()
17:W:iftimes#(true(),x,y) -> c_13()
18:W:isZero#(0()) -> c_14()
19:W:isZero#(s(x)) -> c_15()
20:W:p#(0()) -> c_16()
21:W:p#(s(x)) -> c_17()
22:W:shorter#(cons(x,l),0()) -> c_20()
23:W:shorter#(nil(),y) -> c_22()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: cadr#(cons(x,cons(y,l))) -> c_1()
11: cddr#(cons(x,cons(y,l))) -> c_3()
12: cddr#(cons(x,nil())) -> c_4()
13: cddr#(nil()) -> c_5()
14: if#(true(),b,l) -> c_7()
22: shorter#(cons(x,l),0()) -> c_20()
23: shorter#(nil(),y) -> c_22()
20: p#(0()) -> c_16()
21: p#(s(x)) -> c_17()
16: ifplus#(true(),x,y) -> c_11()
17: iftimes#(true(),x,y) -> c_13()
18: isZero#(0()) -> c_14()
19: isZero#(s(x)) -> c_15()
15: if2#(true(),l) -> c_9(car#(l))
10: car#(cons(x,l)) -> c_2()
* Step 6: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
if#(false(),b,l) -> c_6(if2#(b,l))
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/5,c_9/1,c_10/2,c_11/0,c_12/3
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/2,c_19/3,c_20/0,c_21/1,c_22/0,c_23/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:if#(false(),b,l) -> c_6(if2#(b,l))
-->_1 if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l)):2
2:S:if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l)))
,times#(car(l),cadr(l))
,car#(l)
,cadr#(l)
,cddr#(l))
-->_2 times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x)):8
-->_1 prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0()))):6
3:S:ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x))
-->_1 plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x)):5
4:S:iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x))
-->_2 times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x)):8
-->_1 plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x)):5
5:S:plus#(x,y) -> c_18(ifplus#(isZero(x),x,y),isZero#(x))
-->_1 ifplus#(false(),x,y) -> c_10(plus#(p(x),y),p#(x)):3
6:S:prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,0()),shorter#(l,s(0())))
-->_3 shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y)):7
-->_1 if#(false(),b,l) -> c_6(if2#(b,l)):1
7:S:shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
-->_1 shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y)):7
8:S:times#(x,y) -> c_23(iftimes#(isZero(x),x,y),isZero#(x))
-->_1 iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y),p#(x)):4
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l))),times#(car(l),cadr(l)))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y))
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y))
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,s(0())))
times#(x,y) -> c_23(iftimes#(isZero(x),x,y))
* Step 7: Failure MAYBE
+ Considered Problem:
- Strict DPs:
if#(false(),b,l) -> c_6(if2#(b,l))
if2#(false(),l) -> c_8(prod#(cons(times(car(l),cadr(l)),cddr(l))),times#(car(l),cadr(l)))
ifplus#(false(),x,y) -> c_10(plus#(p(x),y))
iftimes#(false(),x,y) -> c_12(plus#(y,times(p(x),y)),times#(p(x),y))
plus#(x,y) -> c_18(ifplus#(isZero(x),x,y))
prod#(l) -> c_19(if#(shorter(l,0()),shorter(l,s(0())),l),shorter#(l,s(0())))
shorter#(cons(x,l),s(y)) -> c_21(shorter#(l,y))
times#(x,y) -> c_23(iftimes#(isZero(x),x,y))
- Weak TRS:
cadr(cons(x,cons(y,l))) -> y
car(cons(x,l)) -> x
cddr(cons(x,cons(y,l))) -> l
cddr(cons(x,nil())) -> nil()
cddr(nil()) -> nil()
ifplus(false(),x,y) -> s(plus(p(x),y))
ifplus(true(),x,y) -> y
iftimes(false(),x,y) -> plus(y,times(p(x),y))
iftimes(true(),x,y) -> 0()
isZero(0()) -> true()
isZero(s(x)) -> false()
p(0()) -> 0()
p(s(x)) -> x
plus(x,y) -> ifplus(isZero(x),x,y)
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
shorter(nil(),y) -> true()
times(x,y) -> iftimes(isZero(x),x,y)
- Signature:
{cadr/1,car/1,cddr/1,if/3,if2/2,ifplus/3,iftimes/3,isZero/1,p/1,plus/2,prod/1,shorter/2,times/2,cadr#/1
,car#/1,cddr#/1,if#/3,if2#/2,ifplus#/3,iftimes#/3,isZero#/1,p#/1,plus#/2,prod#/1,shorter#/2,times#/2} / {0/0
,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/1,c_10/1,c_11/0,c_12/2
,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/1,c_19/2,c_20/0,c_21/1,c_22/0,c_23/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cadr#,car#,cddr#,if#,if2#,ifplus#,iftimes#,isZero#,p#
,plus#,prod#,shorter#,times#} and constructors {0,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE