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