Certification Problem

Input (TPDB TRS_Standard/Beerendonk_07/5)

The rewrite relation of the following TRS is considered.

cond(true,x)	→	cond(and(even(x),gr(x,0)),p(x))	(1)
and(x,false)	→	false	(2)
and(false,x)	→	false	(3)
and(true,true)	→	true	(4)
even(0)	→	true	(5)
even(s(0))	→	false	(6)
even(s(s(x)))	→	even(x)	(7)
gr(0,x)	→	false	(8)
gr(s(x),0)	→	true	(9)
gr(s(x),s(y))	→	gr(x,y)	(10)
p(0)	→	0	(11)
p(s(x))	→	x	(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.

cond^#(true,x)	→	p^#(x)	(13)
cond^#(true,x)	→	gr^#(x,0)	(14)
cond^#(true,x)	→	even^#(x)	(15)
cond^#(true,x)	→	and^#(even(x),gr(x,0))	(16)
cond^#(true,x)	→	cond^#(and(even(x),gr(x,0)),p(x))	(17)
even^#(s(s(x)))	→	even^#(x)	(18)
gr^#(s(x),s(y))	→	gr^#(x,y)	(19)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

cond^#(true,x)

→

cond^#(and(even(x),gr(x,0)),p(x))

(17)

1.1.1 Reduction Pair Processor with Usable Rules

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

[gr(x₁, x₂)]	=	-2 · x₁ + 0 · x₂ + 0
[s(x₁)]	=	3 · x₁ + 4
[0]	=	0
[and(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + 0
[cond^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[true]	=	2
[false]	=	0
[p(x₁)]	=	-3 · x₁ + 0
[even(x₁)]	=	-∞ · x₁ + 0

together with the usable rules

p(0)	→	0	(11)
p(s(x))	→	x	(12)
gr(0,x)	→	false	(8)
gr(s(x),0)	→	true	(9)
and(x,false)	→	false	(2)
and(false,x)	→	false	(3)
and(true,true)	→	true	(4)

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

cond^#(true,x)

→

cond^#(and(even(x),gr(x,0)),p(x))

(17)

could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair
even^#(s(s(x))) → even^#(x) (18)

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) (18)

1 > 1

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