Certification Problem

Input (TPDB TRS_Standard/Applicative_05/Ex6_11)

The rewrite relation of the following TRS is considered.

app(app(F,app(app(F,f),x)),x)

→

app(app(F,app(G,app(app(F,f),x))),app(f,x))

(1)

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₁),	F2(x₁, x₂)
G	is mapped to	G,	G1(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

F2(F2(f,x),x)	→	F2(G1(F2(f,x)),app(f,x))	(5)
app(F,y1)	→	F1(y1)	(2)
app(F1(x0),y1)	→	F2(x0,y1)	(3)
app(G,y1)	→	G1(y1)	(4)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

F2^#(F2(f,x),x)	→	F2^#(G1(F2(f,x)),app(f,x))	(6)
F2^#(F2(f,x),x)	→	app^#(f,x)	(7)
app^#(F1(x0),y1)	→	F2^#(x0,y1)	(8)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

F2^#(F2(f,x),x) → app^#(f,x) (7)

app^#(F1(x0),y1) → F2^#(x0,y1) (8)

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

[F2(x₁, x₂)] = 1 · x₁ + 1 · x₂

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

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

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

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

app^#(F1(x0),y1) → F2^#(x0,y1) (8)

1 > 1

2 ≥ 2

F2^#(F2(f,x),x) → app^#(f,x) (7)

1 > 1

1 > 2

2 ≥ 2

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