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
         max(cons(x, cons(y, xs))) -> if1(x >= y, x, y, xs)
         if1(true, x, y, xs) -> max(cons(x, xs))
         if1(false, x, y, xs) -> max(cons(y, xs))
         del(x, nil) -> nil
         del(x, cons(y, xs)) -> if2(x = y, x, y, xs)
         if2(true, x, y, xs) -> xs
         if2(false, x, y, xs) -> cons(y, del(x, xs))
         sort(nil) -> nil
         sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))

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_?, f, c), where:

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

***** We apply the Graph Processor on D1 = (P1, R UNION R_?, f, 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_?, f, c) ; D3 = (P3, R UNION R_?, f, c) ; D4 = (P4, R UNION R_?, f, c) }, where:

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

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

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

***** We apply the Theory Arguments Processor on D2 = (P2, R UNION R_?, f, c).

We use the following theory arguments function:

  sort# : []

Processor output: { D5 = (P5, R UNION R_?, f, c) ; D6 = (P6, R UNION R_?, f, c) }, where:

  P5. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs)
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) { x, y }
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) { x, y }

  P6. (1) if1#(true, x, y, xs) => max#(cons(x, xs))
      (2) if1#(false, x, y, xs) => max#(cons(y, xs))

***** We apply the Subterm Criterion Processor on D3 = (P3, R UNION R_?, f, c).

We use the following projection function:

  nu(del#) = 2
  nu(if2#) = 4

We thus have:

  (1) cons(y, xs) |>|  xs
  (2) xs          |>=| xs

We may remove the strictly oriented DPs.

Processor output: { D7 = (P7, R UNION R_?, f, c) }, where:

  P7. (1) if2#(false, x, y, xs) => del#(x, xs)

***** No progress could be made on DP problem D4 = (P4, R UNION R_?, f, c).