Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/016)

The rewrite relation of the following TRS is considered.

app(app(neq,0),0)	→	false	(1)
app(app(neq,0),app(s,y))	→	true	(2)
app(app(neq,app(s,x)),0)	→	true	(3)
app(app(neq,app(s,x)),app(s,y))	→	app(app(neq,x),y)	(4)
app(app(filter,f),nil)	→	nil	(5)
app(app(filter,f),app(app(cons,y),ys))	→	app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(6)
app(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app(app(cons,y),app(app(filter,f),ys))	(7)
app(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app(app(filter,f),ys)	(8)
nonzero	→	app(filter,app(neq,0))	(9)

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(filter,f),app(app(cons,y),ys))	→	app^#(app(filtersub,app(f,y)),f)	(10)
nonzero^#	→	app^#(neq,0)	(11)
app^#(app(neq,app(s,x)),app(s,y))	→	app^#(neq,x)	(12)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(filter,f)	(13)
app^#(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app^#(filter,f)	(14)
app^#(app(neq,app(s,x)),app(s,y))	→	app^#(app(neq,x),y)	(15)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(app(cons,y),app(app(filter,f),ys))	(16)
app^#(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(17)
nonzero^#	→	app^#(filter,app(neq,0))	(18)
app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(filtersub,app(f,y))	(19)
app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(20)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(21)
app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(f,y)	(22)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(f,y)	(22)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(21)
app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(20)
app^#(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(17)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[neq]	=	1
[s]	=	1
[false]	=	1
[nonzero]	=	0
[true]	=	2
[filtersub]	=	1
[0]	=	14235
[nil]	=	17221
[app^#(x₁, x₂)]	=	x₁ + 0
[nonzero^#]	=	0
[cons]	=	1
[filter]	=	1
[app(x₁, x₂)]	=	x₂ + 1

together with the usable rules

app(app(neq,app(s,x)),app(s,y))	→	app(app(neq,x),y)	(4)
app(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app(app(filter,f),ys)	(8)
app(app(neq,0),0)	→	false	(1)
app(app(neq,app(s,x)),0)	→	true	(3)
app(app(filter,f),nil)	→	nil	(5)
app(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app(app(cons,y),app(app(filter,f),ys))	(7)
app(app(filter,f),app(app(cons,y),ys))	→	app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(6)
app(app(neq,0),app(s,y))	→	true	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

app^#(app(filter,f),app(app(cons,y),ys))

→

app^#(f,y)

(22)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

app^#(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(17)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(21)
app^#(app(filter,f),app(app(cons,y),ys))	→	app^#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(20)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[neq]	=	1
[s]	=	1
[false]	=	1
[nonzero]	=	0
[true]	=	282
[filtersub]	=	1
[0]	=	7653
[nil]	=	6996
[app^#(x₁, x₂)]	=	x₁ + x₂ + 0
[nonzero^#]	=	0
[cons]	=	1
[filter]	=	1
[app(x₁, x₂)]	=	x₂ + 6583

together with the usable rules

app(app(neq,app(s,x)),app(s,y))	→	app(app(neq,x),y)	(4)
app(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app(app(filter,f),ys)	(8)
app(app(neq,0),0)	→	false	(1)
app(app(neq,app(s,x)),0)	→	true	(3)
app(app(filter,f),nil)	→	nil	(5)
app(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app(app(cons,y),app(app(filter,f),ys))	(7)
app(app(filter,f),app(app(cons,y),ys))	→	app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(6)
app(app(neq,0),app(s,y))	→	true	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

app^#(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(17)
app^#(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app^#(app(filter,f),ys)	(21)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

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

→

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

(15)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[neq]	=	1
[s]	=	1
[false]	=	1
[nonzero]	=	0
[true]	=	1
[filtersub]	=	1
[0]	=	46572
[nil]	=	42632
[app^#(x₁, x₂)]	=	x₁ + x₂ + 0
[nonzero^#]	=	0
[cons]	=	1
[filter]	=	1
[app(x₁, x₂)]	=	x₂ + 1

together with the usable rules

app(app(neq,app(s,x)),app(s,y))	→	app(app(neq,x),y)	(4)
app(app(app(filtersub,false),f),app(app(cons,y),ys))	→	app(app(filter,f),ys)	(8)
app(app(neq,0),0)	→	false	(1)
app(app(neq,app(s,x)),0)	→	true	(3)
app(app(filter,f),nil)	→	nil	(5)
app(app(app(filtersub,true),f),app(app(cons,y),ys))	→	app(app(cons,y),app(app(filter,f),ys))	(7)
app(app(filter,f),app(app(cons,y),ys))	→	app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))	(6)
app(app(neq,0),app(s,y))	→	true	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

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

→

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

(15)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.