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 DependencyGraphProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 PisEmptyProof (⇔)
↳26 TRUE
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → 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
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND1(true, x, y) → COND2(gr(y, 0), x, y)
COND1(true, x, y) → GR(y, 0)
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
COND2(true, x, y) → GR(y, 0)
COND2(true, x, y) → P(y)
COND2(false, x, y) → COND1(gr(x, 0), p(x), y)
COND2(false, x, y) → GR(x, 0)
COND2(false, x, y) → P(x)
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
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)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
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)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
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:
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
COND2(false, x, y) → COND1(gr(x, 0), p(x), y)
COND1(true, x, y) → COND2(gr(y, 0), x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
COND2(false, x, y) → COND1(gr(x, 0), p(x), y)
COND1(true, x, y) → COND2(gr(y, 0), x, y)
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
COND2(false, x, y) → COND1(gr(x, 0), p(x), y)
COND1(true, x, y) → COND2(gr(y, 0), x, y)
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
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.
COND1(true, x, y) → COND2(gr(y, 0), x, y)
The value of delta used in the strict ordering is 1/8.
POL(COND2(x1, x2, x3)) = 2 + (13/4)x2
POL(true) = 1/2
POL(gr(x1, x2)) = (1/4)x1
POL(0) = 0
POL(p(x1)) = 1/4 + (1/4)x1
POL(false) = 0
POL(COND1(x1, x2, x3)) = 1 + (9/4)x1 + (4)x2
POL(s(x1)) = 4 + (4)x1
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
COND2(false, x, y) → COND1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
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.
COND2(true, x, y) → COND2(gr(y, 0), x, p(y))
The value of delta used in the strict ordering is 1/2.
POL(COND2(x1, x2, x3)) = (2)x1 + (4)x3
POL(true) = 1/4
POL(gr(x1, x2)) = x1
POL(0) = 0
POL(p(x1)) = (1/4)x1
POL(s(x1)) = 1/4 + (4)x1
POL(false) = 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
gr(0, x) → false
gr(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))