MAYBE

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (30ms), SubtermCriterion (1ms), DependencyGraph (13ms), PolynomialLinearRange4iUR (704ms), DependencyGraph (16ms), PolynomialLinearRange8NegiUR (2098ms), DependencyGraph (8ms), ReductionPairSAT (13642ms), DependencyGraph (31ms), SizeChangePrinciple (15ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app^#(app(rec, h), app(g, app(s, x)))	→	app^#(rec, h)		app^#(app(rec, h), app(g, app(s, x)))	→	app^#(app(rec, h), app(g, x))
app^#(app(rec, h), app(g, app(s, x)))	→	app^#(h, x)		app^#(app(rec, h), app(g, app(s, x)))	→	app^#(g, x)
app^#(app(rec, h), app(g, app(s, x)))	→	app^#(app(h, x), app(app(rec, h), app(g, x)))

Rewrite Rules

app(app(rec, h), app(g, 0))

→

g

app(app(rec, h), app(g, app(s, x)))

→

app(app(h, x), app(app(rec, h), app(g, x)))

Original Signature

Termination of terms over the following signature is verified: app, rec, 0, s