YES TRS: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) max/plus interpretations on N: app_A(x1,x2) = max{7, 22 + x1, -4 + x2} app#_A(x1,x2) = max{7, -2 + x1, 7} F_A = 1 F#_A = 6 G_A = 8 G#_A = 0 precedence: app > F > G