We consider universal computability of the LCSTRS with only rule scheme Calc:

  Signature: complist :: funlist -> Int -> Int
             fcons    :: (Int -> Int) -> funlist -> funlist
             fnil     :: funlist

  Rules: complist(nil, x) -> x | x = x
         complist(fcons(F, t), x) -> complist(t, F(x)) | x = x

The system is accessible function passing by a sort ordering with funlist ≻ Int.

We start by computing the initial DP problem D1 = (P1, R UNION R_?, i, c), where:

  P1. (1) complist#(fcons(F, t), x) => complist#(t, F(x)) | x = x

***** We apply the Subterm Criterion Processor on D1 = (P1, R UNION R_?, i, c).

We use the following projection function:

  nu(complist#) = 1

We thus have:

  (1) fcons(F, t) |>| t

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

Processor output: { }.