MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: help(x,s(y),c) -> if(le(c,x),x,s(y),c) if(false(),x,s(y),c) -> minus(x,minus(c,s(y))) if(true(),x,s(y),c) -> help(x,s(y),plus(c,s(y))) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) mod(x,s(y)) -> help(x,s(y),0()) mod(s(x),0()) -> 0() plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {help,if,le,minus,mod,plus} and constructors {0,false,s ,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(0(),y) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(x,0()) -> c_7() minus#(0(),s(y)) -> c_8() minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) mod#(s(x),0()) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(0(),y) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(x,0()) -> c_7() minus#(0(),s(y)) -> c_8() minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) mod#(s(x),0()) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak TRS: help(x,s(y),c) -> if(le(c,x),x,s(y),c) if(false(),x,s(y),c) -> minus(x,minus(c,s(y))) if(true(),x,s(y),c) -> help(x,s(y),plus(c,s(y))) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) mod(x,s(y)) -> help(x,s(y),0()) mod(s(x),0()) -> 0() plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(0(),y) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(x,0()) -> c_7() minus#(0(),s(y)) -> c_8() minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) mod#(s(x),0()) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,y)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(0(),y) -> c_4() le#(s(x),0()) -> c_5() le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(x,0()) -> c_7() minus#(0(),s(y)) -> c_8() minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) mod#(s(x),0()) -> c_11() plus#(x,0()) -> c_12() plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,5,7,8,11,12} by application of Pre({4,5,7,8,11,12}) = {1,2,6,9,13}. Here rules are labelled as follows: 1: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) 2: if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) 3: if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) 4: le#(0(),y) -> c_4() 5: le#(s(x),0()) -> c_5() 6: le#(s(x),s(y)) -> c_6(le#(x,y)) 7: minus#(x,0()) -> c_7() 8: minus#(0(),s(y)) -> c_8() 9: minus#(s(x),s(y)) -> c_9(minus#(x,y)) 10: mod#(x,s(y)) -> c_10(help#(x,s(y),0())) 11: mod#(s(x),0()) -> c_11() 12: plus#(x,0()) -> c_12() 13: plus#(x,s(y)) -> c_13(plus#(x,y)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak DPs: le#(0(),y) -> c_4() le#(s(x),0()) -> c_5() minus#(x,0()) -> c_7() minus#(0(),s(y)) -> c_8() mod#(s(x),0()) -> c_11() plus#(x,0()) -> c_12() - Weak TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) -->_2 le#(s(x),s(y)) -> c_6(le#(x,y)):4 -->_1 if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))):3 -->_1 if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))):2 -->_2 le#(s(x),0()) -> c_5():9 -->_2 le#(0(),y) -> c_4():8 2:S:if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) -->_2 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 -->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 -->_2 minus#(0(),s(y)) -> c_8():11 -->_1 minus#(0(),s(y)) -> c_8():11 -->_1 minus#(x,0()) -> c_7():10 3:S:if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) -->_2 plus#(x,s(y)) -> c_13(plus#(x,y)):7 -->_1 help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)):1 4:S:le#(s(x),s(y)) -> c_6(le#(x,y)) -->_1 le#(s(x),0()) -> c_5():9 -->_1 le#(0(),y) -> c_4():8 -->_1 le#(s(x),s(y)) -> c_6(le#(x,y)):4 5:S:minus#(s(x),s(y)) -> c_9(minus#(x,y)) -->_1 minus#(0(),s(y)) -> c_8():11 -->_1 minus#(x,0()) -> c_7():10 -->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 6:S:mod#(x,s(y)) -> c_10(help#(x,s(y),0())) -->_1 help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)):1 7:S:plus#(x,s(y)) -> c_13(plus#(x,y)) -->_1 plus#(x,0()) -> c_12():13 -->_1 plus#(x,s(y)) -> c_13(plus#(x,y)):7 8:W:le#(0(),y) -> c_4() 9:W:le#(s(x),0()) -> c_5() 10:W:minus#(x,0()) -> c_7() 11:W:minus#(0(),s(y)) -> c_8() 12:W:mod#(s(x),0()) -> c_11() 13:W:plus#(x,0()) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: mod#(s(x),0()) -> c_11() 10: minus#(x,0()) -> c_7() 11: minus#(0(),s(y)) -> c_8() 13: plus#(x,0()) -> c_12() 8: le#(0(),y) -> c_4() 9: le#(s(x),0()) -> c_5() * Step 5: RemoveHeads MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(s(x),s(y)) -> c_9(minus#(x,y)) mod#(x,s(y)) -> c_10(help#(x,s(y),0())) plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) -->_2 le#(s(x),s(y)) -> c_6(le#(x,y)):4 -->_1 if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))):3 -->_1 if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))):2 2:S:if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) -->_2 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 -->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 3:S:if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) -->_2 plus#(x,s(y)) -> c_13(plus#(x,y)):7 -->_1 help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)):1 4:S:le#(s(x),s(y)) -> c_6(le#(x,y)) -->_1 le#(s(x),s(y)) -> c_6(le#(x,y)):4 5:S:minus#(s(x),s(y)) -> c_9(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):5 6:S:mod#(x,s(y)) -> c_10(help#(x,s(y),0())) -->_1 help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)):1 7:S:plus#(x,s(y)) -> c_13(plus#(x,y)) -->_1 plus#(x,s(y)) -> c_13(plus#(x,y)):7 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). [(6,mod#(x,s(y)) -> c_10(help#(x,s(y),0())))] * Step 6: NaturalMI MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(s(x),s(y)) -> c_9(minus#(x,y)) plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1,2}, uargs(c_3) = {1,2}, uargs(c_6) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {help#,if#,le#,minus#,mod#,plus#} TcT has computed the following interpretation: p(0) = [0] [1] p(false) = [0] [0] p(help) = [0 0] x2 + [0 0] x3 + [0] [2 0] [0 1] [0] p(if) = [0 0] x1 + [0 0] x2 + [0 1] x3 + [2 0] x4 + [0] [2 0] [2 1] [2 0] [2 2] [0] p(le) = [1 0] x2 + [0] [0 1] [0] p(minus) = [0 0] x2 + [1] [3 2] [0] p(mod) = [0] [0] p(plus) = [0 2] x1 + [2 0] x2 + [3] [1 0] [0 0] [2] p(s) = [1 1] x1 + [2] [0 0] [0] p(true) = [0] [0] p(help#) = [3 1] x1 + [1 0] x2 + [0] [2 1] [1 0] [2] p(if#) = [3 1] x2 + [1 0] x3 + [0] [0 0] [1 1] [1] p(le#) = [0 0] x2 + [0] [2 1] [0] p(minus#) = [0 0] x1 + [0] [1 0] [0] p(mod#) = [0 0] x1 + [0 0] x2 + [2] [1 1] [2 2] [2] p(plus#) = [0] [1] p(c_1) = [1 0] x1 + [2 0] x2 + [0] [0 1] [0 1] [1] p(c_2) = [1 0] x1 + [1 0] x2 + [0] [1 0] [0 0] [0] p(c_3) = [1 0] x1 + [2 0] x2 + [0] [0 0] [0 3] [0] p(c_4) = [0] [2] p(c_5) = [0] [0] p(c_6) = [2 0] x1 + [0] [1 1] [3] p(c_7) = [0] [1] p(c_8) = [2] [1] p(c_9) = [1 0] x1 + [0] [0 0] [0] p(c_10) = [1 0] x1 + [0] [2 0] [0] p(c_11) = [2] [1] p(c_12) = [1] [0] p(c_13) = [1 0] x1 + [0] [0 0] [1] Following rules are strictly oriented: if#(false(),x,s(y),c) = [3 1] x + [1 1] y + [2] [0 0] [1 1] [3] > [0] [0] = c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) Following rules are (at-least) weakly oriented: help#(x,s(y),c) = [3 1] x + [1 1] y + [2] [2 1] [1 1] [4] >= [3 1] x + [1 1] y + [2] [2 1] [1 1] [4] = c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(true(),x,s(y),c) = [3 1] x + [1 1] y + [2] [0 0] [1 1] [3] >= [3 1] x + [1 1] y + [2] [0 0] [0 0] [3] = c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(s(x),s(y)) = [0 0] y + [0] [2 2] [4] >= [0 0] y + [0] [2 1] [3] = c_6(le#(x,y)) minus#(s(x),s(y)) = [0 0] x + [0] [1 1] [2] >= [0] [0] = c_9(minus#(x,y)) plus#(x,s(y)) = [0] [1] >= [0] [1] = c_13(plus#(x,y)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: help#(x,s(y),c) -> c_1(if#(le(c,x),x,s(y),c),le#(c,x)) if#(true(),x,s(y),c) -> c_3(help#(x,s(y),plus(c,s(y))),plus#(c,s(y))) le#(s(x),s(y)) -> c_6(le#(x,y)) minus#(s(x),s(y)) -> c_9(minus#(x,y)) plus#(x,s(y)) -> c_13(plus#(x,y)) - Weak DPs: if#(false(),x,s(y),c) -> c_2(minus#(x,minus(c,s(y))),minus#(c,s(y))) - Weak TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),s(y)) -> 0() minus(s(x),s(y)) -> minus(x,y) plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) - Signature: {help/3,if/4,le/2,minus/2,mod/2,plus/2,help#/3,if#/4,le#/2,minus#/2,mod#/2,plus#/2} / {0/0,false/0,s/1 ,true/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/1} - Obligation: innermost runtime complexity wrt. defined symbols {help#,if#,le#,minus#,mod#,plus#} and constructors {0 ,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE