MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) double(x) -> permute(x,x,a()) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x permute(x,y,a()) -> permute(isZero(x),x,b()) permute(y,x,c()) -> s(s(permute(x,y,a()))) permute(false(),x,b()) -> permute(ack(x,x),p(x),c()) permute(true(),x,b()) -> 0() plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2} / {0/0,a/0,b/0,c/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ack,double,isZero,p,permute,plus} and constructors {0,a,b ,c,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) isZero#(0()) -> c_5() isZero#(s(x)) -> c_6() p#(0()) -> c_7() p#(s(x)) -> c_8() permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) permute#(true(),x,b()) -> c_12() plus#(x,0()) -> c_13() plus#(x,s(0())) -> c_14() plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(0(),y) -> c_16() plus#(s(x),y) -> c_17(plus#(x,s(y))) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) isZero#(0()) -> c_5() isZero#(s(x)) -> c_6() p#(0()) -> c_7() p#(s(x)) -> c_8() permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) permute#(true(),x,b()) -> c_12() plus#(x,0()) -> c_13() plus#(x,s(0())) -> c_14() plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(0(),y) -> c_16() plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) double(x) -> permute(x,x,a()) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x permute(x,y,a()) -> permute(isZero(x),x,b()) permute(y,x,c()) -> s(s(permute(x,y,a()))) permute(false(),x,b()) -> permute(ack(x,x),p(x),c()) permute(true(),x,b()) -> 0() plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/2,c_10/1,c_11/3,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) isZero#(0()) -> c_5() isZero#(s(x)) -> c_6() p#(0()) -> c_7() p#(s(x)) -> c_8() permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) permute#(true(),x,b()) -> c_12() plus#(x,0()) -> c_13() plus#(x,s(0())) -> c_14() plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(0(),y) -> c_16() plus#(s(x),y) -> c_17(plus#(x,s(y))) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) isZero#(0()) -> c_5() isZero#(s(x)) -> c_6() p#(0()) -> c_7() p#(s(x)) -> c_8() permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) permute#(true(),x,b()) -> c_12() plus#(x,0()) -> c_13() plus#(x,s(0())) -> c_14() plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(0(),y) -> c_16() plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/2,c_10/1,c_11/3,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5,6,7,8,12,13,14,16} by application of Pre({5,6,7,8,12,13,14,16}) = {1,9,11,15,17}. Here rules are labelled as follows: 1: ack#(0(),x) -> c_1(plus#(x,s(0()))) 2: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) 3: ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) 4: double#(x) -> c_4(permute#(x,x,a())) 5: isZero#(0()) -> c_5() 6: isZero#(s(x)) -> c_6() 7: p#(0()) -> c_7() 8: p#(s(x)) -> c_8() 9: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) 10: permute#(y,x,c()) -> c_10(permute#(x,y,a())) 11: permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) 12: permute#(true(),x,b()) -> c_12() 13: plus#(x,0()) -> c_13() 14: plus#(x,s(0())) -> c_14() 15: plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) 16: plus#(0(),y) -> c_16() 17: plus#(s(x),y) -> c_17(plus#(x,s(y))) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak DPs: isZero#(0()) -> c_5() isZero#(s(x)) -> c_6() p#(0()) -> c_7() p#(s(x)) -> c_8() permute#(true(),x,b()) -> c_12() plus#(x,0()) -> c_13() plus#(x,s(0())) -> c_14() plus#(0(),y) -> c_16() - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/2,c_10/1,c_11/3,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ack#(0(),x) -> c_1(plus#(x,s(0()))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(0(),y) -> c_16():17 -->_1 plus#(x,s(0())) -> c_14():16 2:S:ack#(s(x),0()) -> c_2(ack#(x,s(0()))) -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 3:S:ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 4:S:double#(x) -> c_4(permute#(x,x,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)):5 5:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)):7 -->_1 permute#(true(),x,b()) -> c_12():14 -->_2 isZero#(s(x)) -> c_6():11 -->_2 isZero#(0()) -> c_5():10 6:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)):5 7:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) -->_3 p#(s(x)) -> c_8():13 -->_3 p#(0()) -> c_7():12 -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):6 -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 8:S:plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(0())) -> c_14():16 -->_1 plus#(x,0()) -> c_13():15 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 9:S:plus#(s(x),y) -> c_17(plus#(x,s(y))) -->_1 plus#(0(),y) -> c_16():17 -->_1 plus#(x,s(0())) -> c_14():16 -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 10:W:isZero#(0()) -> c_5() 11:W:isZero#(s(x)) -> c_6() 12:W:p#(0()) -> c_7() 13:W:p#(s(x)) -> c_8() 14:W:permute#(true(),x,b()) -> c_12() 15:W:plus#(x,0()) -> c_13() 16:W:plus#(x,s(0())) -> c_14() 17:W:plus#(0(),y) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: isZero#(0()) -> c_5() 11: isZero#(s(x)) -> c_6() 14: permute#(true(),x,b()) -> c_12() 12: p#(0()) -> c_7() 13: p#(s(x)) -> c_8() 15: plus#(x,0()) -> c_13() 16: plus#(x,s(0())) -> c_14() 17: plus#(0(),y) -> c_16() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/2,c_10/1,c_11/3,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ack#(0(),x) -> c_1(plus#(x,s(0()))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 2:S:ack#(s(x),0()) -> c_2(ack#(x,s(0()))) -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 3:S:ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 4:S:double#(x) -> c_4(permute#(x,x,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)):5 5:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)):7 6:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b()),isZero#(x)):5 7:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x),p#(x)) -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):6 -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 8:S:plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 9:S:plus#(s(x),y) -> c_17(plus#(x,s(y))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) double#(x) -> c_4(permute#(x,x,a())) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:ack#(0(),x) -> c_1(plus#(x,s(0()))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 2:S:ack#(s(x),0()) -> c_2(ack#(x,s(0()))) -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 3:S:ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):2 -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 4:S:double#(x) -> c_4(permute#(x,x,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())):5 5:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)):7 6:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())):5 7:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):6 -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):3 -->_2 ack#(0(),x) -> c_1(plus#(x,s(0()))):1 8:S:plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 9:S:plus#(s(x),y) -> c_17(plus#(x,s(y))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):9 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):8 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(4,double#(x) -> c_4(permute#(x,x,a())))] * Step 7: Decompose MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0 ,a/0,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} Problem (S) - Strict DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0 ,a/0,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} ** Step 7.a:1: Failure MAYBE + Considered Problem: - Strict DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 7.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak DPs: ack#(0(),x) -> c_1(plus#(x,s(0()))) plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) plus#(s(x),y) -> c_17(plus#(x,s(y))) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ack#(s(x),0()) -> c_2(ack#(x,s(0()))) -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):6 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):2 2:S:ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) -->_1 ack#(0(),x) -> c_1(plus#(x,s(0()))):6 -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):2 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):2 -->_2 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):1 -->_1 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):1 3:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)):5 4:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())):3 5:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) -->_2 ack#(0(),x) -> c_1(plus#(x,s(0()))):6 -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):4 -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):2 6:W:ack#(0(),x) -> c_1(plus#(x,s(0()))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):8 7:W:plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):8 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):7 8:W:plus#(s(x),y) -> c_17(plus#(x,s(y))) -->_1 plus#(s(x),y) -> c_17(plus#(x,s(y))):8 -->_1 plus#(x,s(s(y))) -> c_15(plus#(s(x),y)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: ack#(0(),x) -> c_1(plus#(x,s(0()))) 8: plus#(s(x),y) -> c_17(plus#(x,s(y))) 7: plus#(x,s(s(y))) -> c_15(plus#(s(x),y)) ** Step 7.b:2: Decompose MAYBE + Considered Problem: - Strict DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) - Weak DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0 ,a/0,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} Problem (S) - Strict DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0 ,a/0,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} *** Step 7.b:2.a:1: Failure MAYBE + Considered Problem: - Strict DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) - Weak DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. *** Step 7.b:2.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak DPs: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)):3 2:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())):1 3:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):5 -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):2 4:W:ack#(s(x),0()) -> c_2(ack#(x,s(0()))) -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):5 5:W:ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) -->_2 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):5 -->_1 ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)):5 -->_2 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):4 -->_1 ack#(s(x),0()) -> c_2(ack#(x,s(0()))):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: ack#(s(x),s(y)) -> c_3(ack#(x,ack(s(x),y)),ack#(s(x),y)) 4: ack#(s(x),0()) -> c_2(ack#(x,s(0()))) *** Step 7.b:2.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/2,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) -->_1 permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)):3 2:S:permute#(y,x,c()) -> c_10(permute#(x,y,a())) -->_1 permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())):1 3:S:permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c()),ack#(x,x)) -->_1 permute#(y,x,c()) -> c_10(permute#(x,y,a())):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c())) *** Step 7.b:2.b:3: Failure MAYBE + Considered Problem: - Strict DPs: permute#(x,y,a()) -> c_9(permute#(isZero(x),x,b())) permute#(y,x,c()) -> c_10(permute#(x,y,a())) permute#(false(),x,b()) -> c_11(permute#(ack(x,x),p(x),c())) - Weak TRS: ack(0(),x) -> plus(x,s(0())) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) isZero(0()) -> true() isZero(s(x)) -> false() p(0()) -> 0() p(s(x)) -> x plus(x,0()) -> x plus(x,s(0())) -> s(x) plus(x,s(s(y))) -> s(plus(s(x),y)) plus(0(),y) -> y plus(s(x),y) -> plus(x,s(y)) - Signature: {ack/2,double/1,isZero/1,p/1,permute/3,plus/2,ack#/2,double#/1,isZero#/1,p#/1,permute#/3,plus#/2} / {0/0,a/0 ,b/0,c/0,false/0,s/1,true/0,c_1/1,c_2/1,c_3/2,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/0 ,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack#,double#,isZero#,p#,permute# ,plus#} and constructors {0,a,b,c,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE