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)	→	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)

Original Signature

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