MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: cons(x,y) -> y cons(x,cons(y,s(z))) -> cons(y,x) cons(cons(x,z),s(y)) -> transform(x) gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y))) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(cons(x,y)) -> y transform(cons(x,y)) -> cons(cons(x,x),x) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons,gcd,max,min,minus,transform} and constructors {0,s} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. cons(x,cons(y,s(z))) -> cons(y,x) cons(cons(x,z),s(y)) -> transform(x) transform(cons(x,y)) -> y transform(cons(x,y)) -> cons(cons(x,x),x) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: cons(x,y) -> y gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y))) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons,gcd,max,min,minus,transform} and constructors {0,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cons#(x,y) -> c_1() gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(x,0()) -> c_3() max#(0(),y) -> c_4() max#(s(x),s(y)) -> c_5(max#(x,y)) min#(x,0()) -> c_6() min#(0(),y) -> c_7() min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(x,0()) -> c_9() minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(x) -> c_11() transform#(s(x)) -> c_12(transform#(x)) Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: cons#(x,y) -> c_1() gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(x,0()) -> c_3() max#(0(),y) -> c_4() max#(s(x),s(y)) -> c_5(max#(x,y)) min#(x,0()) -> c_6() min#(0(),y) -> c_7() min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(x,0()) -> c_9() minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(x) -> c_11() transform#(s(x)) -> c_12(transform#(x)) - Weak TRS: cons(x,y) -> y gcd(s(x),s(y)) -> gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y))) max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1,cons#/2,gcd#/2,max#/2,min#/2,minus#/2,transform#/1} / {0/0,s/1 ,c_1/0,c_2/6,c_3/0,c_4/0,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,gcd#,max#,min#,minus# ,transform#} and constructors {0,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) cons#(x,y) -> c_1() gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(x,0()) -> c_3() max#(0(),y) -> c_4() max#(s(x),s(y)) -> c_5(max#(x,y)) min#(x,0()) -> c_6() min#(0(),y) -> c_7() min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(x,0()) -> c_9() minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(x) -> c_11() transform#(s(x)) -> c_12(transform#(x)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: cons#(x,y) -> c_1() gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(x,0()) -> c_3() max#(0(),y) -> c_4() max#(s(x),s(y)) -> c_5(max#(x,y)) min#(x,0()) -> c_6() min#(0(),y) -> c_7() min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(x,0()) -> c_9() minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(x) -> c_11() transform#(s(x)) -> c_12(transform#(x)) - Weak TRS: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1,cons#/2,gcd#/2,max#/2,min#/2,minus#/2,transform#/1} / {0/0,s/1 ,c_1/0,c_2/6,c_3/0,c_4/0,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,gcd#,max#,min#,minus# ,transform#} and constructors {0,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,6,7,9,11} by application of Pre({1,3,4,6,7,9,11}) = {2,5,8,10,12}. Here rules are labelled as follows: 1: cons#(x,y) -> c_1() 2: gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) 3: max#(x,0()) -> c_3() 4: max#(0(),y) -> c_4() 5: max#(s(x),s(y)) -> c_5(max#(x,y)) 6: min#(x,0()) -> c_6() 7: min#(0(),y) -> c_7() 8: min#(s(x),s(y)) -> c_8(min#(x,y)) 9: minus#(x,0()) -> c_9() 10: minus#(s(x),s(y)) -> c_10(minus#(x,y)) 11: transform#(x) -> c_11() 12: transform#(s(x)) -> c_12(transform#(x)) * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(s(x),s(y)) -> c_5(max#(x,y)) min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(s(x)) -> c_12(transform#(x)) - Weak DPs: cons#(x,y) -> c_1() max#(x,0()) -> c_3() max#(0(),y) -> c_4() min#(x,0()) -> c_6() min#(0(),y) -> c_7() minus#(x,0()) -> c_9() transform#(x) -> c_11() - Weak TRS: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1,cons#/2,gcd#/2,max#/2,min#/2,minus#/2,transform#/1} / {0/0,s/1 ,c_1/0,c_2/6,c_3/0,c_4/0,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,gcd#,max#,min#,minus# ,transform#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) -->_5 transform#(s(x)) -> c_12(transform#(x)):5 -->_2 minus#(s(x),s(y)) -> c_10(minus#(x,y)):4 -->_6 min#(s(x),s(y)) -> c_8(min#(x,y)):3 -->_4 min#(s(x),s(y)) -> c_8(min#(x,y)):3 -->_3 max#(s(x),s(y)) -> c_5(max#(x,y)):2 -->_5 transform#(x) -> c_11():12 -->_2 minus#(x,0()) -> c_9():11 -->_6 min#(0(),y) -> c_7():10 -->_4 min#(0(),y) -> c_7():10 -->_6 min#(x,0()) -> c_6():9 -->_4 min#(x,0()) -> c_6():9 -->_3 max#(0(),y) -> c_4():8 -->_3 max#(x,0()) -> c_3():7 -->_1 gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)):1 2:S:max#(s(x),s(y)) -> c_5(max#(x,y)) -->_1 max#(0(),y) -> c_4():8 -->_1 max#(x,0()) -> c_3():7 -->_1 max#(s(x),s(y)) -> c_5(max#(x,y)):2 3:S:min#(s(x),s(y)) -> c_8(min#(x,y)) -->_1 min#(0(),y) -> c_7():10 -->_1 min#(x,0()) -> c_6():9 -->_1 min#(s(x),s(y)) -> c_8(min#(x,y)):3 4:S:minus#(s(x),s(y)) -> c_10(minus#(x,y)) -->_1 minus#(x,0()) -> c_9():11 -->_1 minus#(s(x),s(y)) -> c_10(minus#(x,y)):4 5:S:transform#(s(x)) -> c_12(transform#(x)) -->_1 transform#(x) -> c_11():12 -->_1 transform#(s(x)) -> c_12(transform#(x)):5 6:W:cons#(x,y) -> c_1() 7:W:max#(x,0()) -> c_3() 8:W:max#(0(),y) -> c_4() 9:W:min#(x,0()) -> c_6() 10:W:min#(0(),y) -> c_7() 11:W:minus#(x,0()) -> c_9() 12:W:transform#(x) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: cons#(x,y) -> c_1() 7: max#(x,0()) -> c_3() 8: max#(0(),y) -> c_4() 9: min#(x,0()) -> c_6() 10: min#(0(),y) -> c_7() 11: minus#(x,0()) -> c_9() 12: transform#(x) -> c_11() * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: gcd#(s(x),s(y)) -> c_2(gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) ,minus#(max(x,y),min(x,transform(y))) ,max#(x,y) ,min#(x,transform(y)) ,transform#(y) ,min#(x,y)) max#(s(x),s(y)) -> c_5(max#(x,y)) min#(s(x),s(y)) -> c_8(min#(x,y)) minus#(s(x),s(y)) -> c_10(minus#(x,y)) transform#(s(x)) -> c_12(transform#(x)) - Weak TRS: max(x,0()) -> x max(0(),y) -> y max(s(x),s(y)) -> s(max(x,y)) min(x,0()) -> 0() min(0(),y) -> 0() min(s(x),s(y)) -> s(min(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> s(minus(x,y)) transform(x) -> s(s(x)) transform(s(x)) -> s(s(transform(x))) - Signature: {cons/2,gcd/2,max/2,min/2,minus/2,transform/1,cons#/2,gcd#/2,max#/2,min#/2,minus#/2,transform#/1} / {0/0,s/1 ,c_1/0,c_2/6,c_3/0,c_4/0,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,gcd#,max#,min#,minus# ,transform#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE