Certification Problem

Input (TPDB TRS_Standard/SK90/2.29)

The rewrite relation of the following TRS is considered.

prime(0)	→	false	(1)
prime(s(0))	→	false	(2)
prime(s(s(x)))	→	prime1(s(s(x)),s(x))	(3)
prime1(x,0)	→	false	(4)
prime1(x,s(0))	→	true	(5)
prime1(x,s(s(y)))	→	and(not(divp(s(s(y)),x)),prime1(x,s(y)))	(6)
divp(x,y)	→	=(rem(x,y),0)	(7)

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.

prime1^#(x,s(s(y)))	→	prime1^#(x,s(y))	(8)
prime^#(s(s(x)))	→	prime1^#(s(s(x)),s(x))	(9)
prime1^#(x,s(s(y)))	→	divp^#(s(s(y)),x)	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

prime1^#(x,s(s(y)))

→

prime1^#(x,s(y))

(8)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[prime(x₁)]	=	0
[and(x₁, x₂)]	=	0
[false]	=	0
[true]	=	0
[prime^#(x₁)]	=	0
[0]	=	0
[=(x₁, x₂)]	=	0
[prime1^#(x₁, x₂)]	=	x₂ + 0
[prime1(x₁, x₂)]	=	0
[rem(x₁, x₂)]	=	0
[divp^#(x₁, x₂)]	=	0
[divp(x₁, x₂)]	=	0
[not(x₁)]	=	0

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

prime1^#(x,s(s(y)))

→

prime1^#(x,s(y))

(8)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.