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