Certification Problem

Input (TPDB TRS_Standard/Applicative_first_order_05/13)

The rewrite relation of the following TRS is considered.

app(app(*,x),app(app(+,y),z))	→	app(app(+,app(app(,x),y)),app(app(,x),z))	(1)
app(app(*,app(app(+,y),z)),x)	→	app(app(+,app(app(,x),y)),app(app(,x),z))	(2)
app(app(,app(app(,x),y)),z)	→	app(app(,x),app(app(,y),z))	(3)
app(app(+,app(app(+,x),y)),z)	→	app(app(+,x),app(app(+,y),z))	(4)
app(app(map,f),nil)	→	nil	(5)
app(app(map,f),app(app(cons,x),xs))	→	app(app(cons,app(f,x)),app(app(map,f),xs))	(6)
app(app(filter,f),nil)	→	nil	(7)
app(app(filter,f),app(app(cons,x),xs))	→	app(app(app(app(filter2,app(f,x)),f),x),xs)	(8)
app(app(app(app(filter2,true),f),x),xs)	→	app(app(cons,x),app(app(filter,f),xs))	(9)
app(app(app(app(filter2,false),f),x),xs)	→	app(app(filter,f),xs)	(10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Uncurrying

We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.

*	is mapped to	*,	*1(x₁),	*2(x₁, x₂)
+	is mapped to	+,	+1(x₁),	+2(x₁, x₂)
map	is mapped to	map,	map1(x₁),	map2(x₁, x₂)
nil	is mapped to	nil
cons	is mapped to	cons,	cons1(x₁),	cons2(x₁, x₂)
filter	is mapped to	filter,	filter1(x₁),	filter3(x₁, x₂)
filter2	is mapped to	filter2,	filter21(x₁),	filter22(x₁, x₂),	filter23(x₁, x₂, x₃),	filter24(x₁,...,x₄)
true	is mapped to	true
false	is mapped to	false

There are no uncurry rules.
No rules have to be added for the eta-expansion.

Uncurrying the rules and adding the uncurrying rules yields the new set of rules

*2(x,+2(y,z))	→	+2(2(x,y),2(x,z))	(25)
*2(+2(y,z),x)	→	+2(2(x,y),2(x,z))	(26)
2(2(x,y),z)	→	2(x,2(y,z))	(27)
+2(+2(x,y),z)	→	+2(x,+2(y,z))	(28)
map2(f,nil)	→	nil	(29)
map2(f,cons2(x,xs))	→	cons2(app(f,x),map2(f,xs))	(30)
filter3(f,nil)	→	nil	(31)
filter3(f,cons2(x,xs))	→	filter24(app(f,x),f,x,xs)	(32)
filter24(true,f,x,xs)	→	cons2(x,filter3(f,xs))	(33)
filter24(false,f,x,xs)	→	filter3(f,xs)	(34)
app(*,y1)	→	*1(y1)	(11)
app(*1(x0),y1)	→	*2(x0,y1)	(12)
app(+,y1)	→	+1(y1)	(13)
app(+1(x0),y1)	→	+2(x0,y1)	(14)
app(map,y1)	→	map1(y1)	(15)
app(map1(x0),y1)	→	map2(x0,y1)	(16)
app(cons,y1)	→	cons1(y1)	(17)
app(cons1(x0),y1)	→	cons2(x0,y1)	(18)
app(filter,y1)	→	filter1(y1)	(19)
app(filter1(x0),y1)	→	filter3(x0,y1)	(20)
app(filter2,y1)	→	filter21(y1)	(21)
app(filter21(x0),y1)	→	filter22(x0,y1)	(22)
app(filter22(x0,x1),y1)	→	filter23(x0,x1,y1)	(23)
app(filter23(x0,x1,x2),y1)	→	filter24(x0,x1,x2,y1)	(24)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

*2^#(x,+2(y,z))	→	+2^#(2(x,y),2(x,z))	(35)
*2^#(x,+2(y,z))	→	*2^#(x,y)	(36)
*2^#(x,+2(y,z))	→	*2^#(x,z)	(37)
*2^#(+2(y,z),x)	→	+2^#(2(x,y),2(x,z))	(38)
*2^#(+2(y,z),x)	→	*2^#(x,y)	(39)
*2^#(+2(y,z),x)	→	*2^#(x,z)	(40)
2^#(2(x,y),z)	→	2^#(x,2(y,z))	(41)
2^#(2(x,y),z)	→	*2^#(y,z)	(42)
+2^#(+2(x,y),z)	→	+2^#(x,+2(y,z))	(43)
+2^#(+2(x,y),z)	→	+2^#(y,z)	(44)
map2^#(f,cons2(x,xs))	→	app^#(f,x)	(45)
map2^#(f,cons2(x,xs))	→	map2^#(f,xs)	(46)
filter3^#(f,cons2(x,xs))	→	filter24^#(app(f,x),f,x,xs)	(47)
filter3^#(f,cons2(x,xs))	→	app^#(f,x)	(48)
filter24^#(true,f,x,xs)	→	filter3^#(f,xs)	(49)
filter24^#(false,f,x,xs)	→	filter3^#(f,xs)	(50)
app^#(*1(x0),y1)	→	*2^#(x0,y1)	(51)
app^#(+1(x0),y1)	→	+2^#(x0,y1)	(52)
app^#(map1(x0),y1)	→	map2^#(x0,y1)	(53)
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(54)
app^#(filter23(x0,x1,x2),y1)	→	filter24^#(x0,x1,x2,y1)	(55)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

app^#(map1(x0),y1)	→	map2^#(x0,y1)	(53)
map2^#(f,cons2(x,xs))	→	app^#(f,x)	(45)
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(54)
filter3^#(f,cons2(x,xs))	→	app^#(f,x)	(48)
app^#(filter23(x0,x1,x2),y1)	→	filter24^#(x0,x1,x2,y1)	(55)
filter24^#(true,f,x,xs)	→	filter3^#(f,xs)	(49)
filter24^#(false,f,x,xs)	→	filter3^#(f,xs)	(50)
map2^#(f,cons2(x,xs))	→	map2^#(f,xs)	(46)

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[map1(x₁)]	=	1 · x₁
[cons2(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[filter1(x₁)]	=	1 · x₁
[filter23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[true]	=	0
[false]	=	0
[map2^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[app^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[filter3^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[filter24^#(x₁,...,x₄)]	=	1 · x₁ + 1 · x₂ + 1 · x₃ + 1 · x₄

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.1.1.1 Size-Change Termination

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

map2^#(f,cons2(x,xs))	→	app^#(f,x)	(45)

1	≥	1
2	>	2
map2^#(f,cons2(x,xs))	→	map2^#(f,xs)	(46)

1	≥	1
2	>	2
filter3^#(f,cons2(x,xs))	→	app^#(f,x)	(48)

1	≥	1
2	>	2
app^#(map1(x0),y1)	→	map2^#(x0,y1)	(53)

1	>	1
2	≥	2
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(54)

1	>	1
2	≥	2
app^#(filter23(x0,x1,x2),y1)	→	filter24^#(x0,x1,x2,y1)	(55)

1	>	1
1	>	2
1	>	3
2	≥	4
filter24^#(true,f,x,xs)	→	filter3^#(f,xs)	(49)

2	≥	1
4	≥	2
filter24^#(false,f,x,xs)	→	filter3^#(f,xs)	(50)

2	≥	1
4	≥	2

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

The 2^nd component contains the pair

*2^#(x,+2(y,z))	→	*2^#(x,z)	(37)
*2^#(x,+2(y,z))	→	*2^#(x,y)	(36)
*2^#(+2(y,z),x)	→	*2^#(x,y)	(39)
*2^#(+2(y,z),x)	→	*2^#(x,z)	(40)
2^#(2(x,y),z)	→	2^#(x,2(y,z))	(41)
2^#(2(x,y),z)	→	*2^#(y,z)	(42)

1.1.1.2 Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

[*2^#(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂
[+2(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁
[*2(x₁, x₂)]	=	1 · x₂ + 1 · x₁ + 1 · x₁ · x₂

together with the usable rules

*2(x,+2(y,z))	→	+2(2(x,y),2(x,z))	(25)
*2(+2(y,z),x)	→	+2(2(x,y),2(x,z))	(26)
2(2(x,y),z)	→	2(x,2(y,z))	(27)
+2(+2(x,y),z)	→	+2(x,+2(y,z))	(28)

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

*2^#(x,+2(y,z))	→	*2^#(x,z)	(37)
*2^#(x,+2(y,z))	→	*2^#(x,y)	(36)
*2^#(+2(y,z),x)	→	*2^#(x,y)	(39)
*2^#(+2(y,z),x)	→	*2^#(x,z)	(40)

could be deleted.

1.1.1.2.1 Size-Change Termination