We consider termination 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, 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, i, c).

We use the following theory arguments function:

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

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, 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))

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