Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/023)

The rewrite relation of the following TRS is considered.

app(id,x)	→	x	(1)
app(plus,0)	→	id	(2)
app(app(plus,app(s,x)),y)	→	app(s,app(app(plus,x),y))	(3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(id)	=	0		weight(id)	=	2
prec(plus)	=	2		weight(plus)	=	1
prec(0)	=	3		weight(0)	=	1
prec(s)	=	4		weight(s)	=	1
prec(app)	=	1		weight(app)	=	0

all of the following rules can be deleted.

app(id,x)	→	x	(1)
app(plus,0)	→	id	(2)
app(app(plus,app(s,x)),y)	→	app(s,app(app(plus,x),y))	(3)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.