Certification Problem

Input (TPDB TRS_Standard/Applicative_first_order_05/perfect)

The rewrite relation of the following TRS is considered.

app(perfectp,0)	→	false	(1)
app(perfectp,app(s,x))	→	app(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x))	(2)
app(app(app(app(f,0),y),0),u)	→	true	(3)
app(app(app(app(f,0),y),app(s,z)),u)	→	false	(4)
app(app(app(app(f,app(s,x)),0),z),u)	→	app(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)	(5)
app(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u))	(6)
app(app(map,fun),nil)	→	nil	(7)
app(app(map,fun),app(app(cons,x),xs))	→	app(app(cons,app(fun,x)),app(app(map,fun),xs))	(8)
app(app(filter,fun),nil)	→	nil	(9)
app(app(filter,fun),app(app(cons,x),xs))	→	app(app(app(app(filter2,app(fun,x)),fun),x),xs)	(10)
app(app(app(app(filter2,true),fun),x),xs)	→	app(app(cons,x),app(app(filter,fun),xs))	(11)
app(app(app(app(filter2,false),fun),x),xs)	→	app(app(filter,fun),xs)	(12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

app^#(perfectp,app(s,x))	→	app^#(s,0)	(13)
app^#(perfectp,app(s,x))	→	app^#(f,x)	(14)
app^#(perfectp,app(s,x))	→	app^#(app(f,x),app(s,0))	(15)
app^#(perfectp,app(s,x))	→	app^#(app(app(f,x),app(s,0)),app(s,x))	(16)
app^#(perfectp,app(s,x))	→	app^#(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x))	(17)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(minus,z)	(18)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(app(minus,z),app(s,x))	(19)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(f,x)	(20)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(app(f,x),u)	(21)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(app(app(f,x),u),app(app(minus,z),app(s,x)))	(22)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)	(23)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(f,x)	(24)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(f,x),u)	(25)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(f,x),u),z)	(26)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(app(f,x),u),z),u)	(27)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(minus,y)	(28)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(minus,y),x)	(29)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(f,app(s,x)),app(app(minus,y),x))	(30)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(f,app(s,x)),app(app(minus,y),x)),z)	(31)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)	(32)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(le,x)	(33)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(le,x),y)	(34)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(if,app(app(le,x),y))	(35)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u))	(36)
app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u))	(37)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(app(map,fun),xs)	(38)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(39)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(cons,app(fun,x))	(40)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(app(cons,app(fun,x)),app(app(map,fun),xs))	(41)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(42)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(filter2,app(fun,x))	(43)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(app(filter2,app(fun,x)),fun)	(44)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(app(app(filter2,app(fun,x)),fun),x)	(45)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(fun,x)),fun),x),xs)	(46)
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(filter,fun)	(47)
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(app(filter,fun),xs)	(48)
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(cons,x)	(49)
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(app(cons,x),app(app(filter,fun),xs))	(50)
app^#(app(app(app(filter2,false),fun),x),xs)	→	app^#(filter,fun)	(51)
app^#(app(app(app(filter2,false),fun),x),xs)	→	app^#(app(filter,fun),xs)	(52)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(fun,x)),fun),x),xs)	(46)
app^#(app(app(app(filter2,false),fun),x),xs)	→	app^#(app(filter,fun),xs)	(52)
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(42)
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(app(filter,fun),xs)	(48)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(39)
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(app(map,fun),xs)	(38)

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(filter,fun),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(fun,x)),fun),x),xs)	(46)

2	>	2
app^#(app(app(app(filter2,false),fun),x),xs)	→	app^#(app(filter,fun),xs)	(52)

2	≥	2
app^#(app(filter,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(42)

2	>	2
1	>	1
app^#(app(app(app(filter2,true),fun),x),xs)	→	app^#(app(filter,fun),xs)	(48)

2	≥	2
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(fun,x)	(39)

2	>	2
1	>	1
app^#(app(map,fun),app(app(cons,x),xs))	→	app^#(app(map,fun),xs)	(38)

2	>	2
1	≥	1

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

The 2^nd component contains the pair

app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)	→	app^#(app(app(app(f,x),u),z),u)	(27)
app^#(app(app(app(f,app(s,x)),0),z),u)	→	app^#(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)	(23)

1.1.2 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[s]

1	0	0
0	0	0
1	0	0

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

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[f]

0	0	0
0	0	0
0	0	0

[minus]

0	0	0
0	0	0
1	0	0

[app(x₁, x₂)]

0	1	0
0	0	1
1	0	0

· x₁ +

1	0	0
0	0	0
1	0	1

· x₂ +

0	0	0
0	0	0
0	0	0

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

app^#(app(app(app(f,app(s,x)),app(s,y)),z),u)

→

app^#(app(app(app(f,x),u),z),u)

(27)

could be deleted.

1.1.2.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[s]

1	0	0
1	0	0
1	0	0

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

0	0	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[0]

0	0	0
0	0	0
0	0	0

[f]

0	0	0
0	0	0
0	0	0

[minus]

1	0	0
0	0	0
0	0	0

[app(x₁, x₂)]

0	1	1
1	0	1
0	1	0

· x₁ +

1	1	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

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

app^#(app(app(app(f,app(s,x)),0),z),u)

→

app^#(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)

(23)

could be deleted.

1.1.2.1.1 P is empty

There are no pairs anymore.