Certification Problem

Input (TPDB TRS_Standard/Applicative_05/TreeHeight)

The rewrite relation of the following TRS is considered.

app(app(map,f),nil)	→	nil	(1)
app(app(map,f),app(app(cons,x),xs))	→	app(app(cons,app(f,x)),app(app(map,f),xs))	(2)
app(app(le,0),y)	→	true	(3)
app(app(le,app(s,x)),0)	→	false	(4)
app(app(le,app(s,x)),app(s,y))	→	app(app(le,x),y)	(5)
app(app(maxlist,x),app(app(cons,y),ys))	→	app(app(if,app(app(le,x),y)),app(app(maxlist,y),ys))	(6)
app(app(maxlist,x),nil)	→	x	(7)
app(height,app(app(node,x),xs))	→	app(s,app(app(maxlist,0),app(app(map,height),xs)))	(8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

app^#(app(map,f),app(app(cons,x),xs))	→	app^#(cons,app(f,x))	(9)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(if,app(app(le,x),y))	(10)
app^#(height,app(app(node,x),xs))	→	app^#(s,app(app(maxlist,0),app(app(map,height),xs)))	(11)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(app(maxlist,y),ys)	(12)
app^#(app(le,app(s,x)),app(s,y))	→	app^#(app(le,x),y)	(13)
app^#(app(le,app(s,x)),app(s,y))	→	app^#(le,x)	(14)
app^#(height,app(app(node,x),xs))	→	app^#(app(maxlist,0),app(app(map,height),xs))	(15)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(app(le,x),y)	(16)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(maxlist,y)	(17)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(app(if,app(app(le,x),y)),app(app(maxlist,y),ys))	(18)
app^#(height,app(app(node,x),xs))	→	app^#(map,height)	(19)
app^#(height,app(app(node,x),xs))	→	app^#(app(map,height),xs)	(20)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(21)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(cons,app(f,x)),app(app(map,f),xs))	(22)
app^#(app(maxlist,x),app(app(cons,y),ys))	→	app^#(le,x)	(23)
app^#(height,app(app(node,x),xs))	→	app^#(maxlist,0)	(24)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(25)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(25)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(21)
app^#(height,app(app(node,x),xs))	→	app^#(app(map,height),xs)	(20)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le]	=	1
[s]	=	34651
[height]	=	32286
[false]	=	101815
[true]	=	51242
[0]	=	19396
[if]	=	56519
[nil]	=	37745
[app^#(x₁, x₂)]	=	x₂ + 0
[map]	=	42781
[maxlist]	=	4140
[cons]	=	21656
[node]	=	20977
[app(x₁, x₂)]	=	x₁ + x₂ + 15922

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

app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(25)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(21)
app^#(height,app(app(node,x),xs))	→	app^#(app(map,height),xs)	(20)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

app^#(app(maxlist,x),app(app(cons,y),ys))

→

app^#(app(maxlist,y),ys)

(12)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le]	=	1
[s]	=	1
[height]	=	13208
[false]	=	7
[true]	=	5
[0]	=	1
[if]	=	1
[nil]	=	30374
[app^#(x₁, x₂)]	=	x₂ + 0
[map]	=	31044
[maxlist]	=	40519
[cons]	=	1
[node]	=	868
[app(x₁, x₂)]	=	x₁ + x₂ + 1

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

app^#(app(maxlist,x),app(app(cons,y),ys))

→

app^#(app(maxlist,y),ys)

(12)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

app^#(app(le,app(s,x)),app(s,y))

→

app^#(app(le,x),y)

(13)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le]	=	1
[s]	=	1
[height]	=	1
[false]	=	7
[true]	=	5
[0]	=	1
[if]	=	1
[nil]	=	53793
[app^#(x₁, x₂)]	=	x₂ + 0
[map]	=	1
[maxlist]	=	1
[cons]	=	1
[node]	=	1
[app(x₁, x₂)]	=	x₁ + x₂ + 1

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

app^#(app(le,app(s,x)),app(s,y))

→

app^#(app(le,x),y)

(13)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.