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

  Signature: cond1  :: Bool -> Int -> o -> o
             cond2  :: Bool -> Int -> o -> o
             cons   :: Int -> o -> o
             if     :: Bool -> Int -> Int -> Int
             max    :: o -> Int
             member :: Int -> o -> Bool
             nil    :: o
             sort   :: o -> o
             st     :: Int -> o -> o
             stNat  :: Bool -> Int -> o -> o

  Rules: sort(l) -> st(0, l)
         st(n, l) -> stNat(n >= 0, n, l)
         stNat(true, n, l) -> cond1(member(n, l), n, l)
         cond1(true, n, l) -> cons(n, st(n + 1, l))
         cond1(false, n, l) -> cond2(n > max(l), n, l)
         cond2(true, n, l) -> nil
         cond2(false, n, l) -> st(n + 1, l)
         member(n, nil) -> false
         member(n, cons(m, l)) -> n = m \/ member(n, l)
         max(nil) -> 0
         max(cons(u, l)) -> if(u > max(l), u, max(l))
         if(true, u, v) -> u
         if(false, u, v) -> v

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

  P1. (1)  sort#(l) => st#(0, l)
      (2)  st#(n, l) => stNat#(n >= 0, n, l)
      (3)  stNat#(true, n, l) => member#(n, l)
      (4)  stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (5)  cond1#(true, n, l) => st#(n + 1, l)
      (6)  cond1#(false, n, l) => max#(l)
      (7)  cond1#(false, n, l) => cond2#(n > max(l), n, l)
      (8)  cond2#(false, n, l) => st#(n + 1, l)
      (9)  member#(n, cons(m, l)) => member#(n, l)
      (10) max#(cons(u, l)) => max#(l)
      (11) max#(cons(u, l)) => max#(l)
      (12) max#(cons(u, l)) => if#(u > max(l), u, max(l))

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

We compute a graph approximation with the following edges:

  1:  2 
  2:  3 4 
  3:  9 
  4:  5 6 7 
  5:  2 
  6:  10 11 12 
  7:
  8:  2 
  9:  9 
  10: 10 11 12 
  11: 10 11 12 
  12:

There are 3 SCCs.

Processor output: { D2 = (P2, R, f, c) ; D3 = (P3, R, f, c) ; D4 = (P4, R, f, c) }, where:

  P2. (1) member#(n, cons(m, l)) => member#(n, l)

  P3. (1) max#(cons(u, l)) => max#(l)
      (2) max#(cons(u, l)) => max#(l)

  P4. (1) st#(n, l) => stNat#(n >= 0, n, l)
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (3) cond1#(true, n, l) => st#(n + 1, l)

***** We apply the Subterm Criterion Processor on D2 = (P2, R, f, c).

We use the following projection function:

  nu(member#) = 2

We thus have:

  (1) cons(m, l) |>| l

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

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

We use the following projection function:

  nu(max#) = 1

We thus have:

  (1) cons(u, l) |>| l
  (2) cons(u, l) |>| l

All DPs are strictly oriented, and may be removed.  Hence, this DP problem is finite.

Processor output: { }.

***** We apply the Theory Arguments Processor on D4 = (P4, R, f, c).

We use the following theory arguments function:

  cond1# : [2]
  st#    : [1]
  stNat# : [1, 2]

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

  P5. (1) st#(n, l) => stNat#(n >= 0, n, l)
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l) { n }
      (3) cond1#(true, n, l) => st#(n + 1, l) { n }

  P6. (1) stNat#(true, n, l) => cond1#(member(n, l), n, l)
      (2) cond1#(true, n, l) => st#(n + 1, l)

***** We apply the Theory Arguments Processor on D5 = (P5, R, f, c).

We use the following theory arguments function:

  cond1# : [2]
  st#    : [1]
  stNat# : [1, 2]

Processor output: { D7 = (P7, R, f, c) ; D8 = (P8, R, f, c) }, where:

  P7. (1) st#(n, l) => stNat#(n >= 0, n, l) { n }
      (2) stNat#(true, n, l) => cond1#(member(n, l), n, l) { n }
      (3) cond1#(true, n, l) => st#(n + 1, l) { n }

  P8. (1) st#(n, l) => stNat#(n >= 0, n, l)

***** We apply the Graph Processor on D6 = (P6, R, f, c).

We compute a graph approximation with the following edges:

  1: 2 
  2:

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

Processor output: { }.

***** No progress could be made on DP problem D7 = (P7, R, f, c).