Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nosorts_FR)

The rewrite relation of the following TRS is considered.

and(tt,X)	→	activate(X)	(1)
plus(N,0)	→	N	(2)
plus(N,s(M))	→	s(plus(N,M))	(3)
x(N,0)	→	0	(4)
x(N,s(M))	→	plus(x(N,M),N)	(5)
activate(X)	→	X	(6)

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.

x^#(N,s(M))	→	x^#(N,M)	(7)
plus^#(N,s(M))	→	plus^#(N,M)	(8)
x^#(N,s(M))	→	plus^#(x(N,M),N)	(9)
and^#(tt,X)	→	activate^#(X)	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

x^#(N,s(M))

→

x^#(N,M)

(7)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	0
[and(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	0
[activate^#(x₁)]	=	0
[x(x₁, x₂)]	=	0
[0]	=	0
[x^#(x₁, x₂)]	=	x₂ + 0
[plus(x₁, x₂)]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	0

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

x^#(N,s(M))

→

x^#(N,M)

(7)

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

plus^#(N,s(M))

→

plus^#(N,M)

(8)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	0
[and(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	x₂ + 0
[activate^#(x₁)]	=	0
[x(x₁, x₂)]	=	0
[0]	=	0
[x^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	0

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

plus^#(N,s(M))

→

plus^#(N,M)

(8)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.