MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) perfectp(0()) -> false() perfectp(s(x)) -> f(x,s(0()),s(x),s(x)) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,if,le,minus,perfectp} and constructors {0,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(0(),y,0(),u) -> c_1() f#(0(),y,s(z),u) -> c_2() f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() le#(0(),y) -> c_7() le#(s(x),0()) -> c_8() le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(0(),y) -> c_10() minus#(s(x),0()) -> c_11() minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(0()) -> c_13() perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(0(),y,0(),u) -> c_1() f#(0(),y,s(z),u) -> c_2() f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() le#(0(),y) -> c_7() le#(s(x),0()) -> c_8() le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(0(),y) -> c_10() minus#(s(x),0()) -> c_11() minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(0()) -> c_13() perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) perfectp(0()) -> false() perfectp(s(x)) -> f(x,s(0()),s(x),s(x)) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/5,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) f#(0(),y,0(),u) -> c_1() f#(0(),y,s(z),u) -> c_2() f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() le#(0(),y) -> c_7() le#(s(x),0()) -> c_8() le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(0(),y) -> c_10() minus#(s(x),0()) -> c_11() minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(0()) -> c_13() perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(0(),y,0(),u) -> c_1() f#(0(),y,s(z),u) -> c_2() f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() le#(0(),y) -> c_7() le#(s(x),0()) -> c_8() le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(0(),y) -> c_10() minus#(s(x),0()) -> c_11() minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(0()) -> c_13() perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/5,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,6,7,8,10,11,13} by application of Pre({1,2,5,6,7,8,10,11,13}) = {3,4,9,12,14}. Here rules are labelled as follows: 1: f#(0(),y,0(),u) -> c_1() 2: f#(0(),y,s(z),u) -> c_2() 3: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) 4: f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) 5: if#(false(),x,y) -> c_5() 6: if#(true(),x,y) -> c_6() 7: le#(0(),y) -> c_7() 8: le#(s(x),0()) -> c_8() 9: le#(s(x),s(y)) -> c_9(le#(x,y)) 10: minus#(0(),y) -> c_10() 11: minus#(s(x),0()) -> c_11() 12: minus#(s(x),s(y)) -> c_12(minus#(x,y)) 13: perfectp#(0()) -> c_13() 14: perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak DPs: f#(0(),y,0(),u) -> c_1() f#(0(),y,s(z),u) -> c_2() if#(false(),x,y) -> c_5() if#(true(),x,y) -> c_6() le#(0(),y) -> c_7() le#(s(x),0()) -> c_8() minus#(0(),y) -> c_10() minus#(s(x),0()) -> c_11() perfectp#(0()) -> c_13() - Weak TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/5,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) -->_2 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_2 minus#(0(),y) -> c_10():12 -->_1 f#(0(),y,s(z),u) -> c_2():7 -->_1 f#(0(),y,0(),u) -> c_1():6 -->_1 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 2:S:f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) -->_4 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_2 le#(s(x),s(y)) -> c_9(le#(x,y)):3 -->_4 minus#(s(x),0()) -> c_11():13 -->_4 minus#(0(),y) -> c_10():12 -->_2 le#(s(x),0()) -> c_8():11 -->_2 le#(0(),y) -> c_7():10 -->_1 if#(true(),x,y) -> c_6():9 -->_1 if#(false(),x,y) -> c_5():8 -->_5 f#(0(),y,s(z),u) -> c_2():7 -->_5 f#(0(),y,0(),u) -> c_1():6 -->_5 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_3 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_5 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 -->_3 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 3:S:le#(s(x),s(y)) -> c_9(le#(x,y)) -->_1 le#(s(x),0()) -> c_8():11 -->_1 le#(0(),y) -> c_7():10 -->_1 le#(s(x),s(y)) -> c_9(le#(x,y)):3 4:S:minus#(s(x),s(y)) -> c_12(minus#(x,y)) -->_1 minus#(s(x),0()) -> c_11():13 -->_1 minus#(0(),y) -> c_10():12 -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 5:S:perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) -->_1 f#(0(),y,s(z),u) -> c_2():7 -->_1 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 6:W:f#(0(),y,0(),u) -> c_1() 7:W:f#(0(),y,s(z),u) -> c_2() 8:W:if#(false(),x,y) -> c_5() 9:W:if#(true(),x,y) -> c_6() 10:W:le#(0(),y) -> c_7() 11:W:le#(s(x),0()) -> c_8() 12:W:minus#(0(),y) -> c_10() 13:W:minus#(s(x),0()) -> c_11() 14:W:perfectp#(0()) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: perfectp#(0()) -> c_13() 6: f#(0(),y,0(),u) -> c_1() 7: f#(0(),y,s(z),u) -> c_2() 8: if#(false(),x,y) -> c_5() 9: if#(true(),x,y) -> c_6() 10: le#(0(),y) -> c_7() 11: le#(s(x),0()) -> c_8() 12: minus#(0(),y) -> c_10() 13: minus#(s(x),0()) -> c_11() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/5,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) -->_2 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_1 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 2:S:f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)) -->_4 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_2 le#(s(x),s(y)) -> c_9(le#(x,y)):3 -->_5 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_3 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 -->_5 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 -->_3 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 3:S:le#(s(x),s(y)) -> c_9(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_9(le#(x,y)):3 4:S:minus#(s(x),s(y)) -> c_12(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 5:S:perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) -->_1 f#(s(x),s(y),z,u) -> c_4(if#(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) ,le#(x,y) ,f#(s(x),minus(y,x),z,u) ,minus#(y,x) ,f#(x,u,z,u)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) if(false(),x,y) -> y if(true(),x,y) -> x le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) - Weak TRS: minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) -->_2 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)):2 -->_1 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 2:S:f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) -->_3 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 le#(s(x),s(y)) -> c_9(le#(x,y)):3 -->_4 f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)):2 -->_2 f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)):2 -->_4 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 -->_2 f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))):1 3:S:le#(s(x),s(y)) -> c_9(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_9(le#(x,y)):3 4:S:minus#(s(x),s(y)) -> c_12(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 5:S:perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))) -->_1 f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)):2 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). [(5,perfectp#(s(x)) -> c_14(f#(x,s(0()),s(x),s(x))))] * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: f#(s(x),0(),z,u) -> c_3(f#(x,u,minus(z,s(x)),u),minus#(z,s(x))) f#(s(x),s(y),z,u) -> c_4(le#(x,y),f#(s(x),minus(y,x),z,u),minus#(y,x),f#(x,u,z,u)) le#(s(x),s(y)) -> c_9(le#(x,y)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) - Weak TRS: minus(0(),y) -> 0() minus(s(x),0()) -> s(x) minus(s(x),s(y)) -> minus(x,y) - Signature: {f/4,if/3,le/2,minus/2,perfectp/1,f#/4,if#/3,le#/2,minus#/2,perfectp#/1} / {0/0,false/0,s/1,true/0,c_1/0 ,c_2/0,c_3/2,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,if#,le#,minus#,perfectp#} and constructors {0,false,s ,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE