WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0 ,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,CONCAT,LESS_LEAVES,MINUS,QUOT,REVERSE,SHUFFLE,app ,concat,less_leaves,minus,quot,reverse,shuffle} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c2,c3 ,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0 ,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,CONCAT,LESS_LEAVES,MINUS,QUOT,REVERSE,SHUFFLE,app ,concat,less_leaves,minus,quot,reverse,shuffle} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c2,c3 ,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0 ,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,CONCAT,LESS_LEAVES,MINUS,QUOT,REVERSE,SHUFFLE,app ,concat,less_leaves,minus,quot,reverse,shuffle} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c2,c3 ,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APP(y,z){y -> add(x,y)} = APP(add(x,y),z) ->^+ c5(APP(y,z)) = C[APP(y,z) = APP(y,z){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0 ,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP,CONCAT,LESS_LEAVES,MINUS,QUOT,REVERSE,SHUFFLE,app ,concat,less_leaves,minus,quot,reverse,shuffle} and constructors {0,add,c,c1,c10,c11,c12,c13,c14,c15,c2,c3 ,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) APP#(nil(),z0) -> c_2() CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) CONCAT#(leaf(),z0) -> c_4() LESS_LEAVES#(z0,leaf()) -> c_5() LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() MINUS#(z0,0()) -> c_9() MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(0(),s(z0)) -> c_11() QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) REVERSE#(nil()) -> c_14() SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) SHUFFLE#(nil()) -> c_16() Weak DPs app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) app#(nil(),z0) -> c_18() concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) concat#(leaf(),z0) -> c_20() less_leaves#(z0,leaf()) -> c_21() less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) less_leaves#(leaf(),cons(z0,z1)) -> c_23() minus#(z0,0()) -> c_24() minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) quot#(0(),s(z0)) -> c_26() quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) reverse#(nil()) -> c_29() shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) shuffle#(nil()) -> c_31() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) APP#(nil(),z0) -> c_2() CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) CONCAT#(leaf(),z0) -> c_4() LESS_LEAVES#(z0,leaf()) -> c_5() LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() MINUS#(z0,0()) -> c_9() MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(0(),s(z0)) -> c_11() QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) REVERSE#(nil()) -> c_14() SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) SHUFFLE#(nil()) -> c_16() - Weak DPs: app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) app#(nil(),z0) -> c_18() concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) concat#(leaf(),z0) -> c_20() less_leaves#(z0,leaf()) -> c_21() less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) less_leaves#(leaf(),cons(z0,z1)) -> c_23() minus#(z0,0()) -> c_24() minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) quot#(0(),s(z0)) -> c_26() quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) reverse#(nil()) -> c_29() shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) shuffle#(nil()) -> c_31() - Weak TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/0,c_12/3,c_13/3,c_14/0,c_15/3,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,8,9,11,14,16} by application of Pre({2,4,5,8,9,11,14,16}) = {1,3,6,7,10,12,13,15}. Here rules are labelled as follows: 1: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) 2: APP#(nil(),z0) -> c_2() 3: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) 4: CONCAT#(leaf(),z0) -> c_4() 5: LESS_LEAVES#(z0,leaf()) -> c_5() 6: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) 7: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) 8: LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() 9: MINUS#(z0,0()) -> c_9() 10: MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) 11: QUOT#(0(),s(z0)) -> c_11() 12: QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) 13: REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) 14: REVERSE#(nil()) -> c_14() 15: SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) 16: SHUFFLE#(nil()) -> c_16() 17: app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) 18: app#(nil(),z0) -> c_18() 19: concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) 20: concat#(leaf(),z0) -> c_20() 21: less_leaves#(z0,leaf()) -> c_21() 22: less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) 23: less_leaves#(leaf(),cons(z0,z1)) -> c_23() 24: minus#(z0,0()) -> c_24() 25: minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) 26: quot#(0(),s(z0)) -> c_26() 27: quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) 28: reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) 29: reverse#(nil()) -> c_29() 30: shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) 31: shuffle#(nil()) -> c_31() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) - Weak DPs: APP#(nil(),z0) -> c_2() CONCAT#(leaf(),z0) -> c_4() LESS_LEAVES#(z0,leaf()) -> c_5() LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() MINUS#(z0,0()) -> c_9() QUOT#(0(),s(z0)) -> c_11() REVERSE#(nil()) -> c_14() SHUFFLE#(nil()) -> c_16() app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) app#(nil(),z0) -> c_18() concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) concat#(leaf(),z0) -> c_20() less_leaves#(z0,leaf()) -> c_21() less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) less_leaves#(leaf(),cons(z0,z1)) -> c_23() minus#(z0,0()) -> c_24() minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) quot#(0(),s(z0)) -> c_26() quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) reverse#(nil()) -> c_29() shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) shuffle#(nil()) -> c_31() - Weak TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/0,c_12/3,c_13/3,c_14/0,c_15/3,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) -->_1 APP#(nil(),z0) -> c_2():9 -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 2:S:CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) -->_1 CONCAT#(leaf(),z0) -> c_4():10 -->_1 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 3:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) -->_3 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 -->_2 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):4 -->_3 concat#(leaf(),z0) -> c_20():20 -->_2 concat#(leaf(),z0) -> c_20():20 -->_1 LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8():12 -->_1 LESS_LEAVES#(z0,leaf()) -> c_5():11 -->_4 CONCAT#(leaf(),z0) -> c_4():10 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):3 -->_4 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 4:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) -->_3 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 -->_2 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 -->_3 concat#(leaf(),z0) -> c_20():20 -->_2 concat#(leaf(),z0) -> c_20():20 -->_1 LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8():12 -->_1 LESS_LEAVES#(z0,leaf()) -> c_5():11 -->_4 CONCAT#(leaf(),z0) -> c_4():10 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):4 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):3 -->_4 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 5:S:MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) -->_1 MINUS#(z0,0()) -> c_9():13 -->_1 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):5 6:S:QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) -->_2 minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)):25 -->_2 minus#(z0,0()) -> c_24():24 -->_1 QUOT#(0(),s(z0)) -> c_11():14 -->_3 MINUS#(z0,0()) -> c_9():13 -->_1 QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)):6 -->_3 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):5 7:S:REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) -->_2 reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)):28 -->_2 reverse#(nil()) -> c_29():29 -->_3 REVERSE#(nil()) -> c_14():15 -->_1 APP#(nil(),z0) -> c_2():9 -->_3 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)):7 -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 8:S:SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) -->_2 reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)):28 -->_2 reverse#(nil()) -> c_29():29 -->_1 SHUFFLE#(nil()) -> c_16():16 -->_3 REVERSE#(nil()) -> c_14():15 -->_1 SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)):8 -->_3 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)):7 9:W:APP#(nil(),z0) -> c_2() 10:W:CONCAT#(leaf(),z0) -> c_4() 11:W:LESS_LEAVES#(z0,leaf()) -> c_5() 12:W:LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() 13:W:MINUS#(z0,0()) -> c_9() 14:W:QUOT#(0(),s(z0)) -> c_11() 15:W:REVERSE#(nil()) -> c_14() 16:W:SHUFFLE#(nil()) -> c_16() 17:W:app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) -->_1 app#(nil(),z0) -> c_18():18 -->_1 app#(add(z0,z1),z2) -> c_17(app#(z1,z2)):17 18:W:app#(nil(),z0) -> c_18() 19:W:concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) -->_1 concat#(leaf(),z0) -> c_20():20 -->_1 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 20:W:concat#(leaf(),z0) -> c_20() 21:W:less_leaves#(z0,leaf()) -> c_21() 22:W:less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) -->_1 less_leaves#(leaf(),cons(z0,z1)) -> c_23():23 -->_1 less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)):22 -->_1 less_leaves#(z0,leaf()) -> c_21():21 -->_3 concat#(leaf(),z0) -> c_20():20 -->_2 concat#(leaf(),z0) -> c_20():20 -->_3 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 -->_2 concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)):19 23:W:less_leaves#(leaf(),cons(z0,z1)) -> c_23() 24:W:minus#(z0,0()) -> c_24() 25:W:minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) -->_1 minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)):25 -->_1 minus#(z0,0()) -> c_24():24 26:W:quot#(0(),s(z0)) -> c_26() 27:W:quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) -->_1 quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)):27 -->_1 quot#(0(),s(z0)) -> c_26():26 -->_2 minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)):25 -->_2 minus#(z0,0()) -> c_24():24 28:W:reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) -->_2 reverse#(nil()) -> c_29():29 -->_2 reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)):28 -->_1 app#(nil(),z0) -> c_18():18 -->_1 app#(add(z0,z1),z2) -> c_17(app#(z1,z2)):17 29:W:reverse#(nil()) -> c_29() 30:W:shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) -->_1 shuffle#(nil()) -> c_31():31 -->_1 shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)):30 -->_2 reverse#(nil()) -> c_29():29 -->_2 reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)):28 31:W:shuffle#(nil()) -> c_31() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 30: shuffle#(add(z0,z1)) -> c_30(shuffle#(reverse(z1)),reverse#(z1)) 31: shuffle#(nil()) -> c_31() 27: quot#(s(z0),s(z1)) -> c_27(quot#(minus(z0,z1),s(z1)),minus#(z0,z1)) 26: quot#(0(),s(z0)) -> c_26() 22: less_leaves#(cons(z0,z1),cons(z2,z3)) -> c_22(less_leaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) 23: less_leaves#(leaf(),cons(z0,z1)) -> c_23() 21: less_leaves#(z0,leaf()) -> c_21() 16: SHUFFLE#(nil()) -> c_16() 15: REVERSE#(nil()) -> c_14() 28: reverse#(add(z0,z1)) -> c_28(app#(reverse(z1),add(z0,nil())),reverse#(z1)) 17: app#(add(z0,z1),z2) -> c_17(app#(z1,z2)) 18: app#(nil(),z0) -> c_18() 29: reverse#(nil()) -> c_29() 14: QUOT#(0(),s(z0)) -> c_11() 25: minus#(s(z0),s(z1)) -> c_25(minus#(z0,z1)) 24: minus#(z0,0()) -> c_24() 13: MINUS#(z0,0()) -> c_9() 11: LESS_LEAVES#(z0,leaf()) -> c_5() 12: LESS_LEAVES#(leaf(),cons(z0,z1)) -> c_8() 19: concat#(cons(z0,z1),z2) -> c_19(concat#(z1,z2)) 20: concat#(leaf(),z0) -> c_20() 10: CONCAT#(leaf(),z0) -> c_4() 9: APP#(nil(),z0) -> c_2() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) - Weak TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/4,c_7/4,c_8/0,c_9/0,c_10/1,c_11/0,c_12/3,c_13/3,c_14/0,c_15/3,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 2:S:CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) -->_1 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 3:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):4 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):3 -->_4 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 4:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):4 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):3 -->_4 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):2 5:S:MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) -->_1 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):5 6:S:QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)) -->_1 QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),minus#(z0,z1),MINUS#(z0,z1)):6 -->_3 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):5 7:S:REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)) -->_3 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)):7 -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 8:S:SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)) -->_1 SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),reverse#(z1),REVERSE#(z1)):8 -->_3 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),reverse#(z1),REVERSE#(z1)):7 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) - Weak TRS: APP(add(z0,z1),z2) -> c5(APP(z1,z2)) APP(nil(),z0) -> c4() CONCAT(cons(z0,z1),z2) -> c11(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c10() LESS_LEAVES(z0,leaf()) -> c12() LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c14(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESS_LEAVES(cons(z0,z1),cons(z2,z3)) -> c15(LESS_LEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESS_LEAVES(leaf(),cons(z0,z1)) -> c13() MINUS(z0,0()) -> c() MINUS(s(z0),s(z1)) -> c1(MINUS(z0,z1)) QUOT(0(),s(z0)) -> c2() QUOT(s(z0),s(z1)) -> c3(QUOT(minus(z0,z1),s(z1)),MINUS(z0,z1)) REVERSE(add(z0,z1)) -> c7(APP(reverse(z1),add(z0,nil())),REVERSE(z1)) REVERSE(nil()) -> c6() SHUFFLE(add(z0,z1)) -> c9(SHUFFLE(reverse(z1)),REVERSE(z1)) SHUFFLE(nil()) -> c8() app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 less_leaves(z0,leaf()) -> false() less_leaves(cons(z0,z1),cons(z2,z3)) -> less_leaves(concat(z0,z1),concat(z2,z3)) less_leaves(leaf(),cons(z0,z1)) -> true() minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) quot(0(),s(z0)) -> 0() quot(s(z0),s(z1)) -> s(quot(minus(z0,z1),s(z1))) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() shuffle(add(z0,z1)) -> add(z0,shuffle(reverse(z1))) shuffle(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) and a lower component APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) Further, following extension rules are added to the lower component. LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z2,z3)):2 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z0,z1)):1 2:S:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z2,z3)):2 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z0,z1)):1 3:S:QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)) -->_1 QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1)),MINUS#(z0,z1)):3 4:S:SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)) -->_1 SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1)),REVERSE#(z1)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1))) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1))) *** Step 1.b:6.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1))) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1))) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_12) = {1}, uargs(c_15) = {1} Following symbols are considered usable: {app,concat,reverse,APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE#,app#,concat#,less_leaves# ,minus#,quot#,reverse#,shuffle#} TcT has computed the following interpretation: p(0) = [0] p(APP) = [2] x2 + [0] p(CONCAT) = [4] x1 + [1] p(LESS_LEAVES) = [1] x1 + [2] x2 + [0] p(MINUS) = [1] x1 + [1] x2 + [1] p(QUOT) = [1] x1 + [8] p(REVERSE) = [1] x1 + [1] p(SHUFFLE) = [8] p(add) = [1] x2 + [1] p(app) = [1] x1 + [1] x2 + [0] p(c) = [1] p(c1) = [1] p(c10) = [8] p(c11) = [1] x1 + [0] p(c12) = [1] p(c13) = [8] p(c14) = [1] p(c15) = [1] x1 + [0] p(c2) = [1] p(c3) = [0] p(c4) = [1] p(c5) = [8] p(c6) = [0] p(c7) = [0] p(c8) = [1] p(c9) = [1] x1 + [1] p(concat) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [2] p(false) = [1] p(leaf) = [6] p(less_leaves) = [1] x1 + [4] x2 + [1] p(minus) = [1] x2 + [0] p(nil) = [0] p(quot) = [8] x1 + [0] p(reverse) = [1] x1 + [1] p(s) = [1] x1 + [0] p(shuffle) = [8] p(true) = [0] p(APP#) = [8] x2 + [2] p(CONCAT#) = [8] x2 + [1] p(LESS_LEAVES#) = [8] x1 + [0] p(MINUS#) = [1] x1 + [2] p(QUOT#) = [0] p(REVERSE#) = [1] x1 + [1] p(SHUFFLE#) = [14] x1 + [2] p(app#) = [1] x2 + [4] p(concat#) = [1] x1 + [1] p(less_leaves#) = [4] x1 + [0] p(minus#) = [1] x1 + [1] x2 + [0] p(quot#) = [1] x1 + [1] p(reverse#) = [1] x1 + [0] p(shuffle#) = [1] p(c_1) = [2] p(c_2) = [0] p(c_3) = [1] x1 + [1] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [12] p(c_7) = [1] x1 + [8] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] p(c_11) = [2] p(c_12) = [8] x1 + [0] p(c_13) = [1] x1 + [2] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] p(c_17) = [1] x1 + [8] p(c_18) = [1] p(c_19) = [1] x1 + [0] p(c_20) = [8] p(c_21) = [1] p(c_22) = [1] x1 + [2] x2 + [2] x3 + [1] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [0] p(c_27) = [2] x1 + [2] x2 + [0] p(c_28) = [1] x2 + [1] p(c_29) = [1] p(c_30) = [2] x2 + [1] p(c_31) = [1] Following rules are strictly oriented: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [8] z0 + [8] z1 + [16] > [8] z0 + [8] z1 + [12] = c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [8] z0 + [8] z1 + [16] > [8] z0 + [8] z1 + [8] = c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) Following rules are (at-least) weakly oriented: QUOT#(s(z0),s(z1)) = [0] >= [0] = c_12(QUOT#(minus(z0,z1),s(z1))) SHUFFLE#(add(z0,z1)) = [14] z1 + [16] >= [14] z1 + [16] = c_15(SHUFFLE#(reverse(z1))) app(add(z0,z1),z2) = [1] z1 + [1] z2 + [1] >= [1] z1 + [1] z2 + [1] = add(z0,app(z1,z2)) app(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [6] >= [1] z0 + [0] = z0 reverse(add(z0,z1)) = [1] z1 + [2] >= [1] z1 + [2] = app(reverse(z1),add(z0,nil())) reverse(nil()) = [1] >= [0] = nil() *** Step 1.b:6.a:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1))) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1))) - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(app) = {1}, uargs(cons) = {2}, uargs(LESS_LEAVES#) = {1,2}, uargs(QUOT#) = {1}, uargs(SHUFFLE#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_12) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(APP) = [0] p(CONCAT) = [0] p(LESS_LEAVES) = [0] p(MINUS) = [0] p(QUOT) = [0] p(REVERSE) = [0] p(SHUFFLE) = [0] p(add) = [1] x2 + [5] p(app) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [0] p(c9) = [1] x1 + [1] x2 + [0] p(concat) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [4] p(false) = [0] p(leaf) = [4] p(less_leaves) = [0] p(minus) = [1] x1 + [0] p(nil) = [0] p(quot) = [1] x2 + [2] p(reverse) = [1] x1 + [6] p(s) = [1] x1 + [1] p(shuffle) = [1] x1 + [0] p(true) = [0] p(APP#) = [1] p(CONCAT#) = [2] x1 + [1] p(LESS_LEAVES#) = [1] x1 + [1] x2 + [0] p(MINUS#) = [2] p(QUOT#) = [1] x1 + [5] x2 + [2] p(REVERSE#) = [2] p(SHUFFLE#) = [1] x1 + [1] p(app#) = [1] x2 + [0] p(concat#) = [1] x1 + [1] p(less_leaves#) = [1] x1 + [1] p(minus#) = [2] x1 + [1] x2 + [0] p(quot#) = [1] x1 + [1] p(reverse#) = [1] x1 + [0] p(shuffle#) = [4] p(c_1) = [1] x1 + [4] p(c_2) = [1] p(c_3) = [4] x1 + [4] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] x1 + [5] p(c_7) = [1] x1 + [0] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] x1 + [1] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [1] x1 + [4] p(c_18) = [2] p(c_19) = [1] x1 + [0] p(c_20) = [0] p(c_21) = [1] p(c_22) = [1] x2 + [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [4] p(c_27) = [1] x1 + [1] x2 + [1] p(c_28) = [2] x2 + [1] p(c_29) = [1] p(c_30) = [4] x1 + [1] x2 + [1] p(c_31) = [0] Following rules are strictly oriented: QUOT#(s(z0),s(z1)) = [1] z0 + [5] z1 + [8] > [1] z0 + [5] z1 + [7] = c_12(QUOT#(minus(z0,z1),s(z1))) Following rules are (at-least) weakly oriented: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [8] >= [1] z0 + [1] z1 + [1] z2 + [1] z3 + [5] = c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [8] >= [1] z0 + [1] z1 + [1] z2 + [1] z3 + [0] = c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) SHUFFLE#(add(z0,z1)) = [1] z1 + [6] >= [1] z1 + [7] = c_15(SHUFFLE#(reverse(z1))) app(add(z0,z1),z2) = [1] z1 + [1] z2 + [5] >= [1] z1 + [1] z2 + [5] = add(z0,app(z1,z2)) app(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [4] >= [1] z0 + [1] z1 + [1] z2 + [4] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [4] >= [1] z0 + [0] = z0 minus(z0,0()) = [1] z0 + [0] >= [1] z0 + [0] = z0 minus(s(z0),s(z1)) = [1] z0 + [1] >= [1] z0 + [0] = minus(z0,z1) reverse(add(z0,z1)) = [1] z1 + [11] >= [1] z1 + [11] = app(reverse(z1),add(z0,nil())) reverse(nil()) = [6] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:6.a:4: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1))) - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1))) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(add) = {2}, uargs(app) = {1}, uargs(cons) = {2}, uargs(LESS_LEAVES#) = {1,2}, uargs(QUOT#) = {1}, uargs(SHUFFLE#) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1}, uargs(c_12) = {1}, uargs(c_15) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(APP) = [0] p(CONCAT) = [0] p(LESS_LEAVES) = [0] p(MINUS) = [0] p(QUOT) = [0] p(REVERSE) = [0] p(SHUFFLE) = [0] p(add) = [1] x2 + [1] p(app) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [1] p(c11) = [1] x1 + [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [0] p(c9) = [1] x1 + [1] x2 + [0] p(concat) = [1] x2 + [0] p(cons) = [1] x2 + [0] p(false) = [0] p(leaf) = [0] p(less_leaves) = [0] p(minus) = [1] x1 + [0] p(nil) = [0] p(quot) = [0] p(reverse) = [1] x1 + [0] p(s) = [1] x1 + [0] p(shuffle) = [0] p(true) = [0] p(APP#) = [1] x2 + [1] p(CONCAT#) = [1] x1 + [0] p(LESS_LEAVES#) = [1] x1 + [1] x2 + [0] p(MINUS#) = [1] x1 + [2] x2 + [0] p(QUOT#) = [1] x1 + [0] p(REVERSE#) = [2] x1 + [2] p(SHUFFLE#) = [1] x1 + [0] p(app#) = [1] x1 + [4] x2 + [0] p(concat#) = [1] x2 + [1] p(less_leaves#) = [4] x1 + [1] p(minus#) = [1] x1 + [1] p(quot#) = [1] x1 + [1] x2 + [1] p(reverse#) = [1] p(shuffle#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [1] x1 + [4] p(c_4) = [4] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [4] p(c_9) = [0] p(c_10) = [1] x1 + [1] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [2] x2 + [1] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [4] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] x1 + [1] x2 + [2] x3 + [0] p(c_23) = [4] p(c_24) = [1] p(c_25) = [2] p(c_26) = [0] p(c_27) = [2] x2 + [1] p(c_28) = [4] x1 + [1] x2 + [2] p(c_29) = [1] p(c_30) = [1] x2 + [4] p(c_31) = [0] Following rules are strictly oriented: SHUFFLE#(add(z0,z1)) = [1] z1 + [1] > [1] z1 + [0] = c_15(SHUFFLE#(reverse(z1))) Following rules are (at-least) weakly oriented: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z1 + [1] z3 + [0] >= [1] z1 + [1] z3 + [0] = c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z1 + [1] z3 + [0] >= [1] z1 + [1] z3 + [0] = c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) QUOT#(s(z0),s(z1)) = [1] z0 + [0] >= [1] z0 + [0] = c_12(QUOT#(minus(z0,z1),s(z1))) app(add(z0,z1),z2) = [1] z1 + [1] z2 + [1] >= [1] z1 + [1] z2 + [1] = add(z0,app(z1,z2)) app(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 concat(cons(z0,z1),z2) = [1] z2 + [0] >= [1] z2 + [0] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 minus(z0,0()) = [1] z0 + [0] >= [1] z0 + [0] = z0 minus(s(z0),s(z1)) = [1] z0 + [0] >= [1] z0 + [0] = minus(z0,z1) reverse(add(z0,z1)) = [1] z1 + [1] >= [1] z1 + [1] = app(reverse(z1),add(z0,nil())) reverse(nil()) = [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:6.a:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_6(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> c_7(LESS_LEAVES#(concat(z0,z1),concat(z2,z3))) QUOT#(s(z0),s(z1)) -> c_12(QUOT#(minus(z0,z1),s(z1))) SHUFFLE#(add(z0,z1)) -> c_15(SHUFFLE#(reverse(z1))) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:6.b:1: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) and a lower component APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) Further, following extension rules are added to the lower component. CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) **** Step 1.b:6.b:1.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) -->_1 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):1 2:S:MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) -->_1 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):2 3:S:REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)) -->_2 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)):3 4:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) -->_1 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):1 5:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) -->_1 CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)):1 6:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)):6 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3):5 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1):4 7:W:QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) -->_1 MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)):2 8:W:QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) -->_1 QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)):8 -->_1 QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1):7 9:W:SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) -->_1 REVERSE#(add(z0,z1)) -> c_13(APP#(reverse(z1),add(z0,nil())),REVERSE#(z1)):3 10:W:SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) -->_1 SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)):10 -->_1 SHUFFLE#(add(z0,z1)) -> REVERSE#(z1):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: REVERSE#(add(z0,z1)) -> c_13(REVERSE#(z1)) **** Step 1.b:6.b:1.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(REVERSE#(z1)) - Weak DPs: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {concat,APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE#,app#,concat#,less_leaves#,minus#,quot# ,reverse#,shuffle#} TcT has computed the following interpretation: p(0) = [3] p(APP) = [1] x2 + [0] p(CONCAT) = [1] p(LESS_LEAVES) = [4] x1 + [0] p(MINUS) = [2] x2 + [2] p(QUOT) = [0] p(REVERSE) = [0] p(SHUFFLE) = [1] x1 + [2] p(add) = [1] p(app) = [4] x1 + [4] x2 + [0] p(c) = [2] p(c1) = [1] x1 + [1] p(c10) = [4] p(c11) = [1] p(c12) = [0] p(c13) = [2] p(c14) = [1] x1 + [1] x2 + [1] p(c15) = [1] x2 + [0] p(c2) = [0] p(c3) = [1] x2 + [1] p(c4) = [2] p(c5) = [1] x1 + [1] p(c6) = [1] p(c7) = [0] p(c8) = [1] p(c9) = [1] x2 + [0] p(concat) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [2] p(false) = [0] p(leaf) = [4] p(less_leaves) = [2] p(minus) = [2] x2 + [2] p(nil) = [2] p(quot) = [2] x1 + [0] p(reverse) = [1] p(s) = [0] p(shuffle) = [2] x1 + [1] p(true) = [2] p(APP#) = [1] x1 + [1] x2 + [1] p(CONCAT#) = [1] x1 + [5] p(LESS_LEAVES#) = [1] x1 + [4] x2 + [2] p(MINUS#) = [0] p(QUOT#) = [1] p(REVERSE#) = [1] p(SHUFFLE#) = [1] p(app#) = [0] p(concat#) = [1] p(less_leaves#) = [1] x2 + [0] p(minus#) = [0] p(quot#) = [1] x1 + [4] x2 + [1] p(reverse#) = [0] p(shuffle#) = [1] x1 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [2] p(c_5) = [2] p(c_6) = [2] x1 + [1] p(c_7) = [4] x1 + [0] p(c_8) = [0] p(c_9) = [4] p(c_10) = [2] x1 + [0] p(c_11) = [2] p(c_12) = [2] x2 + [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] p(c_15) = [1] x1 + [2] p(c_16) = [0] p(c_17) = [1] p(c_18) = [1] p(c_19) = [2] x1 + [2] p(c_20) = [1] p(c_21) = [2] p(c_22) = [2] x3 + [0] p(c_23) = [1] p(c_24) = [2] p(c_25) = [4] p(c_26) = [2] p(c_27) = [4] x1 + [1] p(c_28) = [2] x2 + [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [0] Following rules are strictly oriented: CONCAT#(cons(z0,z1),z2) = [1] z0 + [1] z1 + [7] > [1] z1 + [5] = c_3(CONCAT#(z1,z2)) Following rules are (at-least) weakly oriented: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [4] z2 + [4] z3 + [12] >= [1] z0 + [5] = CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [4] z2 + [4] z3 + [12] >= [1] z2 + [5] = CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [4] z2 + [4] z3 + [12] >= [1] z0 + [1] z1 + [4] z2 + [4] z3 + [2] = LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) = [0] >= [0] = c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) = [1] >= [0] = MINUS#(z0,z1) QUOT#(s(z0),s(z1)) = [1] >= [1] = QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) = [1] >= [1] = c_13(REVERSE#(z1)) SHUFFLE#(add(z0,z1)) = [1] >= [1] = REVERSE#(z1) SHUFFLE#(add(z0,z1)) = [1] >= [1] = SHUFFLE#(reverse(z1)) concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [2] >= [1] z0 + [1] z1 + [1] z2 + [2] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [4] >= [1] z0 + [0] = z0 **** Step 1.b:6.b:1.a:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) REVERSE#(add(z0,z1)) -> c_13(REVERSE#(z1)) - Weak DPs: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE#,app#,concat#,less_leaves#,minus#,quot#,reverse# ,shuffle#} TcT has computed the following interpretation: p(0) = [0] p(APP) = [0] p(CONCAT) = [0] p(LESS_LEAVES) = [0] p(MINUS) = [0] p(QUOT) = [0] p(REVERSE) = [0] p(SHUFFLE) = [0] p(add) = [1] x1 + [0] p(app) = [5] x1 + [7] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [0] p(c9) = [1] x1 + [1] x2 + [0] p(concat) = [0] p(cons) = [1] x2 + [0] p(false) = [0] p(leaf) = [0] p(less_leaves) = [0] p(minus) = [0] p(nil) = [0] p(quot) = [0] p(reverse) = [1] p(s) = [1] x1 + [4] p(shuffle) = [0] p(true) = [0] p(APP#) = [1] x1 + [0] p(CONCAT#) = [0] p(LESS_LEAVES#) = [0] p(MINUS#) = [1] x2 + [0] p(QUOT#) = [1] x2 + [4] p(REVERSE#) = [4] p(SHUFFLE#) = [6] p(app#) = [1] x2 + [1] p(concat#) = [4] x1 + [2] p(less_leaves#) = [2] x1 + [1] x2 + [4] p(minus#) = [1] x1 + [2] p(quot#) = [4] x1 + [1] x2 + [1] p(reverse#) = [2] x1 + [1] p(shuffle#) = [1] p(c_1) = [1] x1 + [1] p(c_2) = [2] p(c_3) = [4] x1 + [0] p(c_4) = [1] p(c_5) = [4] p(c_6) = [2] x1 + [1] p(c_7) = [1] x2 + [1] p(c_8) = [1] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [2] x2 + [1] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [1] x2 + [1] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] p(c_21) = [2] p(c_22) = [1] x1 + [4] p(c_23) = [0] p(c_24) = [1] p(c_25) = [0] p(c_26) = [4] p(c_27) = [0] p(c_28) = [1] x1 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [1] p(c_31) = [0] Following rules are strictly oriented: MINUS#(s(z0),s(z1)) = [1] z1 + [4] > [1] z1 + [0] = c_10(MINUS#(z0,z1)) Following rules are (at-least) weakly oriented: CONCAT#(cons(z0,z1),z2) = [0] >= [0] = c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [0] >= [0] = CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [0] >= [0] = CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [0] >= [0] = LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) QUOT#(s(z0),s(z1)) = [1] z1 + [8] >= [1] z1 + [0] = MINUS#(z0,z1) QUOT#(s(z0),s(z1)) = [1] z1 + [8] >= [1] z1 + [8] = QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) = [4] >= [4] = c_13(REVERSE#(z1)) SHUFFLE#(add(z0,z1)) = [6] >= [4] = REVERSE#(z1) SHUFFLE#(add(z0,z1)) = [6] >= [6] = SHUFFLE#(reverse(z1)) **** Step 1.b:6.b:1.a:4: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: REVERSE#(add(z0,z1)) -> c_13(REVERSE#(z1)) - Weak DPs: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_10) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {app,reverse,APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE#,app#,concat#,less_leaves#,minus# ,quot#,reverse#,shuffle#} TcT has computed the following interpretation: p(0) = [0] p(APP) = [0] p(CONCAT) = [0] p(LESS_LEAVES) = [0] p(MINUS) = [0] p(QUOT) = [0] p(REVERSE) = [0] p(SHUFFLE) = [0] p(add) = [1] x2 + [4] p(app) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [1] x1 + [0] p(c12) = [0] p(c13) = [0] p(c14) = [1] x1 + [1] x2 + [0] p(c15) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [0] p(c9) = [1] x1 + [1] x2 + [0] p(concat) = [2] x1 + [3] p(cons) = [1] x2 + [0] p(false) = [0] p(leaf) = [6] p(less_leaves) = [0] p(minus) = [4] x2 + [0] p(nil) = [0] p(quot) = [0] p(reverse) = [1] x1 + [4] p(s) = [1] x1 + [1] p(shuffle) = [0] p(true) = [0] p(APP#) = [0] p(CONCAT#) = [5] p(LESS_LEAVES#) = [6] p(MINUS#) = [0] p(QUOT#) = [1] p(REVERSE#) = [1] x1 + [0] p(SHUFFLE#) = [1] x1 + [0] p(app#) = [1] x2 + [0] p(concat#) = [4] x2 + [0] p(less_leaves#) = [0] p(minus#) = [1] x1 + [1] x2 + [2] p(quot#) = [1] x1 + [0] p(reverse#) = [0] p(shuffle#) = [0] p(c_1) = [2] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] x2 + [1] p(c_7) = [4] x1 + [2] x2 + [2] p(c_8) = [4] p(c_9) = [1] p(c_10) = [2] x1 + [0] p(c_11) = [0] p(c_12) = [1] x2 + [0] p(c_13) = [1] x1 + [2] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [4] x1 + [0] p(c_18) = [0] p(c_19) = [1] x1 + [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] x3 + [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [1] x2 + [0] p(c_28) = [1] x2 + [0] p(c_29) = [0] p(c_30) = [1] x1 + [0] p(c_31) = [0] Following rules are strictly oriented: REVERSE#(add(z0,z1)) = [1] z1 + [4] > [1] z1 + [2] = c_13(REVERSE#(z1)) Following rules are (at-least) weakly oriented: CONCAT#(cons(z0,z1),z2) = [5] >= [5] = c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [6] >= [5] = CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [6] >= [5] = CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) = [6] >= [6] = LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) = [0] >= [0] = c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) = [1] >= [0] = MINUS#(z0,z1) QUOT#(s(z0),s(z1)) = [1] >= [1] = QUOT#(minus(z0,z1),s(z1)) SHUFFLE#(add(z0,z1)) = [1] z1 + [4] >= [1] z1 + [0] = REVERSE#(z1) SHUFFLE#(add(z0,z1)) = [1] z1 + [4] >= [1] z1 + [4] = SHUFFLE#(reverse(z1)) app(add(z0,z1),z2) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = add(z0,app(z1,z2)) app(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 reverse(add(z0,z1)) = [1] z1 + [8] >= [1] z1 + [8] = app(reverse(z1),add(z0,nil())) reverse(nil()) = [4] >= [0] = nil() **** Step 1.b:6.b:1.a:5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: CONCAT#(cons(z0,z1),z2) -> c_3(CONCAT#(z1,z2)) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) -> c_10(MINUS#(z0,z1)) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) -> c_13(REVERSE#(z1)) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 1.b:6.b:1.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) - Weak DPs: CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 2:W:CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2) -->_1 CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2):2 3:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) -->_1 CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2):2 4:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) -->_1 CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2):2 5:W:LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)):5 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3):4 -->_1 LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1):3 6:W:MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1) -->_1 MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1):6 7:W:QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) -->_1 MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1):6 8:W:QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) -->_1 QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)):8 -->_1 QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1):7 9:W:REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) -->_1 APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)):1 10:W:REVERSE#(add(z0,z1)) -> REVERSE#(z1) -->_1 REVERSE#(add(z0,z1)) -> REVERSE#(z1):10 -->_1 REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())):9 11:W:SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) -->_1 REVERSE#(add(z0,z1)) -> REVERSE#(z1):10 -->_1 REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())):9 12:W:SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) -->_1 SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)):12 -->_1 SHUFFLE#(add(z0,z1)) -> REVERSE#(z1):11 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: QUOT#(s(z0),s(z1)) -> QUOT#(minus(z0,z1),s(z1)) 7: QUOT#(s(z0),s(z1)) -> MINUS#(z0,z1) 6: MINUS#(s(z0),s(z1)) -> MINUS#(z0,z1) 5: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> LESS_LEAVES#(concat(z0,z1),concat(z2,z3)) 4: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) 3: LESS_LEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) 2: CONCAT#(cons(z0,z1),z2) -> CONCAT#(z1,z2) **** Step 1.b:6.b:1.b:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) - Weak DPs: REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 minus(z0,0()) -> z0 minus(s(z0),s(z1)) -> minus(z0,z1) reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) **** Step 1.b:6.b:1.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) - Weak DPs: REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1} Following symbols are considered usable: {app,reverse,APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE#,app#,concat#,less_leaves#,minus# ,quot#,reverse#,shuffle#} TcT has computed the following interpretation: p(0) = [0] p(APP) = [0] p(CONCAT) = [0] p(LESS_LEAVES) = [0] p(MINUS) = [1] x2 + [0] p(QUOT) = [8] p(REVERSE) = [0] p(SHUFFLE) = [1] x1 + [2] p(add) = [1] x2 + [4] p(app) = [1] x1 + [1] x2 + [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c14) = [0] p(c15) = [0] p(c2) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [1] x1 + [1] x2 + [0] p(concat) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(false) = [0] p(leaf) = [0] p(less_leaves) = [0] p(minus) = [0] p(nil) = [0] p(quot) = [1] x1 + [0] p(reverse) = [1] x1 + [2] p(s) = [0] p(shuffle) = [0] p(true) = [0] p(APP#) = [4] x1 + [1] x2 + [8] p(CONCAT#) = [2] x1 + [1] x2 + [0] p(LESS_LEAVES#) = [2] x1 + [1] x2 + [0] p(MINUS#) = [1] x1 + [1] x2 + [0] p(QUOT#) = [1] x1 + [2] x2 + [0] p(REVERSE#) = [4] x1 + [4] p(SHUFFLE#) = [4] x1 + [5] p(app#) = [1] x1 + [1] x2 + [0] p(concat#) = [0] p(less_leaves#) = [1] x1 + [8] x2 + [0] p(minus#) = [0] p(quot#) = [1] x1 + [1] x2 + [0] p(reverse#) = [2] x1 + [0] p(shuffle#) = [8] p(c_1) = [1] x1 + [14] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x2 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [8] x1 + [0] p(c_16) = [0] p(c_17) = [1] x1 + [2] p(c_18) = [1] p(c_19) = [1] x1 + [2] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [2] x2 + [1] p(c_23) = [1] p(c_24) = [0] p(c_25) = [1] x1 + [2] p(c_26) = [1] p(c_27) = [1] x1 + [2] x2 + [0] p(c_28) = [1] x1 + [0] p(c_29) = [1] p(c_30) = [1] x1 + [1] x2 + [2] p(c_31) = [0] Following rules are strictly oriented: APP#(add(z0,z1),z2) = [4] z1 + [1] z2 + [24] > [4] z1 + [1] z2 + [22] = c_1(APP#(z1,z2)) Following rules are (at-least) weakly oriented: REVERSE#(add(z0,z1)) = [4] z1 + [20] >= [4] z1 + [20] = APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) = [4] z1 + [20] >= [4] z1 + [4] = REVERSE#(z1) SHUFFLE#(add(z0,z1)) = [4] z1 + [21] >= [4] z1 + [4] = REVERSE#(z1) SHUFFLE#(add(z0,z1)) = [4] z1 + [21] >= [4] z1 + [13] = SHUFFLE#(reverse(z1)) app(add(z0,z1),z2) = [1] z1 + [1] z2 + [4] >= [1] z1 + [1] z2 + [4] = add(z0,app(z1,z2)) app(nil(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 reverse(add(z0,z1)) = [1] z1 + [6] >= [1] z1 + [6] = app(reverse(z1),add(z0,nil())) reverse(nil()) = [2] >= [0] = nil() **** Step 1.b:6.b:1.b:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: APP#(add(z0,z1),z2) -> c_1(APP#(z1,z2)) REVERSE#(add(z0,z1)) -> APP#(reverse(z1),add(z0,nil())) REVERSE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> REVERSE#(z1) SHUFFLE#(add(z0,z1)) -> SHUFFLE#(reverse(z1)) - Weak TRS: app(add(z0,z1),z2) -> add(z0,app(z1,z2)) app(nil(),z0) -> z0 reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil())) reverse(nil()) -> nil() - Signature: {APP/2,CONCAT/2,LESS_LEAVES/2,MINUS/2,QUOT/2,REVERSE/1,SHUFFLE/1,app/2,concat/2,less_leaves/2,minus/2,quot/2 ,reverse/1,shuffle/1,APP#/2,CONCAT#/2,LESS_LEAVES#/2,MINUS#/2,QUOT#/2,REVERSE#/1,SHUFFLE#/1,app#/2,concat#/2 ,less_leaves#/2,minus#/2,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,c/0,c1/1,c10/0,c11/1,c12/0,c13/0,c14/2 ,c15/2,c2/0,c3/2,c4/0,c5/1,c6/0,c7/2,c8/0,c9/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1 ,c_4/0,c_5/0,c_6/2,c_7/2,c_8/0,c_9/0,c_10/1,c_11/0,c_12/2,c_13/2,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/1 ,c_20/0,c_21/0,c_22/3,c_23/0,c_24/0,c_25/1,c_26/0,c_27/2,c_28/2,c_29/0,c_30/2,c_31/0} - Obligation: innermost runtime complexity wrt. defined symbols {APP#,CONCAT#,LESS_LEAVES#,MINUS#,QUOT#,REVERSE#,SHUFFLE# ,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#} and constructors {0,add,c,c1,c10,c11,c12,c13,c14 ,c15,c2,c3,c4,c5,c6,c7,c8,c9,cons,false,leaf,nil,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))