MAYBE Time: 0.155037 TRS: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} DP: DP: { lt#(s x, s y) -> lt#(x, y), fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), fibo# 0() -> fib# 0(), fibo# s 0() -> fib# s 0(), fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y), if#(true(), c, s s x, a, b) -> lt#(s c, s s x), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b, if#(false(), c, s s x, a, b) -> fibo# a, if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)} TRS: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} UR: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), a(z, w) -> z, a(z, w) -> w} EDG: {(sum#(x, s y) -> sum#(x, y), sum#(x, s y) -> sum#(x, y)) (fibo# 0() -> fib# 0(), fib# s s x -> if#(true(), 0(), s s x, 0(), 0())) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# a) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# 0() -> fib# 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# s x, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# s x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(false(), c, s s x, a, b) -> fibo# b) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(false(), c, s s x, a, b) -> fibo# a) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)) (if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b), sum#(x, s y) -> sum#(x, y)) (fibo# s 0() -> fib# s 0(), fib# s s x -> if#(true(), 0(), s s x, 0(), 0())) (fibo# s s x -> fibo# x, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# x, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(true(), c, s s x, a, b) -> lt#(s c, s s x), lt#(s x, s y) -> lt#(x, y)) (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))} EDG: {(sum#(x, s y) -> sum#(x, y), sum#(x, s y) -> sum#(x, y)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# a) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# 0() -> fib# 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# s x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b), sum#(x, s y) -> sum#(x, y)) (fibo# s s x -> fibo# x, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# x, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(true(), c, s s x, a, b) -> lt#(s c, s s x), lt#(s x, s y) -> lt#(x, y)) (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))} EDG: {(sum#(x, s y) -> sum#(x, y), sum#(x, s y) -> sum#(x, y)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# a) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# 0() -> fib# 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# s x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b), sum#(x, s y) -> sum#(x, y)) (fibo# s s x -> fibo# x, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# x, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(true(), c, s s x, a, b) -> lt#(s c, s s x), lt#(s x, s y) -> lt#(x, y)) (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))} EDG: {(sum#(x, s y) -> sum#(x, y), sum#(x, s y) -> sum#(x, y)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# a) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# b, fibo# 0() -> fib# 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# s x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# x) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s 0() -> fib# s 0()) (if#(false(), c, s s x, a, b) -> fibo# a, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# s x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> lt#(s c, s s x)) (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)) (if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b), sum#(x, s y) -> sum#(x, y)) (fibo# s s x -> fibo# x, fibo# 0() -> fib# 0()) (fibo# s s x -> fibo# x, fibo# s 0() -> fib# s 0()) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# x) (fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x) (fibo# s s x -> fibo# x, fibo# s s x -> sum#(fibo s x, fibo x)) (if#(true(), c, s s x, a, b) -> lt#(s c, s s x), lt#(s x, s y) -> lt#(x, y)) (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))} STATUS: arrows: 0.816568 SCCS (4): Scc: {if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)} Scc: {fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x} Scc: {sum#(x, s y) -> sum#(x, y)} Scc: {lt#(s x, s y) -> lt#(x, y)} SCC (1): Strict: {if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)} Weak: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} Fail SCC (2): Strict: {fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x} Weak: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1, [lt](x0, x1) = x0 + 1, [sum](x0, x1) = x0, [s](x0) = x0 + 1, [fib](x0) = 0, [fibo](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [fibo#](x0) = x0 + 1 Strict: fibo# s s x -> fibo# s x 3 + 1x >= 2 + 1x fibo# s s x -> fibo# x 3 + 1x >= 1 + 1x Weak: if(false(), c, s s x, a, b) -> sum(fibo a, fibo b) 3 + 1x + 0c + 1b + 0a >= 1 + 0b + 1a if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c) 3 + 1x + 0c + 1b + 0a >= 6 + 2x + 1c + 0b sum(x, s y) -> s sum(x, y) 0 + 1x + 0y >= 1 + 1x + 0y sum(x, 0()) -> x 0 + 1x >= 1x fibo s s x -> sum(fibo s x, fibo x) 3 + 1x >= 2 + 1x fibo s 0() -> fib s 0() 3 >= 0 fibo 0() -> fib 0() 2 >= 0 fib s s x -> if(true(), 0(), s s x, 0(), 0()) 0 + 0x >= 4 + 1x fib s 0() -> s 0() 0 >= 2 fib 0() -> s 0() 0 >= 2 lt(s x, s y) -> lt(x, y) 2 + 0x + 1y >= 1 + 0x + 1y lt(0(), s x) -> true() 2 + 1x >= 0 lt(x, 0()) -> false() 2 + 0x >= 0 Qed SCC (1): Strict: {sum#(x, s y) -> sum#(x, y)} Weak: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3, x4) = x0 + x1 + x2 + x3, [lt](x0, x1) = x0 + 1, [sum](x0, x1) = x0, [s](x0) = x0 + 1, [fib](x0) = 0, [fibo](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [sum#](x0, x1) = x0 Strict: sum#(x, s y) -> sum#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if(false(), c, s s x, a, b) -> sum(fibo a, fibo b) 2 + 1x + 1c + 1b + 0a >= 1 + 0b + 1a if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c) 2 + 1x + 1c + 1b + 0a >= 6 + 2x + 2c + 0b sum(x, s y) -> s sum(x, y) 0 + 1x + 0y >= 1 + 1x + 0y sum(x, 0()) -> x 0 + 1x >= 1x fibo s s x -> sum(fibo s x, fibo x) 3 + 1x >= 2 + 1x fibo s 0() -> fib s 0() 3 >= 0 fibo 0() -> fib 0() 2 >= 0 fib s s x -> if(true(), 0(), s s x, 0(), 0()) 0 + 0x >= 4 + 1x fib s 0() -> s 0() 0 >= 2 fib 0() -> s 0() 0 >= 2 lt(s x, s y) -> lt(x, y) 2 + 0x + 1y >= 1 + 0x + 1y lt(0(), s x) -> true() 2 + 1x >= 0 lt(x, 0()) -> false() 2 + 0x >= 0 Qed SCC (1): Strict: {lt#(s x, s y) -> lt#(x, y)} Weak: { lt(x, 0()) -> false(), lt(0(), s x) -> true(), lt(s x, s y) -> lt(x, y), fib 0() -> s 0(), fib s 0() -> s 0(), fib s s x -> if(true(), 0(), s s x, 0(), 0()), fibo 0() -> fib 0(), fibo s 0() -> fib s 0(), fibo s s x -> sum(fibo s x, fibo x), sum(x, 0()) -> x, sum(x, s y) -> s sum(x, y), if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c), if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1, [lt](x0, x1) = x0 + 1, [sum](x0, x1) = x0, [s](x0) = x0 + 1, [fib](x0) = 0, [fibo](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 1, [lt#](x0, x1) = x0 Strict: lt#(s x, s y) -> lt#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if(false(), c, s s x, a, b) -> sum(fibo a, fibo b) 4 + 1x + 0c + 1b + 0a >= 1 + 0b + 1a if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c) 3 + 1x + 0c + 1b + 0a >= 6 + 2x + 1c + 0b sum(x, s y) -> s sum(x, y) 0 + 1x + 0y >= 1 + 1x + 0y sum(x, 0()) -> x 0 + 1x >= 1x fibo s s x -> sum(fibo s x, fibo x) 3 + 1x >= 2 + 1x fibo s 0() -> fib s 0() 3 >= 0 fibo 0() -> fib 0() 2 >= 0 fib s s x -> if(true(), 0(), s s x, 0(), 0()) 0 + 0x >= 4 + 1x fib s 0() -> s 0() 0 >= 2 fib 0() -> s 0() 0 >= 2 lt(s x, s y) -> lt(x, y) 2 + 0x + 1y >= 1 + 0x + 1y lt(0(), s x) -> true() 2 + 1x >= 0 lt(x, 0()) -> false() 2 + 0x >= 1 Qed