YES Time: 0.001339 TRS: { fib 0() -> 0(), fib s 0() -> s 0(), fib s s x -> +(fib s x, fib x), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} DP: DP: {fib# s s x -> fib# x, fib# s s x -> fib# s x, fib# s s x -> +#(fib s x, fib x), +#(x, s y) -> +#(x, y)} TRS: { fib 0() -> 0(), fib s 0() -> s 0(), fib s s x -> +(fib s x, fib x), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} EDG: {(fib# s s x -> +#(fib s x, fib x), +#(x, s y) -> +#(x, y)) (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y)) (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) (fib# s s x -> fib# s x, fib# s s x -> +#(fib s x, fib x)) (fib# s s x -> fib# 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 x))} SCCS (2): Scc: {+#(x, s y) -> +#(x, y)} Scc: {fib# s s x -> fib# x, fib# s s x -> fib# s x} SCC (1): Strict: {+#(x, s y) -> +#(x, y)} Weak: { fib 0() -> 0(), fib s 0() -> s 0(), fib s s x -> +(fib s x, fib x), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} SPSC: Simple Projection: pi(+#) = 1 Strict: {} Qed 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), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} 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), +(x, 0()) -> x, +(x, s y) -> s +(x, y)} SPSC: Simple Projection: pi(fib#) = 0 Strict: {} Qed