Input TRS: 1: inc(s(x)) -> s(inc(x)) 2: inc(0()) -> s(0()) 3: plus(x,y) -> ifPlus(eq(x,0()),minus(x,s(0())),x,inc(x)) 4: ifPlus(false(),x,y,z) -> plus(x,z) 5: ifPlus(true(),x,y,z) -> y 6: minus(s(x),s(y)) -> minus(x,y) 7: minus(0(),x) -> 0() 8: minus(x,0()) -> x 9: minus(x,x) -> 0() 10: eq(s(x),s(y)) -> eq(x,y) 11: eq(0(),s(x)) -> false() 12: eq(s(x),0()) -> false() 13: eq(0(),0()) -> true() 14: eq(x,x) -> true() 15: times(x,y) -> timesIter(x,y,0()) 16: timesIter(x,y,z) -> ifTimes(eq(x,0()),minus(x,s(0())),y,z,plus(y,z)) 17: ifTimes(true(),x,y,z,u) -> z 18: ifTimes(false(),x,y,z,u) -> timesIter(x,y,u) 19: f() -> g() 20: f() -> h() Number of strict rules: 20 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #minus(s(x),s(y)) -> #minus(x,y) #2: #eq(s(x),s(y)) -> #eq(x,y) #3: #timesIter(x,y,z) -> #ifTimes(eq(x,0()),minus(x,s(0())),y,z,plus(y,z)) #4: #timesIter(x,y,z) -> #eq(x,0()) #5: #timesIter(x,y,z) -> #minus(x,s(0())) #6: #timesIter(x,y,z) -> #plus(y,z) #7: #plus(x,y) -> #ifPlus(eq(x,0()),minus(x,s(0())),x,inc(x)) #8: #plus(x,y) -> #eq(x,0()) #9: #plus(x,y) -> #minus(x,s(0())) #10: #plus(x,y) -> #inc(x) #11: #inc(s(x)) -> #inc(x) #12: #times(x,y) -> #timesIter(x,y,0()) #13: #ifPlus(false(),x,y,z) -> #plus(x,z) #14: #ifTimes(false(),x,y,z,u) -> #timesIter(x,y,u) Number of SCCs: 5, DPs: 7, edges: 7 SCC { #11 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h() weight: 0 ifTimes(x1,x2,x3,x4,x5) weight: 0 timesIter(x1,x2,x3) weight: 0 s(x1) weight: (/ 1 2) + x1 minus(x1,x2) weight: 0 #timesIter(x1,x2,x3) weight: 0 #plus(x1,x2) weight: 0 eq(x1,x2) weight: 0 false() weight: 0 #inc(x1) weight: x1 inc(x1) weight: 0 true() weight: 0 f() weight: 0 #eq(x1,x2) weight: 0 #times(x1,x2) weight: 0 0() weight: 0 times(x1,x2) weight: 0 #f() weight: 0 #minus(x1,x2) weight: 0 ifPlus(x1,x2,x3,x4) weight: 0 plus(x1,x2) weight: 0 #ifPlus(x1,x2,x3,x4) weight: 0 g() weight: 0 #ifTimes(x1,x2,x3,x4,x5) weight: 0 Usable rules: { } Removed DPs: #11 Number of SCCs: 4, DPs: 6, edges: 6 SCC { #2 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h() weight: 0 ifTimes(x1,x2,x3,x4,x5) weight: 0 timesIter(x1,x2,x3) weight: 0 s(x1) weight: (/ 1 2) + x1 minus(x1,x2) weight: 0 #timesIter(x1,x2,x3) weight: 0 #plus(x1,x2) weight: 0 eq(x1,x2) weight: 0 false() weight: 0 #inc(x1) weight: 0 inc(x1) weight: 0 true() weight: 0 f() weight: 0 #eq(x1,x2) weight: x2 #times(x1,x2) weight: 0 0() weight: 0 times(x1,x2) weight: 0 #f() weight: 0 #minus(x1,x2) weight: 0 ifPlus(x1,x2,x3,x4) weight: 0 plus(x1,x2) weight: 0 #ifPlus(x1,x2,x3,x4) weight: 0 g() weight: 0 #ifTimes(x1,x2,x3,x4,x5) weight: 0 Usable rules: { } Removed DPs: #2 Number of SCCs: 3, DPs: 5, edges: 5 SCC { #1 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h() weight: 0 ifTimes(x1,x2,x3,x4,x5) weight: 0 timesIter(x1,x2,x3) weight: 0 s(x1) weight: (/ 1 2) + x1 minus(x1,x2) weight: 0 #timesIter(x1,x2,x3) weight: 0 #plus(x1,x2) weight: 0 eq(x1,x2) weight: 0 false() weight: 0 #inc(x1) weight: 0 inc(x1) weight: 0 true() weight: 0 f() weight: 0 #eq(x1,x2) weight: 0 #times(x1,x2) weight: 0 0() weight: 0 times(x1,x2) weight: 0 #f() weight: 0 #minus(x1,x2) weight: x2 ifPlus(x1,x2,x3,x4) weight: 0 plus(x1,x2) weight: 0 #ifPlus(x1,x2,x3,x4) weight: 0 g() weight: 0 #ifTimes(x1,x2,x3,x4,x5) weight: 0 Usable rules: { } Removed DPs: #1 Number of SCCs: 2, DPs: 4, edges: 4 SCC { #7 #13 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... succeeded. h() weight: 0; 0 ifTimes(x1,x2,x3,x4,x5) weight: 0; 0 timesIter(x1,x2,x3) weight: 0; 0 s(x1) weight: max{0, (/ 1 4) + x1_1}; (- (/ 3 8)) minus(x1,x2) weight: max{0, (/ 1 16) + x2_1 + x2_2 + x1_1}; 0 #timesIter(x1,x2,x3) weight: 0; 0 #plus(x1,x2) weight: max{0, (- (/ 1 8)) + x1_1, (/ 1 16) + x2_2, (- (/ 1 2)) + x2_1}; 0 eq(x1,x2) weight: max{0, (- (/ 1 16)) + x1_1}; (- (/ 1 16)) false() weight: (/ 3 16); (- (/ 1 16)) #inc(x1) weight: 0; 0 inc(x1) weight: max{0, (/ 1 4) + x1_1}; (- (/ 1 8)) true() weight: 0; (- (/ 1 16)) f() weight: 0; 0 #eq(x1,x2) weight: 0; 0 #times(x1,x2) weight: 0; 0 0() weight: 0; (- (/ 1 16)) times(x1,x2) weight: 0; 0 #f() weight: 0; 0 #minus(x1,x2) weight: 0; 0 ifPlus(x1,x2,x3,x4) weight: 0; 0 plus(x1,x2) weight: 0; 0 #ifPlus(x1,x2,x3,x4) weight: max{0, (- (/ 1 16)) + x1_1, (- (/ 9 16)) + x2_2, (- (/ 1 16)) + x2_1, (/ 1 8) + x4_2, (- (/ 7 16)) + x4_1}; 0 g() weight: 0; 0 #ifTimes(x1,x2,x3,x4,x5) weight: 0; 0 Usable rules: { 1 2 6..9 12..14 } Removed DPs: #13 Number of SCCs: 1, DPs: 2, edges: 2 SCC { #3 #14 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... succeeded. h() weight: 0; 0 ifTimes(x1,x2,x3,x4,x5) weight: 0; 0 timesIter(x1,x2,x3) weight: 0; 0 s(x1) weight: max{0, (/ 5 16) + x1_1}; (- (/ 1 2)) minus(x1,x2) weight: max{0, (/ 1 16) + x2_1 + x2_2 + x1_1}; 0 #timesIter(x1,x2,x3) weight: max{0, (/ 1 16) + x1_2, (- (/ 3 16)) + x1_1, (- (/ 1 8)) + x2_2, (/ 1 16) + x3_2}; 0 #plus(x1,x2) weight: 0; 0 eq(x1,x2) weight: max{0, (- (/ 3 16)) + x1_1}; (- (/ 1 16)) false() weight: (/ 1 8); (- (/ 1 4)) #inc(x1) weight: 0; 0 inc(x1) weight: max{0, (/ 5 16) + x1_1}; (- (/ 1 16)) true() weight: 0; (- (/ 1 16)) f() weight: 0; 0 #eq(x1,x2) weight: 0; 0 #times(x1,x2) weight: 0; 0 0() weight: 0; (- (/ 1 16)) times(x1,x2) weight: 0; 0 #f() weight: 0; 0 #minus(x1,x2) weight: 0; 0 ifPlus(x1,x2,x3,x4) weight: max{0, (/ 1 4) + x1_2, (/ 1 16) + x3_1}; (- (/ 1 16)) + x4_2 plus(x1,x2) weight: max{0, (- (/ 1 8)) + x2_2}; (- (/ 3 16)) + x1_2 #ifPlus(x1,x2,x3,x4) weight: max{0, x1_1, x2_2, x2_1, x4_2, x4_1}; 0 g() weight: 0; 0 #ifTimes(x1,x2,x3,x4,x5) weight: max{0, x1_2, x1_1, (- (/ 1 16)) + x2_1}; 0 Usable rules: { 1 2 6..9 12..14 } Removed DPs: #14 Number of SCCs: 0, DPs: 0, edges: 0 YES