MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gcd(Cons(x,xs),Nil()) -> Nil() gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) gcd(Nil(),Cons(x,xs)) -> Nil() gcd(Nil(),Nil()) -> Nil() goal(x,y) -> gcd(x,y) gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() gcd[False][Ite](False(),x,y) -> gcd(monus(y,x),x) gcd[False][Ite](True(),x,y) -> gcd(y,monus(x,y)) gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y) gcd[Ite](True(),x,y) -> x monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3} / {Cons/2 ,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,and,eqList,gcd,gcd[False][Ite],gcd[Ite],goal,gt0,lgth ,monus,monus[Ite]} and constructors {Cons,False,Nil,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) @#(Nil(),ys) -> c_2() eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) eqList#(Cons(x,xs),Nil()) -> c_4() eqList#(Nil(),Cons(y,ys)) -> c_5() eqList#(Nil(),Nil()) -> c_6() gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) lgth#(Nil()) -> c_16() monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) Weak DPs and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gcd[Ite]#(True(),x,y) -> c_25() monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) monus[Ite]#(True(),Cons(x,xs),y) -> c_27() and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) @#(Nil(),ys) -> c_2() eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) eqList#(Cons(x,xs),Nil()) -> c_4() eqList#(Nil(),Cons(y,ys)) -> c_5() eqList#(Nil(),Nil()) -> c_6() gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) lgth#(Nil()) -> c_16() monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gcd[Ite]#(True(),x,y) -> c_25() monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) monus[Ite]#(True(),Cons(x,xs),y) -> c_27() - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gcd(Cons(x,xs),Nil()) -> Nil() gcd(Cons(x',xs'),Cons(x,xs)) -> gcd[Ite](eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) gcd(Nil(),Cons(x,xs)) -> Nil() gcd(Nil(),Nil()) -> Nil() gcd[False][Ite](False(),x,y) -> gcd(monus(y,x),x) gcd[False][Ite](True(),x,y) -> gcd(y,monus(x,y)) gcd[Ite](False(),x,y) -> gcd[False][Ite](gt0(x,y),x,y) gcd[Ite](True(),x,y) -> x goal(x,y) -> gcd(x,y) gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) @#(Nil(),ys) -> c_2() and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) eqList#(Cons(x,xs),Nil()) -> c_4() eqList#(Nil(),Cons(y,ys)) -> c_5() eqList#(Nil(),Nil()) -> c_6() gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gcd[Ite]#(True(),x,y) -> c_25() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) lgth#(Nil()) -> c_16() monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) monus[Ite]#(True(),Cons(x,xs),y) -> c_27() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) @#(Nil(),ys) -> c_2() eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) eqList#(Cons(x,xs),Nil()) -> c_4() eqList#(Nil(),Cons(y,ys)) -> c_5() eqList#(Nil(),Nil()) -> c_6() gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) lgth#(Nil()) -> c_16() monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gcd[Ite]#(True(),x,y) -> c_25() monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) monus[Ite]#(True(),Cons(x,xs),y) -> c_27() - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,6,16} by application of Pre({2,4,5,6,16}) = {1,3,15,17}. Here rules are labelled as follows: 1: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) 2: @#(Nil(),ys) -> c_2() 3: eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) 4: eqList#(Cons(x,xs),Nil()) -> c_4() 5: eqList#(Nil(),Cons(y,ys)) -> c_5() 6: eqList#(Nil(),Nil()) -> c_6() 7: gcd#(Cons(x,xs),Nil()) -> c_7() 8: gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) 9: gcd#(Nil(),Cons(x,xs)) -> c_9() 10: gcd#(Nil(),Nil()) -> c_10() 11: goal#(x,y) -> c_11(gcd#(x,y)) 12: gt0#(Cons(x,xs),Nil()) -> c_12() 13: gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) 14: gt0#(Nil(),y) -> c_14() 15: lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) 16: lgth#(Nil()) -> c_16() 17: monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) 18: and#(False(),False()) -> c_18() 19: and#(False(),True()) -> c_19() 20: and#(True(),False()) -> c_20() 21: and#(True(),True()) -> c_21() 22: gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) 23: gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) 24: gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) 25: gcd[Ite]#(True(),x,y) -> c_25() 26: monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) 27: monus[Ite]#(True(),Cons(x,xs),y) -> c_27() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: @#(Nil(),ys) -> c_2() and#(False(),False()) -> c_18() and#(False(),True()) -> c_19() and#(True(),False()) -> c_20() and#(True(),True()) -> c_21() eqList#(Cons(x,xs),Nil()) -> c_4() eqList#(Nil(),Cons(y,ys)) -> c_5() eqList#(Nil(),Nil()) -> c_6() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gcd[Ite]#(True(),x,y) -> c_25() lgth#(Nil()) -> c_16() monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) monus[Ite]#(True(),Cons(x,xs),y) -> c_27() - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) -->_1 @#(Nil(),ys) -> c_2():13 -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) -->_3 eqList#(Nil(),Nil()) -> c_6():20 -->_2 eqList#(Nil(),Nil()) -> c_6():20 -->_3 eqList#(Nil(),Cons(y,ys)) -> c_5():19 -->_2 eqList#(Nil(),Cons(y,ys)) -> c_5():19 -->_3 eqList#(Cons(x,xs),Nil()) -> c_4():18 -->_2 eqList#(Cons(x,xs),Nil()) -> c_4():18 -->_1 and#(True(),True()) -> c_21():17 -->_1 and#(True(),False()) -> c_20():16 -->_1 and#(False(),True()) -> c_19():15 -->_1 and#(False(),False()) -> c_18():14 -->_3 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 3:S:gcd#(Cons(x,xs),Nil()) -> c_7() 4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):23 -->_1 gcd[Ite]#(True(),x,y) -> c_25():24 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 5:S:gcd#(Nil(),Cons(x,xs)) -> c_9() 6:S:gcd#(Nil(),Nil()) -> c_10() 7:S:goal#(x,y) -> c_11(gcd#(x,y)) -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 8:S:gt0#(Cons(x,xs),Nil()) -> c_12() 9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) -->_1 gt0#(Nil(),y) -> c_14():10 -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8 10:S:gt0#(Nil(),y) -> c_14() 11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) -->_2 lgth#(Nil()) -> c_16():25 -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):26 -->_1 monus[Ite]#(True(),Cons(x,xs),y) -> c_27():27 -->_3 lgth#(Nil()) -> c_16():25 -->_2 eqList#(Nil(),Cons(y,ys)) -> c_5():19 -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 13:W:@#(Nil(),ys) -> c_2() 14:W:and#(False(),False()) -> c_18() 15:W:and#(False(),True()) -> c_19() 16:W:and#(True(),False()) -> c_20() 17:W:and#(True(),True()) -> c_21() 18:W:eqList#(Cons(x,xs),Nil()) -> c_4() 19:W:eqList#(Nil(),Cons(y,ys)) -> c_5() 20:W:eqList#(Nil(),Nil()) -> c_6() 21:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 22:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 23:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):22 -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):21 -->_2 gt0#(Nil(),y) -> c_14():10 -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8 24:W:gcd[Ite]#(True(),x,y) -> c_25() 25:W:lgth#(Nil()) -> c_16() 26:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 27:W:monus[Ite]#(True(),Cons(x,xs),y) -> c_27() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 24: gcd[Ite]#(True(),x,y) -> c_25() 25: lgth#(Nil()) -> c_16() 27: monus[Ite]#(True(),Cons(x,xs),y) -> c_27() 14: and#(False(),False()) -> c_18() 15: and#(False(),True()) -> c_19() 16: and#(True(),False()) -> c_20() 17: and#(True(),True()) -> c_21() 18: eqList#(Cons(x,xs),Nil()) -> c_4() 19: eqList#(Nil(),Cons(y,ys)) -> c_5() 20: eqList#(Nil(),Nil()) -> c_6() 13: @#(Nil(),ys) -> c_2() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/3,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)) -->_3 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)) ,eqList#(x,y) ,eqList#(xs,ys)):2 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 3:S:gcd#(Cons(x,xs),Nil()) -> c_7() 4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):23 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 5:S:gcd#(Nil(),Cons(x,xs)) -> c_9() 6:S:gcd#(Nil(),Nil()) -> c_10() 7:S:goal#(x,y) -> c_11(gcd#(x,y)) -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 8:S:gt0#(Cons(x,xs),Nil()) -> c_12() 9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) -->_1 gt0#(Nil(),y) -> c_14():10 -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8 10:S:gt0#(Nil(),y) -> c_14() 11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):26 -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(and#(eqList(x,y),eqList(xs,ys)),eqList#(x,y),eqList#(xs,ys)):2 21:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 22:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 23:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):22 -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):21 -->_2 gt0#(Nil(),y) -> c_14():10 -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8 26:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) * Step 6: RemoveHeads MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() goal#(x,y) -> c_11(gcd#(x,y)) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:@#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 2:S:eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2 -->_1 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2 3:S:gcd#(Cons(x,xs),Nil()) -> c_7() 4:S:gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) -->_1 gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)):15 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2 5:S:gcd#(Nil(),Cons(x,xs)) -> c_9() 6:S:gcd#(Nil(),Nil()) -> c_10() 7:S:goal#(x,y) -> c_11(gcd#(x,y)) -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 8:S:gt0#(Cons(x,xs),Nil()) -> c_12() 9:S:gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) -->_1 gt0#(Nil(),y) -> c_14():10 -->_1 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_1 gt0#(Cons(x,xs),Nil()) -> c_12():8 10:S:gt0#(Nil(),y) -> c_14() 11:S:lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) -->_2 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_1 @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)):1 12:S:monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) -->_1 monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)):16 -->_3 lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)):11 -->_2 eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)):2 13:W:gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 14:W:gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) -->_2 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 -->_1 gcd#(Nil(),Nil()) -> c_10():6 -->_1 gcd#(Nil(),Cons(x,xs)) -> c_9():5 -->_1 gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)) ,Cons(x',xs') ,Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))):4 -->_1 gcd#(Cons(x,xs),Nil()) -> c_7():3 15:W:gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) -->_1 gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)):14 -->_1 gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)):13 -->_2 gt0#(Nil(),y) -> c_14():10 -->_2 gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)):9 -->_2 gt0#(Cons(x,xs),Nil()) -> c_12():8 16:W:monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) -->_1 monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)):12 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,goal#(x,y) -> c_11(gcd#(x,y)))] * Step 7: NaturalMI MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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(c_1) = {1}, uargs(c_3) = {1,2}, uargs(c_8) = {1,2}, uargs(c_13) = {1}, uargs(c_15) = {1,2}, uargs(c_17) = {1,2,3}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_24) = {1,2}, uargs(c_26) = {1} Following symbols are considered usable: {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#} TcT has computed the following interpretation: p(@) = [2] x1 + [3] p(Cons) = [0] p(False) = [0] p(Nil) = [1] p(True) = [0] p(and) = [3] x1 + [0] p(eqList) = [4] x2 + [5] p(gcd) = [1] x1 + [0] p(gcd[False][Ite]) = [0] p(gcd[Ite]) = [4] p(goal) = [4] p(gt0) = [0] p(lgth) = [1] x1 + [0] p(monus) = [0] p(monus[Ite]) = [4] p(@#) = [0] p(and#) = [0] p(eqList#) = [0] p(gcd#) = [1] p(gcd[False][Ite]#) = [2] x2 + [6] x3 + [1] p(gcd[Ite]#) = [4] x2 + [6] x3 + [1] p(goal#) = [1] x1 + [1] p(gt0#) = [0] p(lgth#) = [0] p(monus#) = [0] p(monus[Ite]#) = [0] p(c_1) = [2] x1 + [0] p(c_2) = [1] p(c_3) = [1] x1 + [4] x2 + [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [1] x2 + [0] p(c_9) = [1] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [4] x1 + [1] x2 + [0] p(c_16) = [0] p(c_17) = [4] x1 + [4] x2 + [1] x3 + [0] p(c_18) = [4] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [1] x1 + [4] x2 + [0] p(c_23) = [1] x1 + [4] x2 + [0] p(c_24) = [1] x1 + [1] x2 + [0] p(c_25) = [0] p(c_26) = [1] x1 + [0] p(c_27) = [1] Following rules are strictly oriented: gcd#(Cons(x,xs),Nil()) = [1] > [0] = c_7() Following rules are (at-least) weakly oriented: @#(Cons(x,xs),ys) = [0] >= [0] = c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) = [0] >= [0] = c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x',xs'),Cons(x,xs)) = [1] >= [1] = c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) = [1] >= [1] = c_9() gcd#(Nil(),Nil()) = [1] >= [1] = c_10() gcd[False][Ite]#(False(),x,y) = [2] x + [6] y + [1] >= [1] = c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) = [2] x + [6] y + [1] >= [1] = c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) = [4] x + [6] y + [1] >= [2] x + [6] y + [1] = c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gt0#(Cons(x,xs),Nil()) = [0] >= [0] = c_12() gt0#(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_13(gt0#(xs',xs)) gt0#(Nil(),y) = [0] >= [0] = c_14() lgth#(Cons(x,xs)) = [0] >= [0] = c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) = [0] >= [0] = c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_26(monus#(xs',xs)) * Step 8: NaturalMI MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd#(Cons(x,xs),Nil()) -> c_7() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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(c_1) = {1}, uargs(c_3) = {1,2}, uargs(c_8) = {1,2}, uargs(c_13) = {1}, uargs(c_15) = {1,2}, uargs(c_17) = {1,2,3}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_24) = {1,2}, uargs(c_26) = {1} Following symbols are considered usable: {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#} TcT has computed the following interpretation: p(@) = [4] p(Cons) = [0] p(False) = [0] p(Nil) = [0] p(True) = [0] p(and) = [4] x1 + [0] p(eqList) = [1] x2 + [2] p(gcd) = [1] x2 + [2] p(gcd[False][Ite]) = [1] x2 + [4] x3 + [1] p(gcd[Ite]) = [4] x1 + [2] x2 + [0] p(goal) = [4] x1 + [1] p(gt0) = [0] p(lgth) = [2] x1 + [7] p(monus) = [2] x1 + [1] x2 + [4] p(monus[Ite]) = [3] x1 + [1] p(@#) = [0] p(and#) = [1] x1 + [1] p(eqList#) = [0] p(gcd#) = [2] p(gcd[False][Ite]#) = [1] x3 + [2] p(gcd[Ite]#) = [1] x2 + [2] x3 + [2] p(goal#) = [4] x1 + [2] x2 + [0] p(gt0#) = [0] p(lgth#) = [0] p(monus#) = [0] p(monus[Ite]#) = [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [2] x1 + [1] x2 + [0] p(c_4) = [4] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] p(c_8) = [1] x1 + [4] x2 + [0] p(c_9) = [2] p(c_10) = [1] p(c_11) = [4] x1 + [0] p(c_12) = [0] p(c_13) = [4] x1 + [0] p(c_14) = [0] p(c_15) = [4] x1 + [4] x2 + [0] p(c_16) = [2] p(c_17) = [4] x1 + [4] x2 + [4] x3 + [0] p(c_18) = [1] p(c_19) = [2] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [4] x2 + [0] p(c_23) = [1] x1 + [1] x2 + [0] p(c_24) = [1] x1 + [4] x2 + [0] p(c_25) = [2] p(c_26) = [1] x1 + [0] p(c_27) = [2] Following rules are strictly oriented: gcd#(Nil(),Nil()) = [2] > [1] = c_10() Following rules are (at-least) weakly oriented: @#(Cons(x,xs),ys) = [0] >= [0] = c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) = [0] >= [0] = c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) = [2] >= [2] = c_7() gcd#(Cons(x',xs'),Cons(x,xs)) = [2] >= [2] = c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) = [2] >= [2] = c_9() gcd[False][Ite]#(False(),x,y) = [1] y + [2] >= [2] = c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) = [1] y + [2] >= [2] = c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) = [1] x + [2] y + [2] >= [1] y + [2] = c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gt0#(Cons(x,xs),Nil()) = [0] >= [0] = c_12() gt0#(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_13(gt0#(xs',xs)) gt0#(Nil(),y) = [0] >= [0] = c_14() lgth#(Cons(x,xs)) = [0] >= [0] = c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) = [0] >= [0] = c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_26(monus#(xs',xs)) * Step 9: NaturalMI MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Cons(x,xs)) -> c_9() gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Nil(),Nil()) -> c_10() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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(c_1) = {1}, uargs(c_3) = {1,2}, uargs(c_8) = {1,2}, uargs(c_13) = {1}, uargs(c_15) = {1,2}, uargs(c_17) = {1,2,3}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_24) = {1,2}, uargs(c_26) = {1} Following symbols are considered usable: {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal#,gt0#,lgth#,monus#,monus[Ite]#} TcT has computed the following interpretation: p(@) = [4] x2 + [0] p(Cons) = [0] p(False) = [0] p(Nil) = [0] p(True) = [0] p(and) = [5] x1 + [2] x2 + [6] p(eqList) = [3] x2 + [1] p(gcd) = [0] p(gcd[False][Ite]) = [2] x2 + [1] p(gcd[Ite]) = [0] p(goal) = [0] p(gt0) = [0] p(lgth) = [1] x1 + [0] p(monus) = [0] p(monus[Ite]) = [1] x3 + [5] p(@#) = [0] p(and#) = [0] p(eqList#) = [0] p(gcd#) = [4] p(gcd[False][Ite]#) = [4] p(gcd[Ite]#) = [4] p(goal#) = [2] x2 + [1] p(gt0#) = [0] p(lgth#) = [0] p(monus#) = [0] p(monus[Ite]#) = [0] p(c_1) = [4] x1 + [0] p(c_2) = [0] p(c_3) = [1] x1 + [4] x2 + [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [2] p(c_7) = [4] p(c_8) = [1] x1 + [2] x2 + [0] p(c_9) = [3] p(c_10) = [0] p(c_11) = [1] p(c_12) = [0] p(c_13) = [4] x1 + [0] p(c_14) = [0] p(c_15) = [2] x1 + [1] x2 + [0] p(c_16) = [1] p(c_17) = [4] x1 + [4] x2 + [4] x3 + [0] p(c_18) = [2] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [2] x2 + [0] p(c_23) = [1] x1 + [2] x2 + [0] p(c_24) = [1] x1 + [4] x2 + [0] p(c_25) = [1] p(c_26) = [1] x1 + [0] p(c_27) = [1] Following rules are strictly oriented: gcd#(Nil(),Cons(x,xs)) = [4] > [3] = c_9() Following rules are (at-least) weakly oriented: @#(Cons(x,xs),ys) = [0] >= [0] = c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) = [0] >= [0] = c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x,xs),Nil()) = [4] >= [4] = c_7() gcd#(Cons(x',xs'),Cons(x,xs)) = [4] >= [4] = c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)),eqList#(Cons(x',xs'),Cons(x,xs))) gcd#(Nil(),Nil()) = [4] >= [0] = c_10() gcd[False][Ite]#(False(),x,y) = [4] >= [4] = c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) = [4] >= [4] = c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) = [4] >= [4] = c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) gt0#(Cons(x,xs),Nil()) = [0] >= [0] = c_12() gt0#(Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_13(gt0#(xs',xs)) gt0#(Nil(),y) = [0] >= [0] = c_14() lgth#(Cons(x,xs)) = [0] >= [0] = c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) = [0] >= [0] = c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y),eqList#(lgth(y),Cons(Nil(),Nil())),lgth#(y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) = [0] >= [0] = c_26(monus#(xs',xs)) * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: @#(Cons(x,xs),ys) -> c_1(@#(xs,ys)) eqList#(Cons(x,xs),Cons(y,ys)) -> c_3(eqList#(x,y),eqList#(xs,ys)) gcd#(Cons(x',xs'),Cons(x,xs)) -> c_8(gcd[Ite]#(eqList(Cons(x',xs'),Cons(x,xs)),Cons(x',xs'),Cons(x,xs)) ,eqList#(Cons(x',xs'),Cons(x,xs))) gt0#(Cons(x,xs),Nil()) -> c_12() gt0#(Cons(x',xs'),Cons(x,xs)) -> c_13(gt0#(xs',xs)) gt0#(Nil(),y) -> c_14() lgth#(Cons(x,xs)) -> c_15(@#(Cons(Nil(),Nil()),lgth(xs)),lgth#(xs)) monus#(x,y) -> c_17(monus[Ite]#(eqList(lgth(y),Cons(Nil(),Nil())),x,y) ,eqList#(lgth(y),Cons(Nil(),Nil())) ,lgth#(y)) - Weak DPs: gcd#(Cons(x,xs),Nil()) -> c_7() gcd#(Nil(),Cons(x,xs)) -> c_9() gcd#(Nil(),Nil()) -> c_10() gcd[False][Ite]#(False(),x,y) -> c_22(gcd#(monus(y,x),x),monus#(y,x)) gcd[False][Ite]#(True(),x,y) -> c_23(gcd#(y,monus(x,y)),monus#(x,y)) gcd[Ite]#(False(),x,y) -> c_24(gcd[False][Ite]#(gt0(x,y),x,y),gt0#(x,y)) monus[Ite]#(False(),Cons(x',xs'),Cons(x,xs)) -> c_26(monus#(xs',xs)) - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() eqList(Cons(x,xs),Cons(y,ys)) -> and(eqList(x,y),eqList(xs,ys)) eqList(Cons(x,xs),Nil()) -> False() eqList(Nil(),Cons(y,ys)) -> False() eqList(Nil(),Nil()) -> True() gt0(Cons(x,xs),Nil()) -> True() gt0(Cons(x',xs'),Cons(x,xs)) -> gt0(xs',xs) gt0(Nil(),y) -> False() lgth(Cons(x,xs)) -> @(Cons(Nil(),Nil()),lgth(xs)) lgth(Nil()) -> Nil() monus(x,y) -> monus[Ite](eqList(lgth(y),Cons(Nil(),Nil())),x,y) monus[Ite](False(),Cons(x',xs'),Cons(x,xs)) -> monus(xs',xs) monus[Ite](True(),Cons(x,xs),y) -> xs - Signature: {@/2,and/2,eqList/2,gcd/2,gcd[False][Ite]/3,gcd[Ite]/3,goal/2,gt0/2,lgth/1,monus/2,monus[Ite]/3,@#/2,and#/2 ,eqList#/2,gcd#/2,gcd[False][Ite]#/3,gcd[Ite]#/3,goal#/2,gt0#/2,lgth#/1,monus#/2,monus[Ite]#/3} / {Cons/2 ,False/0,Nil/0,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/1,c_12/0,c_13/1 ,c_14/0,c_15/2,c_16/0,c_17/3,c_18/0,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2,c_25/0,c_26/1,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {@#,and#,eqList#,gcd#,gcd[False][Ite]#,gcd[Ite]#,goal# ,gt0#,lgth#,monus#,monus[Ite]#} and constructors {Cons,False,Nil,True} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE