MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1} / {0/0,A/0,B/0,C/0,s/1,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',fold,foldB,foldC,g} and constructors {0,A,B,C,s ,triple} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f'#(triple(a,b,c),C()) -> c_4() f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) fold#(t,x,0()) -> c_6() fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) foldB#(t,0()) -> c_8() foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,0()) -> c_10() foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) g#(A()) -> c_12() g#(B()) -> c_13() g#(B()) -> c_14() g#(C()) -> c_15() g#(C()) -> c_16() g#(C()) -> c_17() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f'#(triple(a,b,c),C()) -> c_4() f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) fold#(t,x,0()) -> c_6() fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) foldB#(t,0()) -> c_8() foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,0()) -> c_10() foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) g#(A()) -> c_12() g#(B()) -> c_13() g#(B()) -> c_14() g#(C()) -> c_15() g#(C()) -> c_16() g#(C()) -> c_17() - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,6,8,10,12,13,14,15,16,17} by application of Pre({4,6,8,10,12,13,14,15,16,17}) = {1,2,5,7,9,11}. Here rules are labelled as follows: 1: f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) 2: f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) 3: f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) 4: f'#(triple(a,b,c),C()) -> c_4() 5: f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) 6: fold#(t,x,0()) -> c_6() 7: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) 8: foldB#(t,0()) -> c_8() 9: foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) 10: foldC#(t,0()) -> c_10() 11: foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) 12: g#(A()) -> c_12() 13: g#(B()) -> c_13() 14: g#(B()) -> c_14() 15: g#(C()) -> c_15() 16: g#(C()) -> c_16() 17: g#(C()) -> c_17() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak DPs: f'#(triple(a,b,c),C()) -> c_4() fold#(t,x,0()) -> c_6() foldB#(t,0()) -> c_8() foldC#(t,0()) -> c_10() g#(A()) -> c_12() g#(B()) -> c_13() g#(B()) -> c_14() g#(C()) -> c_15() g#(C()) -> c_16() g#(C()) -> c_17() - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) -->_1 f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())):3 -->_1 f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)):2 -->_2 g#(C()) -> c_17():17 -->_2 g#(C()) -> c_16():16 -->_2 g#(C()) -> c_15():15 -->_2 g#(B()) -> c_14():14 -->_2 g#(B()) -> c_13():13 -->_2 g#(A()) -> c_12():12 -->_1 f'#(triple(a,b,c),C()) -> c_4():8 2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)):4 -->_2 foldB#(t,0()) -> c_8():10 3:S:f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 4:S:f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) -->_1 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 -->_1 foldC#(t,0()) -> c_10():11 5:S:fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) -->_2 fold#(t,x,0()) -> c_6():9 -->_2 fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)):5 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 6:S:foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) -->_2 foldB#(t,0()) -> c_8():10 -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 7:S:foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) -->_2 foldC#(t,0()) -> c_10():11 -->_2 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 8:W:f'#(triple(a,b,c),C()) -> c_4() 9:W:fold#(t,x,0()) -> c_6() 10:W:foldB#(t,0()) -> c_8() 11:W:foldC#(t,0()) -> c_10() 12:W:g#(A()) -> c_12() 13:W:g#(B()) -> c_13() 14:W:g#(B()) -> c_14() 15:W:g#(C()) -> c_15() 16:W:g#(C()) -> c_16() 17:W:g#(C()) -> c_17() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: fold#(t,x,0()) -> c_6() 8: f'#(triple(a,b,c),C()) -> c_4() 12: g#(A()) -> c_12() 13: g#(B()) -> c_13() 14: g#(B()) -> c_14() 15: g#(C()) -> c_15() 16: g#(C()) -> c_16() 17: g#(C()) -> c_17() 11: foldC#(t,0()) -> c_10() 10: foldB#(t,0()) -> c_8() * Step 4: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/2,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(t,x) -> c_1(f'#(t,g(x)),g#(x)) -->_1 f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())):3 -->_1 f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)):2 2:S:f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)):4 3:S:f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 4:S:f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) -->_1 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 5:S:fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) -->_2 fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)):5 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 6:S:foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 7:S:foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) -->_2 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 -->_1 f#(t,x) -> c_1(f'#(t,g(x)),g#(x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(t,x) -> c_1(f'#(t,g(x))) * Step 5: Decompose MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + 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: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0 ,B/0,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0 ,A,B,C,s,triple} Problem (S) - Strict DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak DPs: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0 ,B/0,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0 ,c_14/0,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0 ,A,B,C,s,triple} ** Step 5.a:1: DecomposeDG MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) and a lower component f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) Further, following extension rules are added to the lower component. fold#(t,x,s(n)) -> f#(fold(t,x,n),x) fold#(t,x,s(n)) -> fold#(t,x,n) *** Step 5.a:1.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) The strictly oriented rules are moved into the weak component. **** Step 5.a:1.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1,2} Following symbols are considered usable: {f#,f'#,f''#,fold#,foldB#,foldC#,g#} TcT has computed the following interpretation: p(0) = [0] p(A) = [0] p(B) = [0] p(C) = [0] p(f) = [11] p(f') = [3] x2 + [0] p(f'') = [3] x1 + [0] p(fold) = [0] p(foldB) = [7] p(foldC) = [2] x1 + [9] p(g) = [9] p(s) = [1] x1 + [8] p(triple) = [1] x1 + [1] x2 + [0] p(f#) = [1] p(f'#) = [1] x2 + [0] p(f''#) = [1] x1 + [0] p(fold#) = [12] x1 + [4] x2 + [2] x3 + [12] p(foldB#) = [0] p(foldC#) = [1] x1 + [4] x2 + [0] p(g#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [1] x2 + [0] p(c_3) = [4] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [2] p(c_7) = [2] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [4] x1 + [0] p(c_10) = [0] p(c_11) = [1] x1 + [1] x2 + [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] Following rules are strictly oriented: fold#(t,x,s(n)) = [2] n + [12] t + [4] x + [28] > [2] n + [12] t + [4] x + [14] = c_7(f#(fold(t,x,n),x),fold#(t,x,n)) Following rules are (at-least) weakly oriented: **** Step 5.a:1.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 5.a:1.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) -->_2 fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) **** Step 5.a:1.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 5.a:1.b:1: Failure MAYBE + Considered Problem: - Strict DPs: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak DPs: fold#(t,x,s(n)) -> f#(fold(t,x,n),x) fold#(t,x,s(n)) -> fold#(t,x,n) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak DPs: f#(t,x) -> c_1(f'#(t,g(x))) f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) -->_1 f#(t,x) -> c_1(f'#(t,g(x))):2 -->_2 fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)):1 2:W:f#(t,x) -> c_1(f'#(t,g(x))) -->_1 f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())):4 -->_1 f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)):3 3:W:f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)):5 4:W:f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) -->_1 f#(t,x) -> c_1(f'#(t,g(x))):2 5:W:f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) -->_1 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 6:W:foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) -->_2 foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)):6 -->_1 f#(t,x) -> c_1(f'#(t,g(x))):2 7:W:foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) -->_2 foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)):7 -->_1 f#(t,x) -> c_1(f'#(t,g(x))):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: f#(t,x) -> c_1(f'#(t,g(x))) 7: foldC#(t,s(n)) -> c_11(f#(foldC(t,n),C()),foldC#(t,n)) 5: f''#(triple(a,b,c)) -> c_5(foldC#(triple(a,b,0()),c)) 3: f'#(triple(a,b,c),A()) -> c_2(f''#(foldB(triple(s(a),0(),c),b)),foldB#(triple(s(a),0(),c),b)) 6: foldB#(t,s(n)) -> c_9(f#(foldB(t,n),B()),foldB#(t,n)) 4: f'#(triple(a,b,c),B()) -> c_3(f#(triple(a,b,c),A())) ** Step 5.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)) -->_2 fold#(t,x,s(n)) -> c_7(f#(fold(t,x,n),x),fold#(t,x,n)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) ** Step 5.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldB(triple(s(a),0(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,s(c)) f''(triple(a,b,c)) -> foldC(triple(a,b,0()),c) fold(t,x,0()) -> t fold(t,x,s(n)) -> f(fold(t,x,n),x) foldB(t,0()) -> t foldB(t,s(n)) -> f(foldB(t,n),B()) foldC(t,0()) -> t foldC(t,s(n)) -> f(foldC(t,n),C()) g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) ** Step 5.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) The strictly oriented rules are moved into the weak component. *** Step 5.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {f#,f'#,f''#,fold#,foldB#,foldC#,g#} TcT has computed the following interpretation: p(0) = [0] p(A) = [0] p(B) = [0] p(C) = [0] p(f) = [0] p(f') = [0] p(f'') = [1] x1 + [0] p(fold) = [0] p(foldB) = [0] p(foldC) = [0] p(g) = [0] p(s) = [1] x1 + [4] p(triple) = [1] x1 + [1] x2 + [1] x3 + [0] p(f#) = [0] p(f'#) = [0] p(f''#) = [0] p(fold#) = [4] x3 + [0] p(foldB#) = [0] p(foldC#) = [0] p(g#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] x1 + [8] p(c_8) = [1] p(c_9) = [2] p(c_10) = [1] p(c_11) = [1] x2 + [1] p(c_12) = [8] p(c_13) = [1] p(c_14) = [1] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] Following rules are strictly oriented: fold#(t,x,s(n)) = [4] n + [16] > [4] n + [8] = c_7(fold#(t,x,n)) Following rules are (at-least) weakly oriented: *** Step 5.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 5.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) -->_1 fold#(t,x,s(n)) -> c_7(fold#(t,x,n)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: fold#(t,x,s(n)) -> c_7(fold#(t,x,n)) *** Step 5.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {f/2,f'/2,f''/1,fold/3,foldB/2,foldC/2,g/1,f#/2,f'#/2,f''#/1,fold#/3,foldB#/2,foldC#/2,g#/1} / {0/0,A/0,B/0 ,C/0,s/1,triple/3,c_1/1,c_2/2,c_3/1,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/2,c_10/0,c_11/2,c_12/0,c_13/0,c_14/0 ,c_15/0,c_16/0,c_17/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,f'#,f''#,fold#,foldB#,foldC#,g#} and constructors {0,A ,B,C,s,triple} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). MAYBE