YES
0 QTRS
↳1 AAECC Innermost (⇔, 7 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 QDPQMonotonicMRRProof (⇔, 28 ms)
↳20 QDP
↳21 QDPQMonotonicMRRProof (⇔, 0 ms)
↳22 QDP
↳23 QDPOrderProof (⇔, 10 ms)
↳24 QDP
↳25 PisEmptyProof (⇔, 0 ms)
↳26 YES
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
COND(true, x) → AND(even(x), gr(x, 0))
COND(true, x) → EVEN(x)
COND(true, x) → GR(x, 0)
COND(true, x) → P(x)
EVEN(s(s(x))) → EVEN(x)
GR(s(x), s(y)) → GR(x, y)
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
EVEN(s(s(x))) → EVEN(x)
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
EVEN(s(s(x))) → EVEN(x)
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
EVEN(s(s(x))) → EVEN(x)
From the DPs we obtained the following set of size-change graphs:
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
cond(true, x) → cond(and(even(x), gr(x, 0)), p(x))
and(x, false) → false
and(false, x) → false
and(true, true) → true
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
and(x, false) → false
and(false, x) → false
and(true, true) → true
p(0) → 0
p(s(x)) → x
cond(true, x0)
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
cond(true, x0)
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
and(x, false) → false
and(false, x) → false
and(true, true) → true
p(0) → 0
p(s(x)) → x
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
p(s(x)) → x
POL(0) = 0
POL(COND(x1, x2)) = 2·x2
POL(and(x1, x2)) = 2
POL(even(x1)) = 2
POL(false) = 0
POL(gr(x1, x2)) = 2·x1
POL(p(x1)) = x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 0
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
and(x, false) → false
and(false, x) → false
and(true, true) → true
p(0) → 0
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
and(x, false) → false
and(false, x) → false
POL(0) = 1
POL(COND(x1, x2)) = 2·x1
POL(and(x1, x2)) = 1
POL(even(x1)) = x1
POL(false) = 0
POL(gr(x1, x2)) = 2·x1
POL(p(x1)) = 2 + x1
POL(s(x1)) = 1 + x1
POL(true) = 1
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
p(0) → 0
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COND(true, x) → COND(and(even(x), gr(x, 0)), p(x))
p > 0 > false
s=3
0=1
true=2
p=1
COND_2=1
false=1
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
p(0) → 0
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
p(0) → 0
and(x0, false)
and(false, x0)
and(true, true)
even(0)
even(s(0))
even(s(s(x0)))
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(y))
p(0)
p(s(x0))