YES
0 QTRS
↳1 AAECC Innermost (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 2 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 (⇔, 38 ms)
↳20 QDP
↳21 QDPOrderProof (⇔, 0 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
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))
p(s(x)) → x
POL(0) = 1
POL(COND(x1, x2, x3, x4)) = x2 + x3
POL(and(x1, x2)) = 2
POL(false) = 0
POL(gr(x1, x2)) = 2·x2
POL(p(x1)) = x1
POL(s(x1)) = 2 + x1
POL(true) = 0
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
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)
trivial
s_1=4
0=2
true=4
p=3
COND_2=1
false=1
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
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
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))