merge(nil,

merge(

merge(.(

++(nil,

++(.(

if(true,

if(false,

R

↳Dependency Pair Analysis

MERGE(.(x,y), .(u,v)) -> IF(< (x,u), .(x, merge(y, .(u,v))), .(u, merge(.(x,y),v)))

MERGE(.(x,y), .(u,v)) -> MERGE(y, .(u,v))

MERGE(.(x,y), .(u,v)) -> MERGE(.(x,y),v)

++'(.(x,y),z) -> ++'(y,z)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****MERGE(.(***x*,*y*), .(*u*,*v*)) -> MERGE(.(*x*,*y*),*v*)**MERGE(.(***x*,*y*), .(*u*,*v*)) -> MERGE(*y*, .(*u*,*v*))**Rules:**

merge(nil,*y*) ->*y*

merge(*x*, nil) ->*x*

merge(.(*x*,*y*), .(*u*,*v*)) -> if(< (*x*,*u*), .(*x*, merge(*y*, .(*u*,*v*))), .(*u*, merge(.(*x*,*y*),*v*)))

++(nil,*y*) ->*y*

++(.(*x*,*y*),*z*) -> .(*x*, ++(*y*,*z*))

if(true,*x*,*y*) ->*x*

if(false,*x*,*y*) ->*x***Dependency Pair:****++'(.(***x*,*y*),*z*) -> ++'(*y*,*z*)**Rules:**

merge(nil,*y*) ->*y*

merge(*x*, nil) ->*x*

merge(.(*x*,*y*), .(*u*,*v*)) -> if(< (*x*,*u*), .(*x*, merge(*y*, .(*u*,*v*))), .(*u*, merge(.(*x*,*y*),*v*)))

++(nil,*y*) ->*y*

++(.(*x*,*y*),*z*) -> .(*x*, ++(*y*,*z*))

if(true,*x*,*y*) ->*x*

if(false,*x*,*y*) ->*x*

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****MERGE(.(***x*,*y*), .(*u*,*v*)) -> MERGE(.(*x*,*y*),*v*)**MERGE(.(***x*,*y*), .(*u*,*v*)) -> MERGE(*y*, .(*u*,*v*))**Rules:**

merge(nil,*y*) ->*y*

merge(*x*, nil) ->*x*

merge(.(*x*,*y*), .(*u*,*v*)) -> if(< (*x*,*u*), .(*x*, merge(*y*, .(*u*,*v*))), .(*u*, merge(.(*x*,*y*),*v*)))

++(nil,*y*) ->*y*

++(.(*x*,*y*),*z*) -> .(*x*, ++(*y*,*z*))

if(true,*x*,*y*) ->*x*

if(false,*x*,*y*) ->*x***Dependency Pair:****++'(.(***x*,*y*),*z*) -> ++'(*y*,*z*)**Rules:**

merge(nil,*y*) ->*y*

merge(*x*, nil) ->*x*

merge(.(*x*,*y*), .(*u*,*v*)) -> if(< (*x*,*u*), .(*x*, merge(*y*, .(*u*,*v*))), .(*u*, merge(.(*x*,*y*),*v*)))

++(nil,*y*) ->*y*

++(.(*x*,*y*),*z*) -> .(*x*, ++(*y*,*z*))

if(true,*x*,*y*) ->*x*

if(false,*x*,*y*) ->*x*

Duration:

0:00 minutes