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 QDPOrderProof (⇔)
↳20 QDP
↳21 PisEmptyProof (⇔)
↳22 TRUE
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))
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))
The value of delta used in the strict ordering is 1/16.
POL(COND(x1, x2)) = (1/4)x1 + (3)x2
POL(true) = 1/2
POL(and(x1, x2)) = 1/4 + (1/2)x2
POL(even(x1)) = 1/4 + (1/4)x1
POL(gr(x1, x2)) = x1
POL(0) = 0
POL(p(x1)) = (1/4)x1
POL(s(x1)) = 2 + (4)x1
POL(false) = 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
and(true, true) → true
p(0) → 0
and(x, false) → false
and(false, x) → false
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))