The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  P1. (1)  lt#(s(W), s(P)) => lt#(W, P)
      (2)  merge#(cons(Y2, U2), cons(V2, W2)) => lt#(Y2, V2)
      (3)  merge#(cons(Y2, U2), cons(V2, W2)) => merge#(U2, cons(V2, W2))
      (4)  merge#(cons(Y2, U2), cons(V2, W2)) => eq#(Y2, V2)
      (5)  merge#(cons(Y2, U2), cons(V2, W2)) => merge#(U2, W2)
      (6)  merge#(cons(Y2, U2), cons(V2, W2)) => merge#(cons(Y2, U2), W2)
      (7)  merge#(cons(Y2, U2), cons(V2, W2)) => if#(eq(Y2, V2), cons(Y2, merge(U2, W2)), cons(V2, merge(cons(Y2, U2), W2)))
      (8)  merge#(cons(Y2, U2), cons(V2, W2)) => if#(lt(Y2, V2), cons(Y2, merge(U2, cons(V2, W2))), if(eq(Y2, V2), cons(Y2, merge(U2, W2)), cons(V2, merge(cons(Y2, U2), W2))))
      (9)  map#(F3, cons(Y3, U3)) => map#(F3, U3)
      (10) mult#(s(W3), P3) => mult#(W3, P3)
      (11) mult#(s(W3), P3) => plus#(P3, mult(W3, P3))
      (12) plus#(s(Y4), U4) => plus#(Y4, U4)
      (13) list1# => mult#(s(s(0)), X{27})
      (14) list1# => hamming#
      (15) list1# => map#(mult(s(s(0))), hamming)
      (16) list2# => mult#(s(s(s(0))), X{28})
      (17) list2# => hamming#
      (18) list2# => map#(mult(s(s(s(0)))), hamming)
      (19) list3# => mult#(s(s(s(s(s(0))))), X{29})
      (20) list3# => hamming#
      (21) list3# => map#(mult(s(s(s(s(s(0)))))), hamming)
      (22) hamming# => list1#
      (23) hamming# => list2#
      (24) hamming# => list3#
      (25) hamming# => merge#(list2, list3)
      (26) hamming# => merge#(list1, merge(list2, list3))

***** We apply the Graph Processor on P1.

Considering the 6 SCCs, this DP problem is split into the following new problems.

  P2. (1) lt#(s(W), s(P)) => lt#(W, P)

  P3. (1) merge#(cons(Y2, U2), cons(V2, W2)) => merge#(U2, cons(V2, W2))
      (2) merge#(cons(Y2, U2), cons(V2, W2)) => merge#(U2, W2)
      (3) merge#(cons(Y2, U2), cons(V2, W2)) => merge#(cons(Y2, U2), W2)

  P4. (1) map#(F3, cons(Y3, U3)) => map#(F3, U3)

  P5. (1) plus#(s(Y4), U4) => plus#(Y4, U4)

  P6. (1) mult#(s(W3), P3) => mult#(W3, P3)

  P7. (1) list1# => hamming#
      (2) list2# => hamming#
      (3) list3# => hamming#
      (4) hamming# => list1#
      (5) hamming# => list2#
      (6) hamming# => list3#

***** We apply the Subterm Criterion Processor on P2.

We use the following projection function:

  nu(lt#) = 1

We thus have:

  (1) s(W) |>| W

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Subterm Criterion Processor on P3.

We use the following projection function:

  nu(merge#) = 1

We thus have:

  (1) cons(Y2, U2) |>|  U2
  (2) cons(Y2, U2) |>|  U2
  (3) cons(Y2, U2) |>=| cons(Y2, U2)

We may remove the strictly oriented DPs, which yields:

  P8. (1) merge#(cons(Y2, U2), cons(V2, W2)) => merge#(cons(Y2, U2), W2)

***** We apply the Subterm Criterion Processor on P4.

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(Y3, U3) |>| U3

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Subterm Criterion Processor on P5.

We use the following projection function:

  nu(plus#) = 1

We thus have:

  (1) s(Y4) |>| Y4

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** We apply the Subterm Criterion Processor on P6.

We use the following projection function:

  nu(mult#) = 1

We thus have:

  (1) s(W3) |>| W3

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

***** No progress could be made on DP problem P7.