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

  Signature: cons    :: Int -> List -> List
             fold    :: (Int -> Int -> Int) -> Int -> List -> Int
             gcd     :: Int -> Int -> Int
             gcdlist :: List -> Int
             nil     :: List

  Rules: gcd(n, m) -> gcd(-n, m) | n < 0
         gcd(n, m) -> gcd(n, -m) | m < 0
         gcd(n, 0) -> n
         gcd(n, m) -> gcd(m, n % m) | n >= 0 /\ m > 0
         fold(F, n, nil) -> n
         fold(F, n, cons(x, y)) -> F(x, fold(F, n, y))
         gcdlist(l) -> fold(gcd, 0, l)

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) gcd#(n, m) => gcd#(-n, m) | n < 0
      (2) gcd#(n, m) => gcd#(n, -m) | m < 0
      (3) gcd#(n, m) => gcd#(m, n % m) | n >= 0 /\ m > 0
      (4) fold#(F, n, cons(x, y)) => fold#(F, n, y)
      (5) gcdlist#(l) => gcd#(fresh1, fresh2)
      (6) gcdlist#(l) => fold#(gcd, 0, l)

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

We compute a graph approximation with the following edges:

  1: 2 3 
  2: 1 3 
  3: 3 
  4: 4 
  5: 1 2 3 
  6: 4 

There are 3 SCCs.

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

  P2. (1) gcd#(n, m) => gcd#(m, n % m) | n >= 0 /\ m > 0

  P3. (1) gcd#(n, m) => gcd#(-n, m) | n < 0
      (2) gcd#(n, m) => gcd#(n, -m) | m < 0

  P4. (1) fold#(F, n, cons(x, y)) => fold#(F, n, y)

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

We use the following integer mapping:

  J(gcd#) = arg_2 - 1

We thus have:

  (1) n >= 0 /\ m > 0 |= m - 1 > n % m - 1 (and m - 1 >= 0)

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

Processor output: { }.

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

We use the following theory arguments function:

  gcd# : [1]

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

  P5. (1) gcd#(n, m) => gcd#(-n, m) | n < 0
      (2) gcd#(n, m) => gcd#(n, -m) | m < 0 /\ n = n

  P6. (1) gcd#(n, m) => gcd#(n, -m) | m < 0

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

We use the following projection function:

  nu(fold#) = 3

We thus have:

  (1) cons(x, y) |>| y

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

Processor output: { }.

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

We use the following integer mapping:

  J(gcd#) = 0 - arg_1

We thus have:

  (1) n < 0          |= 0 - n >  0 - -n (and 0 - n >= 0)
  (2) m < 0 /\ n = n |= 0 - n >= 0 - n

We may remove the strictly oriented DPs, which yields:

Processor output: { D7 = (P7, R, i, c) }, where:

  P7. (1) gcd#(n, m) => gcd#(n, -m) | m < 0 /\ n = n

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

We compute a graph approximation with the following edges:

  1:

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

Processor output: { }.

***** We apply the Graph Processor on D7 = (P7, R, i, c).

We compute a graph approximation with the following edges:

  1:

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

Processor output: { }.