MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__a#() -> c_1() a__a#() -> c_2() a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) a__f#(X1,X2) -> c_4() a__g#(X1,X2) -> c_5() a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) a__h#(X) -> c_8() mark#(a()) -> c_9(a__a#()) mark#(b()) -> c_10() mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__a#() -> c_1() a__a#() -> c_2() a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) a__f#(X1,X2) -> c_4() a__g#(X1,X2) -> c_5() a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) a__h#(X) -> c_8() mark#(a()) -> c_9(a__a#()) mark#(b()) -> c_10() mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/2,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,5,8,10} by application of Pre({1,2,4,5,8,10}) = {3,6,7,9,11,12,13}. Here rules are labelled as follows: 1: a__a#() -> c_1() 2: a__a#() -> c_2() 3: a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) 4: a__f#(X1,X2) -> c_4() 5: a__g#(X1,X2) -> c_5() 6: a__g#(a(),X) -> c_6(a__f#(b(),X)) 7: a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) 8: a__h#(X) -> c_8() 9: mark#(a()) -> c_9(a__a#()) 10: mark#(b()) -> c_10() 11: mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) 12: mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) 13: mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(a()) -> c_9(a__a#()) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak DPs: a__a#() -> c_1() a__a#() -> c_2() a__f#(X1,X2) -> c_4() a__g#(X1,X2) -> c_5() a__h#(X) -> c_8() mark#(b()) -> c_10() - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/2,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4} by application of Pre({4}) = {3,5,6,7}. Here rules are labelled as follows: 1: a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) 2: a__g#(a(),X) -> c_6(a__f#(b(),X)) 3: a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) 4: mark#(a()) -> c_9(a__a#()) 5: mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) 6: mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) 7: mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) 8: a__a#() -> c_1() 9: a__a#() -> c_2() 10: a__f#(X1,X2) -> c_4() 11: a__g#(X1,X2) -> c_5() 12: a__h#(X) -> c_8() 13: mark#(b()) -> c_10() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak DPs: a__a#() -> c_1() a__a#() -> c_2() a__f#(X1,X2) -> c_4() a__g#(X1,X2) -> c_5() a__h#(X) -> c_8() mark#(a()) -> c_9(a__a#()) mark#(b()) -> c_10() - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/2,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) -->_1 a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)):3 -->_1 a__h#(X) -> c_8():11 -->_2 a__a#() -> c_2():8 -->_2 a__a#() -> c_1():7 2:S:a__g#(a(),X) -> c_6(a__f#(b(),X)) -->_1 a__f#(X1,X2) -> c_4():9 -->_1 a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()):1 3:S:a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) -->_2 mark#(a()) -> c_9(a__a#()):12 -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_2 mark#(b()) -> c_10():13 -->_1 a__g#(X1,X2) -> c_5():10 -->_1 a__g#(a(),X) -> c_6(a__f#(b(),X)):2 4:S:mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) -->_2 mark#(a()) -> c_9(a__a#()):12 -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(b()) -> c_10():13 -->_1 a__f#(X1,X2) -> c_4():9 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()):1 5:S:mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) -->_2 mark#(a()) -> c_9(a__a#()):12 -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(b()) -> c_10():13 -->_1 a__g#(X1,X2) -> c_5():10 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__g#(a(),X) -> c_6(a__f#(b(),X)):2 6:S:mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) -->_2 mark#(a()) -> c_9(a__a#()):12 -->_2 mark#(b()) -> c_10():13 -->_1 a__h#(X) -> c_8():11 -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)):3 7:W:a__a#() -> c_1() 8:W:a__a#() -> c_2() 9:W:a__f#(X1,X2) -> c_4() 10:W:a__g#(X1,X2) -> c_5() 11:W:a__h#(X) -> c_8() 12:W:mark#(a()) -> c_9(a__a#()) -->_1 a__a#() -> c_2():8 -->_1 a__a#() -> c_1():7 13:W:mark#(b()) -> c_10() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: a__f#(X1,X2) -> c_4() 10: a__g#(X1,X2) -> c_5() 11: a__h#(X) -> c_8() 13: mark#(b()) -> c_10() 12: mark#(a()) -> c_9(a__a#()) 7: a__a#() -> c_1() 8: a__a#() -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/2,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()) -->_1 a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)):3 2:S:a__g#(a(),X) -> c_6(a__f#(b(),X)) -->_1 a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()):1 3:S:a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__g#(a(),X) -> c_6(a__f#(b(),X)):2 4:S:mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__f#(X,X) -> c_3(a__h#(a__a()),a__a#()):1 5:S:mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__g#(a(),X) -> c_6(a__f#(b(),X)):2 6:S:mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) -->_2 mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)):6 -->_2 mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)):5 -->_2 mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)):4 -->_1 a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__f#(X,X) -> c_3(a__h#(a__a())) * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: a__f#(X,X) -> c_3(a__h#(a__a())) a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1}, uargs(a__f#) = {1}, uargs(a__g#) = {1}, uargs(a__h#) = {1}, uargs(c_3) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_11) = {1,2}, uargs(c_12) = {1,2}, uargs(c_13) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(a__a) = [0] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [0] p(a__h) = [1] x1 + [0] p(b) = [0] p(f) = [0] p(g) = [0] p(h) = [0] p(mark) = [0] p(a__a#) = [0] p(a__f#) = [1] x1 + [6] p(a__g#) = [1] x1 + [0] p(a__h#) = [1] x1 + [1] p(mark#) = [3] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [4] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [1] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [1] x2 + [0] p(c_12) = [1] x1 + [1] x2 + [0] p(c_13) = [1] x1 + [1] x2 + [7] Following rules are strictly oriented: a__f#(X,X) = [1] X + [6] > [5] = c_3(a__h#(a__a())) Following rules are (at-least) weakly oriented: a__g#(a(),X) = [0] >= [6] = c_6(a__f#(b(),X)) a__h#(X) = [1] X + [1] >= [4] = c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) = [3] >= [9] = c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) = [3] >= [3] = c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) = [3] >= [11] = c_13(a__h#(mark(X)),mark#(X)) a__a() = [0] >= [0] = a() a__a() = [0] >= [0] = b() a__f(X,X) = [1] X + [0] >= [0] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [0] = f(X1,X2) a__g(X1,X2) = [1] X1 + [0] >= [0] = g(X1,X2) a__g(a(),X) = [0] >= [0] = a__f(b(),X) a__h(X) = [1] X + [0] >= [0] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [0] = h(X) mark(a()) = [0] >= [0] = a__a() mark(b()) = [0] >= [0] = b() mark(f(X1,X2)) = [0] >= [0] = a__f(mark(X1),X2) mark(g(X1,X2)) = [0] >= [0] = a__g(mark(X1),X2) mark(h(X)) = [0] >= [0] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: a__g#(a(),X) -> c_6(a__f#(b(),X)) a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak DPs: a__f#(X,X) -> c_3(a__h#(a__a())) - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1}, uargs(a__f#) = {1}, uargs(a__g#) = {1}, uargs(a__h#) = {1}, uargs(c_3) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_11) = {1,2}, uargs(c_12) = {1,2}, uargs(c_13) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(a__a) = [0] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [0] p(a__h) = [1] x1 + [0] p(b) = [0] p(f) = [0] p(g) = [0] p(h) = [0] p(mark) = [0] p(a__a#) = [0] p(a__f#) = [1] x1 + [0] p(a__g#) = [1] x1 + [2] p(a__h#) = [1] x1 + [0] p(mark#) = [1] p(c_1) = [4] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [1] x2 + [7] p(c_12) = [1] x1 + [1] x2 + [0] p(c_13) = [1] x1 + [1] x2 + [0] Following rules are strictly oriented: a__g#(a(),X) = [2] > [0] = c_6(a__f#(b(),X)) Following rules are (at-least) weakly oriented: a__f#(X,X) = [1] X + [0] >= [0] = c_3(a__h#(a__a())) a__h#(X) = [1] X + [0] >= [3] = c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) = [1] >= [8] = c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) = [1] >= [3] = c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) = [1] >= [1] = c_13(a__h#(mark(X)),mark#(X)) a__a() = [0] >= [0] = a() a__a() = [0] >= [0] = b() a__f(X,X) = [1] X + [0] >= [0] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [0] = f(X1,X2) a__g(X1,X2) = [1] X1 + [0] >= [0] = g(X1,X2) a__g(a(),X) = [0] >= [0] = a__f(b(),X) a__h(X) = [1] X + [0] >= [0] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [0] = h(X) mark(a()) = [0] >= [0] = a__a() mark(b()) = [0] >= [0] = b() mark(f(X1,X2)) = [0] >= [0] = a__f(mark(X1),X2) mark(g(X1,X2)) = [0] >= [0] = a__g(mark(X1),X2) mark(h(X)) = [0] >= [0] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: a__h#(X) -> c_7(a__g#(mark(X),X),mark#(X)) mark#(f(X1,X2)) -> c_11(a__f#(mark(X1),X2),mark#(X1)) mark#(g(X1,X2)) -> c_12(a__g#(mark(X1),X2),mark#(X1)) mark#(h(X)) -> c_13(a__h#(mark(X)),mark#(X)) - Weak DPs: a__f#(X,X) -> c_3(a__h#(a__a())) a__g#(a(),X) -> c_6(a__f#(b(),X)) - Weak TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1,a__a#/0,a__f#/2,a__g#/2,a__h#/1,mark#/1} / {a/0,b/0,f/2,g/2,h/1,c_1/0 ,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__a#,a__f#,a__g#,a__h#,mark#} and constructors {a,b,f,g ,h} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE