MAYBE TRS: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} DP: Strict: {min#(s(x), s(y)) -> min#(x, y), max#(s(x), s(y)) -> max#(x, y), -#(s(x), s(y)) -> -#(x, y), gcd#(s(x), s(y)) -> min#(x, y), gcd#(s(x), s(y)) -> max#(x, y), gcd#(s(x), s(y)) -> -#(s(max(x, y)), s(min(x, y))), gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} EDG: {(max#(s(x), s(y)) -> max#(x, y), max#(s(x), s(y)) -> max#(x, y)) (gcd#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y)) (gcd#(s(x), s(y)) -> -#(s(max(x, y)), s(min(x, y))), -#(s(x), s(y)) -> -#(x, y)) (gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y))), gcd#(s(x), s(y)) -> min#(x, y)) (gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y))), gcd#(s(x), s(y)) -> max#(x, y)) (gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y))), gcd#(s(x), s(y)) -> -#(s(max(x, y)), s(min(x, y)))) (gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y))), gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))) (gcd#(s(x), s(y)) -> max#(x, y), max#(s(x), s(y)) -> max#(x, y)) (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y)) (min#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y))} SCCS: Scc: {gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} Scc: {-#(s(x), s(y)) -> -#(x, y)} Scc: {max#(s(x), s(y)) -> max#(x, y)} Scc: {min#(s(x), s(y)) -> min#(x, y)} SCC: Strict: {gcd#(s(x), s(y)) -> gcd#(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} Fail SCC: Strict: {-#(s(x), s(y)) -> -#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} SPSC: Simple Projection: pi(-#) = 0 Strict: {} Qed SCC: Strict: {max#(s(x), s(y)) -> max#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} SPSC: Simple Projection: pi(max#) = 0 Strict: {} Qed SCC: Strict: {min#(s(x), s(y)) -> min#(x, y)} Weak: { min(x, 0()) -> 0(), min(0(), y) -> 0(), min(s(x), s(y)) -> s(min(x, y)), max(x, 0()) -> x, max(0(), y) -> y, max(s(x), s(y)) -> s(max(x, y)), -(x, 0()) -> x, -(s(x), s(y)) -> -(x, y), gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))} SPSC: Simple Projection: pi(min#) = 0 Strict: {} Qed