MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__2ndsneg(X1,X2) -> 2ndsneg(X1,X2) a__2ndsneg(0(),Z) -> rnil() a__2ndsneg(s(N),cons(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z))) a__2ndspos(X1,X2) -> 2ndspos(X1,X2) a__2ndspos(0(),Z) -> rnil() a__2ndspos(s(N),cons(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z))) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__pi(X) -> a__2ndspos(mark(X),a__from(0())) a__pi(X) -> pi(X) a__plus(X1,X2) -> plus(X1,X2) a__plus(0(),Y) -> mark(Y) a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y))) a__square(X) -> a__times(mark(X),mark(X)) a__square(X) -> square(X) a__times(X1,X2) -> times(X1,X2) a__times(0(),Y) -> 0() a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y))) mark(0()) -> 0() mark(2ndsneg(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2)) mark(2ndspos(X1,X2)) -> a__2ndspos(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil()) -> nil() mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(posrecip(X)) -> posrecip(mark(X)) mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2)) mark(rnil()) -> rnil() mark(s(X)) -> s(mark(X)) mark(square(X)) -> a__square(mark(X)) mark(times(X1,X2)) -> a__times(mark(X1),mark(X2)) - Signature: {a__2ndsneg/2,a__2ndspos/2,a__from/1,a__pi/1,a__plus/2,a__square/1,a__times/2,mark/1} / {0/0,2ndsneg/2 ,2ndspos/2,cons/2,from/1,negrecip/1,nil/0,pi/1,plus/2,posrecip/1,rcons/2,rnil/0,s/1,square/1,times/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__2ndsneg,a__2ndspos,a__from,a__pi,a__plus,a__square ,a__times,mark} and constructors {0,2ndsneg,2ndspos,cons,from,negrecip,nil,pi,plus,posrecip,rcons,rnil,s ,square,times} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__2ndsneg#(X1,X2) -> c_1() a__2ndsneg#(0(),Z) -> c_2() a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__2ndspos#(X1,X2) -> c_4() a__2ndspos#(0(),Z) -> c_5() a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__from#(X) -> c_7(mark#(X)) a__from#(X) -> c_8() a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) a__pi#(X) -> c_10() a__plus#(X1,X2) -> c_11() a__plus#(0(),Y) -> c_12(mark#(Y)) a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) a__square#(X) -> c_15() a__times#(X1,X2) -> c_16() a__times#(0(),Y) -> c_17() a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) mark#(0()) -> c_19() mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_22(mark#(X1)) mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) mark#(negrecip(X)) -> c_24(mark#(X)) mark#(nil()) -> c_25() mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(posrecip(X)) -> c_28(mark#(X)) mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) mark#(rnil()) -> c_30() mark#(s(X)) -> c_31(mark#(X)) mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__2ndsneg#(X1,X2) -> c_1() a__2ndsneg#(0(),Z) -> c_2() a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__2ndspos#(X1,X2) -> c_4() a__2ndspos#(0(),Z) -> c_5() a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__from#(X) -> c_7(mark#(X)) a__from#(X) -> c_8() a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) a__pi#(X) -> c_10() a__plus#(X1,X2) -> c_11() a__plus#(0(),Y) -> c_12(mark#(Y)) a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) a__square#(X) -> c_15() a__times#(X1,X2) -> c_16() a__times#(0(),Y) -> c_17() a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) mark#(0()) -> c_19() mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_22(mark#(X1)) mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) mark#(negrecip(X)) -> c_24(mark#(X)) mark#(nil()) -> c_25() mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(posrecip(X)) -> c_28(mark#(X)) mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) mark#(rnil()) -> c_30() mark#(s(X)) -> c_31(mark#(X)) mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__2ndsneg(X1,X2) -> 2ndsneg(X1,X2) a__2ndsneg(0(),Z) -> rnil() a__2ndsneg(s(N),cons(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z))) a__2ndspos(X1,X2) -> 2ndspos(X1,X2) a__2ndspos(0(),Z) -> rnil() a__2ndspos(s(N),cons(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z))) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__pi(X) -> a__2ndspos(mark(X),a__from(0())) a__pi(X) -> pi(X) a__plus(X1,X2) -> plus(X1,X2) a__plus(0(),Y) -> mark(Y) a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y))) a__square(X) -> a__times(mark(X),mark(X)) a__square(X) -> square(X) a__times(X1,X2) -> times(X1,X2) a__times(0(),Y) -> 0() a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y))) mark(0()) -> 0() mark(2ndsneg(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2)) mark(2ndspos(X1,X2)) -> a__2ndspos(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil()) -> nil() mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(posrecip(X)) -> posrecip(mark(X)) mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2)) mark(rnil()) -> rnil() mark(s(X)) -> s(mark(X)) mark(square(X)) -> a__square(mark(X)) mark(times(X1,X2)) -> a__times(mark(X1),mark(X2)) - Signature: {a__2ndsneg/2,a__2ndspos/2,a__from/1,a__pi/1,a__plus/2,a__square/1,a__times/2,mark/1,a__2ndsneg#/2 ,a__2ndspos#/2,a__from#/1,a__pi#/1,a__plus#/2,a__square#/1,a__times#/2,mark#/1} / {0/0,2ndsneg/2,2ndspos/2 ,cons/2,from/1,negrecip/1,nil/0,pi/1,plus/2,posrecip/1,rcons/2,rnil/0,s/1,square/1,times/2,c_1/0,c_2/0,c_3/4 ,c_4/0,c_5/0,c_6/4,c_7/1,c_8/0,c_9/3,c_10/0,c_11/0,c_12/1,c_13/3,c_14/3,c_15/0,c_16/0,c_17/0,c_18/5,c_19/0 ,c_20/3,c_21/3,c_22/1,c_23/2,c_24/1,c_25/0,c_26/2,c_27/3,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__2ndsneg#,a__2ndspos#,a__from#,a__pi#,a__plus# ,a__square#,a__times#,mark#} and constructors {0,2ndsneg,2ndspos,cons,from,negrecip,nil,pi,plus,posrecip ,rcons,rnil,s,square,times} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,5,8,10,11,15,16,17,19,25,30} by application of Pre({1,2,4,5,8,10,11,15,16,17,19,25,30}) = {3,6,7,9,12,13,14,18,20,21,22,23,24,26,27,28,29,31,32,33}. Here rules are labelled as follows: 1: a__2ndsneg#(X1,X2) -> c_1() 2: a__2ndsneg#(0(),Z) -> c_2() 3: a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) 4: a__2ndspos#(X1,X2) -> c_4() 5: a__2ndspos#(0(),Z) -> c_5() 6: a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) 7: a__from#(X) -> c_7(mark#(X)) 8: a__from#(X) -> c_8() 9: a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) 10: a__pi#(X) -> c_10() 11: a__plus#(X1,X2) -> c_11() 12: a__plus#(0(),Y) -> c_12(mark#(Y)) 13: a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) 14: a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) 15: a__square#(X) -> c_15() 16: a__times#(X1,X2) -> c_16() 17: a__times#(0(),Y) -> c_17() 18: a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) 19: mark#(0()) -> c_19() 20: mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 21: mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 22: mark#(cons(X1,X2)) -> c_22(mark#(X1)) 23: mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) 24: mark#(negrecip(X)) -> c_24(mark#(X)) 25: mark#(nil()) -> c_25() 26: mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) 27: mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 28: mark#(posrecip(X)) -> c_28(mark#(X)) 29: mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) 30: mark#(rnil()) -> c_30() 31: mark#(s(X)) -> c_31(mark#(X)) 32: mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) 33: mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__from#(X) -> c_7(mark#(X)) a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) a__plus#(0(),Y) -> c_12(mark#(Y)) a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_22(mark#(X1)) mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) mark#(negrecip(X)) -> c_24(mark#(X)) mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(posrecip(X)) -> c_28(mark#(X)) mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) mark#(s(X)) -> c_31(mark#(X)) mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak DPs: a__2ndsneg#(X1,X2) -> c_1() a__2ndsneg#(0(),Z) -> c_2() a__2ndspos#(X1,X2) -> c_4() a__2ndspos#(0(),Z) -> c_5() a__from#(X) -> c_8() a__pi#(X) -> c_10() a__plus#(X1,X2) -> c_11() a__square#(X) -> c_15() a__times#(X1,X2) -> c_16() a__times#(0(),Y) -> c_17() mark#(0()) -> c_19() mark#(nil()) -> c_25() mark#(rnil()) -> c_30() - Weak TRS: a__2ndsneg(X1,X2) -> 2ndsneg(X1,X2) a__2ndsneg(0(),Z) -> rnil() a__2ndsneg(s(N),cons(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z))) a__2ndspos(X1,X2) -> 2ndspos(X1,X2) a__2ndspos(0(),Z) -> rnil() a__2ndspos(s(N),cons(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z))) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__pi(X) -> a__2ndspos(mark(X),a__from(0())) a__pi(X) -> pi(X) a__plus(X1,X2) -> plus(X1,X2) a__plus(0(),Y) -> mark(Y) a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y))) a__square(X) -> a__times(mark(X),mark(X)) a__square(X) -> square(X) a__times(X1,X2) -> times(X1,X2) a__times(0(),Y) -> 0() a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y))) mark(0()) -> 0() mark(2ndsneg(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2)) mark(2ndspos(X1,X2)) -> a__2ndspos(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil()) -> nil() mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(posrecip(X)) -> posrecip(mark(X)) mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2)) mark(rnil()) -> rnil() mark(s(X)) -> s(mark(X)) mark(square(X)) -> a__square(mark(X)) mark(times(X1,X2)) -> a__times(mark(X1),mark(X2)) - Signature: {a__2ndsneg/2,a__2ndspos/2,a__from/1,a__pi/1,a__plus/2,a__square/1,a__times/2,mark/1,a__2ndsneg#/2 ,a__2ndspos#/2,a__from#/1,a__pi#/1,a__plus#/2,a__square#/1,a__times#/2,mark#/1} / {0/0,2ndsneg/2,2ndspos/2 ,cons/2,from/1,negrecip/1,nil/0,pi/1,plus/2,posrecip/1,rcons/2,rnil/0,s/1,square/1,times/2,c_1/0,c_2/0,c_3/4 ,c_4/0,c_5/0,c_6/4,c_7/1,c_8/0,c_9/3,c_10/0,c_11/0,c_12/1,c_13/3,c_14/3,c_15/0,c_16/0,c_17/0,c_18/5,c_19/0 ,c_20/3,c_21/3,c_22/1,c_23/2,c_24/1,c_25/0,c_26/2,c_27/3,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__2ndsneg#,a__2ndspos#,a__from#,a__pi#,a__plus# ,a__square#,a__times#,mark#} and constructors {0,2ndsneg,2ndspos,cons,from,negrecip,nil,pi,plus,posrecip ,rcons,rnil,s,square,times} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) -->_4 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_4 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_4 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_4 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_4 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_4 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_4 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_4 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_4 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_4 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_4 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_4 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)):2 -->_4 mark#(rnil()) -> c_30():33 -->_3 mark#(rnil()) -> c_30():33 -->_1 mark#(rnil()) -> c_30():33 -->_4 mark#(nil()) -> c_25():32 -->_3 mark#(nil()) -> c_25():32 -->_1 mark#(nil()) -> c_25():32 -->_4 mark#(0()) -> c_19():31 -->_3 mark#(0()) -> c_19():31 -->_1 mark#(0()) -> c_19():31 -->_2 a__2ndspos#(0(),Z) -> c_5():24 -->_2 a__2ndspos#(X1,X2) -> c_4():23 2:S:a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) -->_4 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_4 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_4 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_4 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_4 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_4 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_4 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_4 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_4 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_4 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_4 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_4 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_4 mark#(rnil()) -> c_30():33 -->_3 mark#(rnil()) -> c_30():33 -->_1 mark#(rnil()) -> c_30():33 -->_4 mark#(nil()) -> c_25():32 -->_3 mark#(nil()) -> c_25():32 -->_1 mark#(nil()) -> c_25():32 -->_4 mark#(0()) -> c_19():31 -->_3 mark#(0()) -> c_19():31 -->_1 mark#(0()) -> c_19():31 -->_2 a__2ndsneg#(0(),Z) -> c_2():22 -->_2 a__2ndsneg#(X1,X2) -> c_1():21 -->_2 a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)):1 3:S:a__from#(X) -> c_7(mark#(X)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 4:S:a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(rnil()) -> c_30():33 -->_2 mark#(nil()) -> c_25():32 -->_2 mark#(0()) -> c_19():31 -->_3 a__from#(X) -> c_8():25 -->_1 a__2ndspos#(0(),Z) -> c_5():24 -->_1 a__2ndspos#(X1,X2) -> c_4():23 -->_3 a__from#(X) -> c_7(mark#(X)):3 -->_1 a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)):2 5:S:a__plus#(0(),Y) -> c_12(mark#(Y)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 6:S:a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__plus#(X1,X2) -> c_11():27 -->_1 a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)):6 -->_1 a__plus#(0(),Y) -> c_12(mark#(Y)):5 7:S:a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)):8 -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__times#(0(),Y) -> c_17():30 -->_1 a__times#(X1,X2) -> c_16():29 8:S:a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) -->_5 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_4 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_5 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_4 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_5 mark#(s(X)) -> c_31(mark#(X)):18 -->_4 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_5 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_4 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_5 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_4 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_5 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_4 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_5 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_4 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_5 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_4 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_5 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_4 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_5 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_4 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_5 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_4 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_5 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_4 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_5 mark#(rnil()) -> c_30():33 -->_4 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_5 mark#(nil()) -> c_25():32 -->_4 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_5 mark#(0()) -> c_19():31 -->_4 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_3 a__times#(0(),Y) -> c_17():30 -->_3 a__times#(X1,X2) -> c_16():29 -->_1 a__plus#(X1,X2) -> c_11():27 -->_3 a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)):8 -->_1 a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)):6 -->_1 a__plus#(0(),Y) -> c_12(mark#(Y)):5 9:S:mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__2ndsneg#(0(),Z) -> c_2():22 -->_1 a__2ndsneg#(X1,X2) -> c_1():21 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)):1 10:S:mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__2ndspos#(0(),Z) -> c_5():24 -->_1 a__2ndspos#(X1,X2) -> c_4():23 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)):2 11:S:mark#(cons(X1,X2)) -> c_22(mark#(X1)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 12:S:mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(rnil()) -> c_30():33 -->_2 mark#(nil()) -> c_25():32 -->_2 mark#(0()) -> c_19():31 -->_1 a__from#(X) -> c_8():25 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__from#(X) -> c_7(mark#(X)):3 13:S:mark#(negrecip(X)) -> c_24(mark#(X)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 14:S:mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(rnil()) -> c_30():33 -->_2 mark#(nil()) -> c_25():32 -->_2 mark#(0()) -> c_19():31 -->_1 a__pi#(X) -> c_10():26 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())):4 15:S:mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__plus#(X1,X2) -> c_11():27 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)):6 -->_1 a__plus#(0(),Y) -> c_12(mark#(Y)):5 16:S:mark#(posrecip(X)) -> c_28(mark#(X)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 17:S:mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(rnil()) -> c_30():33 -->_1 mark#(rnil()) -> c_30():33 -->_2 mark#(nil()) -> c_25():32 -->_1 mark#(nil()) -> c_25():32 -->_2 mark#(0()) -> c_19():31 -->_1 mark#(0()) -> c_19():31 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 18:S:mark#(s(X)) -> c_31(mark#(X)) -->_1 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_1 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_1 mark#(rnil()) -> c_30():33 -->_1 mark#(nil()) -> c_25():32 -->_1 mark#(0()) -> c_19():31 -->_1 mark#(s(X)) -> c_31(mark#(X)):18 -->_1 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_1 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_1 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_1 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_1 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_1 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_1 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 19:S:mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(rnil()) -> c_30():33 -->_2 mark#(nil()) -> c_25():32 -->_2 mark#(0()) -> c_19():31 -->_1 a__square#(X) -> c_15():28 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)):7 20:S:mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(rnil()) -> c_30():33 -->_2 mark#(rnil()) -> c_30():33 -->_3 mark#(nil()) -> c_25():32 -->_2 mark#(nil()) -> c_25():32 -->_3 mark#(0()) -> c_19():31 -->_2 mark#(0()) -> c_19():31 -->_1 a__times#(0(),Y) -> c_17():30 -->_1 a__times#(X1,X2) -> c_16():29 -->_3 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_2 mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):20 -->_3 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_2 mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)):19 -->_3 mark#(s(X)) -> c_31(mark#(X)):18 -->_2 mark#(s(X)) -> c_31(mark#(X)):18 -->_3 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_2 mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)):17 -->_3 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_2 mark#(posrecip(X)) -> c_28(mark#(X)):16 -->_3 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_2 mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)):14 -->_3 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_2 mark#(negrecip(X)) -> c_24(mark#(X)):13 -->_3 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_2 mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)):12 -->_3 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_2 mark#(cons(X1,X2)) -> c_22(mark#(X1)):11 -->_3 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_2 mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):9 -->_1 a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)):8 21:W:a__2ndsneg#(X1,X2) -> c_1() 22:W:a__2ndsneg#(0(),Z) -> c_2() 23:W:a__2ndspos#(X1,X2) -> c_4() 24:W:a__2ndspos#(0(),Z) -> c_5() 25:W:a__from#(X) -> c_8() 26:W:a__pi#(X) -> c_10() 27:W:a__plus#(X1,X2) -> c_11() 28:W:a__square#(X) -> c_15() 29:W:a__times#(X1,X2) -> c_16() 30:W:a__times#(0(),Y) -> c_17() 31:W:mark#(0()) -> c_19() 32:W:mark#(nil()) -> c_25() 33:W:mark#(rnil()) -> c_30() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 21: a__2ndsneg#(X1,X2) -> c_1() 22: a__2ndsneg#(0(),Z) -> c_2() 23: a__2ndspos#(X1,X2) -> c_4() 24: a__2ndspos#(0(),Z) -> c_5() 25: a__from#(X) -> c_8() 26: a__pi#(X) -> c_10() 27: a__plus#(X1,X2) -> c_11() 28: a__square#(X) -> c_15() 29: a__times#(X1,X2) -> c_16() 30: a__times#(0(),Y) -> c_17() 31: mark#(0()) -> c_19() 32: mark#(nil()) -> c_25() 33: mark#(rnil()) -> c_30() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: a__2ndsneg#(s(N),cons(X,cons(Y,Z))) -> c_3(mark#(Y),a__2ndspos#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__2ndspos#(s(N),cons(X,cons(Y,Z))) -> c_6(mark#(Y),a__2ndsneg#(mark(N),mark(Z)),mark#(N),mark#(Z)) a__from#(X) -> c_7(mark#(X)) a__pi#(X) -> c_9(a__2ndspos#(mark(X),a__from(0())),mark#(X),a__from#(0())) a__plus#(0(),Y) -> c_12(mark#(Y)) a__plus#(s(X),Y) -> c_13(a__plus#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__square#(X) -> c_14(a__times#(mark(X),mark(X)),mark#(X),mark#(X)) a__times#(s(X),Y) -> c_18(a__plus#(mark(Y),a__times(mark(X),mark(Y))) ,mark#(Y) ,a__times#(mark(X),mark(Y)) ,mark#(X) ,mark#(Y)) mark#(2ndsneg(X1,X2)) -> c_20(a__2ndsneg#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(2ndspos(X1,X2)) -> c_21(a__2ndspos#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_22(mark#(X1)) mark#(from(X)) -> c_23(a__from#(mark(X)),mark#(X)) mark#(negrecip(X)) -> c_24(mark#(X)) mark#(pi(X)) -> c_26(a__pi#(mark(X)),mark#(X)) mark#(plus(X1,X2)) -> c_27(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(posrecip(X)) -> c_28(mark#(X)) mark#(rcons(X1,X2)) -> c_29(mark#(X1),mark#(X2)) mark#(s(X)) -> c_31(mark#(X)) mark#(square(X)) -> c_32(a__square#(mark(X)),mark#(X)) mark#(times(X1,X2)) -> c_33(a__times#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__2ndsneg(X1,X2) -> 2ndsneg(X1,X2) a__2ndsneg(0(),Z) -> rnil() a__2ndsneg(s(N),cons(X,cons(Y,Z))) -> rcons(negrecip(mark(Y)),a__2ndspos(mark(N),mark(Z))) a__2ndspos(X1,X2) -> 2ndspos(X1,X2) a__2ndspos(0(),Z) -> rnil() a__2ndspos(s(N),cons(X,cons(Y,Z))) -> rcons(posrecip(mark(Y)),a__2ndsneg(mark(N),mark(Z))) a__from(X) -> cons(mark(X),from(s(X))) a__from(X) -> from(X) a__pi(X) -> a__2ndspos(mark(X),a__from(0())) a__pi(X) -> pi(X) a__plus(X1,X2) -> plus(X1,X2) a__plus(0(),Y) -> mark(Y) a__plus(s(X),Y) -> s(a__plus(mark(X),mark(Y))) a__square(X) -> a__times(mark(X),mark(X)) a__square(X) -> square(X) a__times(X1,X2) -> times(X1,X2) a__times(0(),Y) -> 0() a__times(s(X),Y) -> a__plus(mark(Y),a__times(mark(X),mark(Y))) mark(0()) -> 0() mark(2ndsneg(X1,X2)) -> a__2ndsneg(mark(X1),mark(X2)) mark(2ndspos(X1,X2)) -> a__2ndspos(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(from(X)) -> a__from(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil()) -> nil() mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2)) mark(posrecip(X)) -> posrecip(mark(X)) mark(rcons(X1,X2)) -> rcons(mark(X1),mark(X2)) mark(rnil()) -> rnil() mark(s(X)) -> s(mark(X)) mark(square(X)) -> a__square(mark(X)) mark(times(X1,X2)) -> a__times(mark(X1),mark(X2)) - Signature: {a__2ndsneg/2,a__2ndspos/2,a__from/1,a__pi/1,a__plus/2,a__square/1,a__times/2,mark/1,a__2ndsneg#/2 ,a__2ndspos#/2,a__from#/1,a__pi#/1,a__plus#/2,a__square#/1,a__times#/2,mark#/1} / {0/0,2ndsneg/2,2ndspos/2 ,cons/2,from/1,negrecip/1,nil/0,pi/1,plus/2,posrecip/1,rcons/2,rnil/0,s/1,square/1,times/2,c_1/0,c_2/0,c_3/4 ,c_4/0,c_5/0,c_6/4,c_7/1,c_8/0,c_9/3,c_10/0,c_11/0,c_12/1,c_13/3,c_14/3,c_15/0,c_16/0,c_17/0,c_18/5,c_19/0 ,c_20/3,c_21/3,c_22/1,c_23/2,c_24/1,c_25/0,c_26/2,c_27/3,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__2ndsneg#,a__2ndspos#,a__from#,a__pi#,a__plus# ,a__square#,a__times#,mark#} and constructors {0,2ndsneg,2ndspos,cons,from,negrecip,nil,pi,plus,posrecip ,rcons,rnil,s,square,times} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE