YES Time: 0.000957 TRS: {dfib(s s x, y) -> dfib(s x, dfib(x, y))} DP: DP: {dfib#(s s x, y) -> dfib#(x, y), dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} TRS: {dfib(s s x, y) -> dfib(s x, dfib(x, y))} EDG: {(dfib#(s s x, y) -> dfib#(x, y), dfib#(s s x, y) -> dfib#(s x, dfib(x, y))) (dfib#(s s x, y) -> dfib#(x, y), dfib#(s s x, y) -> dfib#(x, y)) (dfib#(s s x, y) -> dfib#(s x, dfib(x, y)), dfib#(s s x, y) -> dfib#(x, y)) (dfib#(s s x, y) -> dfib#(s x, dfib(x, y)), dfib#(s s x, y) -> dfib#(s x, dfib(x, y)))} SCCS (1): Scc: {dfib#(s s x, y) -> dfib#(x, y), dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} SCC (2): Strict: {dfib#(s s x, y) -> dfib#(x, y), dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} Weak: {dfib(s s x, y) -> dfib(s x, dfib(x, y))} SPSC: Simple Projection: pi(dfib#) = 0 Strict: {dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} EDG: {(dfib#(s s x, y) -> dfib#(s x, dfib(x, y)), dfib#(s s x, y) -> dfib#(s x, dfib(x, y)))} SCCS (1): Scc: {dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} SCC (1): Strict: {dfib#(s s x, y) -> dfib#(s x, dfib(x, y))} Weak: {dfib(s s x, y) -> dfib(s x, dfib(x, y))} SPSC: Simple Projection: pi(dfib#) = 0 Strict: {} Qed