YES Time: 0.000583 TRS: {a b x -> b b a x} DP: DP: {a# b x -> a# x} TRS: {a b x -> b b a x} EDG: {(a# b x -> a# x, a# b x -> a# x)} SCCS (1): Scc: {a# b x -> a# x} SCC (1): Strict: {a# b x -> a# x} Weak: {a b x -> b b a x} SPSC: Simple Projection: pi(a#) = 0 Strict: {} Qed