YES TRS: { f(0()) -> true(), f(1()) -> false(), f(s(x)) -> f(x), if(true(), s(x), s(y)) -> s(x), if(false(), s(x), s(y)) -> s(y), g(x, c(y)) -> c(g(x, y)), g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))} DP: Strict: { f#(s(x)) -> f#(x), g#(x, c(y)) -> f#(x), g#(x, c(y)) -> if#(f(x), c(g(s(x), y)), c(y)), g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(x, if(f(x), c(g(s(x), y)), c(y))), g#(x, c(y)) -> g#(s(x), y)} Weak: { f(0()) -> true(), f(1()) -> false(), f(s(x)) -> f(x), if(true(), s(x), s(y)) -> s(x), if(false(), s(x), s(y)) -> s(y), g(x, c(y)) -> c(g(x, y)), g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))} EDG: {(f#(s(x)) -> f#(x), f#(s(x)) -> f#(x)) (g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> g#(s(x), y)) (g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> g#(x, if(f(x), c(g(s(x), y)), c(y)))) (g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> g#(x, y)) (g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> if#(f(x), c(g(s(x), y)), c(y))) (g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> f#(x)) (g#(x, c(y)) -> f#(x), f#(s(x)) -> f#(x)) (g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> f#(x)) (g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> if#(f(x), c(g(s(x), y)), c(y))) (g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(x, y)) (g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(x, if(f(x), c(g(s(x), y)), c(y)))) (g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(s(x), y))} SCCS: Scc: {g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(s(x), y)} Scc: {f#(s(x)) -> f#(x)} SCC: Strict: {g#(x, c(y)) -> g#(x, y), g#(x, c(y)) -> g#(s(x), y)} Weak: { f(0()) -> true(), f(1()) -> false(), f(s(x)) -> f(x), if(true(), s(x), s(y)) -> s(x), if(false(), s(x), s(y)) -> s(y), g(x, c(y)) -> c(g(x, y)), g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))} SPSC: Simple Projection: pi(g#) = 1 Strict: {g#(x, c(y)) -> g#(s(x), y)} EDG: {(g#(x, c(y)) -> g#(s(x), y), g#(x, c(y)) -> g#(s(x), y))} SCCS: Scc: {g#(x, c(y)) -> g#(s(x), y)} SCC: Strict: {g#(x, c(y)) -> g#(s(x), y)} Weak: { f(0()) -> true(), f(1()) -> false(), f(s(x)) -> f(x), if(true(), s(x), s(y)) -> s(x), if(false(), s(x), s(y)) -> s(y), g(x, c(y)) -> c(g(x, y)), g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))} SPSC: Simple Projection: pi(g#) = 1 Strict: {} Qed SCC: Strict: {f#(s(x)) -> f#(x)} Weak: { f(0()) -> true(), f(1()) -> false(), f(s(x)) -> f(x), if(true(), s(x), s(y)) -> s(x), if(false(), s(x), s(y)) -> s(y), g(x, c(y)) -> c(g(x, y)), g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))} SPSC: Simple Projection: pi(f#) = 0 Strict: {} Qed