minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
EQUAL(s(x), s(y)) → EQUAL(x, y)
MIN(s(u), s(v)) → MIN(u, v)
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
MINUS(x, y) → EQUAL(min(x, y), y)
MINUS(x, y) → MIN(x, y)
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
EQUAL(s(x), s(y)) → EQUAL(x, y)
MIN(s(u), s(v)) → MIN(u, v)
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
MINUS(x, y) → EQUAL(min(x, y), y)
MINUS(x, y) → MIN(x, y)
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN(s(u), s(v)) → MIN(u, v)
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN(s(u), s(v)) → MIN(u, v)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MIN(s(u), s(v)) → MIN(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
minus(x, x) → 0
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
minus(x0, x1)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
cond(true, x0, x1)
equal(0, s(x0))
minus(x0, x1)
cond(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
MINUS(0, x0) → COND(equal(0, x0), 0, x0)
MINUS(x0, 0) → COND(equal(0, 0), x0, 0)
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
MINUS(x0, 0) → COND(equal(0, 0), x0, 0)
COND(true, x, y) → MINUS(x, s(y))
MINUS(0, x0) → COND(equal(0, x0), 0, x0)
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ NonInfProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(0, x0) → COND(equal(0, x0), 0, x0)
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
MINUS(0, s(x0)) → COND(false, 0, s(x0))
MINUS(0, 0) → COND(true, 0, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(0, s(x0)) → COND(false, 0, s(x0))
MINUS(0, 0) → COND(true, 0, 0)
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ NonInfProof
COND(true, x, y) → MINUS(x, s(y))
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
COND(true, s(z0), s(z1)) → MINUS(s(z0), s(s(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ NonInfProof
COND(true, s(z0), s(z1)) → MINUS(s(z0), s(s(z1)))
MINUS(s(x0), s(x1)) → COND(equal(s(min(x0, x1)), s(x1)), s(x0), s(x1))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
MINUS(s(z0), s(s(z1))) → COND(equal(s(min(z0, s(z1))), s(s(z1))), s(z0), s(s(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
COND(true, s(z0), s(z1)) → MINUS(s(z0), s(s(z1)))
MINUS(s(z0), s(s(z1))) → COND(equal(s(min(z0, s(z1))), s(s(z1))), s(z0), s(s(z1)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
POL(0) = 0
POL(COND(x1, x2, x3)) = -1 - x1 + x2 - x3
POL(MINUS(x1, x2)) = -1 + x1 - x2
POL(c) = -1
POL(equal(x1, x2)) = 0
POL(false) = 2
POL(min(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND(true, x, y) → MINUS(x, s(y))
The following rules are usable:
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
true → equal(0, 0)
false → equal(0, s(y))
false → equal(s(x), 0)
equal(x, y) → equal(s(x), s(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
COND(true, x, y) → MINUS(x, s(y))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(s(x0), s(x1))
equal(s(x0), 0)
equal(0, 0)
min(x0, 0)
equal(s(x0), s(x1))
min(0, x0)
equal(0, s(x0))