We consider universal computability of the STRS with no additional rule schemes:

  Signature: 0     :: nat
             apply :: nat -> nat -> nat
             avg   :: nat -> nat -> nat
             check :: nat -> nat
             fun   :: (nat -> nat) -> nat
             s     :: nat -> nat

  Rules: avg(s(X), Y) -> avg(X, s(Y))
         avg(U, s(s(s(V)))) -> s(avg(s(U), V))
         avg(0, 0) -> 0
         avg(0, s(0)) -> 0
         avg(0, s(s(0))) -> s(0)
         apply(fun(I), P) -> I(check(P))
         check(s(X1)) -> s(check(X1))
         check(0) -> 0

The system does not satisfy the preconditions to apply static dependency pairs: it is not accessible function passing.