R
↳Dependency Pair Analysis
MSORT(.(x, y)) > MIN(x, y)
MSORT(.(x, y)) > MSORT(del(min(x, y), .(x, y)))
MSORT(.(x, y)) > DEL(min(x, y), .(x, y))
MIN(x, .(y, z)) > MIN(x, z)
MIN(x, .(y, z)) > MIN(y, z)
DEL(x, .(y, z)) > DEL(x, z)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
MIN(x, .(y, z)) > MIN(y, z)
MIN(x, .(y, z)) > MIN(x, z)
msort(nil) > nil
msort(.(x, y)) > .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) > x
min(x, .(y, z)) > if(<=(x, y), min(x, z), min(y, z))
del(x, nil) > nil
del(x, .(y, z)) > if(=(x, y), z, .(y, del(x, z)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
MIN(x, .(y, z)) > MIN(y, z)
MIN(x, .(y, z)) > MIN(x, z)
none
innermost




trivial
.(x_{1}, x_{2}) > .(x_{1}, x_{2})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
DEL(x, .(y, z)) > DEL(x, z)
msort(nil) > nil
msort(.(x, y)) > .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) > x
min(x, .(y, z)) > if(<=(x, y), min(x, z), min(y, z))
del(x, nil) > nil
del(x, .(y, z)) > if(=(x, y), z, .(y, del(x, z)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳SizeChange Principle
→DP Problem 3
↳UsableRules
DEL(x, .(y, z)) > DEL(x, z)
none
innermost


trivial
.(x_{1}, x_{2}) > .(x_{1}, x_{2})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
MSORT(.(x, y)) > MSORT(del(min(x, y), .(x, y)))
msort(nil) > nil
msort(.(x, y)) > .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) > x
min(x, .(y, z)) > if(<=(x, y), min(x, z), min(y, z))
del(x, nil) > nil
del(x, .(y, z)) > if(=(x, y), z, .(y, del(x, z)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Rewriting Transformation
MSORT(.(x, y)) > MSORT(del(min(x, y), .(x, y)))
min(x, nil) > x
min(x, .(y, z)) > if(<=(x, y), min(x, z), min(y, z))
del(x, .(y, z)) > if(=(x, y), z, .(y, del(x, z)))
del(x, nil) > nil
innermost
one new Dependency Pair is created:
MSORT(.(x, y)) > MSORT(del(min(x, y), .(x, y)))
MSORT(.(x, y)) > MSORT(if(=(min(x, y), x), y, .(x, del(min(x, y), y))))