MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) if1(false(),x,y) -> true() if1(true(),x,y) -> if2(divides(x,y),x,y) if2(false(),x,y) -> test(x,s(y)) if2(true(),x,y) -> false() prime(x) -> test(x,s(s(0()))) test(x,y) -> if1(gt(x,y),x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div,divides,gt,if1,if2,prime,test} and constructors {0 ,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs div#(0(),0(),z) -> c_1() div#(0(),s(x),z) -> c_2() div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(false(),x,y) -> c_9() if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) if2#(true(),x,y) -> c_12() prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: div#(0(),0(),z) -> c_1() div#(0(),s(x),z) -> c_2() div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(false(),x,y) -> c_9() if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) if2#(true(),x,y) -> c_12() prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) if1(false(),x,y) -> true() if1(true(),x,y) -> if2(divides(x,y),x,y) if2(false(),x,y) -> test(x,s(y)) if2(true(),x,y) -> false() prime(x) -> test(x,s(s(0()))) test(x,y) -> if1(gt(x,y),x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div#(0(),0(),z) -> c_1() div#(0(),s(x),z) -> c_2() div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(false(),x,y) -> c_9() if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) if2#(true(),x,y) -> c_12() prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: div#(0(),0(),z) -> c_1() div#(0(),s(x),z) -> c_2() div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(false(),x,y) -> c_9() if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) if2#(true(),x,y) -> c_12() prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} 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,6,7,9,12} by application of Pre({1,2,6,7,9,12}) = {4,5,8,10,14}. Here rules are labelled as follows: 1: div#(0(),0(),z) -> c_1() 2: div#(0(),s(x),z) -> c_2() 3: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) 4: div#(s(x),s(y),z) -> c_4(div#(x,y,z)) 5: divides#(x,y) -> c_5(div#(x,y,y)) 6: gt#(0(),y) -> c_6() 7: gt#(s(x),0()) -> c_7() 8: gt#(s(x),s(y)) -> c_8(gt#(x,y)) 9: if1#(false(),x,y) -> c_9() 10: if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) 11: if2#(false(),x,y) -> c_11(test#(x,s(y))) 12: if2#(true(),x,y) -> c_12() 13: prime#(x) -> c_13(test#(x,s(s(0())))) 14: test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak DPs: div#(0(),0(),z) -> c_1() div#(0(),s(x),z) -> c_2() gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() if1#(false(),x,y) -> c_9() if2#(true(),x,y) -> c_12() - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 2:S:div#(s(x),s(y),z) -> c_4(div#(x,y,z)) -->_1 div#(0(),s(x),z) -> c_2():10 -->_1 div#(0(),0(),z) -> c_1():9 -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 -->_1 div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))):1 3:S:divides#(x,y) -> c_5(div#(x,y,y)) -->_1 div#(0(),s(x),z) -> c_2():10 -->_1 div#(0(),0(),z) -> c_1():9 -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 4:S:gt#(s(x),s(y)) -> c_8(gt#(x,y)) -->_1 gt#(s(x),0()) -> c_7():12 -->_1 gt#(0(),y) -> c_6():11 -->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):4 5:S:if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) -->_1 if2#(false(),x,y) -> c_11(test#(x,s(y))):6 -->_1 if2#(true(),x,y) -> c_12():14 -->_2 divides#(x,y) -> c_5(div#(x,y,y)):3 6:S:if2#(false(),x,y) -> c_11(test#(x,s(y))) -->_1 test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)):8 7:S:prime#(x) -> c_13(test#(x,s(s(0())))) -->_1 test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)):8 8:S:test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) -->_1 if1#(false(),x,y) -> c_9():13 -->_2 gt#(s(x),0()) -> c_7():12 -->_2 gt#(0(),y) -> c_6():11 -->_1 if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)):5 -->_2 gt#(s(x),s(y)) -> c_8(gt#(x,y)):4 9:W:div#(0(),0(),z) -> c_1() 10:W:div#(0(),s(x),z) -> c_2() 11:W:gt#(0(),y) -> c_6() 12:W:gt#(s(x),0()) -> c_7() 13:W:if1#(false(),x,y) -> c_9() 14:W:if2#(true(),x,y) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: if2#(true(),x,y) -> c_12() 13: if1#(false(),x,y) -> c_9() 11: gt#(0(),y) -> c_6() 12: gt#(s(x),0()) -> c_7() 9: div#(0(),0(),z) -> c_1() 10: div#(0(),s(x),z) -> c_2() * Step 5: RemoveHeads MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) prime#(x) -> c_13(test#(x,s(s(0())))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 2:S:div#(s(x),s(y),z) -> c_4(div#(x,y,z)) -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 -->_1 div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))):1 3:S:divides#(x,y) -> c_5(div#(x,y,y)) -->_1 div#(s(x),s(y),z) -> c_4(div#(x,y,z)):2 4:S:gt#(s(x),s(y)) -> c_8(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):4 5:S:if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) -->_1 if2#(false(),x,y) -> c_11(test#(x,s(y))):6 -->_2 divides#(x,y) -> c_5(div#(x,y,y)):3 6:S:if2#(false(),x,y) -> c_11(test#(x,s(y))) -->_1 test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)):8 7:S:prime#(x) -> c_13(test#(x,s(s(0())))) -->_1 test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)):8 8:S:test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) -->_1 if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)):5 -->_2 gt#(s(x),s(y)) -> c_8(gt#(x,y)):4 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). [(7,prime#(x) -> c_13(test#(x,s(s(0())))))] * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,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(if1#) = {1}, uargs(if2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(div) = [3] x3 + [0] p(divides) = [3] x2 + [0] p(false) = [0] p(gt) = [0] p(if1) = [0] p(if2) = [0] p(prime) = [0] p(s) = [0] p(test) = [0] p(true) = [0] p(div#) = [4] x3 + [0] p(divides#) = [4] x2 + [0] p(gt#) = [0] p(if1#) = [1] x1 + [2] x2 + [7] x3 + [4] p(if2#) = [1] x1 + [2] x2 + [7] p(prime#) = [0] p(test#) = [2] x1 + [7] x2 + [7] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [1] x1 + [1] x2 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [1] x2 + [2] Following rules are strictly oriented: test#(x,y) = [2] x + [7] y + [7] > [2] x + [7] y + [6] = c_14(if1#(gt(x,y),x,y),gt#(x,y)) Following rules are (at-least) weakly oriented: div#(s(x),0(),s(z)) = [0] >= [0] = c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) = [4] z + [0] >= [4] z + [0] = c_4(div#(x,y,z)) divides#(x,y) = [4] y + [0] >= [4] y + [0] = c_5(div#(x,y,y)) gt#(s(x),s(y)) = [0] >= [0] = c_8(gt#(x,y)) if1#(true(),x,y) = [2] x + [7] y + [4] >= [2] x + [7] y + [7] = c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) = [2] x + [7] >= [2] x + [7] = c_11(test#(x,s(y))) div(0(),0(),z) = [3] z + [0] >= [0] = true() div(0(),s(x),z) = [3] z + [0] >= [0] = false() div(s(x),0(),s(z)) = [0] >= [0] = div(s(x),s(z),s(z)) div(s(x),s(y),z) = [3] z + [0] >= [3] z + [0] = div(x,y,z) divides(x,y) = [3] y + [0] >= [3] y + [0] = div(x,y,y) gt(0(),y) = [0] >= [0] = false() gt(s(x),0()) = [0] >= [0] = true() gt(s(x),s(y)) = [0] >= [0] = gt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) - Weak DPs: test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,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(if1#) = {1}, uargs(if2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(div) = [2] p(divides) = [2] p(false) = [2] p(gt) = [2] p(if1) = [0] p(if2) = [0] p(prime) = [0] p(s) = [0] p(test) = [0] p(true) = [2] p(div#) = [0] p(divides#) = [0] p(gt#) = [4] p(if1#) = [1] x1 + [0] p(if2#) = [1] x1 + [5] p(prime#) = [0] p(test#) = [6] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] x1 + [4] p(c_9) = [1] p(c_10) = [1] x1 + [1] x2 + [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [2] p(c_14) = [1] x1 + [1] x2 + [0] Following rules are strictly oriented: if2#(false(),x,y) = [7] > [6] = c_11(test#(x,s(y))) Following rules are (at-least) weakly oriented: div#(s(x),0(),s(z)) = [0] >= [0] = c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) = [0] >= [0] = c_4(div#(x,y,z)) divides#(x,y) = [0] >= [0] = c_5(div#(x,y,y)) gt#(s(x),s(y)) = [4] >= [8] = c_8(gt#(x,y)) if1#(true(),x,y) = [2] >= [7] = c_10(if2#(divides(x,y),x,y),divides#(x,y)) test#(x,y) = [6] >= [6] = c_14(if1#(gt(x,y),x,y),gt#(x,y)) div(0(),0(),z) = [2] >= [2] = true() div(0(),s(x),z) = [2] >= [2] = false() div(s(x),0(),s(z)) = [2] >= [2] = div(s(x),s(z),s(z)) div(s(x),s(y),z) = [2] >= [2] = div(x,y,z) divides(x,y) = [2] >= [2] = div(x,y,y) gt(0(),y) = [2] >= [2] = false() gt(s(x),0()) = [2] >= [2] = true() gt(s(x),s(y)) = [2] >= [2] = gt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) divides#(x,y) -> c_5(div#(x,y,y)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) - Weak DPs: if2#(false(),x,y) -> c_11(test#(x,s(y))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,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(if1#) = {1}, uargs(if2#) = {1}, uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_10) = {1,2}, uargs(c_11) = {1}, uargs(c_14) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(div) = [4] p(divides) = [4] p(false) = [1] p(gt) = [1] p(if1) = [2] x1 + [4] x2 + [0] p(if2) = [4] x1 + [2] x2 + [1] p(prime) = [1] p(s) = [0] p(test) = [1] x2 + [0] p(true) = [1] p(div#) = [0] p(divides#) = [2] p(gt#) = [2] p(if1#) = [1] x1 + [1] x3 + [0] p(if2#) = [1] x1 + [7] p(prime#) = [2] p(test#) = [2] x2 + [3] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [5] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] x1 + [4] p(c_9) = [0] p(c_10) = [1] x1 + [1] x2 + [1] p(c_11) = [1] x1 + [5] p(c_12) = [0] p(c_13) = [4] p(c_14) = [1] x1 + [1] x2 + [0] Following rules are strictly oriented: divides#(x,y) = [2] > [0] = c_5(div#(x,y,y)) Following rules are (at-least) weakly oriented: div#(s(x),0(),s(z)) = [0] >= [0] = c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) = [0] >= [5] = c_4(div#(x,y,z)) gt#(s(x),s(y)) = [2] >= [6] = c_8(gt#(x,y)) if1#(true(),x,y) = [1] y + [1] >= [14] = c_10(if2#(divides(x,y),x,y),divides#(x,y)) if2#(false(),x,y) = [8] >= [8] = c_11(test#(x,s(y))) test#(x,y) = [2] y + [3] >= [1] y + [3] = c_14(if1#(gt(x,y),x,y),gt#(x,y)) div(0(),0(),z) = [4] >= [1] = true() div(0(),s(x),z) = [4] >= [1] = false() div(s(x),0(),s(z)) = [4] >= [4] = div(s(x),s(z),s(z)) div(s(x),s(y),z) = [4] >= [4] = div(x,y,z) divides(x,y) = [4] >= [4] = div(x,y,y) gt(0(),y) = [1] >= [1] = false() gt(s(x),0()) = [1] >= [1] = true() gt(s(x),s(y)) = [1] >= [1] = gt(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: div#(s(x),0(),s(z)) -> c_3(div#(s(x),s(z),s(z))) div#(s(x),s(y),z) -> c_4(div#(x,y,z)) gt#(s(x),s(y)) -> c_8(gt#(x,y)) if1#(true(),x,y) -> c_10(if2#(divides(x,y),x,y),divides#(x,y)) - Weak DPs: divides#(x,y) -> c_5(div#(x,y,y)) if2#(false(),x,y) -> c_11(test#(x,s(y))) test#(x,y) -> c_14(if1#(gt(x,y),x,y),gt#(x,y)) - Weak TRS: div(0(),0(),z) -> true() div(0(),s(x),z) -> false() div(s(x),0(),s(z)) -> div(s(x),s(z),s(z)) div(s(x),s(y),z) -> div(x,y,z) divides(x,y) -> div(x,y,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) - Signature: {div/3,divides/2,gt/2,if1/3,if2/3,prime/1,test/2,div#/3,divides#/2,gt#/2,if1#/3,if2#/3,prime#/1 ,test#/2} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/2,c_11/1 ,c_12/0,c_13/1,c_14/2} - Obligation: innermost runtime complexity wrt. defined symbols {div#,divides#,gt#,if1#,if2#,prime# ,test#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE