R
↳Dependency Pair Analysis
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(insert, f), g), app(app(app(sort, f), g), y))
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(insert, f), g)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(insert, f)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(sort, f), g), y)
APP(app(app(app(insert, f), g), nil), y) -> APP(app(cons, y), nil)
APP(app(app(app(insert, f), g), nil), y) -> APP(cons, y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y)))
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(cons, app(app(f, x), y))
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(f, x), y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(f, x)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(app(app(insert, f), g), z), app(app(g, x), y))
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(app(insert, f), g), z)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(g, x), y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(g, x)
APP(app(max, app(s, x)), app(s, y)) -> APP(app(max, x), y)
APP(app(max, app(s, x)), app(s, y)) -> APP(max, x)
APP(app(min, app(s, x)), app(s, y)) -> APP(app(min, x), y)
APP(app(min, app(s, x)), app(s, y)) -> APP(min, x)
APP(asort, z) -> APP(app(app(sort, min), max), z)
APP(asort, z) -> APP(app(sort, min), max)
APP(asort, z) -> APP(sort, min)
APP(dsort, z) -> APP(app(app(sort, max), min), z)
APP(dsort, z) -> APP(app(sort, max), min)
APP(dsort, z) -> APP(sort, max)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Nar
APP(app(max, app(s, x)), app(s, y)) -> APP(app(max, x), y)
app(app(app(sort, f), g), nil) -> nil
app(app(app(sort, f), g), app(app(cons, x), y)) -> app(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
app(app(app(app(insert, f), g), nil), y) -> app(app(cons, y), nil)
app(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> app(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y)))
app(app(max, 0), y) -> y
app(app(max, x), 0) -> x
app(app(max, app(s, x)), app(s, y)) -> app(app(max, x), y)
app(app(min, 0), y) -> 0
app(app(min, x), 0) -> 0
app(app(min, app(s, x)), app(s, y)) -> app(app(min, x), y)
app(asort, z) -> app(app(app(sort, min), max), z)
app(dsort, z) -> app(app(app(sort, max), min), z)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳A-Transformation
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Nar
APP(app(max, app(s, x)), app(s, y)) -> APP(app(max, x), y)
none
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳ATrans
...
→DP Problem 5
↳Size-Change Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Nar
MAX(s(x), s(y)) -> MAX(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳Nar
APP(app(min, app(s, x)), app(s, y)) -> APP(app(min, x), y)
app(app(app(sort, f), g), nil) -> nil
app(app(app(sort, f), g), app(app(cons, x), y)) -> app(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
app(app(app(app(insert, f), g), nil), y) -> app(app(cons, y), nil)
app(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> app(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y)))
app(app(max, 0), y) -> y
app(app(max, x), 0) -> x
app(app(max, app(s, x)), app(s, y)) -> app(app(max, x), y)
app(app(min, 0), y) -> 0
app(app(min, x), 0) -> 0
app(app(min, app(s, x)), app(s, y)) -> app(app(min, x), y)
app(asort, z) -> app(app(app(sort, min), max), z)
app(dsort, z) -> app(app(app(sort, max), min), z)
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 6
↳A-Transformation
→DP Problem 3
↳Nar
APP(app(min, app(s, x)), app(s, y)) -> APP(app(min, x), y)
none
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 6
↳ATrans
...
→DP Problem 7
↳Size-Change Principle
→DP Problem 3
↳Nar
MIN(s(x), s(y)) -> MIN(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Narrowing Transformation
APP(dsort, z) -> APP(app(app(sort, max), min), z)
APP(asort, z) -> APP(app(app(sort, min), max), z)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(g, x)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(g, x), y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(app(app(insert, f), g), z), app(app(g, x), y))
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(f, x)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(sort, f), g), y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(f, x), y)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
app(app(app(sort, f), g), nil) -> nil
app(app(app(sort, f), g), app(app(cons, x), y)) -> app(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
app(app(app(app(insert, f), g), nil), y) -> app(app(cons, y), nil)
app(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> app(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y)))
app(app(max, 0), y) -> y
app(app(max, x), 0) -> x
app(app(max, app(s, x)), app(s, y)) -> app(app(max, x), y)
app(app(min, 0), y) -> 0
app(app(min, x), 0) -> 0
app(app(min, app(s, x)), app(s, y)) -> app(app(min, x), y)
app(asort, z) -> app(app(app(sort, min), max), z)
app(dsort, z) -> app(app(app(sort, max), min), z)
innermost
two new Dependency Pairs are created:
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
APP(app(app(sort, f''), g''), app(app(cons, x), nil)) -> APP(app(app(app(insert, f''), g''), nil), x)
APP(app(app(sort, f''), g''), app(app(cons, x), app(app(cons, x''), y''))) -> APP(app(app(app(insert, f''), g''), app(app(app(app(insert, f''), g''), app(app(app(sort, f''), g''), y'')), x'')), x)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Nar
→DP Problem 8
↳Remaining Obligation(s)
APP(asort, z) -> APP(app(app(sort, min), max), z)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(g, x)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(g, x), y)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(app(app(insert, f), g), z), app(app(g, x), y))
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(f, x)
APP(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> APP(app(f, x), y)
APP(app(app(sort, f''), g''), app(app(cons, x), app(app(cons, x''), y''))) -> APP(app(app(app(insert, f''), g''), app(app(app(app(insert, f''), g''), app(app(app(sort, f''), g''), y'')), x'')), x)
APP(app(app(sort, f), g), app(app(cons, x), y)) -> APP(app(app(sort, f), g), y)
APP(dsort, z) -> APP(app(app(sort, max), min), z)
app(app(app(sort, f), g), nil) -> nil
app(app(app(sort, f), g), app(app(cons, x), y)) -> app(app(app(app(insert, f), g), app(app(app(sort, f), g), y)), x)
app(app(app(app(insert, f), g), nil), y) -> app(app(cons, y), nil)
app(app(app(app(insert, f), g), app(app(cons, x), z)), y) -> app(app(cons, app(app(f, x), y)), app(app(app(app(insert, f), g), z), app(app(g, x), y)))
app(app(max, 0), y) -> y
app(app(max, x), 0) -> x
app(app(max, app(s, x)), app(s, y)) -> app(app(max, x), y)
app(app(min, 0), y) -> 0
app(app(min, x), 0) -> 0
app(app(min, app(s, x)), app(s, y)) -> app(app(min, x), y)
app(asort, z) -> app(app(app(sort, min), max), z)
app(dsort, z) -> app(app(app(sort, max), min), z)
innermost