Certification Problem

Input (TPDB TRS_Standard/CiME_04/filliatre)

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)
foldf(x,nil)	→	x	(7)
foldf(x,cons(y,z))	→	f(foldf(x,z),y)	(8)
f(t,x)	→	f'(t,g(x))	(9)
f'(triple(a,b,c),C)	→	triple(a,b,cons(C,c))	(10)
f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(11)
f'(triple(a,b,c),A)	→	f''(foldf(triple(cons(A,a),nil,c),b))	(12)
f''(triple(a,b,c))	→	foldf(triple(a,b,nil),c)	(13)

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))	(14)
f'^#(triple(a,b,c),A)	→	foldf^#(triple(cons(A,a),nil,c),b)	(15)
foldf^#(x,cons(y,z))	→	f^#(foldf(x,z),y)	(16)
f'^#(triple(a,b,c),A)	→	f''^#(foldf(triple(cons(A,a),nil,c),b))	(17)
f^#(t,x)	→	g^#(x)	(18)
f''^#(triple(a,b,c))	→	foldf^#(triple(a,b,nil),c)	(19)
foldf^#(x,cons(y,z))	→	foldf^#(x,z)	(20)
f'^#(triple(a,b,c),B)	→	f^#(triple(a,b,c),A)	(21)

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),B)	→	f^#(triple(a,b,c),A)	(21)
foldf^#(x,cons(y,z))	→	foldf^#(x,z)	(20)
f''^#(triple(a,b,c))	→	foldf^#(triple(a,b,nil),c)	(19)
f'^#(triple(a,b,c),A)	→	foldf^#(triple(cons(A,a),nil,c),b)	(15)
f'^#(triple(a,b,c),A)	→	f''^#(foldf(triple(cons(A,a),nil,c),b))	(17)
foldf^#(x,cons(y,z))	→	f^#(foldf(x,z),y)	(16)
f^#(t,x)	→	f'^#(t,g(x))	(14)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[f'^#(x₁, x₂)]	=	x₁ + x₂ + 0
[triple(x₁, x₂, x₃)]	=	x₂ + x₃ + 17888
[foldf^#(x₁, x₂)]	=	x₁ + x₂ + 28225
[C]	=	28230
[f(x₁, x₂)]	=	x₁ + x₂ + 0
[B]	=	28230
[A]	=	28229
[nil]	=	1
[f^#(x₁, x₂)]	=	x₁ + x₂ + 1
[g^#(x₁)]	=	0
[f'(x₁, x₂)]	=	x₁ + x₂ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[foldf(x₁, x₂)]	=	x₁ + x₂ + 0
[g(x₁)]	=	x₁ + 0
[f''(x₁)]	=	x₁ + 28228
[f''^#(x₁)]	=	x₁ + 28227

together with the usable rules

g(C)	→	A	(4)
foldf(x,cons(y,z))	→	f(foldf(x,z),y)	(8)
g(A)	→	A	(1)
g(B)	→	B	(3)
g(C)	→	B	(5)
f'(triple(a,b,c),C)	→	triple(a,b,cons(C,c))	(10)
foldf(x,nil)	→	x	(7)
f'(triple(a,b,c),A)	→	f''(foldf(triple(cons(A,a),nil,c),b))	(12)
f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(11)
f(t,x)	→	f'(t,g(x))	(9)
f''(triple(a,b,c))	→	foldf(triple(a,b,nil),c)	(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))	→	foldf^#(triple(a,b,nil),c)	(19)
f'^#(triple(a,b,c),A)	→	foldf^#(triple(cons(A,a),nil,c),b)	(15)
f'^#(triple(a,b,c),A)	→	f''^#(foldf(triple(cons(A,a),nil,c),b))	(17)
foldf^#(x,cons(y,z))	→	f^#(foldf(x,z),y)	(16)
f^#(t,x)	→	f'^#(t,g(x))	(14)

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

foldf^#(x,cons(y,z))

→

foldf^#(x,z)

(20)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[f'^#(x₁, x₂)]	=	x₂ + 0
[triple(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[foldf^#(x₁, x₂)]	=	x₂ + 28225
[C]	=	1
[f(x₁, x₂)]	=	x₁ + 2
[B]	=	1
[A]	=	1
[nil]	=	1
[f^#(x₁, x₂)]	=	x₁ + 1
[g^#(x₁)]	=	0
[f'(x₁, x₂)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₂ + 2
[foldf(x₁, x₂)]	=	x₁ + x₂ + 0
[g(x₁)]	=	x₁ + 1
[f''(x₁)]	=	x₁ + 1
[f''^#(x₁)]	=	x₁ + 28227

together with the usable rules

g(C)	→	A	(4)
foldf(x,cons(y,z))	→	f(foldf(x,z),y)	(8)
g(A)	→	A	(1)
g(B)	→	B	(3)
g(C)	→	B	(5)
f'(triple(a,b,c),C)	→	triple(a,b,cons(C,c))	(10)
foldf(x,nil)	→	x	(7)
f'(triple(a,b,c),A)	→	f''(foldf(triple(cons(A,a),nil,c),b))	(12)
f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(11)
f(t,x)	→	f'(t,g(x))	(9)
f''(triple(a,b,c))	→	foldf(triple(a,b,nil),c)	(13)
g(C)	→	C	(6)
g(B)	→	A	(2)

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

foldf^#(x,cons(y,z))

→

foldf^#(x,z)

(20)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.