Certification Problem

Input (TPDB TRS_Standard/SK90/2.61)

The rewrite relation of the following TRS is considered.

f(j(x,y),y)	→	g(f(x,k(y)))	(1)
f(x,h1(y,z))	→	h2(0,x,h1(y,z))	(2)
g(h2(x,y,h1(z,u)))	→	h2(s(x),y,h1(z,u))	(3)
h2(x,j(y,h1(z,u)),h1(z,u))	→	h2(s(x),y,h1(s(z),u))	(4)
i(f(x,h(y)))	→	y	(5)
i(h2(s(x),y,h1(x,z)))	→	z	(6)
k(h(x))	→	h1(0,x)	(7)
k(h1(x,y))	→	h1(s(x),y)	(8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

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

prec(i)	=	6		weight(i)	=	1
prec(h)	=	4		weight(h)	=	7
prec(s)	=	5		weight(s)	=	2
prec(h2)	=	1		weight(h2)	=	5
prec(0)	=	11		weight(0)	=	2
prec(h1)	=	2		weight(h1)	=	5
prec(g)	=	0		weight(g)	=	5
prec(k)	=	9		weight(k)	=	2
prec(f)	=	3		weight(f)	=	7
prec(j)	=	8		weight(j)	=	6

all of the following rules can be deleted.

f(j(x,y),y)	→	g(f(x,k(y)))	(1)
f(x,h1(y,z))	→	h2(0,x,h1(y,z))	(2)
g(h2(x,y,h1(z,u)))	→	h2(s(x),y,h1(z,u))	(3)
h2(x,j(y,h1(z,u)),h1(z,u))	→	h2(s(x),y,h1(s(z),u))	(4)
i(f(x,h(y)))	→	y	(5)
i(h2(s(x),y,h1(x,z)))	→	z	(6)
k(h(x))	→	h1(0,x)	(7)
k(h1(x,y))	→	h1(s(x),y)	(8)

1.1 R is empty

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