Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/Ex1SimplyTyped)

The rewrite relation of the following TRS is considered.

app(id,x)	→	x	(1)
app(add,0)	→	id	(2)
app(app(add,app(s,x)),y)	→	app(s,app(app(add,x),y))	(3)
app(app(map,f),nil)	→	nil	(4)
app(app(map,f),app(app(cons,x),xs))	→	app(app(cons,app(f,x)),app(app(map,f),xs))	(5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

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

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

app^#(app(add,app(s,x)),y)	→	app^#(s,app(app(add,x),y))	(6)
app^#(app(add,app(s,x)),y)	→	app^#(app(add,x),y)	(7)
app^#(app(add,app(s,x)),y)	→	app^#(add,x)	(8)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(cons,app(f,x)),app(app(map,f),xs))	(9)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(cons,app(f,x))	(10)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(11)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(12)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

app^#(app(map,f),app(app(cons,x),xs)) → app^#(app(map,f),xs) (12)

app^#(app(map,f),app(app(cons,x),xs)) → app^#(f,x) (11)

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 Size-Change Termination

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

app^#(app(map,f),app(app(cons,x),xs)) → app^#(app(map,f),xs) (12)

1 ≥ 1

2 > 2

app^#(app(map,f),app(app(cons,x),xs)) → app^#(f,x) (11)

1 > 1

2 > 2

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
app^#(app(add,app(s,x)),y) → app^#(app(add,x),y) (7)

1.1.1.2 Usable Rules Processor

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

app(add,0) → id (2)

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

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

[add] = 1

[0] = 1

[id] = 0

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

[s] = 0

together with the usable rule
app(add,0) → id (2)
(w.r.t. the implicit argument filter of the reduction pair), the pair
app^#(app(add,app(s,x)),y) → app^#(app(add,x),y) (7)
and the rule
app(add,0) → id (2)
could be deleted.
1.1.1.2.1.1 P is empty

There are no pairs anymore.