YES Time: 0.008896 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)} UR: {} 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)} STATUS: arrows: 0.000000 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = 0, [fib](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [fib#](x0) = x0 Strict: fib# s s x -> fib# s x 2 + 1x >= 1 + 1x fib# s s x -> fib# x 2 + 1x >= 0 + 1x Weak: fib s s x -> +(fib s x, fib x) 3 + 1x >= 0 + 0x fib s 0() -> s 0() 3 >= 2 fib 0() -> 0() 2 >= 1 Qed