Certification Problem

Input (TPDB TRS_Standard/CiME_04/filliatre2)

The rewrite relation of the following TRS is considered.

g(A)	→	A	(1)
g(B)	→	A	(2)
g(B)	→	B	(3)
g(C)	→	A	(4)
g(C)	→	B	(5)
g(C)	→	C	(6)
foldB(t,0)	→	t	(7)
foldB(t,s(n))	→	f(foldB(t,n),B)	(8)
foldC(t,0)	→	t	(9)
foldC(t,s(n))	→	f(foldC(t,n),C)	(10)
f(t,x)	→	f'(t,g(x))	(11)
f'(triple(a,b,c),C)	→	triple(a,b,s(c))	(12)
f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(13)
f'(triple(a,b,c),A)	→	f''(foldB(triple(s(a),0,c),b))	(14)
f''(triple(a,b,c))	→	foldC(triple(a,b,0),c)	(15)

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.

f^#(t,x)	→	f'^#(t,g(x))	(16)
foldC^#(t,s(n))	→	f^#(foldC(t,n),C)	(17)
foldB^#(t,s(n))	→	foldB^#(t,n)	(18)
foldC^#(t,s(n))	→	foldC^#(t,n)	(19)
f''^#(triple(a,b,c))	→	foldC^#(triple(a,b,0),c)	(20)
f'^#(triple(a,b,c),A)	→	foldB^#(triple(s(a),0,c),b)	(21)
f^#(t,x)	→	g^#(x)	(22)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(23)
foldB^#(t,s(n))	→	f^#(foldB(t,n),B)	(24)
f'^#(triple(a,b,c),A)	→	f''^#(foldB(triple(s(a),0,c),b))	(25)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

f'^#(triple(a,b,c),A)	→	f''^#(foldB(triple(s(a),0,c),b))	(25)
foldB^#(t,s(n))	→	f^#(foldB(t,n),B)	(24)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(23)
foldB^#(t,s(n))	→	foldB^#(t,n)	(18)
foldC^#(t,s(n))	→	f^#(foldC(t,n),C)	(17)
f'^#(triple(a,b,c),A)	→	foldB^#(triple(s(a),0,c),b)	(21)
f''^#(triple(a,b,c))	→	foldC^#(triple(a,b,0),c)	(20)
foldC^#(t,s(n))	→	foldC^#(t,n)	(19)
f^#(t,x)	→	f'^#(t,g(x))	(16)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 23625
[foldC^#(x₁, x₂)]	=	x₁ + x₂ + 0
[f'^#(x₁, x₂)]	=	x₁ + x₂ + 23613
[triple(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[C]	=	4
[f(x₁, x₂)]	=	x₁ + 23625
[B]	=	9
[foldB(x₁, x₂)]	=	x₁ + x₂ + 23612
[0]	=	1
[foldB^#(x₁, x₂)]	=	x₁ + x₂ + 23615
[A]	=	3
[f^#(x₁, x₂)]	=	x₁ + x₂ + 23619
[g^#(x₁)]	=	0
[f'(x₁, x₂)]	=	x₁ + 23625
[foldC(x₁, x₂)]	=	x₁ + x₂ + 1
[g(x₁)]	=	x₁ + 5
[f''(x₁)]	=	x₁ + 2
[f''^#(x₁)]	=	x₁ + 2

together with the usable rules

g(C)	→	A	(4)
f''(triple(a,b,c))	→	foldC(triple(a,b,0),c)	(15)
foldB(t,s(n))	→	f(foldB(t,n),B)	(8)
g(A)	→	A	(1)
g(B)	→	B	(3)
g(C)	→	B	(5)
foldC(t,s(n))	→	f(foldC(t,n),C)	(10)
foldB(t,0)	→	t	(7)
f'(triple(a,b,c),A)	→	f''(foldB(triple(s(a),0,c),b))	(14)
f'(triple(a,b,c),C)	→	triple(a,b,s(c))	(12)
f(t,x)	→	f'(t,g(x))	(11)
foldC(t,0)	→	t	(9)
f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(13)
g(C)	→	C	(6)
g(B)	→	A	(2)

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

f'^#(triple(a,b,c),A)	→	f''^#(foldB(triple(s(a),0,c),b))	(25)
foldB^#(t,s(n))	→	foldB^#(t,n)	(18)
foldC^#(t,s(n))	→	f^#(foldC(t,n),C)	(17)
f''^#(triple(a,b,c))	→	foldC^#(triple(a,b,0),c)	(20)
foldC^#(t,s(n))	→	foldC^#(t,n)	(19)
f^#(t,x)	→	f'^#(t,g(x))	(16)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.