MAYBE TRS: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} DP: Strict: { ge#(0(), s(s(x))) -> ge#(0(), s(x)), ge#(s(x), 0()) -> ge#(x, 0()), ge#(s(x), s(y)) -> ge#(x, y), minus#(0(), s(x)) -> minus#(0(), x), minus#(s(x), 0()) -> minus#(x, 0()), minus#(s(x), s(y)) -> minus#(x, y), plus#(0(), s(x)) -> plus#(0(), x), plus#(s(x), y) -> plus#(x, y), ify#(true(), x, y) -> ge#(x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ge#(y, s(0())), div#(x, y) -> ify#(ge(y, s(0())), x, y), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z), if#(true(), x, y) -> minus#(x, y), if#(true(), x, y) -> div#(minus(x, y), y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} EDG: {(ge#(0(), s(s(x))) -> ge#(0(), s(x)), ge#(0(), s(s(x))) -> ge#(0(), s(x))) (minus#(s(x), 0()) -> minus#(x, 0()), minus#(s(x), 0()) -> minus#(x, 0())) (plus#(0(), s(x)) -> plus#(0(), x), plus#(0(), s(x)) -> plus#(0(), x)) (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y)) (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), 0()) -> minus#(x, 0())) (minus#(s(x), s(y)) -> minus#(x, y), minus#(0(), s(x)) -> minus#(0(), x)) (ify#(true(), x, y) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y)) (ify#(true(), x, y) -> ge#(x, y), ge#(s(x), 0()) -> ge#(x, 0())) (ify#(true(), x, y) -> ge#(x, y), ge#(0(), s(s(x))) -> ge#(0(), s(x))) (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y)) (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y)) (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s(x), y) -> plus#(x, y)) (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(0(), s(x)) -> plus#(0(), x)) (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z)) (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(x, z)) (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z))) (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ify#(ge(y, s(0())), x, y)) (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ge#(y, s(0()))) (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ge#(y, s(0()))) (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ify#(ge(y, s(0())), x, y)) (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z))) (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(x, z)) (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(y, z)) (div#(x, y) -> ge#(y, s(0())), ge#(s(x), s(y)) -> ge#(x, y)) (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> ge#(x, y)) (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y)) (if#(true(), x, y) -> minus#(x, y), minus#(0(), s(x)) -> minus#(0(), x)) (if#(true(), x, y) -> minus#(x, y), minus#(s(x), 0()) -> minus#(x, 0())) (if#(true(), x, y) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y)) (plus#(s(x), y) -> plus#(x, y), plus#(0(), s(x)) -> plus#(0(), x)) (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y)) (ge#(s(x), s(y)) -> ge#(x, y), ge#(0(), s(s(x))) -> ge#(0(), s(x))) (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), 0()) -> ge#(x, 0())) (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y)) (minus#(0(), s(x)) -> minus#(0(), x), minus#(0(), s(x)) -> minus#(0(), x)) (ge#(s(x), 0()) -> ge#(x, 0()), ge#(s(x), 0()) -> ge#(x, 0())) (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s(0()))) (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s(0())), x, y)) (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z))) (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> div#(x, z)) (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> div#(y, z))} SCCS: Scc: { ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ify#(ge(y, s(0())), x, y), div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z), if#(true(), x, y) -> div#(minus(x, y), y)} Scc: {plus#(s(x), y) -> plus#(x, y)} Scc: {plus#(0(), s(x)) -> plus#(0(), x)} Scc: {minus#(s(x), s(y)) -> minus#(x, y)} Scc: {minus#(s(x), 0()) -> minus#(x, 0())} Scc: {minus#(0(), s(x)) -> minus#(0(), x)} Scc: {ge#(s(x), s(y)) -> ge#(x, y)} Scc: {ge#(s(x), 0()) -> ge#(x, 0())} Scc: {ge#(0(), s(s(x))) -> ge#(0(), s(x))} SCC: Strict: { ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ify#(ge(y, s(0())), x, y), div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z), if#(true(), x, y) -> div#(minus(x, y), y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} POLY: Argument Filtering: pi(if#) = [], pi(if) = [], pi(divByZeroError) = [], pi(div#) = 0, pi(div) = [], pi(ify#) = 1, pi(ify) = [], pi(plus) = [0,1], pi(minus) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(ge) = [], pi(true) = [] Usable Rules: {} Interpretation: [if#] = 0, [plus](x0, x1) = x0 + x1 + 1, [minus] = 0 Strict: {ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ify#(ge(y, s(0())), x, y), if#(true(), x, y) -> div#(minus(x, y), y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} EDG: {(ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y)) (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y)) (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s(0())), x, y))} SCCS: Scc: {ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ify#(ge(y, s(0())), x, y), if#(true(), x, y) -> div#(minus(x, y), y)} SCC: Strict: {ify#(true(), x, y) -> if#(ge(x, y), x, y), div#(x, y) -> ify#(ge(y, s(0())), x, y), if#(true(), x, y) -> div#(minus(x, y), y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} Fail SCC: Strict: {plus#(s(x), y) -> plus#(x, y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(plus#) = 0 Strict: {} Qed SCC: Strict: {plus#(0(), s(x)) -> plus#(0(), x)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(plus#) = 1 Strict: {} Qed SCC: Strict: {minus#(s(x), s(y)) -> minus#(x, y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed SCC: Strict: {minus#(s(x), 0()) -> minus#(x, 0())} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed SCC: Strict: {minus#(0(), s(x)) -> minus#(0(), x)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(minus#) = 1 Strict: {} Qed SCC: Strict: {ge#(s(x), s(y)) -> ge#(x, y)} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: Strict: {ge#(s(x), 0()) -> ge#(x, 0())} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: Strict: {ge#(0(), s(s(x))) -> ge#(0(), s(x))} Weak: { ge(0(), 0()) -> true(), ge(0(), s(0())) -> false(), ge(0(), s(s(x))) -> ge(0(), s(x)), ge(s(x), 0()) -> ge(x, 0()), ge(s(x), s(y)) -> ge(x, y), minus(0(), 0()) -> 0(), minus(0(), s(x)) -> minus(0(), x), minus(s(x), 0()) -> s(minus(x, 0())), minus(s(x), s(y)) -> minus(x, y), plus(0(), 0()) -> 0(), plus(0(), s(x)) -> s(plus(0(), x)), plus(s(x), y) -> s(plus(x, y)), ify(true(), x, y) -> if(ge(x, y), x, y), ify(false(), x, y) -> divByZeroError(), div(x, y) -> ify(ge(y, s(0())), x, y), div(plus(x, y), z) -> plus(div(x, z), div(y, z)), if(true(), x, y) -> s(div(minus(x, y), y)), if(false(), x, y) -> 0()} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed