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