log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
DOUBLE(s(x)) → DOUBLE(x)
SQUARE(s(x)) → SQUARE(x)
SQUARE(s(x)) → PLUS(square(x), double(x))
COND(false, x, y) → SQUARE(s(s(y)))
LE(s(u), s(v)) → LE(u, v)
COND(false, x, y) → LOG(x, square(s(s(y))))
SQUARE(s(x)) → DOUBLE(x)
PLUS(n, s(m)) → PLUS(n, m)
LOG(x, s(s(y))) → LE(x, s(s(y)))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
COND(false, x, y) → DOUBLE(log(x, square(s(s(y)))))
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DOUBLE(s(x)) → DOUBLE(x)
SQUARE(s(x)) → SQUARE(x)
SQUARE(s(x)) → PLUS(square(x), double(x))
COND(false, x, y) → SQUARE(s(s(y)))
LE(s(u), s(v)) → LE(u, v)
COND(false, x, y) → LOG(x, square(s(s(y))))
SQUARE(s(x)) → DOUBLE(x)
PLUS(n, s(m)) → PLUS(n, m)
LOG(x, s(s(y))) → LE(x, s(s(y)))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
COND(false, x, y) → DOUBLE(log(x, square(s(s(y)))))
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS(n, s(m)) → PLUS(n, m)
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS(n, s(m)) → PLUS(n, m)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS(n, s(m)) → PLUS(n, m)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
SQUARE(s(x)) → SQUARE(x)
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
SQUARE(s(x)) → SQUARE(x)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
SQUARE(s(x)) → SQUARE(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
LE(s(u), s(v)) → LE(u, v)
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
LE(s(u), s(v)) → LE(u, v)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
LE(s(u), s(v)) → LE(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
COND(false, x, y) → LOG(x, square(s(s(y))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
COND(false, x, y) → LOG(x, square(s(s(y))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
cond(true, x0, x1)
log(x0, s(s(x1)))
square(s(x0))
double(s(x0))
cond(false, x0, x1)
cond(true, x0, x1)
log(x0, s(s(x1)))
cond(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
COND(false, x, y) → LOG(x, square(s(s(y))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, x, y) → LOG(x, s(plus(square(s(y)), double(s(y)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
COND(false, x, y) → LOG(x, s(plus(square(s(y)), double(s(y)))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, x, y) → LOG(x, s(plus(s(plus(square(y), double(y))), double(s(y)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
COND(false, x, y) → LOG(x, s(plus(s(plus(square(y), double(y))), double(s(y)))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, x, y) → LOG(x, s(plus(s(plus(square(y), double(y))), s(s(double(y))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
COND(false, x, y) → LOG(x, s(plus(s(plus(square(y), double(y))), s(s(double(y))))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, x, y) → LOG(x, s(s(plus(s(plus(square(y), double(y))), s(double(y))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
COND(false, x, y) → LOG(x, s(s(plus(s(plus(square(y), double(y))), s(double(y))))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ NonInfProof
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
LOG(s(x0), s(s(y1))) → COND(le(x0, s(y1)), s(x0), y1)
LOG(0, s(s(y1))) → COND(true, 0, y1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
LOG(s(x0), s(s(y1))) → COND(le(x0, s(y1)), s(x0), y1)
LOG(0, s(s(y1))) → COND(true, 0, y1)
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ NonInfProof
LOG(s(x0), s(s(y1))) → COND(le(x0, s(y1)), s(x0), y1)
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ NonInfProof
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(square(s(z1)), double(s(z1)))), double(s(z1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ NonInfProof
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(square(s(z1)), double(s(z1)))), double(s(z1)))))))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(s(plus(square(z1), double(z1))), double(s(z1)))), double(s(z1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(s(plus(square(z1), double(z1))), double(s(z1)))), double(s(z1)))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(s(plus(square(z1), double(z1))), s(s(double(z1))))), double(s(z1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(plus(s(plus(square(z1), double(z1))), s(s(double(z1))))), double(s(z1)))))))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(plus(s(plus(square(z1), double(z1))), s(double(z1))))), double(s(z1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(plus(s(plus(square(z1), double(z1))), s(double(z1))))), double(s(z1)))))))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), double(s(z1)))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), double(s(z1)))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), s(s(double(z1))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), s(s(double(z1))))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), s(double(z1))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ NonInfProof
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), s(double(z1))))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), double(z1))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ NonInfProof
COND(false, s(z0), s(z1)) → LOG(s(z0), s(s(s(s(s(plus(s(s(s(plus(s(plus(square(z1), double(z1))), double(z1))))), double(z1))))))))
LOG(s(x0), s(s(s(y_4)))) → COND(le(x0, s(s(y_4))), s(x0), s(y_4))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
POL(0) = 0
POL(COND(x1, x2, x3)) = -1 - x1 + 2·x2 - x3
POL(LOG(x1, x2)) = 2 + 2·x1 - x2
POL(c) = -2
POL(double(x1)) = 2·x1
POL(false) = 1
POL(le(x1, x2)) = 1
POL(plus(x1, x2)) = x2
POL(s(x1)) = 2 + x1
POL(square(x1)) = 0
POL(true) = 1
The following pairs are in Pbound:
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
The following rules are usable:
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
false → le(s(u), 0)
s(s(double(x))) → double(s(x))
le(u, v) → le(s(u), s(v))
s(plus(n, m)) → plus(n, s(m))
n → plus(n, 0)
true → le(0, v)
0 → double(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
LOG(x, s(s(y))) → COND(le(x, s(s(y))), x, y)
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
COND(false, x, y) → LOG(x, s(s(s(plus(s(plus(square(y), double(y))), double(y))))))
le(0, v) → true
le(s(u), s(v)) → le(u, v)
le(s(u), 0) → false
square(s(x)) → s(plus(square(x), double(x)))
square(0) → 0
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0)
square(0)
le(s(x0), s(x1))
plus(x0, s(x1))
le(s(x0), 0)
plus(x0, 0)
le(0, x0)
square(s(x0))
double(s(x0))