TIMEOUT

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (282ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (105ms), PolynomialLinearRange4iUR (2326ms), DependencyGraph (103ms), PolynomialLinearRange8NegiUR (6959ms), DependencyGraph (136ms), ReductionPairSAT (50071ms), DependencyGraph (timeout)].

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

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(app(curry, g), x), y)	→	app(app(g, x), 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(app(curry, plus), app(s, 0)))
double	→	app(map, app(app(curry, 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, curry, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

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(app(curry, g), x), y)	→	app(app(g, x), 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(app(curry, plus), app(s, 0)))
double	→	app(map, app(app(curry, 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, curry, nil, cons

Strategy

The following SCCs where found

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(app(curry, g), x), y) → app^#(g, 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(app(curry, g), x), y) → app^#(app(g, 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))