We consider termination of the STRS with no additional rule schemes:

  Signature: 0     :: nat
             find0 :: (nat -> nat) -> nat -> nat -> nat
             if    :: nat -> nat -> nat -> nat
             min   :: nat -> nat -> nat
             nul   :: (nat -> nat) -> nat -> nat
             s     :: nat -> nat

  Rules: min(s(X), s(Y)) -> min(X, Y)
         min(X, 0) -> 0
         min(0, X) -> 0
         min(nul(F, Y), Z) -> nul(F, min(Y, Z))
         nul(F, X) -> find0(F, 0, X)
         find0(F, X, 0) -> X
         find0(F, X, s(Y)) -> if(F(X), find0(F, s(X), Y), X)
         if(s(Z), X, Y) -> X
         if(0, X, Y) -> Y

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

No HORPO proof could be found.