Certification Problem

Input (TPDB TRS_Standard/SK90/4.57)

The rewrite relation of the following TRS is considered.

f(x,y,z)	→	g(<=(x,y),x,y,z)	(1)
g(true,x,y,z)	→	z	(2)
g(false,x,y,z)	→	f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))	(3)
p(0)	→	0	(4)
p(s(x))	→	x	(5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(x,y,z)	→	g^#(<=(x,y),x,y,z)	(6)
g^#(false,x,y,z)	→	f^#(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))	(7)
g^#(false,x,y,z)	→	f^#(p(x),y,z)	(8)
g^#(false,x,y,z)	→	p^#(x)	(9)
g^#(false,x,y,z)	→	f^#(p(y),z,x)	(10)
g^#(false,x,y,z)	→	p^#(y)	(11)
g^#(false,x,y,z)	→	f^#(p(z),x,y)	(12)
g^#(false,x,y,z)	→	p^#(z)	(13)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.