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