Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann17)

The rewrite relation of the following TRS is considered.

sum(cons(s(n),x),cons(m,y))	→	sum(cons(n,x),cons(s(m),y))	(1)
sum(cons(0,x),y)	→	sum(x,y)	(2)
sum(nil,y)	→	y	(3)
empty(nil)	→	true	(4)
empty(cons(n,x))	→	false	(5)
tail(nil)	→	nil	(6)
tail(cons(n,x))	→	x	(7)
head(cons(n,x))	→	n	(8)
weight(x)	→	if(empty(x),empty(tail(x)),x)	(9)
if(true,b,x)	→	weight_undefined_error	(10)
if(false,b,x)	→	if2(b,x)	(11)
if2(true,x)	→	head(x)	(12)
if2(false,x)	→	weight(sum(x,cons(0,tail(tail(x)))))	(13)

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.

sum^#(cons(s(n),x),cons(m,y))	→	sum^#(cons(n,x),cons(s(m),y))	(14)
sum^#(cons(0,x),y)	→	sum^#(x,y)	(15)
weight^#(x)	→	tail^#(x)	(16)
weight^#(x)	→	empty^#(tail(x))	(17)
weight^#(x)	→	empty^#(x)	(18)
weight^#(x)	→	if^#(empty(x),empty(tail(x)),x)	(19)
if^#(false,b,x)	→	if2^#(b,x)	(20)
if2^#(true,x)	→	head^#(x)	(21)
if2^#(false,x)	→	tail^#(x)	(22)
if2^#(false,x)	→	tail^#(tail(x))	(23)
if2^#(false,x)	→	sum^#(x,cons(0,tail(tail(x))))	(24)
if2^#(false,x)	→	weight^#(sum(x,cons(0,tail(tail(x)))))	(25)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

if2^#(false,x)	→	weight^#(sum(x,cons(0,tail(tail(x)))))	(25)
weight^#(x)	→	if^#(empty(x),empty(tail(x)),x)	(19)
if^#(false,b,x)	→	if2^#(b,x)	(20)

1.1.1 Reduction Pair Processor with Usable Rules

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

[weight^#(x₁)]	=	1 · x₁ + 2
[nil]	=	0
[tail(x₁)]	=	-1 · x₁ + 0
[cons(x₁, x₂)]	=	-5 · x₁ + 1 · x₂ + 1
[0]	=	3
[if^#(x₁, x₂, x₃)]	=	-8 · x₁ + -1 · x₂ + 0 · x₃ + -∞
[empty(x₁)]	=	2 · x₁ + -∞
[s(x₁)]	=	-∞ · x₁ + 6
[false]	=	3
[if2^#(x₁, x₂)]	=	-1 · x₁ + 0 · x₂ + -∞
[true]	=	2
[sum(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + 0

together with the usable rules

tail(nil)	→	nil	(6)
tail(cons(n,x))	→	x	(7)
sum(cons(s(n),x),cons(m,y))	→	sum(cons(n,x),cons(s(m),y))	(1)
sum(cons(0,x),y)	→	sum(x,y)	(2)
sum(nil,y)	→	y	(3)
empty(nil)	→	true	(4)
empty(cons(n,x))	→	false	(5)

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

weight^#(x)

→

if^#(empty(x),empty(tail(x)),x)

(19)

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

sum^#(cons(s(n),x),cons(m,y))	→	sum^#(cons(n,x),cons(s(m),y))	(14)
sum^#(cons(0,x),y)	→	sum^#(x,y)	(15)

1.1.2 Subterm Criterion Processor

We use the projection to multisets

π(sum^#)	=	{ 1, 1 }
π(sum)	=	{ 2, 2 }
π(cons)	=	{ 2, 2 }

to remove the pairs:

sum^#(cons(0,x),y)

→

sum^#(x,y)

(15)

1.1.2.1 Subterm Criterion Processor

We use the projection to multisets

π(sum^#)	=	{ 1 }
π(cons)	=	{ 1 }

to remove the pairs:

sum^#(cons(s(n),x),cons(m,y))

→

sum^#(cons(n,x),cons(s(m),y))

(14)

1.1.2.1.1 P is empty

There are no pairs anymore.