0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 PisEmptyProof (⇔)
↳20 TRUE
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(plus, app(s, x)), y) → APP(s, app(app(plus, x), y))
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
APP(app(plus, app(s, x)), y) → APP(plus, x)
APP(inc, xs) → APP(app(map, app(plus, app(s, 0))), xs)
APP(inc, xs) → APP(map, app(plus, app(s, 0)))
APP(inc, xs) → APP(plus, app(s, 0))
APP(inc, xs) → APP(s, 0)
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(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
plus1(s(x), y) → plus1(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(plus, app(s, x)), y) → APP(app(plus, x), y)
[plus11, s1]
plus11: multiset
s1: [1]
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
APP(inc, xs) → APP(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(inc, xs) → APP(app(map, app(plus, app(s, 0))), xs)
[inc, map, cons] > [APP1, 0] > plus > s
APP1: [1]
cons: multiset
plus: multiset
map: multiset
inc: multiset
s: multiset
0: multiset
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(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
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)
map > APP1 > [app1, cons]
APP1: multiset
cons: multiset
map: multiset
app1: multiset
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
map1(f, cons(x, xs)) → map1(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)
[map11, cons1]
cons1: multiset
map11: multiset
app(app(plus, 0), y) → y
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
app(inc, xs) → app(app(map, app(plus, app(s, 0))), xs)
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(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
app(inc, x0)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))