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

  Signature: 0@z      :: Int
             1@z      :: Int
             Cond_b14 :: Bool -> Int -> Int -> Int -> o
             b10      :: Int -> Int -> Int -> o
             b14      :: Int -> Int -> Int -> o
             b15      :: Int -> Int -> Int -> o

  Rules: b10(sv14_14, sv23_37, sv24_38) -> b14(sv14_14, sv23_37, sv24_38)
         Cond_b14(true, sv14_14, sv23_37, sv24_38) -> b15(sv14_14, sv23_37, sv24_38)
         b14(sv14_14, sv23_37, sv24_38) -> Cond_b14(sv23_37 >= sv14_14 /\ 1@z < sv14_14 /\ 0@z < sv24_38 /\ 1@z < sv23_37, sv14_14, sv23_37, sv24_38)
         b15(sv14_14, sv23_37, sv24_38) -> b10(sv14_14, sv23_37 - sv14_14, sv24_38 + 1@z)

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) b10#(sv14_14, sv23_37, sv24_38) => b14#(sv14_14, sv23_37, sv24_38)
      (2) Cond_b14#(true, sv14_14, sv23_37, sv24_38) => b15#(sv14_14, sv23_37, sv24_38)
      (3) b14#(sv14_14, sv23_37, sv24_38) => Cond_b14#(sv23_37 >= sv14_14 /\ 1@z < sv14_14 /\ 0@z < sv24_38 /\ 1@z < sv23_37, sv14_14, sv23_37, sv24_38)
      (4) b15#(sv14_14, sv23_37, sv24_38) => b10#(sv14_14, sv23_37 - sv14_14, sv24_38 + 1@z)

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

We compute a graph approximation with the following edges:

  1: 3 
  2: 4 
  3:
  4: 1 

As there are no SCCs, this DP problem is removed.

Processor output: { }.