MAYBE

The TRS could not be proven terminating. The proof attempt took 5190 ms.

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (37ms), SubtermCriterion (1ms), DependencyGraph (12ms), PolynomialLinearRange4iUR (590ms), DependencyGraph (11ms), PolynomialLinearRange8NegiUR (1428ms), DependencyGraph (10ms), ReductionPairSAT (2910ms), DependencyGraph (10ms), SizeChangePrinciple (15ms)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

app#(app(fix, f), x)app#(fix, f)app#(app(app(subst, f), g), x)app#(g, x)
app#(app(app(subst, f), g), x)app#(app(f, x), app(g, x))app#(app(fix, f), x)app#(app(f, app(fix, f)), x)
app#(app(fix, f), x)app#(f, app(fix, f))app#(app(app(subst, f), g), x)app#(f, x)

Rewrite Rules

app(app(const, x), y)xapp(app(app(subst, f), g), x)app(app(f, x), app(g, x))
app(app(fix, f), x)app(app(f, app(fix, f)), x)

Original Signature

Termination of terms over the following signature is verified: app, const, fix, subst