YES
(VAR f x)
(RULES 
app(app(F,app(app(F,f),x)),x) -> app(app(F,app(G,app(app(F,f),x))),app(f,x))
)

Proving termination of rewriting for Ex6_11:

-> Dependency pairs:
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,app(G,app(app(F,f),x))),app(f,x))
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(F,app(G,app(app(F,f),x)))
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(G,app(app(F,f),x))
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,f),x)
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(F,f)
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(f,x)

-> Proof of termination for Ex6_11_1:
-> -> Dependency pairs in cycle:
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,app(G,app(app(F,f),x))),app(f,x))
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(f,x)
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,f),x)

UsableRules:
app(app(F,app(app(F,f),x)),x) -> app(app(F,app(G,app(app(F,f),x))),app(f,x))

Polynomial Interpretation:

[app](X1,X2) = 4.X1 + 1/2.X2
[F] = 4
[G] = 0
[nF_app](X1,X2) = 4.X1

TIME: 3.1681e-2

-> -> Dependency pairs in cycle:
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,app(G,app(app(F,f),x))),app(f,x))
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(f,x)

UsableRules:
app(app(F,app(app(F,f),x)),x) -> app(app(F,app(G,app(app(F,f),x))),app(f,x))

Polynomial Interpretation:

[app](X1,X2) = 4.X1 + 1/2.X2
[F] = 4
[G] = 0
[nF_app](X1,X2) = 4.X1

TIME: 3.2e-4

-> -> Dependency pairs in cycle:
nF_app(app(F,app(app(F,f),x)),x) -> nF_app(app(F,app(G,app(app(F,f),x))),app(f,x))

UsableRules:
app(app(F,app(app(F,f),x)),x) -> app(app(F,app(G,app(app(F,f),x))),app(f,x))

Polynomial Interpretation:

[app](X1,X2) = 4.X1 + 1/2.X2
[F] = 4
[G] = 0
[nF_app](X1,X2) = 4.X1

TIME: 3.73e-4


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 4
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.