YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 ATransformationProof (⇔, 0 ms)
↳11 QDP
↳12 QReductionProof (⇔, 0 ms)
↳13 QDP
↳14 MRRProof (⇔, 5 ms)
↳15 QDP
↳16 DependencyGraphProof (⇔, 0 ms)
↳17 TRUE
↳18 QDP
↳19 UsableRulesProof (⇔, 0 ms)
↳20 QDP
↳21 ATransformationProof (⇔, 0 ms)
↳22 QDP
↳23 QReductionProof (⇔, 0 ms)
↳24 QDP
↳25 QDPOrderProof (⇔, 0 ms)
↳26 QDP
↳27 PisEmptyProof (⇔, 0 ms)
↳28 YES
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QDPSizeChangeProof (⇔, 0 ms)
↳33 YES
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, app(p, app(s, x))), app(p, app(s, y)))
APP(app(minus, app(s, x)), app(s, y)) → APP(minus, app(p, app(s, x)))
APP(app(minus, app(s, x)), app(s, y)) → APP(p, app(s, x))
APP(app(minus, app(s, x)), app(s, y)) → APP(p, app(s, y))
APP(app(div, app(s, x)), app(s, y)) → APP(s, app(app(div, app(app(minus, x), y)), app(s, y)))
APP(app(div, app(s, x)), app(s, y)) → APP(app(div, app(app(minus, x), y)), app(s, y))
APP(app(div, app(s, x)), app(s, y)) → APP(div, app(app(minus, x), y))
APP(app(div, app(s, x)), app(s, y)) → APP(app(minus, x), y)
APP(app(div, app(s, x)), app(s, y)) → APP(minus, x)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
minus1(s(x), s(y)) → minus1(p(s(x)), p(s(y)))
p(s(x)) → x
map(x0, nil)
map(x0, cons(x1, x2))
minus(x0, 0)
minus(s(x0), s(x1))
p(s(x0))
div(0, s(x0))
div(s(x0), s(x1))
map(x0, nil)
map(x0, cons(x1, x2))
minus(x0, 0)
minus(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
minus1(s(x), s(y)) → minus1(p(s(x)), p(s(y)))
p(s(x)) → x
p(s(x0))
p(s(x)) → x
POL(minus1(x1, x2)) = 2·x1 + x2
POL(p(x1)) = x1
POL(s(x1)) = 2 + 2·x1
minus1(s(x), s(y)) → minus1(p(s(x)), p(s(y)))
p(s(x0))
APP(app(div, app(s, x)), app(s, y)) → APP(app(div, app(app(minus, x), y)), app(s, y))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
APP(app(div, app(s, x)), app(s, y)) → APP(app(div, app(app(minus, x), y)), app(s, y))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
div1(s(x), s(y)) → div1(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(x)) → x
map(x0, nil)
map(x0, cons(x1, x2))
minus(x0, 0)
minus(s(x0), s(x1))
p(s(x0))
div(0, s(x0))
div(s(x0), s(x1))
map(x0, nil)
map(x0, cons(x1, x2))
div(0, s(x0))
div(s(x0), s(x1))
div1(s(x), s(y)) → div1(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(x)) → x
minus(x0, 0)
minus(s(x0), s(x1))
p(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
div1(s(x), s(y)) → div1(minus(x, y), s(y))
trivial
s_1=1
dummyConstant=1
minus(x, 0) → x
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(x)) → x
minus(x0, 0)
minus(s(x0), s(x1))
p(s(x0))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, app(p, app(s, x))), app(p, app(s, y)))
app(p, app(s, x)) → x
app(app(div, 0), app(s, y)) → 0
app(app(div, app(s, x)), app(s, y)) → app(s, app(app(div, app(app(minus, x), y)), app(s, y)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(p, app(s, x0))
app(app(div, 0), app(s, x0))
app(app(div, app(s, x0)), app(s, x1))
From the DPs we obtained the following set of size-change graphs: