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)

   R

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

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

• 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