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

  Signature: cons   :: Int -> list -> list
             fold   :: Int -> (Int -> Int -> Int) -> list -> Int
             init   :: Int -> list
             map    :: (Int -> Int) -> list -> list
             nil    :: list
             sumfun :: (Int -> Int) -> Int -> Int

  Rules: sumfun(F, x) -> F(x) | x <= 0
         sumfun(F, x) -> F(x) + sumfun(F, x - 1) | x > 0
         fold(v, G, nil) -> v | v = v
         fold(v, G, cons(h, t)) -> fold(G(v, h), G, t) | v = v /\ h = h
         map(F, nil) -> nil
         map(F, cons(h, t)) -> cons(F(H), map(F, t)) | h = h /\ H = H
         init(n) -> nil | n < 0
         init(n) -> cons(n, init(n - 1)) | n >= 0
         sumfun(F, n) -> fold(0 + F(n), [+], map(F, init(n - 1))) | n >= 0
         x + fold(y, [+], z) -> fold(a, [+], z) | a = x + y

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)  sumfun#(F, x) => +#(x, -1) | x > 0
      (2)  sumfun#(F, x) => sumfun#(F, x - 1) | x > 0
      (3)  sumfun#(F, x) => +#(F(x), sumfun(F, x - 1)) | x > 0
      (4)  fold#(v, G, cons(h, t)) => fold#(G(v, h), G, t) | v = v /\ h = h
      (5)  map#(F, cons(h, t)) => map#(F, t) | h = h /\ H = H
      (6)  init#(n) => +#(n, -1) | n >= 0
      (7)  init#(n) => init#(n - 1) | n >= 0
      (8)  sumfun#(F, n) => +#(0, F(n)) | n >= 0
      (9)  sumfun#(F, n) => +#(fresh1, fresh2) | n >= 0
      (10) sumfun#(F, n) => +#(n, -1) | n >= 0
      (11) sumfun#(F, n) => init#(n - 1) | n >= 0
      (12) sumfun#(F, n) => map#(F, init(n - 1)) | n >= 0
      (13) sumfun#(F, n) => fold#(0 + F(n), [+], map(F, init(n - 1))) | n >= 0
      (14) +#(x, fold(y, [+], z)) => +#(fresh1, fresh2) | a = x + y
      (15) +#(x, fold(y, [+], z)) => fold#(a, [+], z) | a = x + y

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

We compute a graph approximation with the following edges:

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

There are 5 SCCs.

Processor output: { D2 = (P2, R, i, c) ; D3 = (P3, R, i, c) ; D4 = (P4, R, i, c) ; D5 = (P5, R, i, c) ; D6 = (P6, R, i, c) }, where:

  P2. (1) fold#(v, G, cons(h, t)) => fold#(G(v, h), G, t) | v = v /\ h = h

  P3. (1) +#(x, fold(y, [+], z)) => +#(fresh1, fresh2) | a = x + y

  P4. (1) init#(n) => init#(n - 1) | n >= 0

  P5. (1) map#(F, cons(h, t)) => map#(F, t) | h = h /\ H = H

  P6. (1) sumfun#(F, x) => sumfun#(F, x - 1) | x > 0

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

We use the following projection function:

  nu(fold#) = 3

We thus have:

  (1) cons(h, t) |>| t

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

Processor output: { }.

***** We apply the Usable Rules Processor on D3 = (P3, R, i, c).

We obtain 0 usable rules (out of 10 rules in the input problem).

Processor output: { D7 = (P3, {}, i, c) }.

***** We apply the Integer Function Processor on D4 = (P4, R, i, c).

We use the following integer mapping:

  J(init#) = arg_1 + 1

We thus have:

  (1) n >= 0 |= n + 1 > n - 1 + 1 (and n + 1 >= 0)

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

Processor output: { }.

***** We apply the Subterm Criterion Processor on D5 = (P5, R, i, c).

We use the following projection function:

  nu(map#) = 2

We thus have:

  (1) cons(h, t) |>| t

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

Processor output: { }.

***** We apply the Integer Function Processor on D6 = (P6, R, i, c).

We use the following integer mapping:

  J(sumfun#) = arg_2

We thus have:

  (1) x > 0 |= x > x - 1 (and x >= 0)

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

Processor output: { }.

***** No progress could be made on DP problem D7 = (P3, {}, i, c).