Consider the TRS R consisting of the rewrite rules 1: min(x,0) -> 0 2: min(0,y) -> 0 3: min(s(x),s(y)) -> s(min(x,y)) 4: max(x,0) -> x 5: max(0,y) -> y 6: max(s(x),s(y)) -> s(max(x,y)) 7: x - 0 -> x 8: s(x) - s(y) -> x - y 9: gcd(s(x),s(y),z) -> gcd(max(x,y) - min(x,y),s(min(x,y)),z) 10: gcd(x,s(y),s(z)) -> gcd(x,max(y,z) - min(y,z),s(min(y,z))) 11: gcd(s(x),y,s(z)) -> gcd(max(x,z) - min(x,z),y,s(min(x,z))) 12: gcd(x,0,0) -> x 13: gcd(0,y,0) -> y 14: gcd(0,0,z) -> z There are 15 dependency pairs: 15: MIN(s(x),s(y)) -> MIN(x,y) 16: MAX(s(x),s(y)) -> MAX(x,y) 17: s(x) -# s(y) -> x -# y 18: GCD(s(x),s(y),z) -> GCD(max(x,y) - min(x,y),s(min(x,y)),z) 19: GCD(s(x),s(y),z) -> max(x,y) -# min(x,y) 20: GCD(s(x),s(y),z) -> MAX(x,y) 21: GCD(s(x),s(y),z) -> MIN(x,y) 22: GCD(x,s(y),s(z)) -> GCD(x,max(y,z) - min(y,z),s(min(y,z))) 23: GCD(x,s(y),s(z)) -> max(y,z) -# min(y,z) 24: GCD(x,s(y),s(z)) -> MAX(y,z) 25: GCD(x,s(y),s(z)) -> MIN(y,z) 26: GCD(s(x),y,s(z)) -> GCD(max(x,z) - min(x,z),y,s(min(x,z))) 27: GCD(s(x),y,s(z)) -> max(x,z) -# min(x,z) 28: GCD(s(x),y,s(z)) -> MAX(x,z) 29: GCD(s(x),y,s(z)) -> MIN(x,z) The approximated dependency graph contains 4 SCCs: {17}, {16}, {15} and {18,22,26}. - Consider the SCC {17}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [-#](x,y) = x + y + 1, rule 17 is strictly decreasing. - Consider the SCC {16}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [MAX](x,y) = x + y + 1, rule 16 is strictly decreasing. - Consider the SCC {15}. There are no usable rules. By taking the polynomial interpretation [s](x) = x + 1 and [MIN](x,y) = x + y + 1, rule 15 is strictly decreasing. - Consider the SCC {18,22,26}. The usable rules are {1-8}. By taking the polynomial interpretation [0] = 0, [GCD](x,y,z) = 3x + 2y + z + 1, [s](x) = 3x + 3, [min](x,y) = x, [-](x,y) = x + 1 and [max](x,y) = x + y + 1, the rules in {1-3} are weakly decreasing and the rules in {4-8,18,22,26} are strictly decreasing. Hence the TRS is terminating.