Certification Problem

Input (TPDB TRS_Standard/Applicative_first_order_05/#3.48)

The rewrite relation of the following TRS is considered.

app(f,0)	→	true	(1)
app(f,1)	→	false	(2)
app(f,app(s,x))	→	app(f,x)	(3)
app(app(app(if,true),app(s,x)),app(s,y))	→	app(s,x)	(4)
app(app(app(if,false),app(s,x)),app(s,y))	→	app(s,y)	(5)
app(app(g,x),app(c,y))	→	app(c,app(app(g,x),y))	(6)
app(app(g,x),app(c,y))	→	app(app(g,x),app(app(app(if,app(f,x)),app(c,app(app(g,app(s,x)),y))),app(c,y)))	(7)
app(app(map,fun),nil)	→	nil	(8)
app(app(map,fun),app(app(cons,x),xs))	→	app(app(cons,app(fun,x)),app(app(map,fun),xs))	(9)
app(app(filter,fun),nil)	→	nil	(10)
app(app(filter,fun),app(app(cons,x),xs))	→	app(app(app(app(filter2,app(fun,x)),fun),x),xs)	(11)
app(app(app(app(filter2,true),fun),x),xs)	→	app(app(cons,x),app(app(filter,fun),xs))	(12)
app(app(app(app(filter2,false),fun),x),xs)	→	app(app(filter,fun),xs)	(13)

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.

f	is mapped to	f,	f1(x₁)
0	is mapped to	0
true	is mapped to	true
1	is mapped to	1
false	is mapped to	false
s	is mapped to	s,	s1(x₁)
if	is mapped to	if,	if1(x₁),	if2(x₁, x₂),	if3(x₁, x₂, x₃)
g	is mapped to	g,	g1(x₁),	g2(x₁, x₂)
c	is mapped to	c,	c1(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₄)

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

f1(0)	→	true	(32)
f1(1)	→	false	(33)
f1(s1(x))	→	f1(x)	(34)
if3(true,s1(x),s1(y))	→	s1(x)	(35)
if3(false,s1(x),s1(y))	→	s1(y)	(36)
g2(x,c1(y))	→	c1(g2(x,y))	(37)
g2(x,c1(y))	→	g2(x,if3(f1(x),c1(g2(s1(x),y)),c1(y)))	(38)
map2(fun,nil)	→	nil	(39)
map2(fun,cons2(x,xs))	→	cons2(app(fun,x),map2(fun,xs))	(40)
filter3(fun,nil)	→	nil	(41)
filter3(fun,cons2(x,xs))	→	filter24(app(fun,x),fun,x,xs)	(42)
filter24(true,fun,x,xs)	→	cons2(x,filter3(fun,xs))	(43)
filter24(false,fun,x,xs)	→	filter3(fun,xs)	(44)
app(f,y1)	→	f1(y1)	(14)
app(s,y1)	→	s1(y1)	(15)
app(if,y1)	→	if1(y1)	(16)
app(if1(x0),y1)	→	if2(x0,y1)	(17)
app(if2(x0,x1),y1)	→	if3(x0,x1,y1)	(18)
app(g,y1)	→	g1(y1)	(19)
app(g1(x0),y1)	→	g2(x0,y1)	(20)
app(c,y1)	→	c1(y1)	(21)
app(map,y1)	→	map1(y1)	(22)
app(map1(x0),y1)	→	map2(x0,y1)	(23)
app(cons,y1)	→	cons1(y1)	(24)
app(cons1(x0),y1)	→	cons2(x0,y1)	(25)
app(filter,y1)	→	filter1(y1)	(26)
app(filter1(x0),y1)	→	filter3(x0,y1)	(27)
app(filter2,y1)	→	filter21(y1)	(28)
app(filter21(x0),y1)	→	filter22(x0,y1)	(29)
app(filter22(x0,x1),y1)	→	filter23(x0,x1,y1)	(30)
app(filter23(x0,x1,x2),y1)	→	filter24(x0,x1,x2,y1)	(31)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f1^#(s1(x))	→	f1^#(x)	(45)
g2^#(x,c1(y))	→	g2^#(x,y)	(46)
g2^#(x,c1(y))	→	g2^#(x,if3(f1(x),c1(g2(s1(x),y)),c1(y)))	(47)
g2^#(x,c1(y))	→	if3^#(f1(x),c1(g2(s1(x),y)),c1(y))	(48)
g2^#(x,c1(y))	→	f1^#(x)	(49)
g2^#(x,c1(y))	→	g2^#(s1(x),y)	(50)
map2^#(fun,cons2(x,xs))	→	app^#(fun,x)	(51)
map2^#(fun,cons2(x,xs))	→	map2^#(fun,xs)	(52)
filter3^#(fun,cons2(x,xs))	→	filter24^#(app(fun,x),fun,x,xs)	(53)
filter3^#(fun,cons2(x,xs))	→	app^#(fun,x)	(54)
filter24^#(true,fun,x,xs)	→	filter3^#(fun,xs)	(55)
filter24^#(false,fun,x,xs)	→	filter3^#(fun,xs)	(56)
app^#(f,y1)	→	f1^#(y1)	(57)
app^#(if2(x0,x1),y1)	→	if3^#(x0,x1,y1)	(58)
app^#(g1(x0),y1)	→	g2^#(x0,y1)	(59)
app^#(map1(x0),y1)	→	map2^#(x0,y1)	(60)
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(61)
app^#(filter23(x0,x1,x2),y1)	→	filter24^#(x0,x1,x2,y1)	(62)

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)	(60)
map2^#(fun,cons2(x,xs))	→	app^#(fun,x)	(51)
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(61)
filter3^#(fun,cons2(x,xs))	→	filter24^#(app(fun,x),fun,x,xs)	(53)
filter24^#(true,fun,x,xs)	→	filter3^#(fun,xs)	(55)
filter3^#(fun,cons2(x,xs))	→	app^#(fun,x)	(54)
app^#(filter23(x0,x1,x2),y1)	→	filter24^#(x0,x1,x2,y1)	(62)
filter24^#(false,fun,x,xs)	→	filter3^#(fun,xs)	(56)
map2^#(fun,cons2(x,xs))	→	map2^#(fun,xs)	(52)

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^#(fun,cons2(x,xs))	→	app^#(fun,x)	(51)

1	≥	1
2	>	2
map2^#(fun,cons2(x,xs))	→	map2^#(fun,xs)	(52)

1	≥	1
2	>	2
filter3^#(fun,cons2(x,xs))	→	app^#(fun,x)	(54)

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

1	>	1
2	≥	2
filter3^#(fun,cons2(x,xs))	→	filter24^#(app(fun,x),fun,x,xs)	(53)

1	≥	2
2	>	3
2	>	4
app^#(filter1(x0),y1)	→	filter3^#(x0,y1)	(61)

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

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

2	≥	1
4	≥	2
filter24^#(false,fun,x,xs)	→	filter3^#(fun,xs)	(56)

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

g2^#(x,c1(y)) → g2^#(s1(x),y) (50)

g2^#(x,c1(y)) → g2^#(x,y) (46)

1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[c1(x₁)] = 1 · x₁

[s1(x₁)] = 1 · x₁

[g2^#(x₁, 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.2.1 Size-Change Termination

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

g2^#(x,c1(y)) → g2^#(s1(x),y) (50)

2 > 2

g2^#(x,c1(y)) → g2^#(x,y) (46)

1 ≥ 1

2 > 2

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

1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[s1(x₁)] = 1 · x₁

[f1^#(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.3.1 Size-Change Termination

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

f1^#(s1(x)) → f1^#(x) (45)

1 > 1

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