0 QTRS
↳1 AAECC Innermost (⇔)
↳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 QDPOrderProof (⇔)
↳27 QDP
↳28 PisEmptyProof (⇔)
↳29 TRUE
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
COND1(true, x) → COND2(even(x), x)
COND1(true, x) → EVEN(x)
COND2(true, x) → COND1(neq(x, 0), div2(x))
COND2(true, x) → NEQ(x, 0)
COND2(true, x) → DIV2(x)
COND2(false, x) → COND1(neq(x, 0), p(x))
COND2(false, x) → NEQ(x, 0)
COND2(false, x) → P(x)
NEQ(s(x), s(y)) → NEQ(x, y)
EVEN(s(s(x))) → EVEN(x)
DIV2(s(s(x))) → DIV2(x)
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
DIV2(s(s(x))) → DIV2(x)
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
DIV2(s(s(x))) → DIV2(x)
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
DIV2(s(s(x))) → DIV2(x)
From the DPs we obtained the following set of size-change graphs:
EVEN(s(s(x))) → EVEN(x)
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
EVEN(s(s(x))) → EVEN(x)
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
EVEN(s(s(x))) → EVEN(x)
From the DPs we obtained the following set of size-change graphs:
COND2(true, x) → COND1(neq(x, 0), div2(x))
COND1(true, x) → COND2(even(x), x)
COND2(false, x) → COND1(neq(x, 0), p(x))
cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
COND2(true, x) → COND1(neq(x, 0), div2(x))
COND1(true, x) → COND2(even(x), x)
COND2(false, x) → COND1(neq(x, 0), p(x))
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
cond1(true, x0)
cond2(true, x0)
cond2(false, x0)
COND2(true, x) → COND1(neq(x, 0), div2(x))
COND1(true, x) → COND2(even(x), x)
COND2(false, x) → COND1(neq(x, 0), p(x))
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COND2(true, x) → COND1(neq(x, 0), div2(x))
COND1(true, x) → COND2(even(x), x)
COND2(false, x) → COND1(neq(x, 0), p(x))
The value of delta used in the strict ordering is 1/2.
POL(COND2(x1, x2)) = 3/2 + (5/4)x2
POL(true) = 4
POL(COND1(x1, x2)) = (1/2)x1 + (5/4)x2
POL(neq(x1, x2)) = x1 + (1/4)x2
POL(0) = 1/4
POL(div2(x1)) = 1/2 + (1/2)x1
POL(even(x1)) = 0
POL(false) = 0
POL(p(x1)) = 1/4 + (1/4)x1
POL(s(x1)) = 4 + (4)x1
neq(s(x), 0) → true
neq(0, 0) → false
p(s(x)) → x
p(0) → 0
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(y))
even(0)
even(s(0))
even(s(s(x0)))
div2(0)
div2(s(0))
div2(s(s(x0)))
p(0)
p(s(x0))