We consider termination of the LCSTRS with only rule scheme Calc:

  Signature: comp    :: ((Int -> Int) -> Int) -> (Int -> Int -> Int) -> Int -> Int
             minus   :: Int -> Int -> Int
             readint :: (Int -> Int) -> Int
             sub     :: Int

  Rules: minus(x, y) -> x - y | x = x /\ y = y
         readint(k) -> k(n) | n = n
         comp(f, g, x) -> f(g(x)) | x = x
         sub -> readint(comp(readint, minus))

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) sub# => readint#(fresh1)
      (2) sub# => minus#(fresh1, fresh2)
      (3) sub# => comp#(readint, minus, fresh1)
      (4) sub# => readint#(comp(readint, minus))

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

We compute a graph approximation with the following edges:

  1:
  2:
  3:
  4:

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

Processor output: { }.