Certification Problem

Input (TPDB TRS_Standard/CiME_04/filliatre3)

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)
fold(t,x,0)	→	t	(16)
fold(t,x,s(n))	→	f(fold(t,x,n),x)	(17)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair
fold^#(t,x,s(n)) → fold^#(t,x,n) (28)

1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

fold^#(t,x,s(n)) → fold^#(t,x,n) (28)

3 > 3

2 ≥ 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 2^nd component contains the pair

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

1.1.2 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[f''^#(x₁)]	=	4 · x₁ + 1
[0]	=	0
[f^#(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 4
[foldC(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 1
[g(x₁)]	=	1 · x₁ + 0
[C]	=	5
[foldC^#(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 0
[f'^#(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 1
[foldB(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[triple(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 0
[A]	=	0
[f(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 2
[foldB^#(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 1
[f''(x₁)]	=	1 · x₁ + 2
[f'(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 2
[s(x₁)]	=	1 · x₁ + 7
[B]	=	5

together with the usable rules

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)
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)
foldC(t,0)	→	t	(9)
foldC(t,s(n))	→	f(foldC(t,n),C)	(10)

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

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

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.