Certification Problem

Input (TPDB TRS_Standard/Applicative_05/ReverseLastInit)

The rewrite relation of the following TRS is considered.

app(app(app(compose,f),g),x)	→	app(g,app(f,x))	(1)
app(reverse,l)	→	app(app(reverse2,l),nil)	(2)
app(app(reverse2,nil),l)	→	l	(3)
app(app(reverse2,app(app(cons,x),xs)),l)	→	app(app(reverse2,xs),app(app(cons,x),l))	(4)
app(hd,app(app(cons,x),xs))	→	x	(5)
app(tl,app(app(cons,x),xs))	→	xs	(6)
last	→	app(app(compose,hd),reverse)	(7)
init	→	app(app(compose,reverse),app(app(compose,tl),reverse))	(8)

Prove or disprove termination.

Yes.

The following set of initial dependency pairs has been identified.

app^#(reverse,l)	→	app^#(reverse2,l)	(9)
app^#(app(app(compose,f),g),x)	→	app^#(f,x)	(10)
app^#(app(reverse2,app(app(cons,x),xs)),l)	→	app^#(app(cons,x),l)	(11)
init^#	→	app^#(app(compose,tl),reverse)	(12)
app^#(app(reverse2,app(app(cons,x),xs)),l)	→	app^#(app(reverse2,xs),app(app(cons,x),l))	(13)
app^#(app(reverse2,app(app(cons,x),xs)),l)	→	app^#(reverse2,xs)	(14)
init^#	→	app^#(app(compose,reverse),app(app(compose,tl),reverse))	(15)
init^#	→	app^#(compose,tl)	(16)
app^#(app(app(compose,f),g),x)	→	app^#(g,app(f,x))	(17)
last^#	→	app^#(app(compose,hd),reverse)	(18)
app^#(reverse,l)	→	app^#(app(reverse2,l),nil)	(19)
init^#	→	app^#(compose,reverse)	(20)
last^#	→	app^#(compose,hd)	(21)

The dependency pairs are split into 2 components.

The 1^st component contains the pair

app^#(app(app(compose,f),g),x)	→	app^#(f,x)	(10)
app^#(app(app(compose,f),g),x)	→	app^#(g,app(f,x))	(17)

Using the Max-polynomial interpretation

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

app^#(app(app(compose,f),g),x)	→	app^#(f,x)	(10)
app^#(app(app(compose,f),g),x)	→	app^#(g,app(f,x))	(17)

could be deleted.

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

app^#(app(reverse2,app(app(cons,x),xs)),l)

→

app^#(app(reverse2,xs),app(app(cons,x),l))

(13)