Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.29)

The rewrite relation of the following TRS is considered.

even(0)	→	true	(1)
even(s(0))	→	false	(2)
even(s(s(x)))	→	even(x)	(3)
half(0)	→	0	(4)
half(s(s(x)))	→	s(half(x))	(5)
plus(0,y)	→	y	(6)
plus(s(x),y)	→	s(plus(x,y))	(7)
times(0,y)	→	0	(8)
times(s(x),y)	→	if_times(even(s(x)),s(x),y)	(9)
if_times(true,s(x),y)	→	plus(times(half(s(x)),y),times(half(s(x)),y))	(10)
if_times(false,s(x),y)	→	plus(y,times(x,y))	(11)

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.

even^#(s(s(x)))	→	even^#(x)	(12)
half^#(s(s(x)))	→	half^#(x)	(13)
plus^#(s(x),y)	→	plus^#(x,y)	(14)
times^#(s(x),y)	→	even^#(s(x))	(15)
times^#(s(x),y)	→	if_times^#(even(s(x)),s(x),y)	(16)
if_times^#(true,s(x),y)	→	half^#(s(x))	(17)
if_times^#(true,s(x),y)	→	times^#(half(s(x)),y)	(18)
if_times^#(true,s(x),y)	→	plus^#(times(half(s(x)),y),times(half(s(x)),y))	(19)
if_times^#(false,s(x),y)	→	times^#(x,y)	(20)
if_times^#(false,s(x),y)	→	plus^#(y,times(x,y))	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

if_times^#(false,s(x),y)	→	times^#(x,y)	(20)
times^#(s(x),y)	→	if_times^#(even(s(x)),s(x),y)	(16)
if_times^#(true,s(x),y)	→	times^#(half(s(x)),y)	(18)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(if_times^#)	=	{ 2 }
π(times^#)	=	{ 1 }
π(half)	=	{ 1 }
π(s)	=	{ 1, 1, 1 }

to remove the pairs:

if_times^#(false,s(x),y)

→

times^#(x,y)

(20)

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[false]	=	0
[even(x₁)]	=	3 · x₁ + 4
[s(x₁)]	=	1 · x₁ + 1
[half(x₁)]	=	-1 · x₁ + 0
[0]	=	0
[times^#(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[if_times^#(x₁, x₂, x₃)]	=	-4 · x₁ + -1 · x₂ + -∞ · x₃ + 0
[true]	=	1

together with the usable rules

even(s(0))	→	false	(2)
even(s(s(x)))	→	even(x)	(3)
even(0)	→	true	(1)
half(s(s(x)))	→	s(half(x))	(5)
half(0)	→	0	(4)

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

times^#(s(x),y)

→

if_times^#(even(s(x)),s(x),y)

(16)

could be deleted.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair
plus^#(s(x),y) → plus^#(x,y) (14)

1.1.2 Size-Change Termination

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

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

2 ≥ 2

1 > 1

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

1.1.3 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 4^th component contains the pair
even^#(s(s(x))) → even^#(x) (12)

1.1.4 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) (12)

1 > 1

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