TIMEOUT

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (189ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (73ms), PolynomialLinearRange4iUR (2214ms), DependencyGraph (69ms), PolynomialLinearRange8NegiUR (5200ms), DependencyGraph (60ms), ReductionPairSAT (52156ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

app^#(app(times, app(s, x)), y)	→	app^#(app(plus, app(app(times, x), y)), y)		app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(fold, f), x)
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(f, y), app(app(app(fold, f), x), z))		app^#(app(plus, app(s, x)), y)	→	app^#(plus, x)
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(app(fold, f), x), z)		app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(f, y)
app^#(app(times, app(s, x)), y)	→	app^#(plus, app(app(times, x), y))		app^#(app(times, app(s, x)), y)	→	app^#(times, x)
app^#(app(plus, app(s, x)), y)	→	app^#(s, app(app(plus, x), y))		app^#(app(times, app(s, x)), y)	→	app^#(app(times, x), y)
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(fold, f)		app^#(app(plus, app(s, x)), y)	→	app^#(app(plus, x), y)

Rewrite Rules

app(app(app(fold, f), x), nil)	→	x		app(app(app(fold, f), x), app(app(cons, y), z))	→	app(app(f, y), app(app(app(fold, f), x), z))
app(app(plus, 0), y)	→	y		app(app(plus, app(s, x)), y)	→	app(s, app(app(plus, x), y))
app(app(times, 0), y)	→	0		app(app(times, app(s, x)), y)	→	app(app(plus, app(app(times, x), y)), y)
sum	→	app(app(fold, add), 0)		prod	→	app(app(fold, mul), app(s, 0))

Original Signature

Termination of terms over the following signature is verified: plus, app, 0, s, times, sum, mul, add, fold, prod, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

app^#(app(times, app(s, x)), y)	→	app^#(app(plus, app(app(times, x), y)), y)		app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(fold, f), x)
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(f, y), app(app(app(fold, f), x), z))		app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(app(app(fold, f), x), z)
app^#(app(plus, app(s, x)), y)	→	app^#(plus, x)		prod^#	→	app^#(app(fold, mul), app(s, 0))
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(f, y)		app^#(app(times, app(s, x)), y)	→	app^#(plus, app(app(times, x), y))
app^#(app(times, app(s, x)), y)	→	app^#(times, x)		app^#(app(plus, app(s, x)), y)	→	app^#(s, app(app(plus, x), y))
sum^#	→	app^#(app(fold, add), 0)		app^#(app(times, app(s, x)), y)	→	app^#(app(times, x), y)
prod^#	→	app^#(fold, mul)		prod^#	→	app^#(s, 0)
app^#(app(app(fold, f), x), app(app(cons, y), z))	→	app^#(fold, f)		sum^#	→	app^#(fold, add)
app^#(app(plus, app(s, x)), y)	→	app^#(app(plus, x), y)

Rewrite Rules

app(app(app(fold, f), x), nil)	→	x		app(app(app(fold, f), x), app(app(cons, y), z))	→	app(app(f, y), app(app(app(fold, f), x), z))
app(app(plus, 0), y)	→	y		app(app(plus, app(s, x)), y)	→	app(s, app(app(plus, x), y))
app(app(times, 0), y)	→	0		app(app(times, app(s, x)), y)	→	app(app(plus, app(app(times, x), y)), y)
sum	→	app(app(fold, add), 0)		prod	→	app(app(fold, mul), app(s, 0))

Original Signature

Termination of terms over the following signature is verified: app, plus, 0, s, times, sum, fold, add, mul, nil, cons, prod

Strategy

The following SCCs where found

app^#(app(times, app(s, x)), y) → app^#(plus, app(app(times, x), y))	app^#(app(times, app(s, x)), y) → app^#(app(plus, app(app(times, x), y)), y)
app^#(app(app(fold, f), x), app(app(cons, y), z)) → app^#(app(fold, f), x)	app^#(app(times, app(s, x)), y) → app^#(times, x)
app^#(app(plus, app(s, x)), y) → app^#(s, app(app(plus, x), y))	app^#(app(app(fold, f), x), app(app(cons, y), z)) → app^#(app(f, y), app(app(app(fold, f), x), z))
app^#(app(times, app(s, x)), y) → app^#(app(times, x), y)	app^#(app(app(fold, f), x), app(app(cons, y), z)) → app^#(app(app(fold, f), x), z)
app^#(app(app(fold, f), x), app(app(cons, y), z)) → app^#(fold, f)	app^#(app(plus, app(s, x)), y) → app^#(plus, x)
app^#(app(plus, app(s, x)), y) → app^#(app(plus, x), y)	app^#(app(app(fold, f), x), app(app(cons, y), z)) → app^#(f, y)