R
↳Dependency Pair Analysis
APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))
APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)
APP(app(., app(app(., x), y)), z) -> APP(., y)
APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
APP(i, app(app(., x), y)) -> APP(., app(i, y))
APP(i, app(app(., x), y)) -> APP(i, y)
APP(i, app(app(., x), y)) -> APP(i, x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
APP(i, app(app(., x), y)) -> APP(i, x)
APP(i, app(app(., x), y)) -> APP(i, y)
APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)
APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))
app(app(., 1), x) -> x
app(app(., x), 1) -> x
app(app(., app(i, x)), x) -> 1
app(app(., x), app(i, x)) -> 1
app(app(., app(i, y)), app(app(., y), z)) -> z
app(app(., y), app(app(., app(i, y)), z)) -> z
app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
app(i, 1) -> 1
app(i, app(i, x)) -> x
app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))
APP(i, app(app(., x), y)) -> APP(i, x)
APP(i, app(app(., x), y)) -> APP(i, y)
APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)
app(app(., 1), x) -> x
app(app(., x), 1) -> x
app(app(., app(i, x)), x) -> 1
app(app(., x), app(i, x)) -> 1
app(app(., app(i, y)), app(app(., y), z)) -> z
app(app(., y), app(app(., app(i, y)), z)) -> z
app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
app(i, 1) -> 1
app(i, app(i, x)) -> x
app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))
POL(i) = 0 POL(1) = 0 POL(.) = 1 POL(APP(x1, x2)) = 1 + x1 + x2 POL(app(x1, x2)) = x1 + x2
APP(x1, x2) -> APP(x1, x2)
app(x1, x2) -> app(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))
app(app(., 1), x) -> x
app(app(., x), 1) -> x
app(app(., app(i, x)), x) -> 1
app(app(., x), app(i, x)) -> 1
app(app(., app(i, y)), app(app(., y), z)) -> z
app(app(., y), app(app(., app(i, y)), z)) -> z
app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
app(i, 1) -> 1
app(i, app(i, x)) -> x
app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))