YES TRS: {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))} DP: Strict: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v)} Weak: {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))} EDG: {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v)) (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v)) (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))) (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))) (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v)) (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v)) (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))) (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(y, u, v)) (if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))} SCCS: Scc: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v)} SCC: Strict: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(y, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v)} Weak: {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v)} EDG: {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v)) (if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))) (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v))) (if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v))} SCCS: Scc: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v)} SCC: Strict: {if#(if(x, y, z), u, v) -> if#(x, if(y, u, v), if(z, u, v)), if#(if(x, y, z), u, v) -> if#(z, u, v)} Weak: {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(if(x, y, z), u, v) -> if#(z, u, v)} EDG: {(if#(if(x, y, z), u, v) -> if#(z, u, v), if#(if(x, y, z), u, v) -> if#(z, u, v))} SCCS: Scc: {if#(if(x, y, z), u, v) -> if#(z, u, v)} SCC: Strict: {if#(if(x, y, z), u, v) -> if#(z, u, v)} Weak: {if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))} SPSC: Simple Projection: pi(if#) = 0 Strict: {} Qed