f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
F(true, x, y) → F(gt(x, y), x, round(s(y)))
F(true, x, y) → GT(x, y)
F(true, x, y) → ROUND(s(y))
GT(s(u), s(v)) → GT(u, v)
ROUND(s(s(x))) → ROUND(x)
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(true, x, y) → F(gt(x, y), x, round(s(y)))
F(true, x, y) → GT(x, y)
F(true, x, y) → ROUND(s(y))
GT(s(u), s(v)) → GT(u, v)
ROUND(s(s(x))) → ROUND(x)
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
ROUND(s(s(x))) → ROUND(x)
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
ROUND(s(s(x))) → ROUND(x)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
ROUND(s(s(x))) → ROUND(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
F(true, x, y) → F(gt(x, y), x, round(s(y)))
f(true, x, y) → f(gt(x, y), x, round(s(y)))
round(0) → 0
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F(true, x, y) → F(gt(x, y), x, round(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
f(true, x0, x1)
gt(s(x0), 0)
f(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
F(true, x, y) → F(gt(x, y), x, round(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), round(s(s(x1))))
F(true, s(x0), 0) → F(true, s(x0), round(s(0)))
F(true, 0, x0) → F(false, 0, round(s(x0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
F(true, s(x0), 0) → F(true, s(x0), round(s(0)))
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), round(s(s(x1))))
F(true, 0, x0) → F(false, 0, round(s(x0)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ NonInfProof
F(true, s(x0), 0) → F(true, s(x0), round(s(0)))
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), round(s(s(x1))))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), s(s(round(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
F(true, s(x0), 0) → F(true, s(x0), round(s(0)))
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), s(s(round(x1))))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ NonInfProof
F(true, s(x0), s(x1)) → F(gt(x0, x1), s(x0), s(s(round(x1))))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
F(true, s(z0), s(s(y_1))) → F(gt(z0, s(y_1)), s(z0), s(s(round(s(y_1)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
F(true, s(z0), s(s(y_1))) → F(gt(z0, s(y_1)), s(z0), s(s(round(s(y_1)))))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)
POL(0) = 0
POL(F(x1, x2, x3)) = -1 - x1 + x2 - x3
POL(c) = -1
POL(false) = 0
POL(gt(x1, x2)) = 0
POL(round(x1)) = x1
POL(s(x1)) = 2 + x1
POL(true) = 0
The following pairs are in Pbound:
F(true, x, y) → F(gt(x, y), x, round(s(y)))
The following rules are usable:
F(true, x, y) → F(gt(x, y), x, round(s(y)))
0 → round(0)
gt(u, v) → gt(s(u), s(v))
false → gt(0, v)
s(s(round(x))) → round(s(s(x)))
s(s(0)) → round(s(0))
true → gt(s(u), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ QDP
↳ PisEmptyProof
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
round(s(0)) → s(s(0))
round(s(s(x))) → s(s(round(x)))
round(0) → 0
round(s(s(x0)))
round(0)
gt(0, x0)
round(s(0))
gt(s(x0), s(x1))
gt(s(x0), 0)