Certification Problem

Input (TPDB TRS_Standard/CiME_04/append-hard)

The rewrite relation of the following TRS is considered.

is_empty(nil)	→	true	(1)
is_empty(cons(x,l))	→	false	(2)
hd(cons(x,l))	→	x	(3)
tl(cons(x,l))	→	l	(4)
append(l1,l2)	→	ifappend(l1,l2,is_empty(l1))	(5)
ifappend(l1,l2,true)	→	l2	(6)
ifappend(l1,l2,false)	→	cons(hd(l1),append(tl(l1),l2))	(7)

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.

append^#(l1,l2)	→	is_empty^#(l1)	(8)
append^#(l1,l2)	→	ifappend^#(l1,l2,is_empty(l1))	(9)
ifappend^#(l1,l2,false)	→	tl^#(l1)	(10)
ifappend^#(l1,l2,false)	→	append^#(tl(l1),l2)	(11)
ifappend^#(l1,l2,false)	→	hd^#(l1)	(12)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

ifappend^#(l1,l2,false)	→	append^#(tl(l1),l2)	(11)
append^#(l1,l2)	→	ifappend^#(l1,l2,is_empty(l1))	(9)

1.1.1 Reduction Pair Processor with Usable Rules

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

[false]	=	1
[is_empty(x₁)]	=	0 · x₁ + -∞
[cons(x₁, x₂)]	=	0 · x₁ + 8 · x₂ + 1
[nil]	=	1
[append^#(x₁, x₂)]	=	1 · x₁ + -∞ · x₂ + 1
[ifappend^#(x₁, x₂, x₃)]	=	0 · x₁ + -∞ · x₂ + 0 · x₃ + 0
[tl(x₁)]	=	-8 · x₁ + 0
[true]	=	0

together with the usable rules

tl(cons(x,l))	→	l	(4)
is_empty(nil)	→	true	(1)
is_empty(cons(x,l))	→	false	(2)

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

append^#(l1,l2)

→

ifappend^#(l1,l2,is_empty(l1))

(9)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.