YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 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 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 84 ms)
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QReductionProof (⇔, 0 ms)
↳38 QDP
↳39 QDPOrderProof (⇔, 29 ms)
↳40 QDP
↳41 DependencyGraphProof (⇔, 0 ms)
↳42 TRUE
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
CHECK(s(s(s(x)))) → CHECK(s(x))
HALF(s(s(x))) → HALF(x)
PLUS(s(x), y) → PLUS(x, y)
TIMES(x, y) → TIMESITER(x, y, 0)
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
TIMESITER(x, y, z) → CHECK(x)
TIMESITER(x, y, z) → PLUS(z, y)
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
IF(odd, x, y, z, u) → P(x)
IF(even, x, y, z, u) → PLUS(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(z))
IF(even, x, y, z, u) → HALF(x)
IF(even, x, y, z, u) → HALF(z)
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(s(z)))
IF(even, x, y, z, u) → HALF(s(z))
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
HALF(s(s(x))) → HALF(x)
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
HALF(s(s(x))) → HALF(x)
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
CHECK(s(s(s(x)))) → CHECK(s(x))
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
CHECK(s(s(s(x)))) → CHECK(s(x))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
CHECK(s(s(s(x)))) → CHECK(s(x))
From the DPs we obtained the following set of size-change graphs:
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(z))
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(s(z)))
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → if(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
if(zero, x, y, z, u) → z
if(odd, x, y, z, u) → timesIter(p(x), y, u)
if(even, x, y, z, u) → plus(timesIter(half(x), y, half(z)), timesIter(half(x), y, half(s(z))))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(z))
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(s(z)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2)
p(s(x0))
p(0)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
times(x0, x1)
timesIter(x0, x1, x2)
if(zero, x0, x1, x2, x3)
if(odd, x0, x1, x2, x3)
if(even, x0, x1, x2, x3)
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(z))
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(s(z)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
p(s(x0))
p(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(z))
IF(even, x, y, z, u) → TIMESITER(half(x), y, half(s(z)))
The value of delta used in the strict ordering is 1/8.
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = [4] + [1/4]x1 + [2]x2 + x3
POL(TIMESITER(x1, x2, x3)) = [4] + [4]x1 + x2
POL(check(x1)) = [2]x1
POL(even) = [1/2]
POL(half(x1)) = [1/2]x1
POL(odd) = 0
POL(p(x1)) = [1/2]x1
POL(plus(x1, x2)) = [4]x1 + x2
POL(s(x1)) = [4] + [2]x1
POL(zero) = 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
p(s(x)) → x
p(0) → 0
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
p(s(x0))
p(0)
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
half(0)
half(s(0))
half(s(s(x0)))
plus(0, x0)
plus(s(x0), x1)
p(s(x0))
p(0)
half(0)
half(s(0))
half(s(s(x0)))
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
plus(0, x0)
plus(s(x0), x1)
p(s(x0))
p(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(odd, x, y, z, u) → TIMESITER(p(x), y, u)
The value of delta used in the strict ordering is 2.
POL(0) = [4]
POL(IF(x1, x2, x3, x4, x5)) = [2]x1 + [1/4]x2
POL(TIMESITER(x1, x2, x3)) = [2] + x1
POL(check(x1)) = [1] + [1/4]x1
POL(even) = [1]
POL(odd) = [4]
POL(p(x1)) = [4] + [1/4]x1
POL(plus(x1, x2)) = 0
POL(s(x1)) = [4] + [4]x1
POL(zero) = [1/4]
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
p(s(x)) → x
p(0) → 0
TIMESITER(x, y, z) → IF(check(x), x, y, z, plus(z, y))
p(s(x)) → x
p(0) → 0
check(0) → zero
check(s(0)) → odd
check(s(s(0))) → even
check(s(s(s(x)))) → check(s(x))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
check(0)
check(s(0))
check(s(s(0)))
check(s(s(s(x0))))
plus(0, x0)
plus(s(x0), x1)
p(s(x0))
p(0)