Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann12)

The rewrite relation of the following TRS is considered.

half(0)	→	0	(1)
half(s(0))	→	0	(2)
half(s(s(x)))	→	s(half(x))	(3)
le(0,y)	→	true	(4)
le(s(x),0)	→	false	(5)
le(s(x),s(y))	→	le(x,y)	(6)
inc(0)	→	0	(7)
inc(s(x))	→	s(inc(x))	(8)
log(x)	→	log2(x,0)	(9)
log2(x,y)	→	if(le(x,s(0)),x,inc(y))	(10)
if(true,x,s(y))	→	y	(11)
if(false,x,y)	→	log2(half(x),y)	(12)

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.

half^#(s(s(x)))	→	half^#(x)	(13)
le^#(s(x),s(y))	→	le^#(x,y)	(14)
inc^#(s(x))	→	inc^#(x)	(15)
log^#(x)	→	log2^#(x,0)	(16)
log2^#(x,y)	→	inc^#(y)	(17)
log2^#(x,y)	→	le^#(x,s(0))	(18)
log2^#(x,y)	→	if^#(le(x,s(0)),x,inc(y))	(19)
if^#(false,x,y)	→	half^#(x)	(20)
if^#(false,x,y)	→	log2^#(half(x),y)	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

if^#(false,x,y)	→	log2^#(half(x),y)	(21)
log2^#(x,y)	→	if^#(le(x,s(0)),x,inc(y))	(19)

1.1.1 Reduction Pair Processor with Usable Rules

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

[true]	=	0
[if^#(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 0 · x₃ + 0
[half(x₁)]	=	1/2 · x₁ + 0
[le(x₁, x₂)]	=	1/2 · x₁ + 0 · x₂ + 0
[false]	=	1/2
[0]	=	0
[log2^#(x₁, x₂)]	=	2 · x₁ + 0 · x₂ + 0
[inc(x₁)]	=	0 · x₁ + 2
[s(x₁)]	=	1 · x₁ + 2

together with the usable rules

half(0)	→	0	(1)
half(s(0))	→	0	(2)
half(s(s(x)))	→	s(half(x))	(3)
le(0,y)	→	true	(4)
le(s(x),s(y))	→	le(x,y)	(6)
le(s(x),0)	→	false	(5)

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

if^#(false,x,y)

→

log2^#(half(x),y)

(21)

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
half^#(s(s(x))) → half^#(x) (13)

1.1.2 Size-Change Termination

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

half^#(s(s(x))) → half^#(x) (13)

1 > 1

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

1.1.3 Size-Change Termination

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

le^#(s(x),s(y)) → le^#(x,y) (14)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair
inc^#(s(x)) → inc^#(x) (15)

1.1.4 Size-Change Termination

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

inc^#(s(x)) → inc^#(x) (15)

1 > 1

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