Input TRS: 1: 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)))) 2: n(0(),y) -> 0() 3: n(x,0()) -> 0() 4: n(s(x),s(y)) -> s(n(x,y)) 5: m(0(),y) -> y 6: m(x,0()) -> x 7: m(s(x),s(y)) -> s(m(x,y)) 8: k(0(),s(y)) -> 0() 9: k(s(x),s(y)) -> s(k(minus(x,y),s(y))) 10: t(x) -> p(x,x) 11: p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) 12: p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) 13: p(0(),y) -> y 14: p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) 15: minus(x,0()) -> x 16: minus(s(x),s(y)) -> minus(x,y) 17: id(x) -> x 18: if(true(),x,y) -> x 19: if(false(),x,y) -> y 20: not(x) -> if(x,false(),true()) 21: and(x,false()) -> false() 22: and(true(),true()) -> true() 23: f(0()) -> true() 24: f(s(x)) -> h(x) 25: h(0()) -> false() 26: h(s(x)) -> f(x) 27: gt(s(x),0()) -> true() 28: gt(0(),y) -> false() 29: gt(s(x),s(y)) -> gt(x,y) Number of strict rules: 29 Direct Order(PosReal,>,Poly) ... failed. Freezing f gt 1: g(s(x),s(y)) -> if(and(f❆1_s(x),f❆1_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)))) 2: n(0(),y) -> 0() 3: n(x,0()) -> 0() 4: n(s(x),s(y)) -> s(n(x,y)) 5: m(0(),y) -> y 6: m(x,0()) -> x 7: m(s(x),s(y)) -> s(m(x,y)) 8: k(0(),s(y)) -> 0() 9: k(s(x),s(y)) -> s(k(minus(x,y),s(y))) 10: t(x) -> p(x,x) 11: p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) 12: p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) 13: p(0(),y) -> y 14: p(id(x),s(y)) -> s(p(x,if(gt❆1_s(y,y),y,s(y)))) 15: minus(x,0()) -> x 16: minus(s(x),s(y)) -> minus(x,y) 17: id(x) -> x 18: if(true(),x,y) -> x 19: if(false(),x,y) -> y 20: not(x) -> if(x,false(),true()) 21: and(x,false()) -> false() 22: and(true(),true()) -> true() 23: f❆1_0() -> true() 24: f❆1_s(x) -> h(x) 25: h(0()) -> false() 26: h(s(x)) -> f(x) 27: gt❆1_s(x,0()) -> true() 28: gt❆1_0(y) -> false() 29: gt❆1_s(x,s(y)) -> gt(x,y) 30: gt(0(),_1) ->= gt❆1_0(_1) 31: gt(s(_1),_2) ->= gt❆1_s(_1,_2) 32: f(0()) ->= f❆1_0() 33: f(s(_1)) ->= f❆1_s(_1) Number of strict rules: 29 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #gt❆1_s(x,s(y)) -> #gt(x,y) #2: #k(s(x),s(y)) -> #k(minus(x,y),s(y)) #3: #k(s(x),s(y)) -> #minus(x,y) #4: #p(s(x),s(y)) -> #p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) #5: #p(s(x),s(y)) -> #if(gt(x,y),x,y) #6: #p(s(x),s(y)) -> #gt(x,y) #7: #p(s(x),s(y)) -> #if(not(gt(x,y)),id(x),id(y)) #8: #p(s(x),s(y)) -> #not(gt(x,y)) #9: #p(s(x),s(y)) -> #gt(x,y) #10: #p(s(x),s(y)) -> #id(x) #11: #p(s(x),s(y)) -> #id(y) #12: #f❆1_s(x) -> #h(x) #13: #p(s(x),x) -> #p(if(gt(x,x),id(x),id(x)),s(x)) #14: #p(s(x),x) -> #if(gt(x,x),id(x),id(x)) #15: #p(s(x),x) -> #gt(x,x) #16: #p(s(x),x) -> #id(x) #17: #p(s(x),x) -> #id(x) #18: #gt(s(_1),_2) ->? #gt❆1_s(_1,_2) #19: #p(id(x),s(y)) -> #p(x,if(gt❆1_s(y,y),y,s(y))) #20: #p(id(x),s(y)) -> #if(gt❆1_s(y,y),y,s(y)) #21: #p(id(x),s(y)) -> #gt❆1_s(y,y) #22: #gt(0(),_1) ->? #gt❆1_0(_1) #23: #not(x) -> #if(x,false(),true()) #24: #m(s(x),s(y)) -> #m(x,y) #25: #t(x) -> #p(x,x) #26: #f(s(_1)) ->? #f❆1_s(_1) #27: #f(0()) ->? #f❆1_0() #28: #h(s(x)) -> #f(x) #29: #minus(s(x),s(y)) -> #minus(x,y) #30: #g(s(x),s(y)) -> #if(and(f❆1_s(x),f❆1_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)))) #31: #g(s(x),s(y)) -> #and(f❆1_s(x),f❆1_s(y)) #32: #g(s(x),s(y)) -> #f❆1_s(x) #33: #g(s(x),s(y)) -> #f❆1_s(y) #34: #g(s(x),s(y)) -> #t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) #35: #g(s(x),s(y)) -> #g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) #36: #g(s(x),s(y)) -> #k(minus(m(x,y),n(x,y)),s(s(0()))) #37: #g(s(x),s(y)) -> #minus(m(x,y),n(x,y)) #38: #g(s(x),s(y)) -> #m(x,y) #39: #g(s(x),s(y)) -> #n(x,y) #40: #g(s(x),s(y)) -> #k(n(s(x),s(y)),s(s(0()))) #41: #g(s(x),s(y)) -> #n(s(x),s(y)) #42: #g(s(x),s(y)) -> #g(minus(m(x,y),n(x,y)),n(s(x),s(y))) #43: #g(s(x),s(y)) -> #minus(m(x,y),n(x,y)) #44: #g(s(x),s(y)) -> #m(x,y) #45: #g(s(x),s(y)) -> #n(x,y) #46: #g(s(x),s(y)) -> #n(s(x),s(y)) #47: #n(s(x),s(y)) -> #n(x,y) Number of SCCs: 8, DPs: 14, edges: 22 SCC { #29 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: 0 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: x2 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { } Removed DPs: #29 Number of SCCs: 7, DPs: 13, edges: 21 SCC { #47 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: 0 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: x2 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { } Removed DPs: #47 Number of SCCs: 6, DPs: 12, edges: 20 SCC { #24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: 0 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: x1 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { } Removed DPs: #24 Number of SCCs: 5, DPs: 11, edges: 19 SCC { #2 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: (/ 1 4) + x1 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: x1 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { 15 16 } Removed DPs: #2 Number of SCCs: 4, DPs: 10, edges: 18 SCC { #1 #18 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 1 2) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: (/ 1 4) + x1 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: x1 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: (/ 1 4) + x2 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: x2 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 #18 Number of SCCs: 3, DPs: 8, edges: 16 SCC { #12 #26 #28 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: (/ 1 2) + x1 s(x1) weight: (/ 3 4) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: 0 gt(x1,x2) weight: 0 minus(x1,x2) weight: (/ 1 2) + x1 and(x1,x2) weight: 0 k(x1,x2) weight: 0 t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 #h(x1) weight: x1 #k(x1,x2) weight: x1 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: (/ 1 2) #f❆1_0() weight: 0 #f(x1) weight: (/ 1 4) + x1 #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: 0 Usable rules: { } Removed DPs: #12 #26 #28 Number of SCCs: 2, DPs: 5, edges: 13 SCC { #35 #42 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 5 16) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: max{0, (/ 1 16) + x1} gt(x1,x2) weight: 0 minus(x1,x2) weight: max{0, x1} and(x1,x2) weight: 0 k(x1,x2) weight: max{0, (/ 1 16) + x1} t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: (/ 1 16) if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 4) + x1} #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 4) + x1} Usable rules: { 2..9 15 16 } Removed DPs: #42 Number of SCCs: 2, DPs: 4, edges: 10 SCC { #35 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 7 16) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: max{0, (/ 1 16) + x1} gt(x1,x2) weight: 0 minus(x1,x2) weight: max{0, x1} and(x1,x2) weight: 0 k(x1,x2) weight: max{0, (/ 1 16) + x1} t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: 0 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: (/ 1 16) if(x1,x2,x3) weight: 0 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 4) + x1} #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: 0 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: 0 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} Usable rules: { 2..9 15 16 } Removed DPs: #35 Number of SCCs: 1, DPs: 3, edges: 9 SCC { #4 #13 #19 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: 0 s(x1) weight: (/ 5 16) + x1 gt❆1_0(x1) weight: 0 n(x1,x2) weight: max{0, (/ 1 16) + x1} gt(x1,x2) weight: max{(/ 1 2) + x2, (/ 7 16) + x1} minus(x1,x2) weight: max{0, x1} and(x1,x2) weight: 0 k(x1,x2) weight: max{0, (/ 1 16) + x1} t(x1) weight: 0 false() weight: (/ 1 16) #id(x1) weight: 0 #p(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 4) + x1} true() weight: (/ 9 16) f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: (/ 1 16) if(x1,x2,x3) weight: max{0, x3, (/ 1 16) + x2} #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: 0 #f❆1_0() weight: 0 #f(x1) weight: 0 #g(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 4) + x1} #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: (/ 3 16) + x1 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: max{(/ 1 16) + x2, (/ 7 16) + x1} f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: x1 m(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} Usable rules: { 17..19 } Removed DPs: #4 #13 Number of SCCs: 2, DPs: 1, edges: 1 SCC { #19 } Removing DPs: Order(PosReal,>,Sum)... succeeded. h(x1) weight: 0 #f❆1_s(x1) weight: (/ 1 8) s(x1) weight: (/ 1 4) gt❆1_0(x1) weight: (/ 5 8) + x1 n(x1,x2) weight: (/ 1 8) + x2 gt(x1,x2) weight: (/ 1 2) minus(x1,x2) weight: (/ 1 8) and(x1,x2) weight: 0 k(x1,x2) weight: (/ 1 8) t(x1) weight: 0 false() weight: 0 #id(x1) weight: 0 #p(x1,x2) weight: x1 true() weight: 0 f❆1_s(x1) weight: 0 f(x1) weight: 0 #not(x1) weight: 0 p(x1,x2) weight: 0 0() weight: 0 if(x1,x2,x3) weight: (/ 1 8) + x2 + x3 #h(x1) weight: 0 #k(x1,x2) weight: 0 #gt❆1_0(x1) weight: 0 #gt(x1,x2) weight: (/ 1 8) #f❆1_0() weight: 0 #f(x1) weight: (/ 1 16) #g(x1,x2) weight: 0 #gt❆1_s(x1,x2) weight: 0 #minus(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 id(x1) weight: (/ 1 8) + x1 #t(x1) weight: 0 #n(x1,x2) weight: 0 #m(x1,x2) weight: 0 gt❆1_s(x1,x2) weight: (/ 1 8) + x1 + x2 f❆1_0() weight: 0 g(x1,x2) weight: 0 #and(x1,x2) weight: 0 not(x1) weight: 0 m(x1,x2) weight: (/ 1 8) Usable rules: { 18 19 } Removed DPs: #19 Number of SCCs: 1, DPs: 0, edges: 0 YES