Certification Problem

Input (TPDB TRS_Standard/Beerendonk_07/10)

The rewrite relation of the following TRS is considered.

cond1(true,x)	→	cond2(even(x),x)	(1)
cond2(true,x)	→	cond1(neq(x,0),div2(x))	(2)
cond2(false,x)	→	cond1(neq(x,0),p(x))	(3)
neq(0,0)	→	false	(4)
neq(0,s(x))	→	true	(5)
neq(s(x),0)	→	true	(6)
neq(s(x),s(y))	→	neq(x,y)	(7)
even(0)	→	true	(8)
even(s(0))	→	false	(9)
even(s(s(x)))	→	even(x)	(10)
div2(0)	→	0	(11)
div2(s(0))	→	0	(12)
div2(s(s(x)))	→	s(div2(x))	(13)
p(0)	→	0	(14)
p(s(x))	→	x	(15)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

cond1^#(true,x)	→	even^#(x)	(16)
cond1^#(true,x)	→	cond2^#(even(x),x)	(17)
cond2^#(true,x)	→	div2^#(x)	(18)
cond2^#(true,x)	→	neq^#(x,0)	(19)
cond2^#(true,x)	→	cond1^#(neq(x,0),div2(x))	(20)
cond2^#(false,x)	→	p^#(x)	(21)
cond2^#(false,x)	→	neq^#(x,0)	(22)
cond2^#(false,x)	→	cond1^#(neq(x,0),p(x))	(23)
neq^#(s(x),s(y))	→	neq^#(x,y)	(24)
even^#(s(s(x)))	→	even^#(x)	(25)
div2^#(s(s(x)))	→	div2^#(x)	(26)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

cond2^#(false,x)	→	cond1^#(neq(x,0),p(x))	(23)
cond1^#(true,x)	→	cond2^#(even(x),x)	(17)
cond2^#(true,x)	→	cond1^#(neq(x,0),div2(x))	(20)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the rationals with delta = 1/64

[0]	=	0
[p(x₁)]	=	1/2 · x₁ + 0
[neq(x₁, x₂)]	=	1/2 · x₁ + 0 · x₂ + 1/2
[true]	=	2
[false]	=	0
[cond1^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 1
[s(x₁)]	=	2 · x₁ + 3
[cond2^#(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 2
[div2(x₁)]	=	1/2 · x₁ + 0
[even(x₁)]	=	0 · x₁ + 0

together with the usable rules

p(0)	→	0	(14)
p(s(x))	→	x	(15)
neq(0,0)	→	false	(4)
neq(s(x),0)	→	true	(6)
div2(0)	→	0	(11)
div2(s(0))	→	0	(12)
div2(s(s(x)))	→	s(div2(x))	(13)

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

cond1^#(true,x)

→

cond2^#(even(x),x)

(17)

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
even^#(s(s(x))) → even^#(x) (25)

1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

even^#(s(s(x))) → even^#(x) (25)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
div2^#(s(s(x))) → div2^#(x) (26)

1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

div2^#(s(s(x))) → div2^#(x) (26)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.