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

  Signature: branch :: a -> b -> b -> b
             leaf   :: a -> b
             mapbt  :: (a -> a) -> b -> b

  Rules: mapbt(F, leaf(Y)) -> leaf(F(Y))
         mapbt(G, branch(P, V, W)) -> branch(G(P), mapbt(G, V), mapbt(G, W))

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, f, c), where:

  P1. (1) mapbt#(G, branch(P, V, W)) => mapbt#(G, V)
      (2) mapbt#(G, branch(P, V, W)) => mapbt#(G, W)

***** We apply the Subterm Criterion Processor on D1 = (P1, R, f, c).

We use the following projection function:

  nu(mapbt#) = 2

We thus have:

  (1) branch(P, V, W) |>| V
  (2) branch(P, V, W) |>| W

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

Processor output: { }.