0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 QDPOrderProof (⇔)
↳8 QDP
↳9 PisEmptyProof (⇔)
↳10 TRUE
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), 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(add, app(s, x)), y) → APP(s, app(app(add, x), y))
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
APP(app(add, app(s, x)), y) → APP(add, 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(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), 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(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), 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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(add, app(s, x)), y) → APP(app(add, x), y)
map > [app1, add, id] > APP2
s > [app1, add, id] > APP2
0 > [app1, add, id] > APP2
APP2: multiset
app1: multiset
map: multiset
cons: multiset
add: multiset
s: multiset
0: multiset
id: multiset
app(add, 0) → id
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), 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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app2 > map
app2: multiset
map: multiset
cons: multiset
app(id, x) → x
app(add, 0) → id
app(app(add, app(s, x)), y) → app(s, app(app(add, x), 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))