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 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(map, f), xs) → AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) → AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) → AP(isEmpty, xs)
AP(ap(ap(if, false), f), xs) → AP(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
AP(ap(ap(if, false), f), xs) → AP(cons, ap(f, ap(last, xs)))
AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
AP(ap(ap(if, false), f), xs) → AP(last, xs)
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
AP(ap(ap(if, false), f), xs) → AP(map, f)
AP(ap(ap(if, false), f), xs) → AP(dropLast, xs)
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
dropLast1(cons(x, cons(y, ys))) → dropLast1(cons(y, ys))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(dropLast, ap(ap(cons, y), ys))
cons2 > dropLast11
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
last1(cons(x, cons(y, ys))) → last1(cons(y, ys))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → AP(last, ap(ap(cons, y), ys))
cons2 > last11
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(ap(ap(if, false), f), xs) → AP(f, ap(last, xs))
map > [AP1, ap1, false] > if > last
map > [AP1, ap1, false] > isEmpty
map > [AP1, ap1, false] > dropLast > cons > last
map > [AP1, ap1, false] > dropLast > nil
AP(ap(map, f), xs) → AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(ap(if, false), f), xs) → AP(ap(map, f), ap(dropLast, xs))
ap(ap(map, f), xs) → ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) → nil
ap(ap(ap(if, false), f), xs) → ap(ap(cons, ap(f, ap(last, xs))), ap(ap(map, f), ap(dropLast, xs)))
ap(isEmpty, nil) → true
ap(isEmpty, ap(ap(cons, x), xs)) → false
ap(last, ap(ap(cons, x), nil)) → x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(last, ap(ap(cons, y), ys))
ap(dropLast, nil) → nil
ap(dropLast, ap(ap(cons, x), nil)) → nil
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) → ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(ap(map, x0), x1)
ap(ap(ap(if, true), x0), x1)
ap(ap(ap(if, false), x0), x1)
ap(isEmpty, nil)
ap(isEmpty, ap(ap(cons, x0), x1))
ap(last, ap(ap(cons, x0), nil))
ap(last, ap(ap(cons, x0), ap(ap(cons, x1), x2)))
ap(dropLast, nil)
ap(dropLast, ap(ap(cons, x0), nil))
ap(dropLast, ap(ap(cons, x0), ap(ap(cons, x1), x2)))