msort(nil) -> nil

msort(.(

min(

min(

del(

del(

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)

Furthermore,

R

↳DPs

→DP Problem 1

↳Polynomial Ordering

→DP Problem 2

↳Polo

→DP Problem 3

↳Rw

**MIN( x, .(y, z)) -> MIN(y, 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

The following dependency pairs can be strictly oriented:

MIN(x, .(y,z)) -> MIN(y,z)

MIN(x, .(y,z)) -> MIN(x,z)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(MIN(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(.(x)_{1}, x_{2})= 1 + x _{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 4

↳Dependency Graph

→DP Problem 2

↳Polo

→DP Problem 3

↳Rw

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polynomial Ordering

→DP Problem 3

↳Rw

**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

The following dependency pair can be strictly oriented:

DEL(x, .(y,z)) -> DEL(x,z)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(DEL(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(.(x)_{1}, x_{2})= 1 + x _{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 5

↳Dependency Graph

→DP Problem 3

↳Rw

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Rewriting Transformation

**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

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

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))))

The transformation is resulting in no new DP problems.

Duration:

0:00 minutes