MAYBE TRS: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} DP: Strict: { plus#(s(x), y) -> plus#(x, y), times#(s(x), y) -> plus#(y, times(x, y)), times#(s(x), y) -> times#(x, y), exp#(x, s(y)) -> times#(x, exp(x, y)), exp#(x, s(y)) -> exp#(x, y), ge#(s(x), s(y)) -> ge#(x, y), towerIter#(c, x, y, z) -> ge#(c, x), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), tower#(x, y) -> towerIter#(0(), x, y, s(0())), help#(false(), c, x, y, z) -> exp#(y, z), help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z))} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} EDG: {(times#(s(x), y) -> plus#(y, times(x, y)), plus#(s(x), y) -> plus#(x, y)) (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z))) (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> exp#(y, z)) (help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z)), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z)) (help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z)), towerIter#(c, x, y, z) -> ge#(c, x)) (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> times#(x, y)) (times#(s(x), y) -> times#(x, y), times#(s(x), y) -> plus#(y, times(x, y))) (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y)) (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s(y)) -> times#(x, exp(x, y))) (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s(y)) -> exp#(x, y)) (exp#(x, s(y)) -> exp#(x, y), exp#(x, s(y)) -> times#(x, exp(x, y))) (exp#(x, s(y)) -> exp#(x, y), exp#(x, s(y)) -> exp#(x, y)) (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y)) (tower#(x, y) -> towerIter#(0(), x, y, s(0())), towerIter#(c, x, y, z) -> ge#(c, x)) (tower#(x, y) -> towerIter#(0(), x, y, s(0())), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z)) (exp#(x, s(y)) -> times#(x, exp(x, y)), times#(s(x), y) -> plus#(y, times(x, y))) (exp#(x, s(y)) -> times#(x, exp(x, y)), times#(s(x), y) -> times#(x, y)) (towerIter#(c, x, y, z) -> ge#(c, x), ge#(s(x), s(y)) -> ge#(x, y))} SCCS: Scc: { towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z))} Scc: {ge#(s(x), s(y)) -> ge#(x, y)} Scc: {exp#(x, s(y)) -> exp#(x, y)} Scc: {times#(s(x), y) -> times#(x, y)} Scc: {plus#(s(x), y) -> plus#(x, y)} SCC: Strict: { towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s(c), x, y, exp(y, z))} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} Fail SCC: Strict: {ge#(s(x), s(y)) -> ge#(x, y)} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: Strict: {exp#(x, s(y)) -> exp#(x, y)} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} SPSC: Simple Projection: pi(exp#) = 1 Strict: {} Qed SCC: Strict: {times#(s(x), y) -> times#(x, y)} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} SPSC: Simple Projection: pi(times#) = 0 Strict: {} Qed SCC: Strict: {plus#(s(x), y) -> plus#(x, y)} Weak: { plus(0(), x) -> x, plus(s(x), y) -> s(plus(x, y)), times(0(), y) -> 0(), times(s(x), y) -> plus(y, times(x, y)), exp(x, 0()) -> s(0()), exp(x, s(y)) -> times(x, exp(x, y)), ge(x, 0()) -> true(), ge(0(), s(x)) -> false(), ge(s(x), s(y)) -> ge(x, y), towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z), tower(x, y) -> towerIter(0(), x, y, s(0())), help(true(), c, x, y, z) -> z, help(false(), c, x, y, z) -> towerIter(s(c), x, y, exp(y, z))} SPSC: Simple Projection: pi(plus#) = 0 Strict: {} Qed