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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(t,x)	→	f'^#(t,g(x))	(18)
foldC^#(t,s(n))	→	f^#(foldC(t,n),C)	(19)
fold^#(t,x,s(n))	→	fold^#(t,x,n)	(20)
foldB^#(t,s(n))	→	foldB^#(t,n)	(21)
f''^#(triple(a,b,c))	→	foldC^#(triple(a,b,0),c)	(22)
foldC^#(t,s(n))	→	foldC^#(t,n)	(23)
foldB^#(t,s(n))	→	f^#(foldB(t,n),B)	(24)
f'^#(triple(a,b,c),A)	→	foldB^#(triple(s(a),0,c),b)	(25)
f^#(t,x)	→	g^#(x)	(26)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(27)
fold^#(t,x,s(n))	→	f^#(fold(t,x,n),x)	(28)
f'^#(triple(a,b,c),A)	→	f''^#(foldB(triple(s(a),0,c),b))	(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)

(20)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

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

→

fold^#(t,x,n)

(20)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

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

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 145146
[foldC^#(x₁, x₂)]	=	x₁ + x₂ + 0
[f'^#(x₁, x₂)]	=	x₁ + 119705
[triple(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[C]	=	1
[f(x₁, x₂)]	=	x₁ + 145146
[B]	=	3
[foldB(x₁, x₂)]	=	x₁ + x₂ + 22541
[fold^#(x₁, x₂, x₃)]	=	0
[0]	=	48581
[foldB^#(x₁, x₂)]	=	x₁ + x₂ + 71123
[A]	=	5
[f^#(x₁, x₂)]	=	x₁ + 119705
[g^#(x₁)]	=	0
[fold(x₁, x₂, x₃)]	=	0
[f'(x₁, x₂)]	=	x₁ + 145146
[foldC(x₁, x₂)]	=	x₁ + x₂ + 25440
[g(x₁)]	=	x₁ + 1
[f''(x₁)]	=	x₁ + 74024
[f''^#(x₁)]	=	x₁ + 48582

together with the usable rules

f''(triple(a,b,c))	→	foldC(triple(a,b,0),c)	(15)
foldB(t,s(n))	→	f(foldB(t,n),B)	(8)
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)

(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))	(29)
f''^#(triple(a,b,c))	→	foldC^#(triple(a,b,0),c)	(22)
foldB^#(t,s(n))	→	foldB^#(t,n)	(21)
foldC^#(t,s(n))	→	f^#(foldC(t,n),C)	(19)
f'^#(triple(a,b,c),A)	→	foldB^#(triple(s(a),0,c),b)	(25)
foldB^#(t,s(n))	→	f^#(foldB(t,n),B)	(24)
foldC^#(t,s(n))	→	foldC^#(t,n)	(23)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

f^#(t,x)	→	f'^#(t,g(x))	(18)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(27)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[foldC^#(x₁, x₂)]	=	0
[f'^#(x₁, x₂)]	=	x₂ + 119705
[triple(x₁, x₂, x₃)]	=	1
[C]	=	31252
[f(x₁, x₂)]	=	x₁ + 0
[B]	=	54889
[foldB(x₁, x₂)]	=	x₁ + x₂ + 39787
[fold^#(x₁, x₂, x₃)]	=	0
[0]	=	12237
[foldB^#(x₁, x₂)]	=	71123
[A]	=	31250
[f^#(x₁, x₂)]	=	x₂ + 143343
[g^#(x₁)]	=	0
[fold(x₁, x₂, x₃)]	=	0
[f'(x₁, x₂)]	=	x₁ + 0
[foldC(x₁, x₂)]	=	x₁ + 0
[g(x₁)]	=	x₁ + 23637
[f''(x₁)]	=	1
[f''^#(x₁)]	=	x₁ + 48582

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^#(t,x)	→	f'^#(t,g(x))	(18)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(27)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.