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

↳Remaining

**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: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

MIN(x,_{1}x) ->_{2}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

↳Remaining

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

↳Remaining

**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: Homeomorphic Embedding Order with EMB

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

↳Remaining

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

↳Remaining Obligation(s)

The following remains to be proven:

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

Duration:

0:00 minutes