0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 ATransformationProof (⇔)
↳9 QDP
↳10 QDPSizeChangeProof (⇔)
↳11 TRUE
↳12 QDP
↳13 UsableRulesProof (⇔)
↳14 QDP
↳15 MNOCProof (⇔)
↳16 QDP
↳17 ATransformationProof (⇔)
↳18 QDP
↳19 MRRProof (⇔)
↳20 QDP
↳21 DependencyGraphProof (⇔)
↳22 TRUE
↳23 QDP
↳24 QDPApplicativeOrderProof (⇔)
↳25 QDP
↳26 PisEmptyProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QDPSizeChangeProof (⇔)
↳32 TRUE
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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
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), app(id, y))), app(s, y)))
APP(app(div, app(s, x)), app(s, y)) → APP(app(div, app(app(minus, x), app(id, y))), app(s, y))
APP(app(div, app(s, x)), app(s, y)) → APP(div, app(app(minus, x), app(id, y)))
APP(app(div, app(s, x)), app(s, y)) → APP(app(minus, x), app(id, y))
APP(app(div, app(s, x)), app(s, y)) → APP(minus, x)
APP(app(div, app(s, x)), app(s, y)) → APP(id, y)
APP(id, x) → APP(s, app(s, app(s, x)))
APP(id, x) → APP(s, app(s, x))
APP(id, x) → APP(s, x)
APP(id, app(p, x)) → APP(id, app(s, app(id, x)))
APP(id, app(p, x)) → APP(s, app(id, x))
APP(id, app(p, x)) → APP(id, 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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
APP(id, app(p, x)) → APP(id, 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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
APP(id, app(p, x)) → APP(id, x)
id(p(x)) → id(x)
From the DPs we obtained the following set of size-change graphs:
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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, 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(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(p, app(s, x0))
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(x)) → x
p(s(x0))
p(s(x)) → x
POL(minus(x1, x2)) = x1 + x2
POL(p(x1)) = x1
POL(s(x1)) = 1 + x1
minus(s(x), s(y)) → minus(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), app(id, 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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
div1(s(x), s(y)) → div1(minus(x, id(y)), s(y))
id(x) → x
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, 0) → x
p(s(x)) → x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(div, app(s, x)), app(s, y)) → APP(app(div, app(app(minus, x), app(id, y))), app(s, y))
POL(0) = 0
POL(div1(x1, x2)) = x1
POL(id(x1)) = x1
POL(minus(x1, x2)) = x1
POL(p(x1)) = x1
POL(s(x1)) = 1 + x1
app(id, x) → x
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, x), 0) → x
app(p, app(s, x)) → 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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
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), app(id, y))), app(s, y)))
app(id, x) → x
app(id, x) → app(s, app(s, app(s, x)))
app(id, app(p, x)) → app(id, app(s, app(id, x)))
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)
From the DPs we obtained the following set of size-change graphs: