The system is accessible function passing by a sort ordering that equates all sorts. We start by computing the following initial DP problem: 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 P1. 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.