MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1} / {c/0,f/1,false/0,if/3,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f,a__if,mark} and constructors {c,f,false,if,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__f#(X) -> c_2() a__if#(X1,X2,X3) -> c_3() a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(c()) -> c_6() mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(false()) -> c_8() mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) mark#(true()) -> c_10() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__f#(X) -> c_2() a__if#(X1,X2,X3) -> c_3() a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(c()) -> c_6() mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(false()) -> c_8() mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) mark#(true()) -> c_10() - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,6,8,10} by application of Pre({2,3,6,8,10}) = {1,4,5,7,9}. Here rules are labelled as follows: 1: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) 2: a__f#(X) -> c_2() 3: a__if#(X1,X2,X3) -> c_3() 4: a__if#(false(),X,Y) -> c_4(mark#(Y)) 5: a__if#(true(),X,Y) -> c_5(mark#(X)) 6: mark#(c()) -> c_6() 7: mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) 8: mark#(false()) -> c_8() 9: mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) 10: mark#(true()) -> c_10() * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) - Weak DPs: a__f#(X) -> c_2() a__if#(X1,X2,X3) -> c_3() mark#(c()) -> c_6() mark#(false()) -> c_8() mark#(true()) -> c_10() - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) -->_2 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_2 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_1 a__if#(true(),X,Y) -> c_5(mark#(X)):3 -->_1 a__if#(false(),X,Y) -> c_4(mark#(Y)):2 -->_2 mark#(true()) -> c_10():10 -->_2 mark#(false()) -> c_8():9 -->_2 mark#(c()) -> c_6():8 -->_1 a__if#(X1,X2,X3) -> c_3():7 2:S:a__if#(false(),X,Y) -> c_4(mark#(Y)) -->_1 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_1 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_1 mark#(true()) -> c_10():10 -->_1 mark#(false()) -> c_8():9 -->_1 mark#(c()) -> c_6():8 3:S:a__if#(true(),X,Y) -> c_5(mark#(X)) -->_1 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_1 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_1 mark#(true()) -> c_10():10 -->_1 mark#(false()) -> c_8():9 -->_1 mark#(c()) -> c_6():8 4:S:mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) -->_2 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_2 mark#(true()) -> c_10():10 -->_2 mark#(false()) -> c_8():9 -->_2 mark#(c()) -> c_6():8 -->_1 a__f#(X) -> c_2():6 -->_2 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_1 a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)):1 5:S:mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) -->_3 mark#(true()) -> c_10():10 -->_2 mark#(true()) -> c_10():10 -->_3 mark#(false()) -> c_8():9 -->_2 mark#(false()) -> c_8():9 -->_3 mark#(c()) -> c_6():8 -->_2 mark#(c()) -> c_6():8 -->_1 a__if#(X1,X2,X3) -> c_3():7 -->_3 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_2 mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)):5 -->_3 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_2 mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)):4 -->_1 a__if#(true(),X,Y) -> c_5(mark#(X)):3 -->_1 a__if#(false(),X,Y) -> c_4(mark#(Y)):2 6:W:a__f#(X) -> c_2() 7:W:a__if#(X1,X2,X3) -> c_3() 8:W:mark#(c()) -> c_6() 9:W:mark#(false()) -> c_8() 10:W:mark#(true()) -> c_10() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: a__f#(X) -> c_2() 7: a__if#(X1,X2,X3) -> c_3() 8: mark#(c()) -> c_6() 9: mark#(false()) -> c_8() 10: mark#(true()) -> c_10() * Step 4: WeightGap MAYBE + Considered Problem: - Strict DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + 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__if) = {1,2}, uargs(a__f#) = {1}, uargs(a__if#) = {1,2}, uargs(c_1) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2,3} Following symbols are considered usable: all TcT has computed the following interpretation: p(a__f) = [1] x1 + [0] p(a__if) = [1] x1 + [1] x2 + [0] p(c) = [0] p(f) = [0] p(false) = [0] p(if) = [0] p(mark) = [0] p(true) = [0] p(a__f#) = [1] x1 + [5] p(a__if#) = [1] x1 + [1] x2 + [0] p(mark#) = [1] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [1] x3 + [0] p(c_10) = [0] Following rules are strictly oriented: a__f#(X) = [1] X + [5] > [1] = c_1(a__if#(mark(X),c(),f(true())),mark#(X)) Following rules are (at-least) weakly oriented: a__if#(false(),X,Y) = [1] X + [0] >= [1] = c_4(mark#(Y)) a__if#(true(),X,Y) = [1] X + [0] >= [1] = c_5(mark#(X)) mark#(f(X)) = [1] >= [6] = c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) = [1] >= [2] = c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) a__f(X) = [1] X + [0] >= [0] = a__if(mark(X),c(),f(true())) a__f(X) = [1] X + [0] >= [0] = f(X) a__if(X1,X2,X3) = [1] X1 + [1] X2 + [0] >= [0] = if(X1,X2,X3) a__if(false(),X,Y) = [1] X + [0] >= [0] = mark(Y) a__if(true(),X,Y) = [1] X + [0] >= [0] = mark(X) mark(c()) = [0] >= [0] = c() mark(f(X)) = [0] >= [0] = a__f(mark(X)) mark(false()) = [0] >= [0] = false() mark(if(X1,X2,X3)) = [0] >= [0] = a__if(mark(X1),mark(X2),X3) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap MAYBE + Considered Problem: - Strict DPs: a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) - Weak DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + 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__if) = {1,2}, uargs(a__f#) = {1}, uargs(a__if#) = {1,2}, uargs(c_1) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2,3} Following symbols are considered usable: all TcT has computed the following interpretation: p(a__f) = [1] x1 + [0] p(a__if) = [1] x1 + [1] x2 + [0] p(c) = [0] p(f) = [0] p(false) = [0] p(if) = [0] p(mark) = [0] p(true) = [0] p(a__f#) = [1] x1 + [1] p(a__if#) = [1] x1 + [1] x2 + [1] p(mark#) = [0] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [4] p(c_6) = [2] p(c_7) = [1] x1 + [1] x2 + [7] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [1] x3 + [7] p(c_10) = [0] Following rules are strictly oriented: a__if#(false(),X,Y) = [1] X + [1] > [0] = c_4(mark#(Y)) Following rules are (at-least) weakly oriented: a__f#(X) = [1] X + [1] >= [1] = c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(true(),X,Y) = [1] X + [1] >= [4] = c_5(mark#(X)) mark#(f(X)) = [0] >= [8] = c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) = [0] >= [8] = c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) a__f(X) = [1] X + [0] >= [0] = a__if(mark(X),c(),f(true())) a__f(X) = [1] X + [0] >= [0] = f(X) a__if(X1,X2,X3) = [1] X1 + [1] X2 + [0] >= [0] = if(X1,X2,X3) a__if(false(),X,Y) = [1] X + [0] >= [0] = mark(Y) a__if(true(),X,Y) = [1] X + [0] >= [0] = mark(X) mark(c()) = [0] >= [0] = c() mark(f(X)) = [0] >= [0] = a__f(mark(X)) mark(false()) = [0] >= [0] = false() mark(if(X1,X2,X3)) = [0] >= [0] = a__if(mark(X1),mark(X2),X3) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: a__if#(true(),X,Y) -> c_5(mark#(X)) mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) - Weak DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(false(),X,Y) -> c_4(mark#(Y)) - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + 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__if) = {1,2}, uargs(a__f#) = {1}, uargs(a__if#) = {1,2}, uargs(c_1) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2,3} Following symbols are considered usable: all TcT has computed the following interpretation: p(a__f) = [1] x1 + [0] p(a__if) = [1] x1 + [1] x2 + [0] p(c) = [0] p(f) = [0] p(false) = [0] p(if) = [0] p(mark) = [0] p(true) = [0] p(a__f#) = [1] x1 + [5] p(a__if#) = [1] x1 + [1] x2 + [3] p(mark#) = [2] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [1] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [1] x1 + [1] x2 + [1] x3 + [5] p(c_10) = [0] Following rules are strictly oriented: a__if#(true(),X,Y) = [1] X + [3] > [2] = c_5(mark#(X)) Following rules are (at-least) weakly oriented: a__f#(X) = [1] X + [5] >= [5] = c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(false(),X,Y) = [1] X + [3] >= [3] = c_4(mark#(Y)) mark#(f(X)) = [2] >= [7] = c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) = [2] >= [12] = c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) a__f(X) = [1] X + [0] >= [0] = a__if(mark(X),c(),f(true())) a__f(X) = [1] X + [0] >= [0] = f(X) a__if(X1,X2,X3) = [1] X1 + [1] X2 + [0] >= [0] = if(X1,X2,X3) a__if(false(),X,Y) = [1] X + [0] >= [0] = mark(Y) a__if(true(),X,Y) = [1] X + [0] >= [0] = mark(X) mark(c()) = [0] >= [0] = c() mark(f(X)) = [0] >= [0] = a__f(mark(X)) mark(false()) = [0] >= [0] = false() mark(if(X1,X2,X3)) = [0] >= [0] = a__if(mark(X1),mark(X2),X3) mark(true()) = [0] >= [0] = true() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: mark#(f(X)) -> c_7(a__f#(mark(X)),mark#(X)) mark#(if(X1,X2,X3)) -> c_9(a__if#(mark(X1),mark(X2),X3),mark#(X1),mark#(X2)) - Weak DPs: a__f#(X) -> c_1(a__if#(mark(X),c(),f(true())),mark#(X)) a__if#(false(),X,Y) -> c_4(mark#(Y)) a__if#(true(),X,Y) -> c_5(mark#(X)) - Weak TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__if(false(),X,Y) -> mark(Y) a__if(true(),X,Y) -> mark(X) mark(c()) -> c() mark(f(X)) -> a__f(mark(X)) mark(false()) -> false() mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(true()) -> true() - Signature: {a__f/1,a__if/3,mark/1,a__f#/1,a__if#/3,mark#/1} / {c/0,f/1,false/0,if/3,true/0,c_1/2,c_2/0,c_3/0,c_4/1 ,c_5/1,c_6/0,c_7/2,c_8/0,c_9/3,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__f#,a__if#,mark#} and constructors {c,f,false,if,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE