We consider termination of the STRS with no additional rule schemes:

  Signature: 0       :: b
             cons    :: b -> c -> c
             eq      :: b -> b -> a
             false   :: a
             hamming :: c
             if      :: a -> c -> c -> c
             list1   :: c
             list2   :: c
             list3   :: c
             lt      :: b -> b -> a
             map     :: (b -> b) -> c -> c
             merge   :: c -> c -> c
             mult    :: b -> b -> b
             nil     :: c
             plus    :: b -> b -> b
             s       :: b -> b
             true    :: a

  Rules: if(true, X, Y) -> X
         if(false, U, V) -> V
         lt(s(W), s(P)) -> lt(W, P)
         lt(0, s(X1)) -> true
         lt(Y1, 0) -> false
         eq(U1, U1) -> true
         eq(s(V1), 0) -> false
         eq(0, s(W1)) -> false
         merge(P1, nil) -> P1
         merge(nil, X2) -> X2
         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))))
         map(J2, nil) -> nil
         map(F3, cons(Y3, U3)) -> cons(F3(Y3), map(F3, U3))
         mult(0, V3) -> 0
         mult(s(W3), P3) -> plus(P3, mult(W3, P3))
         plus(0, X4) -> 0
         plus(s(Y4), U4) -> s(plus(Y4, U4))
         list1 -> map(mult(s(s(0))), hamming)
         list2 -> map(mult(s(s(s(0)))), hamming)
         list3 -> map(mult(s(s(s(s(s(0)))))), hamming)
         hamming -> cons(s(0), merge(list1, merge(list2, list3)))

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

We start by computing the initial DP problem D1 = (P1, R, i, c), where:

  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)), fresh1)
      (14) list1# => hamming#
      (15) list1# => map#(mult(s(s(0))), hamming)
      (16) list2# => mult#(s(s(s(0))), fresh1)
      (17) list2# => hamming#
      (18) list2# => map#(mult(s(s(s(0)))), hamming)
      (19) list3# => mult#(s(s(s(s(s(0))))), fresh1)
      (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 D1 = (P1, R, i, c).

We compute a graph approximation with the following edges:

  1:  1 
  2:  1 
  3:  2 3 4 5 6 7 8 
  4:
  5:  2 3 4 5 6 7 8 
  6:  2 3 4 5 6 7 8 
  7:
  8:
  9:  9 
  10: 10 11 
  11: 12 
  12: 12 
  13: 10 11 
  14: 22 23 24 25 26 
  15: 9 
  16: 10 11 
  17: 22 23 24 25 26 
  18: 9 
  19: 10 11 
  20: 22 23 24 25 26 
  21: 9 
  22: 13 14 15 
  23: 16 17 18 
  24: 19 20 21 
  25: 2 3 4 5 6 7 8 
  26: 2 3 4 5 6 7 8 

There are 6 SCCs.

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) ; D5 = (P5, R, i, c) ; D6 = (P6, R, i, c) ; D7 = (P7, R, i, c) }, where:

  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 D2 = (P2, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D3 = (P3, R, i, c).

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.

Processor output: { D8 = (P8, R, i, c) }, where:

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

***** We apply the Subterm Criterion Processor on D4 = (P4, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D5 = (P5, R, i, c).

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.

Processor output: { }.

***** We apply the Subterm Criterion Processor on D6 = (P6, R, i, c).

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.

Processor output: { }.

***** We apply the Chaining Processor Processor on D7 = (P7, R, i, c).

We chain DPs according to the following mapping:


  hamming# => hamming# | true /\ true  is obtained by chaining  hamming# => list1# and list1# => hamming#


The following DPs were deleted:

hamming# => list1#

list1# => hamming#


By chaining, we added 1 DPs and removed 2 DPs.

Processor output: { D9 = (P9, R, i, c) }, where:

  P9. (1) list2# => hamming#
      (2) list3# => hamming#
      (3) hamming# => list2#
      (4) hamming# => list3#
      (5) hamming# => hamming# | true /\ true

***** We apply the Subterm Criterion Processor on D8 = (P8, R, i, c).

We use the following projection function:

  nu(merge#) = 2

We thus have:

  (1) cons(V2, W2) |>| W2

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

Processor output: { }.

***** We apply the Chaining Processor Processor on D9 = (P9, R, i, c).

We chain DPs according to the following mapping:


  hamming# => hamming# | true /\ true  is obtained by chaining  hamming# => list2# and list2# => hamming#


The following DPs were deleted:

hamming# => list2#

list2# => hamming#


By chaining, we added 1 DPs and removed 2 DPs.

Processor output: { D10 = (P10, R, i, c) }, where:

  P10. (1) list3# => hamming#
       (2) hamming# => list3#
       (3) hamming# => hamming# | true /\ true

***** We apply the Chaining Processor Processor on D10 = (P10, R, i, c).

We chain DPs according to the following mapping:


  hamming# => hamming# | true /\ true  is obtained by chaining  hamming# => list3# and list3# => hamming#


The following DPs were deleted:

hamming# => list3#

list3# => hamming#


By chaining, we added 1 DPs and removed 2 DPs.

Processor output: { D11 = (P11, R, i, c) }, where:

  P11. (1) hamming# => hamming# | true /\ true

***** We apply the Usable Rules Processor on D11 = (P11, R, i, c).

We obtain 0 usable rules (out of 21 rules in the input problem).

Processor output: { D12 = (P11, {}, i, c) }.

***** No progress could be made on DP problem D12 = (P11, {}, i, c).