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 PisEmptyProof (⇔)
↳18 TRUE
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(:, app(app(:, x), z))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(:, x)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, app(app(:, x), y)), z)), u)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(:, app(app(:, app(app(:, x), y)), z))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), y)), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(:, app(app(:, x), y))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), y)
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(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(filter2, app(f, x)), f), x)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(filter2, app(f, x)), f)
APP(app(filter, f), app(app(cons, x), xs)) → APP(filter2, app(f, x))
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(cons, x), app(app(filter, f), xs))
APP(app(app(app(filter2, true), f), x), xs) → APP(cons, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, true), f), x), xs) → APP(filter, f)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, false), f), x), xs) → APP(filter, f)
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, app(app(:, x), y)), z)), u)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), y)), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), y)
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
:1(:(:(:(C, x), y), z), u) → :1(x, z)
:1(:(:(:(C, x), y), z), u) → :1(:(x, z), :(:(:(x, y), z), u))
:1(:(:(:(C, x), y), z), u) → :1(:(:(x, y), z), u)
:1(:(:(:(C, x), y), z), u) → :1(:(x, y), z)
:1(:(:(:(C, x), y), z), u) → :1(x, y)
:(:(:(:(C, x), y), z), u) → :(:(x, z), :(:(:(x, y), z), u))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, app(app(:, x), y)), z)), u)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, app(app(:, x), y)), z)
APP(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → APP(app(:, x), y)
:11 > :2
C > :2
:2: [1,2]
:11: [1]
C: []
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
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(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), 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)
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
map > app2 > filter
cons > filter
filter2 > filter
true > app2 > filter
false > app2 > filter
cons: []
true: []
map: []
false: []
app2: [2,1]
filter2: []
filter: []
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), 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)
cons2 > map12
cons2: [1,2]
map12: [1,2]
app(app(:, app(app(:, app(app(:, app(app(:, C), x)), y)), z)), u) → app(app(:, app(app(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
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(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(:, app(app(:, app(app(:, app(app(:, C), x0)), x1)), x2)), x3)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)