Certification Problem

Input (TPDB TRS_Standard/SK90/4.54)

The rewrite relation of the following TRS is considered.

g(f(x,y))

→

f(f(g(g(x)),g(g(y))),f(g(g(x)),g(g(y))))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Innermost Lhss Increase

We add the following left hand sides to the innermost strategy.

g(f(x0,x1))

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

g^#(f(x,y))	→	g^#(g(x))	(2)
g^#(f(x,y))	→	g^#(x)	(3)
g^#(f(x,y))	→	g^#(g(y))	(4)
g^#(f(x,y))	→	g^#(y)	(5)

It remains to prove infiniteness of the resulting DP problem.

1.1.1 Narrowing Processor

We consider narrowings of the pair below position 1 to get the following set of pairs

g^#(f(f(x0,x1),y1))

→

g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))

(6)

1.1.1.1 Narrowing Processor

We consider narrowings of the pair below position 1 to get the following set of pairs

g^#(f(y0,f(x0,x1)))

→

g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))

(7)

1.1.1.1.1 Instantiation Processor

The pairs are instantiated to the following pairs.

g^#(f(x,y))	→	g^#(y)	(5)
g^#(f(f(x0,x1),y1))	→	g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))	(6)
g^#(f(y0,f(x0,x1)))	→	g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))	(7)
g^#(f(f(y_0,y_1),x1))	→	g^#(f(y_0,y_1))	(8)
g^#(f(f(f(y_0,y_1),y_2),x1))	→	g^#(f(f(y_0,y_1),y_2))	(9)
g^#(f(f(y_0,f(y_1,y_2)),x1))	→	g^#(f(y_0,f(y_1,y_2)))	(10)

1.1.1.1.1.1 Instantiation Processor

The pairs are instantiated to the following pairs.

g^#(f(f(x0,x1),y1))	→	g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))	(6)
g^#(f(y0,f(x0,x1)))	→	g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))	(7)
g^#(f(f(y_0,y_1),x1))	→	g^#(f(y_0,y_1))	(8)
g^#(f(f(f(y_0,y_1),y_2),x1))	→	g^#(f(f(y_0,y_1),y_2))	(9)
g^#(f(f(y_0,f(y_1,y_2)),x1))	→	g^#(f(y_0,f(y_1,y_2)))	(10)
g^#(f(x0,f(y_0,y_1)))	→	g^#(f(y_0,y_1))	(11)
g^#(f(x0,f(f(y_0,y_1),y_2)))	→	g^#(f(f(y_0,y_1),y_2))	(12)
g^#(f(x0,f(y_0,f(y_1,y_2))))	→	g^#(f(y_0,f(y_1,y_2)))	(13)
g^#(f(x0,f(f(f(y_0,y_1),y_2),y_3)))	→	g^#(f(f(f(y_0,y_1),y_2),y_3))	(14)
g^#(f(x0,f(f(y_0,f(y_1,y_2)),y_3)))	→	g^#(f(f(y_0,f(y_1,y_2)),y_3))	(15)

1.1.1.1.1.1.1 Full Strategy Switch Processor

We have a locally confluent overlay TRS, no overlaps between P and R, and the strategy is less than innermost. Hence, it suffices to prove non-termination for the full rewrite relation.

Local Confluence Proof

All critical pairs are joinable within 0 step(s). 0

1.1.1.1.1.1.1.1 Loop

The following loop proves infiniteness of the DP problem.

t₀	=	g^#(f(f(x0,x1),y1))
	→_P	g^#(f(f(g(g(x0)),g(g(x1))),f(g(g(x0)),g(g(x1)))))
	=	t₁

where t₁ = t₀σ and σ = {x0/g(g(x0)), x1/g(g(x1)), y1/f(g(g(x0)),g(g(x1)))}