MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) app(nil(),k) -> k gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {app,gt,id,if,minus,not,plus,quot,sum} and constructors {0 ,cons,false,nil,s,true,zero} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) app(nil(),k) -> k gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {app,gt,id,if,minus,not,plus,quot,sum} and constructors {0 ,cons,false,nil,s,true,zero} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs app#(l,nil()) -> c_1() app#(cons(x,l),k) -> c_2(app#(l,k)) app#(nil(),k) -> c_3() gt#(s(x),s(y)) -> c_4(gt#(x,y)) gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) not#(x) -> c_13(if#(x,false(),true())) plus#(0(),y) -> c_14() plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(app(l,cons(x,cons(y,k)))) -> c_21(sum#(app(l,sum(cons(x,cons(y,k))))) ,app#(l,sum(cons(x,cons(y,k)))) ,sum#(cons(x,cons(y,k)))) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) sum#(cons(x,nil())) -> c_23() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: app#(l,nil()) -> c_1() app#(cons(x,l),k) -> c_2(app#(l,k)) app#(nil(),k) -> c_3() gt#(s(x),s(y)) -> c_4(gt#(x,y)) gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) not#(x) -> c_13(if#(x,false(),true())) plus#(0(),y) -> c_14() plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(app(l,cons(x,cons(y,k)))) -> c_21(sum#(app(l,sum(cons(x,cons(y,k))))) ,app#(l,sum(cons(x,cons(y,k)))) ,sum#(cons(x,cons(y,k)))) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) sum#(cons(x,nil())) -> c_23() - Weak TRS: app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) app(nil(),k) -> k gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/5,c_16/1,c_17/8,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y app#(l,nil()) -> c_1() app#(cons(x,l),k) -> c_2(app#(l,k)) app#(nil(),k) -> c_3() gt#(s(x),s(y)) -> c_4(gt#(x,y)) gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) not#(x) -> c_13(if#(x,false(),true())) plus#(0(),y) -> c_14() plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) sum#(cons(x,nil())) -> c_23() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(l,nil()) -> c_1() app#(cons(x,l),k) -> c_2(app#(l,k)) app#(nil(),k) -> c_3() gt#(s(x),s(y)) -> c_4(gt#(x,y)) gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) not#(x) -> c_13(if#(x,false(),true())) plus#(0(),y) -> c_14() plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) sum#(cons(x,nil())) -> c_23() - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/5,c_16/1,c_17/8,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,6,7,8,9,10,14,18,19,22} by application of Pre({1,3,5,6,7,8,9,10,14,18,19,22}) = {2,4,11,12,13,15,16,17,20,21}. Here rules are labelled as follows: 1: app#(l,nil()) -> c_1() 2: app#(cons(x,l),k) -> c_2(app#(l,k)) 3: app#(nil(),k) -> c_3() 4: gt#(s(x),s(y)) -> c_4(gt#(x,y)) 5: gt#(s(x),zero()) -> c_5() 6: gt#(zero(),y) -> c_6() 7: id#(x) -> c_7() 8: if#(false(),x,y) -> c_8() 9: if#(true(),x,y) -> c_9() 10: minus#(x,0()) -> c_10() 11: minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) 12: minus#(s(x),s(y)) -> c_12(minus#(x,y)) 13: not#(x) -> c_13(if#(x,false(),true())) 14: plus#(0(),y) -> c_14() 15: plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) 16: plus#(s(x),y) -> c_16(plus#(x,y)) 17: plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) 18: plus#(zero(),y) -> c_18() 19: quot#(0(),s(y)) -> c_19() 20: quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) 21: sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) 22: sum#(cons(x,nil())) -> c_23() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: app#(cons(x,l),k) -> c_2(app#(l,k)) gt#(s(x),s(y)) -> c_4(gt#(x,y)) minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) not#(x) -> c_13(if#(x,false(),true())) plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) - Weak DPs: app#(l,nil()) -> c_1() app#(nil(),k) -> c_3() gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() plus#(0(),y) -> c_14() plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() sum#(cons(x,nil())) -> c_23() - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/5,c_16/1,c_17/8,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5} by application of Pre({5}) = {8}. Here rules are labelled as follows: 1: app#(cons(x,l),k) -> c_2(app#(l,k)) 2: gt#(s(x),s(y)) -> c_4(gt#(x,y)) 3: minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) 4: minus#(s(x),s(y)) -> c_12(minus#(x,y)) 5: not#(x) -> c_13(if#(x,false(),true())) 6: plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) 7: plus#(s(x),y) -> c_16(plus#(x,y)) 8: plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) 9: quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) 10: sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) 11: app#(l,nil()) -> c_1() 12: app#(nil(),k) -> c_3() 13: gt#(s(x),zero()) -> c_5() 14: gt#(zero(),y) -> c_6() 15: id#(x) -> c_7() 16: if#(false(),x,y) -> c_8() 17: if#(true(),x,y) -> c_9() 18: minus#(x,0()) -> c_10() 19: plus#(0(),y) -> c_14() 20: plus#(zero(),y) -> c_18() 21: quot#(0(),s(y)) -> c_19() 22: sum#(cons(x,nil())) -> c_23() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: app#(cons(x,l),k) -> c_2(app#(l,k)) gt#(s(x),s(y)) -> c_4(gt#(x,y)) minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) - Weak DPs: app#(l,nil()) -> c_1() app#(nil(),k) -> c_3() gt#(s(x),zero()) -> c_5() gt#(zero(),y) -> c_6() id#(x) -> c_7() if#(false(),x,y) -> c_8() if#(true(),x,y) -> c_9() minus#(x,0()) -> c_10() not#(x) -> c_13(if#(x,false(),true())) plus#(0(),y) -> c_14() plus#(zero(),y) -> c_18() quot#(0(),s(y)) -> c_19() sum#(cons(x,nil())) -> c_23() - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/5,c_16/1,c_17/8,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:app#(cons(x,l),k) -> c_2(app#(l,k)) -->_1 app#(nil(),k) -> c_3():11 -->_1 app#(l,nil()) -> c_1():10 -->_1 app#(cons(x,l),k) -> c_2(app#(l,k)):1 2:S:gt#(s(x),s(y)) -> c_4(gt#(x,y)) -->_1 gt#(zero(),y) -> c_6():13 -->_1 gt#(s(x),zero()) -> c_5():12 -->_1 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 3:S:minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) -->_2 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_2 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_2 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_2 plus#(zero(),y) -> c_18():20 -->_2 plus#(0(),y) -> c_14():19 -->_1 minus#(x,0()) -> c_10():17 -->_1 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 4:S:minus#(s(x),s(y)) -> c_12(minus#(x,y)) -->_1 minus#(x,0()) -> c_10():17 -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 5:S:plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(zero(),y) -> c_18():20 -->_1 plus#(0(),y) -> c_14():19 -->_2 if#(true(),x,y) -> c_9():16 -->_2 if#(false(),x,y) -> c_8():15 -->_5 id#(x) -> c_7():14 -->_4 id#(x) -> c_7():14 -->_3 gt#(zero(),y) -> c_6():13 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_3 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 6:S:plus#(s(x),y) -> c_16(plus#(x,y)) -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(zero(),y) -> c_18():20 -->_1 plus#(0(),y) -> c_14():19 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 7:S:plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) -->_5 not#(x) -> c_13(if#(x,false(),true())):18 -->_1 plus#(zero(),y) -> c_18():20 -->_1 plus#(0(),y) -> c_14():19 -->_4 if#(true(),x,y) -> c_9():16 -->_2 if#(true(),x,y) -> c_9():16 -->_4 if#(false(),x,y) -> c_8():15 -->_2 if#(false(),x,y) -> c_8():15 -->_8 id#(x) -> c_7():14 -->_7 id#(x) -> c_7():14 -->_6 gt#(zero(),y) -> c_6():13 -->_3 gt#(zero(),y) -> c_6():13 -->_6 gt#(s(x),zero()) -> c_5():12 -->_3 gt#(s(x),zero()) -> c_5():12 -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_6 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 -->_3 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 8:S:quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) -->_1 quot#(0(),s(y)) -> c_19():21 -->_2 minus#(x,0()) -> c_10():17 -->_1 quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)):8 -->_2 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_2 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 9:S:sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) -->_1 sum#(cons(x,nil())) -> c_23():22 -->_2 plus#(zero(),y) -> c_18():20 -->_2 plus#(0(),y) -> c_14():19 -->_1 sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)):9 -->_2 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_2 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_2 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 10:W:app#(l,nil()) -> c_1() 11:W:app#(nil(),k) -> c_3() 12:W:gt#(s(x),zero()) -> c_5() 13:W:gt#(zero(),y) -> c_6() 14:W:id#(x) -> c_7() 15:W:if#(false(),x,y) -> c_8() 16:W:if#(true(),x,y) -> c_9() 17:W:minus#(x,0()) -> c_10() 18:W:not#(x) -> c_13(if#(x,false(),true())) -->_1 if#(true(),x,y) -> c_9():16 -->_1 if#(false(),x,y) -> c_8():15 19:W:plus#(0(),y) -> c_14() 20:W:plus#(zero(),y) -> c_18() 21:W:quot#(0(),s(y)) -> c_19() 22:W:sum#(cons(x,nil())) -> c_23() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 22: sum#(cons(x,nil())) -> c_23() 21: quot#(0(),s(y)) -> c_19() 17: minus#(x,0()) -> c_10() 14: id#(x) -> c_7() 19: plus#(0(),y) -> c_14() 20: plus#(zero(),y) -> c_18() 18: not#(x) -> c_13(if#(x,false(),true())) 15: if#(false(),x,y) -> c_8() 16: if#(true(),x,y) -> c_9() 12: gt#(s(x),zero()) -> c_5() 13: gt#(zero(),y) -> c_6() 10: app#(l,nil()) -> c_1() 11: app#(nil(),k) -> c_3() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: app#(cons(x,l),k) -> c_2(app#(l,k)) gt#(s(x),s(y)) -> c_4(gt#(x,y)) minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),if#(gt(x,x),id(x),id(x)),gt#(x,x),id#(x),id#(x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/5,c_16/1,c_17/8,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:app#(cons(x,l),k) -> c_2(app#(l,k)) -->_1 app#(cons(x,l),k) -> c_2(app#(l,k)):1 2:S:gt#(s(x),s(y)) -> c_4(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 3:S:minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) -->_2 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_2 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_2 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 4:S:minus#(s(x),s(y)) -> c_12(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_1 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 5:S:plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)) -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_3 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 6:S:plus#(s(x),y) -> c_16(plus#(x,y)) -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 7:S:plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)) -->_1 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_1 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_1 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 -->_6 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 -->_3 gt#(s(x),s(y)) -> c_4(gt#(x,y)):2 8:S:quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) -->_1 quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)):8 -->_2 minus#(s(x),s(y)) -> c_12(minus#(x,y)):4 -->_2 minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)):3 9:S:sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) -->_1 sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)):9 -->_2 plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) ,if#(gt(x,y),x,y) ,gt#(x,y) ,if#(not(gt(x,y)),id(x),id(y)) ,not#(gt(x,y)) ,gt#(x,y) ,id#(x) ,id#(y)):7 -->_2 plus#(s(x),y) -> c_16(plus#(x,y)):6 -->_2 plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)) ,if#(gt(x,x),id(x),id(x)) ,gt#(x,x) ,id#(x) ,id#(x)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: app#(cons(x,l),k) -> c_2(app#(l,k)) gt#(s(x),s(y)) -> c_4(gt#(x,y)) minus#(minus(x,y),z) -> c_11(minus#(x,plus(y,z)),plus#(y,z)) minus#(s(x),s(y)) -> c_12(minus#(x,y)) plus#(s(x),x) -> c_15(plus#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) plus#(s(x),y) -> c_16(plus#(x,y)) plus#(s(x),s(y)) -> c_17(plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) quot#(s(x),s(y)) -> c_20(quot#(minus(x,y),s(y)),minus#(x,y)) sum#(cons(x,cons(y,l))) -> c_22(sum#(cons(plus(x,y),l)),plus#(x,y)) - Weak TRS: gt(s(x),s(y)) -> gt(x,y) gt(s(x),zero()) -> true() gt(zero(),y) -> false() id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x minus(x,0()) -> x minus(minus(x,y),z) -> minus(x,plus(y,z)) minus(s(x),s(y)) -> minus(x,y) not(x) -> if(x,false(),true()) plus(0(),y) -> y plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(s(x),y) -> s(plus(x,y)) plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(zero(),y) -> y - Signature: {app/2,gt/2,id/1,if/3,minus/2,not/1,plus/2,quot/2,sum/1,app#/2,gt#/2,id#/1,if#/3,minus#/2,not#/1,plus#/2 ,quot#/2,sum#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,zero/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/0 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/1,c_13/1,c_14/0,c_15/2,c_16/1,c_17/3,c_18/0,c_19/0,c_20/2,c_21/3,c_22/2 ,c_23/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#,gt#,id#,if#,minus#,not#,plus#,quot# ,sum#} and constructors {0,cons,false,nil,s,true,zero} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE