NO
0 QTRS
↳1 AAECC Innermost (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 MNOCProof (⇔, 0 ms)
↳30 QDP
↳31 NonLoopProof (⇒, 26 ms)
↳32 NO
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
WHILE(true, s(s(s(i)))) → WHILE(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
WHILE(true, s(s(s(i)))) → GT(s(s(s(i))), s(0))
WHILE(true, s(s(s(i)))) → F(s(s(s(i))))
F(i) → IF(neq(i, s(s(0))), i)
F(i) → NEQ(i, s(s(0)))
GT(s(x), s(y)) → GT(x, y)
IF(true, i) → PLUS(i, s(0))
NEQ(s(x), s(y)) → NEQ(x, y)
PLUS(s(x), y) → PLUS(x, s(y))
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
PLUS(s(x), y) → PLUS(x, s(y))
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
PLUS(s(x), y) → PLUS(x, s(y))
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
PLUS(s(x), y) → PLUS(x, s(y))
From the DPs we obtained the following set of size-change graphs:
NEQ(s(x), s(y)) → NEQ(x, y)
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
NEQ(s(x), s(y)) → NEQ(x, y)
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
NEQ(s(x), s(y)) → NEQ(x, y)
From the DPs we obtained the following set of size-change graphs:
GT(s(x), s(y)) → GT(x, y)
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
GT(s(x), s(y)) → GT(x, y)
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
WHILE(true, s(s(s(i)))) → WHILE(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y
while(true, s(s(s(x0))))
f(x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
gt(0, 0)
gt(0, s(x0))
if(true, x0)
if(false, x0)
neq(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
plus(s(x0), x1)
plus(0, x0)
WHILE(true, s(s(s(i)))) → WHILE(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
while(true, s(s(s(i)))) → while(gt(s(s(s(i))), s(0)), f(s(s(s(i)))))
f(i) → if(neq(i, s(s(0))), i)
gt(s(x), s(y)) → gt(x, y)
gt(s(x), 0) → true
gt(0, 0) → false
gt(0, s(y)) → false
if(true, i) → plus(i, s(0))
if(false, i) → i
neq(s(x), s(y)) → neq(x, y)
neq(0, 0) → false
neq(0, s(y)) → true
neq(s(x), 0) → true
plus(s(x), y) → plus(x, s(y))
plus(0, y) → y