Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex8_BLR02_FR)

The rewrite relation of the following TRS is considered.

fib(N)	→	sel(N,fib1(s(0),s(0)))	(1)
fib1(X,Y)	→	cons(X,n__fib1(Y,n__add(X,Y)))	(2)
add(0,X)	→	X	(3)
add(s(X),Y)	→	s(add(X,Y))	(4)
sel(0,cons(X,XS))	→	X	(5)
sel(s(N),cons(X,XS))	→	sel(N,activate(XS))	(6)
fib1(X1,X2)	→	n__fib1(X1,X2)	(7)
add(X1,X2)	→	n__add(X1,X2)	(8)
activate(n__fib1(X1,X2))	→	fib1(activate(X1),activate(X2))	(9)
activate(n__add(X1,X2))	→	add(activate(X1),activate(X2))	(10)
activate(X)	→	X	(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.

sel^#(s(N),cons(X,XS))	→	activate^#(XS)	(12)
activate^#(n__add(X1,X2))	→	add^#(activate(X1),activate(X2))	(13)
fib^#(N)	→	sel^#(N,fib1(s(0),s(0)))	(14)
add^#(s(X),Y)	→	add^#(X,Y)	(15)
activate^#(n__add(X1,X2))	→	activate^#(X1)	(16)
fib^#(N)	→	fib1^#(s(0),s(0))	(17)
activate^#(n__fib1(X1,X2))	→	activate^#(X2)	(18)
activate^#(n__fib1(X1,X2))	→	fib1^#(activate(X1),activate(X2))	(19)
sel^#(s(N),cons(X,XS))	→	sel^#(N,activate(XS))	(20)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(21)
activate^#(n__fib1(X1,X2))	→	activate^#(X1)	(22)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

sel^#(s(N),cons(X,XS))

→

sel^#(N,activate(XS))

(20)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	1
[activate^#(x₁)]	=	0
[n__add(x₁, x₂)]	=	2
[fib1^#(x₁, x₂)]	=	0
[n__fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[fib1(x₁, x₂)]	=	x₁ + x₂ + 0
[fib(x₁)]	=	0
[0]	=	20163
[sel^#(x₁, x₂)]	=	x₁ + 0
[sel(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 1
[fib^#(x₁)]	=	0

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

sel^#(s(N),cons(X,XS))

→

sel^#(N,activate(XS))

(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

activate^#(n__fib1(X1,X2))	→	activate^#(X1)	(22)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(21)
activate^#(n__fib1(X1,X2))	→	activate^#(X2)	(18)
activate^#(n__add(X1,X2))	→	activate^#(X1)	(16)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	1
[activate^#(x₁)]	=	x₁ + 0
[n__add(x₁, x₂)]	=	x₁ + x₂ + 2
[fib1^#(x₁, x₂)]	=	0
[n__fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[fib1(x₁, x₂)]	=	x₁ + x₂ + 0
[fib(x₁)]	=	0
[0]	=	20163
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[add^#(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₁ + 1
[fib^#(x₁)]	=	0

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

activate^#(n__fib1(X1,X2))	→	activate^#(X1)	(22)
activate^#(n__add(X1,X2))	→	activate^#(X2)	(21)
activate^#(n__fib1(X1,X2))	→	activate^#(X2)	(18)
activate^#(n__add(X1,X2))	→	activate^#(X1)	(16)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

add^#(s(X),Y)

→

add^#(X,Y)

(15)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	1
[activate^#(x₁)]	=	0
[n__add(x₁, x₂)]	=	x₁ + x₂ + 2
[fib1^#(x₁, x₂)]	=	0
[n__fib1(x₁, x₂)]	=	x₁ + x₂ + 1
[fib1(x₁, x₂)]	=	x₁ + x₂ + 0
[fib(x₁)]	=	0
[0]	=	42736
[sel^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	x₁ + 1
[fib^#(x₁)]	=	0

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

add^#(s(X),Y)

→

add^#(X,Y)

(15)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.