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

  Signature: cons :: Int -> o -> o
             del  :: Int -> o -> o
             if1  :: Bool -> Int -> Int -> o -> Int
             if2  :: Bool -> Int -> Int -> o -> o
             max  :: o -> Int
             nil  :: o
             sort :: o -> o

  Rules: max(nil) -> 0
         max(cons(x, nil)) -> x | x = x
         max(cons(x, cons(y, xs))) -> if1(x >= y, x, y, xs) | x = x /\ y = y
         if1(true, x, y, xs) -> max(cons(x, xs)) | x = x /\ y = y
         if1(false, x, y, xs) -> max(cons(y, xs)) | x = x /\ y = y
         del(x, nil) -> nil | x = x
         del(x, cons(y, xs)) -> if2(x = y, x, y, xs) | x = x /\ y = y
         if2(true, x, y, xs) -> xs | x = x /\ y = y
         if2(false, x, y, xs) -> cons(y, del(x, xs)) | x = x /\ y = y
         sort(nil) -> nil
         sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs)))) | x = x

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) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs) | x = x /\ y = y
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) | x = x /\ y = y
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) | x = x /\ y = y
      (4) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs) | x = x /\ y = y
      (5) if2#(false, x, y, xs) => del#(x, xs) | x = x /\ y = y
      (6) sort#(cons(x, xs)) => max#(cons(x, xs)) | x = x
      (7) sort#(cons(x, xs)) => max#(cons(x, xs)) | x = x
      (8) sort#(cons(x, xs)) => del#(max(cons(x, xs)), cons(x, xs)) | x = x
      (9) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs))) | x = x

***** 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: 1 
  4: 5 
  5: 4 
  6: 1 
  7: 1 
  8: 4 
  9: 6 7 8 9 

There are 3 SCCs.

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

  P2. (1) max#(cons(x, cons(y, xs))) => if1#(x >= y, x, y, xs) | x = x /\ y = y
      (2) if1#(true, x, y, xs) => max#(cons(x, xs)) | x = x /\ y = y
      (3) if1#(false, x, y, xs) => max#(cons(y, xs)) | x = x /\ y = y

  P3. (1) del#(x, cons(y, xs)) => if2#(x = y, x, y, xs) | x = x /\ y = y
      (2) if2#(false, x, y, xs) => del#(x, xs) | x = x /\ y = y

  P4. (1) sort#(cons(x, xs)) => sort#(del(max(cons(x, xs)), cons(x, xs))) | x = x

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

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

Processor output: { D5 = (P2, {}, i, c) }.

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

We use the following projection function:

  nu(del#) = 2
  nu(if2#) = 4

We thus have:

  (1) cons(y, xs) |>|  xs
  (2) xs          |>=| xs

We may remove the strictly oriented DPs.

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

  P5. (1) if2#(false, x, y, xs) => del#(x, xs) | x = x /\ y = y

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

We obtain 9 usable rules (out of 11 rules in the input problem).

Processor output: { D7 = (P4, R2, i, c) }, where:

  R2. (1) del(x, nil) -> nil | x = x
      (2) del(x, cons(y, xs)) -> if2(x = y, x, y, xs) | x = x /\ y = y
      (3) if1(true, x, y, xs) -> max(cons(x, xs)) | x = x /\ y = y
      (4) if1(false, x, y, xs) -> max(cons(y, xs)) | x = x /\ y = y
      (5) if2(true, x, y, xs) -> xs | x = x /\ y = y
      (6) if2(false, x, y, xs) -> cons(y, del(x, xs)) | x = x /\ y = y
      (7) max(nil) -> 0
      (8) max(cons(x, nil)) -> x | x = x
      (9) max(cons(x, cons(y, xs))) -> if1(x >= y, x, y, xs) | x = x /\ y = y

***** We apply the Usable rules with respect to an argument wiltering [with HORPO] Processor on D5 = (P2, {}, i, c).

Constrained HORPO yields:

  max#1(cons2(x, cons2(y, xs))) (>) if1#4(x >= y, x, y, xs) | x = x /\ y = y
  if1#4(true, x, y, xs) (>) max#1(cons2(x, xs)) | x = x /\ y = y
  if1#4(false, x, y, xs) (>) max#1(cons2(y, xs)) | x = x /\ y = y

We do this using the following settings:

* Disregarded arguments:

  cons2 1 
  if1#4 2 

* Precedence and permutation:

    cons2  { 2 }
  = if1#4  { 4 } 1 _ 3
  > max#1  { 1 }

* Well-founded theory orderings:

  [>]_{Bool} = {(true,false)}
  [>]_{Int}  = {(x,y) | x < 1000 /\ x < y }

Processor output: { }.

***** We apply the Graph Processor on D6 = (P5, 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: { }.

***** No progress could be made on DP problem D7 = (P4, R2, i, c).