MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,f,g,gt,h,id,if,k,m,minus,n,not,p ,t} and constructors {0,false,s,true} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. p(id(x),s(y)) -> s(p(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: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,f,g,gt,h,id,if,k,m,minus,n,not,p ,t} and constructors {0,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs and#(x,false()) -> c_1() and#(true(),true()) -> c_2() f#(0()) -> c_3() f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(0()) -> c_9() h#(s(x)) -> c_10(f#(x)) id#(x) -> c_11() if#(false(),x,y) -> c_12() if#(true(),x,y) -> c_13() k#(0(),s(y)) -> c_14() k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(x,0()) -> c_16() m#(0(),y) -> c_17() m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(x,0()) -> c_19() minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(x,0()) -> c_21() n#(0(),y) -> c_22() n#(s(x),s(y)) -> c_23(n#(x,y)) not#(x) -> c_24(if#(x,false(),true())) p#(0(),y) -> c_25() p#(s(x),x) -> c_26(p#(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)) p#(s(x),s(y)) -> c_27(p#(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)) t#(x) -> c_28(p#(x,x)) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: and#(x,false()) -> c_1() and#(true(),true()) -> c_2() f#(0()) -> c_3() f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(0()) -> c_9() h#(s(x)) -> c_10(f#(x)) id#(x) -> c_11() if#(false(),x,y) -> c_12() if#(true(),x,y) -> c_13() k#(0(),s(y)) -> c_14() k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(x,0()) -> c_16() m#(0(),y) -> c_17() m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(x,0()) -> c_19() minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(x,0()) -> c_21() n#(0(),y) -> c_22() n#(s(x),s(y)) -> c_23(n#(x,y)) not#(x) -> c_24(if#(x,false(),true())) p#(0(),y) -> c_25() p#(s(x),x) -> c_26(p#(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)) p#(s(x),s(y)) -> c_27(p#(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)) t#(x) -> c_28(p#(x,x)) - Weak TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3 ,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p# ,t#} and constructors {0,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,6,7,9,11,12,13,14,16,17,19,21,22,25} by application of Pre({1,2,3,6,7,9,11,12,13,14,16,17,19,21,22,25}) = {4,5,8,10,15,18,20,23,24,26,27,28}. Here rules are labelled as follows: 1: and#(x,false()) -> c_1() 2: and#(true(),true()) -> c_2() 3: f#(0()) -> c_3() 4: f#(s(x)) -> c_4(h#(x)) 5: g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) 6: gt#(0(),y) -> c_6() 7: gt#(s(x),0()) -> c_7() 8: gt#(s(x),s(y)) -> c_8(gt#(x,y)) 9: h#(0()) -> c_9() 10: h#(s(x)) -> c_10(f#(x)) 11: id#(x) -> c_11() 12: if#(false(),x,y) -> c_12() 13: if#(true(),x,y) -> c_13() 14: k#(0(),s(y)) -> c_14() 15: k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) 16: m#(x,0()) -> c_16() 17: m#(0(),y) -> c_17() 18: m#(s(x),s(y)) -> c_18(m#(x,y)) 19: minus#(x,0()) -> c_19() 20: minus#(s(x),s(y)) -> c_20(minus#(x,y)) 21: n#(x,0()) -> c_21() 22: n#(0(),y) -> c_22() 23: n#(s(x),s(y)) -> c_23(n#(x,y)) 24: not#(x) -> c_24(if#(x,false(),true())) 25: p#(0(),y) -> c_25() 26: p#(s(x),x) -> c_26(p#(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)) 27: p#(s(x),s(y)) -> c_27(p#(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)) 28: t#(x) -> c_28(p#(x,x)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(s(x)) -> c_10(f#(x)) k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(s(x),s(y)) -> c_23(n#(x,y)) not#(x) -> c_24(if#(x,false(),true())) p#(s(x),x) -> c_26(p#(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)) p#(s(x),s(y)) -> c_27(p#(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)) t#(x) -> c_28(p#(x,x)) - Weak DPs: and#(x,false()) -> c_1() and#(true(),true()) -> c_2() f#(0()) -> c_3() gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() h#(0()) -> c_9() id#(x) -> c_11() if#(false(),x,y) -> c_12() if#(true(),x,y) -> c_13() k#(0(),s(y)) -> c_14() m#(x,0()) -> c_16() m#(0(),y) -> c_17() minus#(x,0()) -> c_19() n#(x,0()) -> c_21() n#(0(),y) -> c_22() p#(0(),y) -> c_25() - Weak TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3 ,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p# ,t#} and constructors {0,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {9} by application of Pre({9}) = {11}. Here rules are labelled as follows: 1: f#(s(x)) -> c_4(h#(x)) 2: g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) 3: gt#(s(x),s(y)) -> c_8(gt#(x,y)) 4: h#(s(x)) -> c_10(f#(x)) 5: k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) 6: m#(s(x),s(y)) -> c_18(m#(x,y)) 7: minus#(s(x),s(y)) -> c_20(minus#(x,y)) 8: n#(s(x),s(y)) -> c_23(n#(x,y)) 9: not#(x) -> c_24(if#(x,false(),true())) 10: p#(s(x),x) -> c_26(p#(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)) 11: p#(s(x),s(y)) -> c_27(p#(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)) 12: t#(x) -> c_28(p#(x,x)) 13: and#(x,false()) -> c_1() 14: and#(true(),true()) -> c_2() 15: f#(0()) -> c_3() 16: gt#(0(),y) -> c_6() 17: gt#(s(x),0()) -> c_7() 18: h#(0()) -> c_9() 19: id#(x) -> c_11() 20: if#(false(),x,y) -> c_12() 21: if#(true(),x,y) -> c_13() 22: k#(0(),s(y)) -> c_14() 23: m#(x,0()) -> c_16() 24: m#(0(),y) -> c_17() 25: minus#(x,0()) -> c_19() 26: n#(x,0()) -> c_21() 27: n#(0(),y) -> c_22() 28: p#(0(),y) -> c_25() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(s(x)) -> c_10(f#(x)) k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(s(x),s(y)) -> c_23(n#(x,y)) p#(s(x),x) -> c_26(p#(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)) p#(s(x),s(y)) -> c_27(p#(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)) t#(x) -> c_28(p#(x,x)) - Weak DPs: and#(x,false()) -> c_1() and#(true(),true()) -> c_2() f#(0()) -> c_3() gt#(0(),y) -> c_6() gt#(s(x),0()) -> c_7() h#(0()) -> c_9() id#(x) -> c_11() if#(false(),x,y) -> c_12() if#(true(),x,y) -> c_13() k#(0(),s(y)) -> c_14() m#(x,0()) -> c_16() m#(0(),y) -> c_17() minus#(x,0()) -> c_19() n#(x,0()) -> c_21() n#(0(),y) -> c_22() not#(x) -> c_24(if#(x,false(),true())) p#(0(),y) -> c_25() - Weak TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3 ,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p# ,t#} and constructors {0,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(s(x)) -> c_4(h#(x)) -->_1 h#(s(x)) -> c_10(f#(x)):4 -->_1 h#(0()) -> c_9():17 2:S:g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) -->_5 t#(x) -> c_28(p#(x,x)):11 -->_17 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_16 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_12 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_10 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_14 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_8 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_15 m#(s(x),s(y)) -> c_18(m#(x,y)):6 -->_9 m#(s(x),s(y)) -> c_18(m#(x,y)):6 -->_11 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 -->_7 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 -->_16 n#(0(),y) -> c_22():26 -->_10 n#(0(),y) -> c_22():26 -->_16 n#(x,0()) -> c_21():25 -->_10 n#(x,0()) -> c_21():25 -->_14 minus#(x,0()) -> c_19():24 -->_8 minus#(x,0()) -> c_19():24 -->_15 m#(0(),y) -> c_17():23 -->_9 m#(0(),y) -> c_17():23 -->_15 m#(x,0()) -> c_16():22 -->_9 m#(x,0()) -> c_16():22 -->_11 k#(0(),s(y)) -> c_14():21 -->_7 k#(0(),s(y)) -> c_14():21 -->_1 if#(true(),x,y) -> c_13():20 -->_1 if#(false(),x,y) -> c_12():19 -->_2 and#(true(),true()) -> c_2():13 -->_2 and#(x,false()) -> c_1():12 -->_13 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))):2 -->_6 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))):2 -->_4 f#(s(x)) -> c_4(h#(x)):1 -->_3 f#(s(x)) -> c_4(h#(x)):1 3:S:gt#(s(x),s(y)) -> c_8(gt#(x,y)) -->_1 gt#(s(x),0()) -> c_7():16 -->_1 gt#(0(),y) -> c_6():15 -->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 4:S:h#(s(x)) -> c_10(f#(x)) -->_1 f#(0()) -> c_3():14 -->_1 f#(s(x)) -> c_4(h#(x)):1 5:S:k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) -->_2 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_2 minus#(x,0()) -> c_19():24 -->_1 k#(0(),s(y)) -> c_14():21 -->_1 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 6:S:m#(s(x),s(y)) -> c_18(m#(x,y)) -->_1 m#(0(),y) -> c_17():23 -->_1 m#(x,0()) -> c_16():22 -->_1 m#(s(x),s(y)) -> c_18(m#(x,y)):6 7:S:minus#(s(x),s(y)) -> c_20(minus#(x,y)) -->_1 minus#(x,0()) -> c_19():24 -->_1 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 8:S:n#(s(x),s(y)) -> c_23(n#(x,y)) -->_1 n#(0(),y) -> c_22():26 -->_1 n#(x,0()) -> c_21():25 -->_1 n#(s(x),s(y)) -> c_23(n#(x,y)):8 9:S:p#(s(x),x) -> c_26(p#(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 p#(s(x),s(y)) -> c_27(p#(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)):10 -->_1 p#(0(),y) -> c_25():28 -->_2 if#(true(),x,y) -> c_13():20 -->_2 if#(false(),x,y) -> c_12():19 -->_5 id#(x) -> c_11():18 -->_4 id#(x) -> c_11():18 -->_3 gt#(0(),y) -> c_6():15 -->_1 p#(s(x),x) -> c_26(p#(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)):9 -->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 10:S:p#(s(x),s(y)) -> c_27(p#(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_24(if#(x,false(),true())):27 -->_1 p#(0(),y) -> c_25():28 -->_4 if#(true(),x,y) -> c_13():20 -->_2 if#(true(),x,y) -> c_13():20 -->_4 if#(false(),x,y) -> c_12():19 -->_2 if#(false(),x,y) -> c_12():19 -->_8 id#(x) -> c_11():18 -->_7 id#(x) -> c_11():18 -->_6 gt#(s(x),0()) -> c_7():16 -->_3 gt#(s(x),0()) -> c_7():16 -->_6 gt#(0(),y) -> c_6():15 -->_3 gt#(0(),y) -> c_6():15 -->_1 p#(s(x),s(y)) -> c_27(p#(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)):10 -->_1 p#(s(x),x) -> c_26(p#(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)):9 -->_6 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 -->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 11:S:t#(x) -> c_28(p#(x,x)) -->_1 p#(0(),y) -> c_25():28 -->_1 p#(s(x),s(y)) -> c_27(p#(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)):10 12:W:and#(x,false()) -> c_1() 13:W:and#(true(),true()) -> c_2() 14:W:f#(0()) -> c_3() 15:W:gt#(0(),y) -> c_6() 16:W:gt#(s(x),0()) -> c_7() 17:W:h#(0()) -> c_9() 18:W:id#(x) -> c_11() 19:W:if#(false(),x,y) -> c_12() 20:W:if#(true(),x,y) -> c_13() 21:W:k#(0(),s(y)) -> c_14() 22:W:m#(x,0()) -> c_16() 23:W:m#(0(),y) -> c_17() 24:W:minus#(x,0()) -> c_19() 25:W:n#(x,0()) -> c_21() 26:W:n#(0(),y) -> c_22() 27:W:not#(x) -> c_24(if#(x,false(),true())) -->_1 if#(true(),x,y) -> c_13():20 -->_1 if#(false(),x,y) -> c_12():19 28:W:p#(0(),y) -> c_25() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: and#(x,false()) -> c_1() 13: and#(true(),true()) -> c_2() 21: k#(0(),s(y)) -> c_14() 22: m#(x,0()) -> c_16() 23: m#(0(),y) -> c_17() 24: minus#(x,0()) -> c_19() 25: n#(x,0()) -> c_21() 26: n#(0(),y) -> c_22() 15: gt#(0(),y) -> c_6() 16: gt#(s(x),0()) -> c_7() 18: id#(x) -> c_11() 27: not#(x) -> c_24(if#(x,false(),true())) 19: if#(false(),x,y) -> c_12() 20: if#(true(),x,y) -> c_13() 28: p#(0(),y) -> c_25() 17: h#(0()) -> c_9() 14: f#(0()) -> c_3() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(s(x)) -> c_10(f#(x)) k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(s(x),s(y)) -> c_23(n#(x,y)) p#(s(x),x) -> c_26(p#(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)) p#(s(x),s(y)) -> c_27(p#(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)) t#(x) -> c_28(p#(x,x)) - Weak TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3 ,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/17,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/0,c_26/5,c_27/8,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p# ,t#} and constructors {0,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(s(x)) -> c_4(h#(x)) -->_1 h#(s(x)) -> c_10(f#(x)):4 2:S:g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) -->_5 t#(x) -> c_28(p#(x,x)):11 -->_17 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_16 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_12 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_10 n#(s(x),s(y)) -> c_23(n#(x,y)):8 -->_14 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_8 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_15 m#(s(x),s(y)) -> c_18(m#(x,y)):6 -->_9 m#(s(x),s(y)) -> c_18(m#(x,y)):6 -->_11 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 -->_7 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 -->_13 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))):2 -->_6 g#(s(x),s(y)) -> c_5(if#(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) ,and#(f(s(x)),f(s(y))) ,f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))):2 -->_4 f#(s(x)) -> c_4(h#(x)):1 -->_3 f#(s(x)) -> c_4(h#(x)):1 3:S:gt#(s(x),s(y)) -> c_8(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 4:S:h#(s(x)) -> c_10(f#(x)) -->_1 f#(s(x)) -> c_4(h#(x)):1 5:S:k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) -->_2 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 -->_1 k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)):5 6:S:m#(s(x),s(y)) -> c_18(m#(x,y)) -->_1 m#(s(x),s(y)) -> c_18(m#(x,y)):6 7:S:minus#(s(x),s(y)) -> c_20(minus#(x,y)) -->_1 minus#(s(x),s(y)) -> c_20(minus#(x,y)):7 8:S:n#(s(x),s(y)) -> c_23(n#(x,y)) -->_1 n#(s(x),s(y)) -> c_23(n#(x,y)):8 9:S:p#(s(x),x) -> c_26(p#(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 p#(s(x),s(y)) -> c_27(p#(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)):10 -->_1 p#(s(x),x) -> c_26(p#(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)):9 -->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 10:S:p#(s(x),s(y)) -> c_27(p#(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 p#(s(x),s(y)) -> c_27(p#(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)):10 -->_1 p#(s(x),x) -> c_26(p#(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)):9 -->_6 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 -->_3 gt#(s(x),s(y)) -> c_8(gt#(x,y)):3 11:S:t#(x) -> c_28(p#(x,x)) -->_1 p#(s(x),s(y)) -> c_27(p#(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)):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g#(s(x),s(y)) -> c_5(f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: f#(s(x)) -> c_4(h#(x)) g#(s(x),s(y)) -> c_5(f#(s(x)) ,f#(s(y)) ,t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) ,k#(minus(m(x,y),n(x,y)),s(s(0()))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,k#(n(s(x),s(y)),s(s(0()))) ,n#(s(x),s(y)) ,g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) ,minus#(m(x,y),n(x,y)) ,m#(x,y) ,n#(x,y) ,n#(s(x),s(y))) gt#(s(x),s(y)) -> c_8(gt#(x,y)) h#(s(x)) -> c_10(f#(x)) k#(s(x),s(y)) -> c_15(k#(minus(x,y),s(y)),minus#(x,y)) m#(s(x),s(y)) -> c_18(m#(x,y)) minus#(s(x),s(y)) -> c_20(minus#(x,y)) n#(s(x),s(y)) -> c_23(n#(x,y)) p#(s(x),x) -> c_26(p#(if(gt(x,x),id(x),id(x)),s(x)),gt#(x,x)) p#(s(x),s(y)) -> c_27(p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))),gt#(x,y),gt#(x,y)) t#(x) -> c_28(p#(x,x)) - Weak TRS: and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))) ,t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) ,g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) h(0()) -> false() h(s(x)) -> f(x) id(x) -> x if(false(),x,y) -> y if(true(),x,y) -> x k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) m(x,0()) -> x m(0(),y) -> y m(s(x),s(y)) -> s(m(x,y)) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) n(x,0()) -> 0() n(0(),y) -> 0() n(s(x),s(y)) -> s(n(x,y)) not(x) -> if(x,false(),true()) p(0(),y) -> y p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) t(x) -> p(x,x) - Signature: {and/2,f/1,g/2,gt/2,h/1,id/1,if/3,k/2,m/2,minus/2,n/2,not/1,p/2,t/1,and#/2,f#/1,g#/2,gt#/2,h#/1,id#/1,if#/3 ,k#/2,m#/2,minus#/2,n#/2,not#/1,p#/2,t#/1} / {0/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/15,c_6/0 ,c_7/0,c_8/1,c_9/0,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/1,c_19/0,c_20/1,c_21/0 ,c_22/0,c_23/1,c_24/1,c_25/0,c_26/2,c_27/3,c_28/1} - Obligation: innermost runtime complexity wrt. defined symbols {and#,f#,g#,gt#,h#,id#,if#,k#,m#,minus#,n#,not#,p# ,t#} and constructors {0,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE