YES TRS: { if(true(), X, Y) -> X, if(false(), X, Y) -> activate(Y), f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true()} RUF: Strict: { if(true(), X, Y) -> X, f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true()} Weak: {} DP: Strict: { f#(X) -> if#(X, c(), n__f(n__true())), activate#(n__f(X)) -> f#(activate(X)), activate#(n__f(X)) -> activate#(X), activate#(n__true()) -> true#()} Weak: { if(true(), X, Y) -> X, f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true()} EDG: {(activate#(n__f(X)) -> f#(activate(X)), f#(X) -> if#(X, c(), n__f(n__true()))) (activate#(n__f(X)) -> activate#(X), activate#(n__f(X)) -> f#(activate(X))) (activate#(n__f(X)) -> activate#(X), activate#(n__f(X)) -> activate#(X)) (activate#(n__f(X)) -> activate#(X), activate#(n__true()) -> true#())} SCCS: Scc: {activate#(n__f(X)) -> activate#(X)} SCC: Strict: {activate#(n__f(X)) -> activate#(X)} Weak: { if(true(), X, Y) -> X, f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true()} SPSC: Simple Projection: pi(activate#) = 0 Strict: {} Qed