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, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
and(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
cond(true, x, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
and(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND(true, x, y, z) → COND(and(gr(x, z), gr(y, z)), p(x), p(y), z)
COND(true, x, y, z) → AND(gr(x, z), gr(y, z))
COND(true, x, y, z) → GR(x, z)
COND(true, x, y, z) → GR(y, z)
COND(true, x, y, z) → P(x)
COND(true, x, y, z) → P(y)
GR(s(x), s(y)) → GR(x, y)
cond(true, x, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
and(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond(true, x, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
and(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond(true, x0, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
cond(true, x0, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
From the DPs we obtained the following set of size-change graphs:
COND(true, x, y, z) → COND(and(gr(x, z), gr(y, z)), p(x), p(y), z)
cond(true, x, y, z) → cond(and(gr(x, z), gr(y, z)), p(x), p(y), z)
and(true, true) → true
and(x, false) → false
and(false, x) → false
gr(0, 0) → false
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, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND(true, x, y, z) → COND(and(gr(x, z), gr(y, z)), p(x), p(y), z)
gr(0, 0) → false
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(x, false) → false
and(false, x) → false
p(0) → 0
p(s(x)) → x
cond(true, x0, x1, x2)
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
cond(true, x0, x1, x2)
COND(true, x, y, z) → COND(and(gr(x, z), gr(y, z)), p(x), p(y), z)
gr(0, 0) → false
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(x, false) → false
and(false, x) → false
p(0) → 0
p(s(x)) → x
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
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, y, z) → COND(and(gr(x, z), gr(y, z)), p(x), p(y), z)
The value of delta used in the strict ordering is 3/8.
POL(COND(x1, x2, x3, x4)) = (1/4)x1 + (4)x2 + (4)x3
POL(true) = 2
POL(and(x1, x2)) = 1/2 + (1/2)x1 + (1/4)x2
POL(gr(x1, x2)) = (9/4)x1
POL(p(x1)) = (1/4)x1
POL(s(x1)) = 1 + (4)x1
POL(0) = 0
POL(false) = 0
gr(s(x), 0) → true
gr(0, x) → false
gr(0, 0) → false
and(false, x) → false
and(x, false) → false
and(true, true) → true
gr(s(x), s(y)) → gr(x, y)
p(s(x)) → x
p(0) → 0
gr(0, 0) → false
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
and(true, true) → true
and(x, false) → false
and(false, x) → false
p(0) → 0
p(s(x)) → x
and(true, true)
and(x0, false)
and(false, x0)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))