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