We consider universal computability of the LCTRS with only rule scheme Calc:

  Signature: cons :: Int -> o -> o
             del  :: Int -> o -> o
             if1  :: Bool -> Int -> Int -> o -> Int
             if2  :: Bool -> Int -> Int -> o -> o
             max  :: o -> Int
             nil  :: o
             sort :: o -> o

  Rules: max(nil) -> 0
         max(cons(x, nil)) -> x | x = x
         max(cons(x, cons(y, xs))) -> if1(x >= y, x, y, xs) | x = x /\ y = y
         if1(true, x, y, xs) -> max(cons(x, xs)) | x = x /\ y = y
         if1(false, x, y, xs) -> max(cons(y, xs)) | x = x /\ y = y
         del(x, nil) -> nil | x = x
         del(x, cons(y, xs)) -> if2(x = y, x, y, xs) | x = x /\ y = y
         if2(true, x, y, xs) -> xs | x = x /\ y = y
         if2(false, x, y, xs) -> cons(y, del(x, xs)) | x = x /\ y = y
         sort(nil) -> nil
         sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs)))) | x = x

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 UNION R_?, i, c), where:

  P1. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs) | x = x /\ y = y
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) | x = x /\ y = y
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) | x = x /\ y = y
      (4) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs) | x = x /\ y = y
      (5) if2#(false, x, y, xs) => del#(x, xs) | x = x /\ y = y
      (6) sort#(cons(x, xs)) => max#(cons(x, xs)) | x = x
      (7) sort#(cons(x, xs)) => max#(cons(x, xs)) | x = x
      (8) sort#(cons(x, xs)) => del#(max(cons(x, xs)), cons(x, xs)) | x = x
      (9) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs))) | x = x

***** We apply the Graph Processor on D1 = (P1, R UNION R_?, i, c).

We compute a graph approximation with the following edges:

  1: 2 3 
  2: 1 
  3: 1 
  4: 5 
  5: 4 
  6: 1 
  7: 1 
  8: 4 
  9: 6 7 8 9 

There are 3 SCCs.

Processor output: { D2 = (P2, R UNION R_?, i, c) ; D3 = (P3, R UNION R_?, i, c) ; D4 = (P4, R UNION R_?, i, c) }, where:

  P2. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs) | x = x /\ y = y
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) | x = x /\ y = y
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) | x = x /\ y = y

  P3. (1) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs) | x = x /\ y = y
      (2) if2#(false, x, y, xs) => del#(x, xs) | x = x /\ y = y

  P4. (1) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs))) | x = x

***** No progress could be made on DP problem D2 = (P2, R UNION R_?, i, c).