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

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

**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 AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

Used Argument Filtering System:

MIN(x,_{1}x) -> MIN(_{2}x,_{1}x)_{2}

.(x,_{1}x) -> .(_{2}x,_{1}x)_{2}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 4

↳Dependency Graph

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

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

↳AFS

→DP Problem 2

↳Argument Filtering and Ordering

→DP Problem 3

↳AFS

**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 AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

Used Argument Filtering System:

DEL(x,_{1}x) -> DEL(_{2}x,_{1}x)_{2}

.(x,_{1}x) -> .(_{2}x,_{1}x)_{2}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 5

↳Dependency Graph

→DP Problem 3

↳AFS

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

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳Argument Filtering and 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)))

The following usable rules w.r.t. to the AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

Used Argument Filtering System:

MSORT(x) -> MSORT(_{1}x)_{1}

.(x,_{1}x) -> .(_{2}x,_{1}x)_{2}

del(x,_{1}x) ->_{2}x_{1}

min(x,_{1}x) -> min(_{2}x,_{1}x)_{2}

if(x,_{1}x,_{2}x) ->_{3}x_{1}

<=(x,_{1}x) -> <=(_{2}x,_{1}x)_{2}

=(x,_{1}x) ->_{2}x_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→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