MAYBE Time: 0.003235 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} DP: DP: { min#(s x, s y) -> min#(x, y), max#(s x, s y) -> max#(x, y), minus#(s x, s y) -> minus#(x, any y), minus#(s x, s y) -> any# y, any# s x -> any# x, gcd#(s x, s y) -> min#(x, y), gcd#(s x, s y) -> max#(x, y), gcd#(s x, s y) -> minus#(max(x, y), min(x, y)), gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y))} 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} EDG: {(min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (gcd#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y)) (minus#(s x, s y) -> any# y, any# s x -> any# x) (gcd#(s x, s y) -> minus#(max(x, y), min(x, y)), minus#(s x, s y) -> any# y) (gcd#(s x, s y) -> minus#(max(x, y), min(x, y)), minus#(s x, s y) -> minus#(x, any y)) (minus#(s x, s y) -> minus#(x, any y), minus#(s x, s y) -> minus#(x, any y)) (minus#(s x, s y) -> minus#(x, any y), minus#(s x, s y) -> any# y) (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> min#(x, y)) (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> max#(x, y)) (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> minus#(max(x, y), min(x, y))) (gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y)), gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y))) (gcd#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y)) (any# s x -> any# x, any# s x -> any# x)} STATUS: arrows: 0.827160 SCCS (5): Scc: {gcd#(s x, s y) -> gcd#(minus(max(x, y), min(x, y)), s min(x, y))} Scc: {minus#(s x, s y) -> minus#(x, any y)} Scc: {max#(s x, s y) -> max#(x, y)} Scc: {min#(s x, s y) -> min#(x, y)} Scc: {any# s x -> any# x} SCC (1): Strict: {gcd#(s x, s y) -> gcd#(minus(max(x, y), 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} Open SCC (1): Strict: {minus#(s x, s y) -> minus#(x, any 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} Open SCC (1): 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} Open SCC (1): 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} Open SCC (1): Strict: {any# s x -> any# x} 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), minus(x, 0()) -> x, minus(s x, s y) -> s minus(x, any y), any x -> x, any s x -> s s any x, gcd(s x, s y) -> gcd(minus(max(x, y), min(x, y)), s min(x, y))} Open