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

  Signature: cond :: Bool -> Int -> Int
             f91  :: Int -> Int

  Rules: f91(n) -> cond(n <= 100, n)
         cond(true, n) -> f91(f91(n + 11))
         cond(false, n) -> n - 10

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) f91#(n) => cond#(n <= 100, n)
      (2) cond#(true, n) => f91#(n + 11)
      (3) cond#(true, n) => f91#(f91(n + 11))

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

We use the following theory arguments function:

  cond# : [1, 2]
  f91#  : []

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

  P2. (1) f91#(n) => cond#(n <= 100, n)
      (2) cond#(true, n) => f91#(n + 11) | n = n
      (3) cond#(true, n) => f91#(f91(n + 11)) | n = n

  P3. (1) cond#(true, n) => f91#(n + 11)
      (2) cond#(true, n) => f91#(f91(n + 11))

***** We apply the Usable Rules Processor on D2 = (P2, R UNION R_?, i, c).

All known rules are usable, but the Usable Rules method is applicable so the extra rules are not usable, and may be dropped.

Processor output: { D4 = (P2, R, i, c) }.

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

We compute a graph approximation with the following edges:

  1:
  2:

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

Processor output: { }.

***** No progress could be made on DP problem D4 = (P2, R, i, c).