Certification Problem

Input (TPDB TRS_Standard/Various_04/19)

The rewrite relation of the following TRS is considered.

:(x,x)	→	e	(1)
:(x,e)	→	x	(2)
i(:(x,y))	→	:(y,x)	(3)
:(:(x,y),z)	→	:(x,:(z,i(y)))	(4)
:(e,x)	→	i(x)	(5)
i(i(x))	→	x	(6)
i(e)	→	e	(7)
:(x,:(y,i(x)))	→	i(y)	(8)
:(x,:(y,:(i(x),z)))	→	:(i(z),y)	(9)
:(i(x),:(y,x))	→	i(y)	(10)
:(i(x),:(y,:(x,z)))	→	:(i(z),y)	(11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

:^#(x,:(y,:(i(x),z)))	→	i^#(z)	(12)
:^#(e,x)	→	i^#(x)	(13)
:^#(:(x,y),z)	→	:^#(x,:(z,i(y)))	(14)
:^#(:(x,y),z)	→	i^#(y)	(15)
i^#(:(x,y))	→	:^#(y,x)	(16)
:^#(:(x,y),z)	→	:^#(z,i(y))	(17)
:^#(i(x),:(y,x))	→	i^#(y)	(18)
:^#(i(x),:(y,:(x,z)))	→	:^#(i(z),y)	(19)
:^#(x,:(y,:(i(x),z)))	→	:^#(i(z),y)	(20)
:^#(x,:(y,i(x)))	→	i^#(y)	(21)
:^#(i(x),:(y,:(x,z)))	→	i^#(z)	(22)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

:^#(i(x),:(y,:(x,z)))	→	i^#(z)	(22)
:^#(x,:(y,i(x)))	→	i^#(y)	(21)
:^#(x,:(y,:(i(x),z)))	→	:^#(i(z),y)	(20)
:^#(i(x),:(y,:(x,z)))	→	:^#(i(z),y)	(19)
:^#(:(x,y),z)	→	i^#(y)	(15)
:^#(:(x,y),z)	→	:^#(x,:(z,i(y)))	(14)
:^#(e,x)	→	i^#(x)	(13)
:^#(i(x),:(y,x))	→	i^#(y)	(18)
:^#(:(x,y),z)	→	:^#(z,i(y))	(17)
i^#(:(x,y))	→	:^#(y,x)	(16)
:^#(x,:(y,:(i(x),z)))	→	i^#(z)	(12)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[:^#(x₁, x₂)]	=	x₁ + x₂ + 0
[:(x₁, x₂)]	=	x₁ + x₂ + 1
[i(x₁)]	=	x₁ + 0
[e]	=	1
[i^#(x₁)]	=	x₁ + 0

together with the usable rules

:(:(x,y),z)	→	:(x,:(z,i(y)))	(4)
:(x,:(y,i(x)))	→	i(y)	(8)
:(x,x)	→	e	(1)
i(:(x,y))	→	:(y,x)	(3)
:(e,x)	→	i(x)	(5)
:(i(x),:(y,x))	→	i(y)	(10)
i(e)	→	e	(7)
:(i(x),:(y,:(x,z)))	→	:(i(z),y)	(11)
:(x,:(y,:(i(x),z)))	→	:(i(z),y)	(9)
i(i(x))	→	x	(6)
:(x,e)	→	x	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

:^#(i(x),:(y,:(x,z)))	→	i^#(z)	(22)
:^#(x,:(y,i(x)))	→	i^#(y)	(21)
:^#(x,:(y,:(i(x),z)))	→	:^#(i(z),y)	(20)
:^#(i(x),:(y,:(x,z)))	→	:^#(i(z),y)	(19)
:^#(:(x,y),z)	→	i^#(y)	(15)
:^#(e,x)	→	i^#(x)	(13)
:^#(i(x),:(y,x))	→	i^#(y)	(18)
:^#(:(x,y),z)	→	:^#(z,i(y))	(17)
i^#(:(x,y))	→	:^#(y,x)	(16)
:^#(x,:(y,:(i(x),z)))	→	i^#(z)	(12)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

:^#(:(x,y),z)

→

:^#(x,:(z,i(y)))

(14)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[:^#(x₁, x₂)]	=	x₁ + 0
[:(x₁, x₂)]	=	x₁ + x₂ + 1
[i(x₁)]	=	x₁ + 0
[e]	=	1
[i^#(x₁)]	=	0

together with the usable rules

:(:(x,y),z)	→	:(x,:(z,i(y)))	(4)
:(x,:(y,i(x)))	→	i(y)	(8)
:(x,x)	→	e	(1)
i(:(x,y))	→	:(y,x)	(3)
:(e,x)	→	i(x)	(5)
:(i(x),:(y,x))	→	i(y)	(10)
i(e)	→	e	(7)
:(i(x),:(y,:(x,z)))	→	:(i(z),y)	(11)
:(x,:(y,:(i(x),z)))	→	:(i(z),y)	(9)
i(i(x))	→	x	(6)
:(x,e)	→	x	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

:^#(:(x,y),z)

→

:^#(x,:(z,i(y)))

(14)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.