0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 Rewriting (⇔)
↳36 QDP
↳37 Instantiation (⇔)
↳38 QDP
↳39 Rewriting (⇔)
↳40 QDP
↳41 Instantiation (⇔)
↳42 QDP
↳43 NonInfProof (⇔)
↳44 QDP
↳45 PisEmptyProof (⇔)
↳46 TRUE
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
LT(s(x), s(y)) → LT(x, y)
FIBO(0) → FIB(0)
FIBO(s(0)) → FIB(s(0))
FIBO(s(s(x))) → SUM(fibo(s(x)), fibo(x))
FIBO(s(s(x))) → FIBO(s(x))
FIBO(s(s(x))) → FIBO(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(true, c, s(s(x)), a, b) → LT(s(c), s(s(x)))
IF(false, c, s(s(x)), a, b) → SUM(fibo(a), fibo(b))
IF(false, c, s(s(x)), a, b) → FIBO(a)
IF(false, c, s(s(x)), a, b) → FIBO(b)
SUM(x, s(y)) → SUM(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
SUM(x, s(y)) → SUM(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
SUM(x, s(y)) → SUM(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
SUM(x, s(y)) → SUM(x, y)
From the DPs we obtained the following set of size-change graphs:
FIBO(s(s(x))) → FIBO(s(x))
FIBO(s(s(x))) → FIBO(x)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
FIBO(s(s(x))) → FIBO(s(x))
FIBO(s(s(x))) → FIBO(x)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
FIBO(s(s(x))) → FIBO(s(x))
FIBO(s(s(x))) → FIBO(x)
From the DPs we obtained the following set of size-change graphs:
LT(s(x), s(y)) → LT(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
LT(s(x), s(y)) → LT(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
LT(s(x), s(y)) → LT(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(true, c, s(s(x)), a, b) → IF(lt(s(c), s(s(x))), s(c), s(s(x)), b, c)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
fibo(0) → fib(0)
fibo(s(0)) → fib(s(0))
fibo(s(s(x))) → sum(fibo(s(x)), fibo(x))
fib(0) → s(0)
fib(s(0)) → s(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))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
IF(true, c, s(s(x)), a, b) → IF(lt(s(c), s(s(x))), s(c), s(s(x)), b, c)
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
fibo(0)
fibo(s(0))
fibo(s(s(x0)))
fib(0)
fib(s(0))
fib(s(s(x0)))
if(true, x0, s(s(x1)), x2, x3)
if(false, x0, s(s(x1)), x2, x3)
sum(x0, 0)
sum(x0, s(x1))
IF(true, c, s(s(x)), a, b) → IF(lt(s(c), s(s(x))), s(c), s(s(x)), b, c)
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(s(s(z0)), s(s(z1))), s(s(z0)), s(s(z1)), z0, s(z0))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(s(s(z0)), s(s(z1))), s(s(z0)), s(s(z1)), z0, s(z0))
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
IF(true, c, s(s(x)), a, b) → IF(lt(c, s(x)), s(c), s(s(x)), b, c)
IF(true, c, s(s(x)), a, b) → IF(lt(c, s(x)), s(c), s(s(x)), b, c)
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(s(z0), s(z1)), s(s(z0)), s(s(z1)), z0, s(z0))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(s(z0), s(z1)), s(s(z0)), s(s(z1)), z0, s(z0))
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(z0, z1), s(s(z0)), s(s(z1)), z0, s(z0))
IF(true, s(z0), s(s(z1)), z3, z0) → IF(lt(z0, z1), s(s(z0)), s(s(z1)), z0, s(z0))
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
IF(true, s(s(z0)), s(s(z1)), z0, s(z0)) → IF(lt(s(z0), z1), s(s(s(z0))), s(s(z1)), s(z0), s(s(z0)))
IF(true, s(s(z0)), s(s(z1)), z0, s(z0)) → IF(lt(s(z0), z1), s(s(s(z0))), s(s(z1)), s(z0), s(s(z0)))
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
(1) (IF(lt(s(x0), x1), s(s(s(x0))), s(s(x1)), s(x0), s(s(x0)))=IF(true, s(s(x2)), s(s(x3)), x2, s(x2)) ⇒ IF(true, s(s(x2)), s(s(x3)), x2, s(x2))≥IF(lt(s(x2), x3), s(s(s(x2))), s(s(x3)), s(x2), s(s(x2))))
(2) (s(x0)=x4∧lt(x4, x1)=true ⇒ IF(true, s(s(s(x0))), s(s(x1)), s(x0), s(s(x0)))≥IF(lt(s(s(x0)), x1), s(s(s(s(x0)))), s(s(x1)), s(s(x0)), s(s(s(x0)))))
(3) (lt(x6, x5)=true∧s(x0)=s(x6)∧(∀x7:lt(x6, x5)=true∧s(x7)=x6 ⇒ IF(true, s(s(s(x7))), s(s(x5)), s(x7), s(s(x7)))≥IF(lt(s(s(x7)), x5), s(s(s(s(x7)))), s(s(x5)), s(s(x7)), s(s(s(x7))))) ⇒ IF(true, s(s(s(x0))), s(s(s(x5))), s(x0), s(s(x0)))≥IF(lt(s(s(x0)), s(x5)), s(s(s(s(x0)))), s(s(s(x5))), s(s(x0)), s(s(s(x0)))))
(4) (true=true∧s(x0)=0 ⇒ IF(true, s(s(s(x0))), s(s(s(x8))), s(x0), s(s(x0)))≥IF(lt(s(s(x0)), s(x8)), s(s(s(s(x0)))), s(s(s(x8))), s(s(x0)), s(s(s(x0)))))
(5) (lt(x6, x5)=true ⇒ IF(true, s(s(s(x6))), s(s(s(x5))), s(x6), s(s(x6)))≥IF(lt(s(s(x6)), s(x5)), s(s(s(s(x6)))), s(s(s(x5))), s(s(x6)), s(s(s(x6)))))
(6) (lt(x11, x10)=true∧(lt(x11, x10)=true ⇒ IF(true, s(s(s(x11))), s(s(s(x10))), s(x11), s(s(x11)))≥IF(lt(s(s(x11)), s(x10)), s(s(s(s(x11)))), s(s(s(x10))), s(s(x11)), s(s(s(x11))))) ⇒ IF(true, s(s(s(s(x11)))), s(s(s(s(x10)))), s(s(x11)), s(s(s(x11))))≥IF(lt(s(s(s(x11))), s(s(x10))), s(s(s(s(s(x11))))), s(s(s(s(x10)))), s(s(s(x11))), s(s(s(s(x11))))))
(7) (true=true ⇒ IF(true, s(s(s(0))), s(s(s(s(x12)))), s(0), s(s(0)))≥IF(lt(s(s(0)), s(s(x12))), s(s(s(s(0)))), s(s(s(s(x12)))), s(s(0)), s(s(s(0)))))
(8) (IF(true, s(s(s(x11))), s(s(s(x10))), s(x11), s(s(x11)))≥IF(lt(s(s(x11)), s(x10)), s(s(s(s(x11)))), s(s(s(x10))), s(s(x11)), s(s(s(x11)))) ⇒ IF(true, s(s(s(s(x11)))), s(s(s(s(x10)))), s(s(x11)), s(s(s(x11))))≥IF(lt(s(s(s(x11))), s(s(x10))), s(s(s(s(s(x11))))), s(s(s(s(x10)))), s(s(s(x11))), s(s(s(s(x11))))))
(9) (IF(true, s(s(s(0))), s(s(s(s(x12)))), s(0), s(s(0)))≥IF(lt(s(s(0)), s(s(x12))), s(s(s(s(0)))), s(s(s(s(x12)))), s(s(0)), s(s(s(0)))))
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = -1 - x1 - x2 + x3 - x4 + x5
POL(c) = -1
POL(false) = 0
POL(lt(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF(true, s(s(z0)), s(s(z1)), z0, s(z0)) → IF(lt(s(z0), z1), s(s(s(z0))), s(s(z1)), s(z0), s(s(z0)))
The following rules are usable:
IF(true, s(s(z0)), s(s(z1)), z0, s(z0)) → IF(lt(s(z0), z1), s(s(s(z0))), s(s(z1)), s(z0), s(s(z0)))
lt(x, y) → lt(s(x), s(y))
true → lt(0, s(x))
false → lt(x, 0)
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))