R
↳Dependency Pair Analysis
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)
R
↳DPs
→DP Problem 1
↳A-Transformation
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), y)), z)
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(:, 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(:, x), z)), app(app(:, app(app(:, app(app(:, x), y)), z)), u))
innermost
R
↳DPs
→DP Problem 1
↳ATrans
→DP Problem 2
↳Argument Filtering and Ordering
:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, z), :(:(:(x, y), z), u))
:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))
innermost
:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, z), :(:(:(x, y), z), u))
:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))
trivial
:'(x1, x2) -> x1
:(x1, x2) -> :(x1, x2)
R
↳DPs
→DP Problem 1
↳ATrans
→DP Problem 2
↳AFS
...
→DP Problem 3
↳Dependency Graph
:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))
innermost