MAYBE MAYBE TRS: { app(app(F(), app(app(F(), f), x)), x) -> app(app(F(), app(G(), app(app(F(), f), x))), app(f, x)) } DUP: We consider a duplicating system. Trs: { app(app(F(), app(app(F(), f), x)), x) -> app(app(F(), app(G(), app(app(F(), f), x))), app(f, x)) } Fail