Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/test76)

The rewrite relation of the following TRS is considered.

+(X,0)	→	X	(1)
+(X,s(Y))	→	s(+(X,Y))	(2)
f(0,s(0),X)	→	f(X,+(X,X),X)	(3)
g(X,Y)	→	X	(4)
g(X,Y)	→	Y	(5)

The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	f(g(0,s(0)),+(g(0,s(0)),g(0,s(0))),g(0,s(0)))
	→	f(g(0,s(0)),+(s(0),g(0,s(0))),g(0,s(0)))
	→	f(g(0,s(0)),+(s(0),0),g(0,s(0)))
	→	f(g(0,s(0)),s(0),g(0,s(0)))
	→	f(0,s(0),g(0,s(0)))
	→	f(g(0,s(0)),+(g(0,s(0)),g(0,s(0))),g(0,s(0)))
	=	t₅

where t₅ = t₀