Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/reverse)

The rewrite relation of the following TRS is considered.

isEmpty(nil)	→	true	(1)
isEmpty(cons(x,xs))	→	false	(2)
last(cons(x,nil))	→	x	(3)
last(cons(x,cons(y,ys)))	→	last(cons(y,ys))	(4)
dropLast(nil)	→	nil	(5)
dropLast(cons(x,nil))	→	nil	(6)
dropLast(cons(x,cons(y,ys)))	→	cons(x,dropLast(cons(y,ys)))	(7)
append(nil,ys)	→	ys	(8)
append(cons(x,xs),ys)	→	cons(x,append(xs,ys))	(9)
reverse(xs)	→	rev(xs,nil)	(10)
rev(xs,ys)	→	if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)	(11)
if(true,xs,ys,zs)	→	zs	(12)
if(false,xs,ys,zs)	→	rev(xs,ys)	(13)

Prove or disprove termination.

Yes.

The following set of initial dependency pairs has been identified.

last^#(cons(x,cons(y,ys)))	→	last^#(cons(y,ys))	(14)
dropLast^#(cons(x,cons(y,ys)))	→	dropLast^#(cons(y,ys))	(15)
append^#(cons(x,xs),ys)	→	append^#(xs,ys)	(16)
reverse^#(xs)	→	rev^#(xs,nil)	(17)
rev^#(xs,ys)	→	last^#(xs)	(18)
rev^#(xs,ys)	→	append^#(ys,last(xs))	(19)
rev^#(xs,ys)	→	dropLast^#(xs)	(20)
rev^#(xs,ys)	→	isEmpty^#(xs)	(21)
rev^#(xs,ys)	→	if^#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)	(22)
if^#(false,xs,ys,zs)	→	rev^#(xs,ys)	(23)

The dependency pairs are split into 4 components.

The 1^st component contains the pair

if^#(false,xs,ys,zs)	→	rev^#(xs,ys)	(23)
rev^#(xs,ys)	→	if^#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)	(22)

Using the linear polynomial interpretation over the arctic semiring over the integers

together with the usable rules

(w.r.t. the implicit argument filter of the reduction pair), the pair

rev^#(xs,ys)

→

if^#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)

(22)

could be deleted.

The dependency pairs are split into 0 components.