YES TRS: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} DP: Strict: { min#(s(X), s(Y)) -> min#(X, Y), quot#(s(X), s(Y)) -> min#(X, Y), quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)), log#(s(s(X))) -> quot#(X, s(s(0()))), log#(s(s(X))) -> log#(s(quot(X, s(s(0())))))} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} EDG: {(quot#(s(X), s(Y)) -> min#(X, Y), min#(s(X), s(Y)) -> min#(X, Y)) (quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)), quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))) (quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y)), quot#(s(X), s(Y)) -> min#(X, Y)) (log#(s(s(X))) -> log#(s(quot(X, s(s(0()))))), log#(s(s(X))) -> quot#(X, s(s(0())))) (log#(s(s(X))) -> log#(s(quot(X, s(s(0()))))), log#(s(s(X))) -> log#(s(quot(X, s(s(0())))))) (log#(s(s(X))) -> quot#(X, s(s(0()))), quot#(s(X), s(Y)) -> min#(X, Y)) (log#(s(s(X))) -> quot#(X, s(s(0()))), quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))) (min#(s(X), s(Y)) -> min#(X, Y), min#(s(X), s(Y)) -> min#(X, Y))} SCCS: Scc: {log#(s(s(X))) -> log#(s(quot(X, s(s(0())))))} Scc: {quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))} Scc: {min#(s(X), s(Y)) -> min#(X, Y)} SCC: Strict: {log#(s(s(X))) -> log#(s(quot(X, s(s(0())))))} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} POLY: Argument Filtering: pi(log#) = 0, pi(log) = [], pi(quot) = 0, pi(s) = [0], pi(0) = [], pi(min) = 0 Usable Rules: {} Interpretation: [s](x0) = x0 + 1 Strict: {} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} Qed SCC: Strict: {quot#(s(X), s(Y)) -> quot#(min(X, Y), s(Y))} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} POLY: Argument Filtering: pi(log) = [], pi(quot#) = 0, pi(quot) = [], pi(s) = [0], pi(0) = [], pi(min) = 0 Usable Rules: {} Interpretation: [s](x0) = x0 + 1 Strict: {} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} Qed SCC: Strict: {min#(s(X), s(Y)) -> min#(X, Y)} Weak: { min(X, 0()) -> X, min(s(X), s(Y)) -> min(X, Y), quot(0(), s(Y)) -> 0(), quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))), log(s(0())) -> 0(), log(s(s(X))) -> s(log(s(quot(X, s(s(0()))))))} SPSC: Simple Projection: pi(min#) = 0 Strict: {} Qed