Certification Problem

Input (TPDB TRS_Standard/Applicative_05/Ex6Recursor)

The rewrite relation of the following TRS is considered.

app(app(app(rec,f),x),0)	→	x	(1)
app(app(app(rec,f),x),app(s,y))	→	app(app(f,app(s,y)),app(app(app(rec,f),x),y))	(2)

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.

rec	is mapped to	rec,	rec1(x₁),	rec2(x₁, x₂),	rec3(x₁, x₂, x₃)
0	is mapped to	0
s	is mapped to	s,	s1(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

rec3(f,x,0)	→	x	(7)
rec3(f,x,s1(y))	→	app(app(f,s1(y)),rec3(f,x,y))	(8)
app(rec,y1)	→	rec1(y1)	(3)
app(rec1(x0),y1)	→	rec2(x0,y1)	(4)
app(rec2(x0,x1),y1)	→	rec3(x0,x1,y1)	(5)
app(s,y1)	→	s1(y1)	(6)

1.1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

Hence, it suffices to show innermost termination in the following.

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

rec3^#(f,x,s1(y))	→	app^#(app(f,s1(y)),rec3(f,x,y))	(9)
rec3^#(f,x,s1(y))	→	app^#(f,s1(y))	(10)
rec3^#(f,x,s1(y))	→	rec3^#(f,x,y)	(11)
app^#(rec2(x0,x1),y1)	→	rec3^#(x0,x1,y1)	(12)

1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

[rec3^#(x₁, x₂, x₃)]

· x₁ +

· x₂ +

-∞

· x₃

[s1(x₁)]

-∞

· x₁

[app^#(x₁, x₂)]

-∞

· x₁ +

· x₂

[app(x₁, x₂)]

-∞

· x₁ +

· x₂

[rec3(x₁, x₂, x₃)]

· x₁ +

· x₂ +

-∞

· x₃

[rec2(x₁, x₂)]

· x₁ +

· x₂

[rec]

[rec1(x₁)]

· x₁

[s]

[0]

the pair

rec3^#(f,x,s1(y))

→

app^#(f,s1(y))

(10)

could be deleted.

1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 1 to get the following set of pairs

rec3^#(rec,y1,s1(y2))	→	app^#(rec1(s1(y2)),rec3(rec,y1,y2))	(13)
rec3^#(rec1(x0),y1,s1(y2))	→	app^#(rec2(x0,s1(y2)),rec3(rec1(x0),y1,y2))	(14)
rec3^#(rec2(x0,x1),y1,s1(y2))	→	app^#(rec3(x0,x1,s1(y2)),rec3(rec2(x0,x1),y1,y2))	(15)
rec3^#(s,y1,s1(y2))	→	app^#(s1(s1(y2)),rec3(s,y1,y2))	(16)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

rec3^#(f,x,s1(y))	→	rec3^#(f,x,y)	(11)
rec3^#(rec1(x0),y1,s1(y2))	→	app^#(rec2(x0,s1(y2)),rec3(rec1(x0),y1,y2))	(14)
app^#(rec2(x0,x1),y1)	→	rec3^#(x0,x1,y1)	(12)
rec3^#(rec2(x0,x1),y1,s1(y2))	→	app^#(rec3(x0,x1,s1(y2)),rec3(rec2(x0,x1),y1,y2))	(15)

1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1 Forward Instantiation Processor

We instantiate the pair to the following set of pairs

rec3^#(x0,x1,s1(s1(y_2)))	→	rec3^#(x0,x1,s1(y_2))	(18)
rec3^#(rec1(y_0),x1,s1(s1(y_2)))	→	rec3^#(rec1(y_0),x1,s1(y_2))	(19)
rec3^#(rec2(y_0,y_1),x1,s1(s1(y_3)))	→	rec3^#(rec2(y_0,y_1),x1,s1(y_3))	(20)

1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

We instantiate the pair to the following set of pairs

app^#(rec2(rec1(y_0),x1),s1(y_2))	→	rec3^#(rec1(y_0),x1,s1(y_2))	(21)
app^#(rec2(rec2(y_0,y_1),x1),s1(y_3))	→	rec3^#(rec2(y_0,y_1),x1,s1(y_3))	(22)
app^#(rec2(x0,x1),s1(s1(y_2)))	→	rec3^#(x0,x1,s1(s1(y_2)))	(23)
app^#(rec2(rec1(y_0),x1),s1(s1(y_2)))	→	rec3^#(rec1(y_0),x1,s1(s1(y_2)))	(24)
app^#(rec2(rec2(y_0,y_1),x1),s1(s1(y_3)))	→	rec3^#(rec2(y_0,y_1),x1,s1(s1(y_3)))	(25)

1.1.1.1.1.1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 2 to get the following set of pairs

rec3^#(rec1(y0),x1,s1(0))	→	app^#(rec2(y0,s1(0)),x1)	(26)
rec3^#(rec1(y0),x1,s1(s1(x2)))	→	app^#(rec2(y0,s1(s1(x2))),app(app(rec1(y0),s1(x2)),rec3(rec1(y0),x1,x2)))	(27)

1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position 2 to get the following set of pairs

rec3^#(rec2(y0,y1),x1,s1(0))	→	app^#(app(app(y0,s1(0)),rec3(y0,y1,0)),x1)	(30)
rec3^#(rec2(y0,y1),x1,s1(s1(x2)))	→	app^#(app(app(y0,s1(s1(x2))),rec3(y0,y1,s1(x2))),app(app(rec2(y0,y1),s1(x2)),rec3(rec2(y0,y1),x1,x2)))	(31)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rewriting Processor

We rewrite the right hand side of the pair resulting in

→

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

We instantiate the pair to the following set of pairs

rec3^#(rec1(rec1(y_0)),s1(y_2),s1(0))	→	app^#(rec2(rec1(y_0),s1(0)),s1(y_2))	(36)
rec3^#(rec1(rec2(y_0,y_1)),s1(y_3),s1(0))	→	app^#(rec2(rec2(y_0,y_1),s1(0)),s1(y_3))	(37)
rec3^#(rec1(x0),s1(s1(y_2)),s1(0))	→	app^#(rec2(x0,s1(0)),s1(s1(y_2)))	(38)
rec3^#(rec1(rec1(y_0)),s1(s1(y_2)),s1(0))	→	app^#(rec2(rec1(y_0),s1(0)),s1(s1(y_2)))	(39)
rec3^#(rec1(rec2(y_0,y_1)),s1(s1(y_3)),s1(0))	→	app^#(rec2(rec2(y_0,y_1),s1(0)),s1(s1(y_3)))	(40)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

[rec3^#(x₁, x₂, x₃)]

-∞

0	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂ +

0	0	0
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[s1(x₁)]

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁

[rec1(x₁)]

-∞

0	-∞	-∞
1	0	0
0	0	0

· x₁

[rec2(x₁, x₂)]

-∞

0	0	-∞
1	0	0
2	1	1

· x₁ +

0	-∞	-∞
0	-∞	-∞
0	0	0

· x₂

[app^#(x₁, x₂)]

-∞

0	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂

[rec3(x₁, x₂, x₃)]

1	0	0
2	1	1
2	1	1

· x₁ +

0	-∞	-∞
1	0	0
1	0	0

· x₂ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[0]

[app(x₁, x₂)]

0	0	-∞
1	-∞	0
-∞	1	0

· x₁ +

0	-∞	-∞
1	0	0
0	0	0

· x₂

[rec]

[s]

-∞

the pairs

rec3^#(rec1(rec2(y_0,y_1)),s1(y_3),s1(0))	→	app^#(rec2(rec2(y_0,y_1),s1(0)),s1(y_3))	(37)
rec3^#(rec1(rec2(y_0,y_1)),s1(s1(y_3)),s1(0))	→	app^#(rec2(rec2(y_0,y_1),s1(0)),s1(s1(y_3)))	(40)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

[rec3^#(x₁, x₂, x₃)]

-∞

1	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂ +

-∞	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[s1(x₁)]

-∞

-∞	-∞	-∞
-∞	-∞	-∞
0	0	0

· x₁

[rec1(x₁)]

-∞

0	0	-∞
-∞	0	-∞
0	0	0

· x₁

[rec2(x₁, x₂)]

-∞

0	0	-∞
1	1	-∞
0	-∞	0

· x₁ +

-∞	-∞	-∞
0	0	-∞
0	0	0

· x₂

[app^#(x₁, x₂)]

-∞

0	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂

[rec3(x₁, x₂, x₃)]

1	1	-∞
1	1	-∞
1	1	0

· x₁ +

0	0	-∞
0	0	-∞
0	0	0

· x₂ +

-∞	-∞	-∞
-∞	-∞	-∞
0	0	0

· x₃

[0]

[app(x₁, x₂)]

0	0	-∞
1	0	-∞
0	0	0

· x₁ +

0	0	-∞
0	0	-∞
0	0	0

· x₂

[rec]

-∞

[s]

-∞

the pairs

app^#(rec2(rec2(y_0,y_1),x1),s1(y_3))	→	rec3^#(rec2(y_0,y_1),x1,s1(y_3))	(22)
app^#(rec2(rec2(y_0,y_1),x1),s1(s1(y_3)))	→	rec3^#(rec2(y_0,y_1),x1,s1(s1(y_3)))	(25)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

[rec3^#(x₁, x₂, x₃)]

-∞

0	0	1
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

0	0	0
-∞	-∞	-∞
-∞	-∞	-∞

· x₂ +

-∞	-∞	0
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[s1(x₁)]

-∞

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁

[rec1(x₁)]

-∞

0	0	0
-∞	-∞	0
0	-∞	0

· x₁

[rec2(x₁, x₂)]

-∞

0	-∞	-∞
0	0	-∞
1	0	1

· x₁ +

0	0	-∞
-∞	-∞	-∞
0	0	0

· x₂

[app^#(x₁, x₂)]

-∞

0	0	0
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂

[rec3(x₁, x₂, x₃)]

1	0	1
1	0	1
1	0	1

· x₁ +

0	0	0
0	0	0
0	0	0

· x₂ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[0]

[app(x₁, x₂)]

0	-∞	0
0	0	0
1	0	0

· x₁ +

0	0	0
-∞	-∞	0
0	0	0

· x₂

[rec]

[s]

-∞

the pair

rec3^#(rec2(y0,y1),x1,s1(0))

→

app^#(app(app(y0,s1(0)),y1),x1)

(32)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals

[rec3^#(x₁, x₂, x₃)]

-∞

0	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂ +

0	-∞	0
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[s1(x₁)]

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁

[rec1(x₁)]

0	0	0
-∞	0	-∞
0	0	0

· x₁

[rec2(x₁, x₂)]

-∞

3	3	3
0	0	0
0	0	0

· x₁ +

0	3	0
-∞	0	-∞
0	0	0

· x₂

[app^#(x₁, x₂)]

-∞

-∞	0	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₂

[rec3(x₁, x₂, x₃)]

3	3	3
0	0	0
3	3	3

· x₁ +

0	3	0
-∞	0	-∞
0	3	0

· x₂ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

· x₃

[app(x₁, x₂)]

0	0	3
-∞	0	0
0	0	0

· x₁ +

0	3	0
-∞	0	-∞
0	0	0

· x₂

[0]

[rec]

[s]

-∞

the pair

rec3^#(rec2(y0,y1),x1,s1(s1(x2)))

→

app^#(app(app(y0,s1(s1(x2))),app(app(y0,s1(x2)),rec3(y0,y1,x2))),app(app(app(y0,s1(x2)),rec3(y0,y1,x2)),rec3(rec2(y0,y1),x1,x2)))

(35)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(rec1)

weight(rec1)

in combination with the following argument filter

π(rec3^#)	=	1
π(rec1)	=	[1]
π(rec2)	=	1
π(app^#)	=	1

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

rec3^#(rec1(y0),x1,s1(s1(x2)))	→	app^#(rec2(y0,s1(s1(x2))),rec3(y0,s1(x2),rec3(rec1(y0),x1,x2)))	(29)
rec3^#(rec1(rec1(y_0)),s1(y_2),s1(0))	→	app^#(rec2(rec1(y_0),s1(0)),s1(y_2))	(36)
rec3^#(rec1(x0),s1(s1(y_2)),s1(0))	→	app^#(rec2(x0,s1(0)),s1(s1(y_2)))	(38)
rec3^#(rec1(rec1(y_0)),s1(s1(y_2)),s1(0))	→	app^#(rec2(rec1(y_0),s1(0)),s1(s1(y_2)))	(39)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

rec3^#(x0,x1,s1(s1(y_2)))	→	rec3^#(x0,x1,s1(y_2))	(18)
rec3^#(rec1(y_0),x1,s1(s1(y_2)))	→	rec3^#(rec1(y_0),x1,s1(y_2))	(19)
rec3^#(rec2(y_0,y_1),x1,s1(s1(y_3)))	→	rec3^#(rec2(y_0,y_1),x1,s1(y_3))	(20)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

There are no rules.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

There are no lhss.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.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.

rec3^#(rec2(y_0,y_1),x1,s1(s1(y_3)))	→	rec3^#(rec2(y_0,y_1),x1,s1(y_3))	(20)

1	≥	1
2	≥	2
3	>	3
rec3^#(x0,x1,s1(s1(y_2)))	→	rec3^#(x0,x1,s1(y_2))	(18)

1	≥	1
2	≥	2
3	>	3
rec3^#(rec1(y_0),x1,s1(s1(y_2)))	→	rec3^#(rec1(y_0),x1,s1(y_2))	(19)

1	≥	1
2	≥	2
3	>	3

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