TIMEOUT

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (214ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (66ms), PolynomialLinearRange4iUR (1866ms), DependencyGraph (64ms), PolynomialLinearRange8NegiUR (5361ms), DependencyGraph (98ms), ReductionPairSAT (52287ms)].

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(map, f), app(app(cons, x), xs))	→	app^#(app(cons, app(f, x)), app(app(map, f), xs))
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(f, x)		app^#(app(plus, app(s, x)), y)	→	app^#(plus, x)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(app(map, f), xs)		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(plus, app(s, x)), y)	→	app^#(app(plus, x), y)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(map, f)		app^#(app(map, f), app(app(cons, x), xs))	→	app^#(cons, app(f, x))

Rewrite Rules

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)
app(app(map, f), nil)	→	nil		app(app(map, f), app(app(cons, x), xs))	→	app(app(cons, app(f, x)), app(app(map, f), xs))
inc	→	app(map, app(plus, app(s, 0)))		double	→	app(map, app(times, app(s, app(s, 0))))

Original Signature

Termination of terms over the following signature is verified: plus, app, 0, inc, s, times, map, double, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

inc^#	→	app^#(s, 0)		inc^#	→	app^#(map, app(plus, app(s, 0)))
app^#(app(times, app(s, x)), y)	→	app^#(app(plus, app(app(times, x), y)), y)		app^#(app(map, f), app(app(cons, x), xs))	→	app^#(app(cons, app(f, x)), app(app(map, f), xs))
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(f, x)		inc^#	→	app^#(plus, app(s, 0))
double^#	→	app^#(map, app(times, app(s, app(s, 0))))		app^#(app(plus, app(s, x)), y)	→	app^#(plus, x)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(app(map, f), xs)		double^#	→	app^#(times, app(s, app(s, 0)))
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))		double^#	→	app^#(s, app(s, 0))
double^#	→	app^#(s, 0)		app^#(app(times, app(s, x)), y)	→	app^#(app(times, x), y)
app^#(app(plus, app(s, x)), y)	→	app^#(app(plus, x), y)		app^#(app(map, f), app(app(cons, x), xs))	→	app^#(map, f)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(cons, app(f, x))

Rewrite Rules

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)
app(app(map, f), nil)	→	nil		app(app(map, f), app(app(cons, x), xs))	→	app(app(cons, app(f, x)), app(app(map, f), xs))
inc	→	app(map, app(plus, app(s, 0)))		double	→	app(map, app(times, app(s, app(s, 0))))

Original Signature

Termination of terms over the following signature is verified: app, plus, 0, s, inc, times, map, double, nil, cons

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(map, f), app(app(cons, x), xs)) → app^#(f, x)	app^#(app(map, f), app(app(cons, x), xs)) → app^#(app(cons, app(f, x)), app(app(map, f), xs))
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(plus, app(s, x)), y) → app^#(plus, x)
app^#(app(map, f), app(app(cons, x), xs)) → app^#(app(map, f), xs)	app^#(app(plus, app(s, x)), y) → app^#(app(plus, x), y)
app^#(app(map, f), app(app(cons, x), xs)) → app^#(cons, app(f, x))	app^#(app(map, f), app(app(cons, x), xs)) → app^#(map, f)