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

↳Polo

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

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

↳Polo

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polynomial Ordering

→DP Problem 3

↳Polo

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

The following dependency pair can be strictly oriented:

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

There are no usable rules 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

↳Polo

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

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polynomial Ordering

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

The following dependency pair can be strictly oriented:

MSORT(.(x,y)) -> MSORT(del(min(x,y), .(x,y)))

Additionally, the following usable rules w.r.t. to the implicit AFS can be oriented:

del(x, nil) -> nil

del(x, .(y,z)) -> if(=(x,y),z, .(y, del(x,z)))

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(if(x)_{1}, x_{2}, x_{3})= 0 _{ }^{ }_{ }^{ }POL(MSORT(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(=(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(min(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(.(x)_{1}, x_{2})= 1 _{ }^{ }_{ }^{ }POL(del(x)_{1}, x_{2})= 0 _{ }^{ }_{ }^{ }POL(<=(x)_{1}, x_{2})= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 3

↳Polo

→DP Problem 6

↳Dependency Graph

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

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes