MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(x,0(),0()) -> s(x) f(0(),y,0()) -> s(y) f(0(),0(),z) -> s(z) f(0(),s(0()),s(0())) -> s(s(0())) f(0(),s(0()),s(s(z))) -> f(0(),s(0()),z) f(0(),s(s(y)),s(0())) -> f(0(),y,s(0())) f(0(),s(s(y)),s(s(z))) -> f(0(),y,f(0(),s(s(y)),s(z))) f(s(x),0(),s(z)) -> f(x,s(0()),z) f(s(x),s(y),0()) -> f(x,y,s(0())) f(s(x),s(y),s(z)) -> f(x,y,f(s(x),s(y),z)) f(s(0()),y,z) -> f(0(),s(y),s(z)) - Signature: {f/3} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {0,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(x,0(),0()) -> c_1() f#(0(),y,0()) -> c_2() f#(0(),0(),z) -> c_3() f#(0(),s(0()),s(0())) -> c_4() f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(x,0(),0()) -> c_1() f#(0(),y,0()) -> c_2() f#(0(),0(),z) -> c_3() f#(0(),s(0()),s(0())) -> c_4() f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) - Weak TRS: f(x,0(),0()) -> s(x) f(0(),y,0()) -> s(y) f(0(),0(),z) -> s(z) f(0(),s(0()),s(0())) -> s(s(0())) f(0(),s(0()),s(s(z))) -> f(0(),s(0()),z) f(0(),s(s(y)),s(0())) -> f(0(),y,s(0())) f(0(),s(s(y)),s(s(z))) -> f(0(),y,f(0(),s(s(y)),s(z))) f(s(x),0(),s(z)) -> f(x,s(0()),z) f(s(x),s(y),0()) -> f(x,y,s(0())) f(s(x),s(y),s(z)) -> f(x,y,f(s(x),s(y),z)) f(s(0()),y,z) -> f(0(),s(y),s(z)) - Signature: {f/3,f#/3} / {0/0,s/1,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/1,c_9/1,c_10/2,c_11/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {0,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4} by application of Pre({1,2,3,4}) = {5,6,7,8,9,10,11}. Here rules are labelled as follows: 1: f#(x,0(),0()) -> c_1() 2: f#(0(),y,0()) -> c_2() 3: f#(0(),0(),z) -> c_3() 4: f#(0(),s(0()),s(0())) -> c_4() 5: f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) 6: f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) 7: f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) 8: f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) 9: f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) 10: f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) 11: f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) - Weak DPs: f#(x,0(),0()) -> c_1() f#(0(),y,0()) -> c_2() f#(0(),0(),z) -> c_3() f#(0(),s(0()),s(0())) -> c_4() - Weak TRS: f(x,0(),0()) -> s(x) f(0(),y,0()) -> s(y) f(0(),0(),z) -> s(z) f(0(),s(0()),s(0())) -> s(s(0())) f(0(),s(0()),s(s(z))) -> f(0(),s(0()),z) f(0(),s(s(y)),s(0())) -> f(0(),y,s(0())) f(0(),s(s(y)),s(s(z))) -> f(0(),y,f(0(),s(s(y)),s(z))) f(s(x),0(),s(z)) -> f(x,s(0()),z) f(s(x),s(y),0()) -> f(x,y,s(0())) f(s(x),s(y),s(z)) -> f(x,y,f(s(x),s(y),z)) f(s(0()),y,z) -> f(0(),s(y),s(z)) - Signature: {f/3,f#/3} / {0/0,s/1,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/1,c_9/1,c_10/2,c_11/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),y,0()) -> c_2():9 -->_1 f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)):1 2:S:f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),0(),z) -> c_3():10 -->_1 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 3:S:f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),0(),z) -> c_3():10 -->_1 f#(0(),y,0()) -> c_2():9 -->_1 f#(x,0(),0()) -> c_1():8 -->_2 f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))):3 -->_1 f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))):3 -->_2 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 -->_1 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 -->_1 f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)):1 4:S:f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) -->_1 f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))):7 -->_1 f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)):6 -->_1 f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))):5 -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),y,0()) -> c_2():9 -->_1 f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)):1 5:S:f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) -->_1 f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))):7 -->_1 f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)):6 -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),0(),z) -> c_3():10 -->_1 f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)):4 -->_1 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 6:S:f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) -->_2 f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))):7 -->_1 f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))):7 -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),0(),z) -> c_3():10 -->_1 f#(0(),y,0()) -> c_2():9 -->_1 f#(x,0(),0()) -> c_1():8 -->_2 f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)):6 -->_1 f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)):6 -->_2 f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))):5 -->_1 f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))):5 -->_1 f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)):4 -->_1 f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))):3 -->_1 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 -->_1 f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)):1 7:S:f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) -->_1 f#(0(),s(0()),s(0())) -> c_4():11 -->_1 f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))):3 -->_1 f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))):2 -->_1 f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)):1 8:W:f#(x,0(),0()) -> c_1() 9:W:f#(0(),y,0()) -> c_2() 10:W:f#(0(),0(),z) -> c_3() 11:W:f#(0(),s(0()),s(0())) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: f#(x,0(),0()) -> c_1() 10: f#(0(),0(),z) -> c_3() 9: f#(0(),y,0()) -> c_2() 11: f#(0(),s(0()),s(0())) -> c_4() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: f#(0(),s(0()),s(s(z))) -> c_5(f#(0(),s(0()),z)) f#(0(),s(s(y)),s(0())) -> c_6(f#(0(),y,s(0()))) f#(0(),s(s(y)),s(s(z))) -> c_7(f#(0(),y,f(0(),s(s(y)),s(z))),f#(0(),s(s(y)),s(z))) f#(s(x),0(),s(z)) -> c_8(f#(x,s(0()),z)) f#(s(x),s(y),0()) -> c_9(f#(x,y,s(0()))) f#(s(x),s(y),s(z)) -> c_10(f#(x,y,f(s(x),s(y),z)),f#(s(x),s(y),z)) f#(s(0()),y,z) -> c_11(f#(0(),s(y),s(z))) - Weak TRS: f(x,0(),0()) -> s(x) f(0(),y,0()) -> s(y) f(0(),0(),z) -> s(z) f(0(),s(0()),s(0())) -> s(s(0())) f(0(),s(0()),s(s(z))) -> f(0(),s(0()),z) f(0(),s(s(y)),s(0())) -> f(0(),y,s(0())) f(0(),s(s(y)),s(s(z))) -> f(0(),y,f(0(),s(s(y)),s(z))) f(s(x),0(),s(z)) -> f(x,s(0()),z) f(s(x),s(y),0()) -> f(x,y,s(0())) f(s(x),s(y),s(z)) -> f(x,y,f(s(x),s(y),z)) f(s(0()),y,z) -> f(0(),s(y),s(z)) - Signature: {f/3,f#/3} / {0/0,s/1,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/2,c_8/1,c_9/1,c_10/2,c_11/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE