MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
foldl#3(x2,Nil()) -> x2
foldl#3(x6,Cons(x4,x2)) -> foldl#3(max#2(x6,x4),x2)
main(x1) -> foldl#3(0(),scanr#3(x1))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1} / {0/0,Cons/2,M/1,Nil/0,S/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1,foldl#3,main,max#2,minus#2,plus#2
,scanr#3} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x2,Nil()) -> c_8()
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(0(),x8) -> c_11()
max#2#(S(x12),0()) -> c_12()
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(0(),x16) -> c_14()
minus#2#(S(x20),0()) -> c_15()
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(0(),S(x2)) -> c_17()
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
scanr#3#(Nil()) -> c_20()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x2,Nil()) -> c_8()
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(0(),x8) -> c_11()
max#2#(S(x12),0()) -> c_12()
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(0(),x16) -> c_14()
minus#2#(S(x20),0()) -> c_15()
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(0(),S(x2)) -> c_17()
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
scanr#3#(Nil()) -> c_20()
- Weak TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
foldl#3(x2,Nil()) -> x2
foldl#3(x6,Cons(x4,x2)) -> foldl#3(max#2(x6,x4),x2)
main(x1) -> foldl#3(0(),scanr#3(x1))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1,cond_scanr_f_z_xs_1#/2
,foldl#3#/2,main#/1,max#2#/2,minus#2#/2,plus#2#/2,scanr#3#/1} / {0/0,Cons/2,M/1,Nil/0,S/1,c_1/0,c_2/0,c_3/0
,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/2,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/0,c_18/1,c_19/2
,c_20/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#
,plus#2#,scanr#3#} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x2,Nil()) -> c_8()
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(0(),x8) -> c_11()
max#2#(S(x12),0()) -> c_12()
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(0(),x16) -> c_14()
minus#2#(S(x20),0()) -> c_15()
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(0(),S(x2)) -> c_17()
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
scanr#3#(Nil()) -> c_20()
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x2,Nil()) -> c_8()
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(0(),x8) -> c_11()
max#2#(S(x12),0()) -> c_12()
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(0(),x16) -> c_14()
minus#2#(S(x20),0()) -> c_15()
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(0(),S(x2)) -> c_17()
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
scanr#3#(Nil()) -> c_20()
- Weak TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1,cond_scanr_f_z_xs_1#/2
,foldl#3#/2,main#/1,max#2#/2,minus#2#/2,plus#2#/2,scanr#3#/1} / {0/0,Cons/2,M/1,Nil/0,S/1,c_1/0,c_2/0,c_3/0
,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/2,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/0,c_18/1,c_19/2
,c_20/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#
,plus#2#,scanr#3#} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,3,4,6,8,11,12,14,15,17,20}
by application of
Pre({1,2,3,4,6,8,11,12,14,15,17,20}) = {7,9,10,13,16,18,19}.
Here rules are labelled as follows:
1: cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
2: cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
3: cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
4: cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
5: cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
6: cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
7: cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
8: foldl#3#(x2,Nil()) -> c_8()
9: foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
10: main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
11: max#2#(0(),x8) -> c_11()
12: max#2#(S(x12),0()) -> c_12()
13: max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
14: minus#2#(0(),x16) -> c_14()
15: minus#2#(S(x20),0()) -> c_15()
16: minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
17: plus#2#(0(),S(x2)) -> c_17()
18: plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
19: scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
20: scanr#3#(Nil()) -> c_20()
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
- Weak DPs:
cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
foldl#3#(x2,Nil()) -> c_8()
max#2#(0(),x8) -> c_11()
max#2#(S(x12),0()) -> c_12()
minus#2#(0(),x16) -> c_14()
minus#2#(S(x20),0()) -> c_15()
plus#2#(0(),S(x2)) -> c_17()
scanr#3#(Nil()) -> c_20()
- Weak TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1,cond_scanr_f_z_xs_1#/2
,foldl#3#/2,main#/1,max#2#/2,minus#2#/2,plus#2#/2,scanr#3#/1} / {0/0,Cons/2,M/1,Nil/0,S/1,c_1/0,c_2/0,c_3/0
,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/2,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/0,c_18/1,c_19/2
,c_20/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#
,plus#2#,scanr#3#} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
-->_1 plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2))):7
2:S:cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
-->_1 minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2)):6
-->_1 minus#2#(S(x20),0()) -> c_15():18
-->_1 minus#2#(0(),x16) -> c_14():17
3:S:foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
-->_2 max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2)):5
-->_2 max#2#(S(x12),0()) -> c_12():16
-->_2 max#2#(0(),x8) -> c_11():15
-->_1 foldl#3#(x2,Nil()) -> c_8():14
-->_1 foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4)):3
4:S:main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
-->_2 scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2)):8
-->_2 scanr#3#(Nil()) -> c_20():20
-->_1 foldl#3#(x2,Nil()) -> c_8():14
-->_1 foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4)):3
5:S:max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
-->_1 max#2#(S(x12),0()) -> c_12():16
-->_1 max#2#(0(),x8) -> c_11():15
-->_1 max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2)):5
6:S:minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
-->_1 minus#2#(S(x20),0()) -> c_15():18
-->_1 minus#2#(0(),x16) -> c_14():17
-->_1 minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2)):6
7:S:plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
-->_1 plus#2#(0(),S(x2)) -> c_17():19
-->_1 plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2))):7
8:S:scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
-->_2 scanr#3#(Nil()) -> c_20():20
-->_1 cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6():13
-->_1 cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4():12
-->_1 cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3():11
-->_1 cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2():10
-->_1 cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1():9
-->_2 scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2)):8
-->_1 cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4)):2
-->_1 cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2))):1
9:W:cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
10:W:cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
11:W:cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
12:W:cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
13:W:cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
14:W:foldl#3#(x2,Nil()) -> c_8()
15:W:max#2#(0(),x8) -> c_11()
16:W:max#2#(S(x12),0()) -> c_12()
17:W:minus#2#(0(),x16) -> c_14()
18:W:minus#2#(S(x20),0()) -> c_15()
19:W:plus#2#(0(),S(x2)) -> c_17()
20:W:scanr#3#(Nil()) -> c_20()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: cond_scanr_f_z_xs_1#(Cons(0(),x11),0()) -> c_1()
10: cond_scanr_f_z_xs_1#(Cons(0(),x11),M(x2)) -> c_2()
11: cond_scanr_f_z_xs_1#(Cons(0(),x11),S(x2)) -> c_3()
12: cond_scanr_f_z_xs_1#(Cons(S(x2),x11),0()) -> c_4()
13: cond_scanr_f_z_xs_1#(Cons(S(x40),x23),M(0())) -> c_6()
20: scanr#3#(Nil()) -> c_20()
14: foldl#3#(x2,Nil()) -> c_8()
15: max#2#(0(),x8) -> c_11()
16: max#2#(S(x12),0()) -> c_12()
17: minus#2#(0(),x16) -> c_14()
18: minus#2#(S(x20),0()) -> c_15()
19: plus#2#(0(),S(x2)) -> c_17()
* Step 5: NaturalMI MAYBE
+ Considered Problem:
- Strict DPs:
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
- Weak TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1,cond_scanr_f_z_xs_1#/2
,foldl#3#/2,main#/1,max#2#/2,minus#2#/2,plus#2#/2,scanr#3#/1} / {0/0,Cons/2,M/1,Nil/0,S/1,c_1/0,c_2/0,c_3/0
,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/2,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/0,c_18/1,c_19/2
,c_20/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#
,plus#2#,scanr#3#} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_9) = {1,2},
uargs(c_10) = {1,2},
uargs(c_13) = {1},
uargs(c_16) = {1},
uargs(c_18) = {1},
uargs(c_19) = {1,2}
Following symbols are considered usable:
{cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#,plus#2#,scanr#3#}
TcT has computed the following interpretation:
p(0) = [3]
p(Cons) = [1]
p(M) = [0]
p(Nil) = [1]
p(S) = [0]
p(cond_scanr_f_z_xs_1) = [6] x1 + [2]
p(foldl#3) = [2] x1 + [0]
p(main) = [1] x1 + [4]
p(max#2) = [4] x1 + [2] x2 + [0]
p(minus#2) = [1] x2 + [1]
p(plus#2) = [4] x1 + [2]
p(scanr#3) = [0]
p(cond_scanr_f_z_xs_1#) = [0]
p(foldl#3#) = [0]
p(main#) = [6]
p(max#2#) = [0]
p(minus#2#) = [0]
p(plus#2#) = [0]
p(scanr#3#) = [0]
p(c_1) = [1]
p(c_2) = [0]
p(c_3) = [1]
p(c_4) = [0]
p(c_5) = [2] x1 + [0]
p(c_6) = [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [1]
p(c_9) = [1] x1 + [1] x2 + [0]
p(c_10) = [4] x1 + [1] x2 + [5]
p(c_11) = [0]
p(c_12) = [1]
p(c_13) = [2] x1 + [0]
p(c_14) = [1]
p(c_15) = [1]
p(c_16) = [4] x1 + [0]
p(c_17) = [0]
p(c_18) = [1] x1 + [0]
p(c_19) = [2] x1 + [2] x2 + [0]
p(c_20) = [1]
Following rules are strictly oriented:
main#(x1) = [6]
> [5]
= c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
Following rules are (at-least) weakly oriented:
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) = [0]
>= [0]
= c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) = [0]
>= [0]
= c_7(minus#2#(x8,x4))
foldl#3#(x6,Cons(x4,x2)) = [0]
>= [0]
= c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
max#2#(S(x4),S(x2)) = [0]
>= [0]
= c_13(max#2#(x4,x2))
minus#2#(S(x4),S(x2)) = [0]
>= [0]
= c_16(minus#2#(x4,x2))
plus#2#(S(x4),S(x2)) = [0]
>= [0]
= c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) = [0]
>= [0]
= c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
* Step 6: Failure MAYBE
+ Considered Problem:
- Strict DPs:
cond_scanr_f_z_xs_1#(Cons(S(x2),x11),S(x4)) -> c_5(plus#2#(S(x4),S(x2)))
cond_scanr_f_z_xs_1#(Cons(S(x8),x23),M(S(x4))) -> c_7(minus#2#(x8,x4))
foldl#3#(x6,Cons(x4,x2)) -> c_9(foldl#3#(max#2(x6,x4),x2),max#2#(x6,x4))
max#2#(S(x4),S(x2)) -> c_13(max#2#(x4,x2))
minus#2#(S(x4),S(x2)) -> c_16(minus#2#(x4,x2))
plus#2#(S(x4),S(x2)) -> c_18(plus#2#(x4,S(x2)))
scanr#3#(Cons(x4,x2)) -> c_19(cond_scanr_f_z_xs_1#(scanr#3(x2),x4),scanr#3#(x2))
- Weak DPs:
main#(x1) -> c_10(foldl#3#(0(),scanr#3(x1)),scanr#3#(x1))
- Weak TRS:
cond_scanr_f_z_xs_1(Cons(0(),x11),0()) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),M(x2)) -> Cons(0(),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(0(),x11),S(x2)) -> Cons(S(x2),Cons(0(),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),0()) -> Cons(S(x2),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x2),x11),S(x4)) -> Cons(plus#2(S(x4),S(x2)),Cons(S(x2),x11))
cond_scanr_f_z_xs_1(Cons(S(x40),x23),M(0())) -> Cons(S(x40),Cons(S(x40),x23))
cond_scanr_f_z_xs_1(Cons(S(x8),x23),M(S(x4))) -> Cons(minus#2(x8,x4),Cons(S(x8),x23))
max#2(0(),x8) -> x8
max#2(S(x12),0()) -> S(x12)
max#2(S(x4),S(x2)) -> S(max#2(x4,x2))
minus#2(0(),x16) -> 0()
minus#2(S(x20),0()) -> S(x20)
minus#2(S(x4),S(x2)) -> minus#2(x4,x2)
plus#2(0(),S(x2)) -> S(x2)
plus#2(S(x4),S(x2)) -> S(plus#2(x4,S(x2)))
scanr#3(Cons(x4,x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2),x4)
scanr#3(Nil()) -> Cons(0(),Nil())
- Signature:
{cond_scanr_f_z_xs_1/2,foldl#3/2,main/1,max#2/2,minus#2/2,plus#2/2,scanr#3/1,cond_scanr_f_z_xs_1#/2
,foldl#3#/2,main#/1,max#2#/2,minus#2#/2,plus#2#/2,scanr#3#/1} / {0/0,Cons/2,M/1,Nil/0,S/1,c_1/0,c_2/0,c_3/0
,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/2,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/1,c_17/0,c_18/1,c_19/2
,c_20/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_scanr_f_z_xs_1#,foldl#3#,main#,max#2#,minus#2#
,plus#2#,scanr#3#} and constructors {0,Cons,M,Nil,S}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE