MAYBE TRS: {cond(true(), x, y) -> s(minus(x, s(y))), equal(s(x), s(y)) -> equal(x, y), equal(s(x), 0()) -> false(), equal(0(), s(y)) -> false(), equal(0(), 0()) -> true(), min(u, 0()) -> 0(), min(s(u), s(v)) -> s(min(u, v)), min(0(), v) -> 0(), minus(x, y) -> cond(equal(min(x, y), y), x, y)} DP: Strict: {cond#(true(), x, y) -> minus#(x, s(y)), equal#(s(x), s(y)) -> equal#(x, y), min#(s(u), s(v)) -> min#(u, v), minus#(x, y) -> cond#(equal(min(x, y), y), x, y), minus#(x, y) -> equal#(min(x, y), y), minus#(x, y) -> min#(x, y)} Weak: {cond(true(), x, y) -> s(minus(x, s(y))), equal(s(x), s(y)) -> equal(x, y), equal(s(x), 0()) -> false(), equal(0(), s(y)) -> false(), equal(0(), 0()) -> true(), min(u, 0()) -> 0(), min(s(u), s(v)) -> s(min(u, v)), min(0(), v) -> 0(), minus(x, y) -> cond(equal(min(x, y), y), x, y)} EDG: {(equal#(s(x), s(y)) -> equal#(x, y), equal#(s(x), s(y)) -> equal#(x, y)) (cond#(true(), x, y) -> minus#(x, s(y)), minus#(x, y) -> min#(x, y)) (cond#(true(), x, y) -> minus#(x, s(y)), minus#(x, y) -> equal#(min(x, y), y)) (cond#(true(), x, y) -> minus#(x, s(y)), minus#(x, y) -> cond#(equal(min(x, y), y), x, y)) (minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s(y))) (minus#(x, y) -> equal#(min(x, y), y), equal#(s(x), s(y)) -> equal#(x, y)) (minus#(x, y) -> min#(x, y), min#(s(u), s(v)) -> min#(u, v)) (min#(s(u), s(v)) -> min#(u, v), min#(s(u), s(v)) -> min#(u, v))} SCCS: Scc: {min#(s(u), s(v)) -> min#(u, v)} Scc: {equal#(s(x), s(y)) -> equal#(x, y)} Scc: {cond#(true(), x, y) -> minus#(x, s(y)), minus#(x, y) -> cond#(equal(min(x, y), y), x, y)} SCC: Strict: {min#(s(u), s(v)) -> min#(u, v)} Weak: {cond(true(), x, y) -> s(minus(x, s(y))), equal(s(x), s(y)) -> equal(x, y), equal(s(x), 0()) -> false(), equal(0(), s(y)) -> false(), equal(0(), 0()) -> true(), min(u, 0()) -> 0(), min(s(u), s(v)) -> s(min(u, v)), min(0(), v) -> 0(), minus(x, y) -> cond(equal(min(x, y), y), x, y)} SPSC: Simple Projection: pi(min#) = 0 Strict: {} Qed SCC: Strict: {equal#(s(x), s(y)) -> equal#(x, y)} Weak: {cond(true(), x, y) -> s(minus(x, s(y))), equal(s(x), s(y)) -> equal(x, y), equal(s(x), 0()) -> false(), equal(0(), s(y)) -> false(), equal(0(), 0()) -> true(), min(u, 0()) -> 0(), min(s(u), s(v)) -> s(min(u, v)), min(0(), v) -> 0(), minus(x, y) -> cond(equal(min(x, y), y), x, y)} SPSC: Simple Projection: pi(equal#) = 0 Strict: {} Qed SCC: Strict: {cond#(true(), x, y) -> minus#(x, s(y)), minus#(x, y) -> cond#(equal(min(x, y), y), x, y)} Weak: {cond(true(), x, y) -> s(minus(x, s(y))), equal(s(x), s(y)) -> equal(x, y), equal(s(x), 0()) -> false(), equal(0(), s(y)) -> false(), equal(0(), 0()) -> true(), min(u, 0()) -> 0(), min(s(u), s(v)) -> s(min(u, v)), min(0(), v) -> 0(), minus(x, y) -> cond(equal(min(x, y), y), x, y)} Fail