Certification Problem

Input (TPDB TRS_Standard/Applicative_first_order_05/11)

The rewrite relation of the following TRS is considered.

app(D,t)	→	1	(1)
app(D,constant)	→	0	(2)
app(D,app(app(+,x),y))	→	app(app(+,app(D,x)),app(D,y))	(3)
app(D,app(app(*,x),y))	→	app(app(+,app(app(,y),app(D,x))),app(app(,x),app(D,y)))	(4)
app(D,app(app(-,x),y))	→	app(app(-,app(D,x)),app(D,y))	(5)
app(D,app(minus,x))	→	app(minus,app(D,x))	(6)
app(D,app(app(div,x),y))	→	app(app(-,app(app(div,app(D,x)),y)),app(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2)))	(7)
app(D,app(ln,x))	→	app(app(div,app(D,x)),x)	(8)
app(D,app(app(pow,x),y))	→	app(app(+,app(app(,app(app(,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))),app(app(,app(app(,app(app(pow,x),y)),app(ln,x))),app(D,y)))	(9)
app(app(map,f),nil)	→	nil	(10)
app(app(map,f),app(app(cons,x),xs))	→	app(app(cons,app(f,x)),app(app(map,f),xs))	(11)
app(app(filter,f),nil)	→	nil	(12)
app(app(filter,f),app(app(cons,x),xs))	→	app(app(app(app(filter2,app(f,x)),f),x),xs)	(13)
app(app(app(app(filter2,true),f),x),xs)	→	app(app(cons,x),app(app(filter,f),xs))	(14)
app(app(app(app(filter2,false),f),x),xs)	→	app(app(filter,f),xs)	(15)

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^#(D,app(app(+,x),y))	→	app^#(D,y)	(16)
app^#(D,app(app(+,x),y))	→	app^#(D,x)	(17)
app^#(D,app(app(+,x),y))	→	app^#(+,app(D,x))	(18)
app^#(D,app(app(+,x),y))	→	app^#(app(+,app(D,x)),app(D,y))	(19)
app^#(D,app(app(*,x),y))	→	app^#(D,y)	(20)
app^#(D,app(app(*,x),y))	→	app^#(app(*,x),app(D,y))	(21)
app^#(D,app(app(*,x),y))	→	app^#(D,x)	(22)
app^#(D,app(app(*,x),y))	→	app^#(*,y)	(23)
app^#(D,app(app(*,x),y))	→	app^#(app(*,y),app(D,x))	(24)
app^#(D,app(app(*,x),y))	→	app^#(+,app(app(*,y),app(D,x)))	(25)
app^#(D,app(app(*,x),y))	→	app^#(app(+,app(app(,y),app(D,x))),app(app(,x),app(D,y)))	(26)
app^#(D,app(app(-,x),y))	→	app^#(D,y)	(27)
app^#(D,app(app(-,x),y))	→	app^#(D,x)	(28)
app^#(D,app(app(-,x),y))	→	app^#(-,app(D,x))	(29)
app^#(D,app(app(-,x),y))	→	app^#(app(-,app(D,x)),app(D,y))	(30)
app^#(D,app(minus,x))	→	app^#(D,x)	(31)
app^#(D,app(minus,x))	→	app^#(minus,app(D,x))	(32)
app^#(D,app(app(div,x),y))	→	app^#(pow,y)	(33)
app^#(D,app(app(div,x),y))	→	app^#(app(pow,y),2)	(34)
app^#(D,app(app(div,x),y))	→	app^#(D,y)	(35)
app^#(D,app(app(div,x),y))	→	app^#(*,x)	(36)
app^#(D,app(app(div,x),y))	→	app^#(app(*,x),app(D,y))	(37)
app^#(D,app(app(div,x),y))	→	app^#(div,app(app(*,x),app(D,y)))	(38)
app^#(D,app(app(div,x),y))	→	app^#(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2))	(39)
app^#(D,app(app(div,x),y))	→	app^#(D,x)	(40)
app^#(D,app(app(div,x),y))	→	app^#(div,app(D,x))	(41)
app^#(D,app(app(div,x),y))	→	app^#(app(div,app(D,x)),y)	(42)
app^#(D,app(app(div,x),y))	→	app^#(-,app(app(div,app(D,x)),y))	(43)
app^#(D,app(app(div,x),y))	→	app^#(app(-,app(app(div,app(D,x)),y)),app(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2)))	(44)
app^#(D,app(ln,x))	→	app^#(D,x)	(45)
app^#(D,app(ln,x))	→	app^#(div,app(D,x))	(46)
app^#(D,app(ln,x))	→	app^#(app(div,app(D,x)),x)	(47)
app^#(D,app(app(pow,x),y))	→	app^#(D,y)	(48)
app^#(D,app(app(pow,x),y))	→	app^#(ln,x)	(49)
app^#(D,app(app(pow,x),y))	→	app^#(*,app(app(pow,x),y))	(50)
app^#(D,app(app(pow,x),y))	→	app^#(app(*,app(app(pow,x),y)),app(ln,x))	(51)
app^#(D,app(app(pow,x),y))	→	app^#(,app(app(,app(app(pow,x),y)),app(ln,x)))	(52)
app^#(D,app(app(pow,x),y))	→	app^#(app(,app(app(,app(app(pow,x),y)),app(ln,x))),app(D,y))	(53)
app^#(D,app(app(pow,x),y))	→	app^#(D,x)	(54)
app^#(D,app(app(pow,x),y))	→	app^#(-,y)	(55)
app^#(D,app(app(pow,x),y))	→	app^#(app(-,y),1)	(56)
app^#(D,app(app(pow,x),y))	→	app^#(app(pow,x),app(app(-,y),1))	(57)
app^#(D,app(app(pow,x),y))	→	app^#(*,y)	(58)
app^#(D,app(app(pow,x),y))	→	app^#(app(*,y),app(app(pow,x),app(app(-,y),1)))	(59)
app^#(D,app(app(pow,x),y))	→	app^#(,app(app(,y),app(app(pow,x),app(app(-,y),1))))	(60)
app^#(D,app(app(pow,x),y))	→	app^#(app(,app(app(,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))	(61)
app^#(D,app(app(pow,x),y))	→	app^#(+,app(app(,app(app(,y),app(app(pow,x),app(app(-,y),1)))),app(D,x)))	(62)
app^#(D,app(app(pow,x),y))	→	app^#(app(+,app(app(,app(app(,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))),app(app(,app(app(,app(app(pow,x),y)),app(ln,x))),app(D,y)))	(63)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(64)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(65)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(cons,app(f,x))	(66)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(cons,app(f,x)),app(app(map,f),xs))	(67)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(f,x)	(68)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(filter2,app(f,x))	(69)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(app(filter2,app(f,x)),f)	(70)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(app(app(filter2,app(f,x)),f),x)	(71)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(f,x)),f),x),xs)	(72)
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(filter,f)	(73)
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(app(filter,f),xs)	(74)
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(cons,x)	(75)
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(app(cons,x),app(app(filter,f),xs))	(76)
app^#(app(app(app(filter2,false),f),x),xs)	→	app^#(filter,f)	(77)
app^#(app(app(app(filter2,false),f),x),xs)	→	app^#(app(filter,f),xs)	(78)

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,x),xs))	→	app^#(f,x)	(68)
app^#(app(app(app(filter2,false),f),x),xs)	→	app^#(app(filter,f),xs)	(78)
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(app(filter,f),xs)	(74)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(65)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(64)

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,f),app(app(cons,x),xs))	→	app^#(f,x)	(68)

2	>	2
1	>	1
app^#(app(app(app(filter2,false),f),x),xs)	→	app^#(app(filter,f),xs)	(78)

2	≥	2
app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(app(filter,f),xs)	(74)

2	≥	2
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(65)

2	>	2
1	>	1
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(64)

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^#(D,app(app(pow,x),y))	→	app^#(D,x)	(54)
app^#(D,app(app(pow,x),y))	→	app^#(D,y)	(48)
app^#(D,app(ln,x))	→	app^#(D,x)	(45)
app^#(D,app(app(div,x),y))	→	app^#(D,x)	(40)
app^#(D,app(app(div,x),y))	→	app^#(D,y)	(35)
app^#(D,app(minus,x))	→	app^#(D,x)	(31)
app^#(D,app(app(-,x),y))	→	app^#(D,x)	(28)
app^#(D,app(app(-,x),y))	→	app^#(D,y)	(27)
app^#(D,app(app(*,x),y))	→	app^#(D,x)	(22)
app^#(D,app(app(*,x),y))	→	app^#(D,y)	(20)
app^#(D,app(app(+,x),y))	→	app^#(D,x)	(17)
app^#(D,app(app(+,x),y))	→	app^#(D,y)	(16)

1.1.2 Subterm Criterion Processor

We use the projection

π(app^#)

and remove the pairs:

app^#(D,app(app(pow,x),y))	→	app^#(D,x)	(54)
app^#(D,app(app(pow,x),y))	→	app^#(D,y)	(48)
app^#(D,app(ln,x))	→	app^#(D,x)	(45)
app^#(D,app(app(div,x),y))	→	app^#(D,x)	(40)
app^#(D,app(app(div,x),y))	→	app^#(D,y)	(35)
app^#(D,app(minus,x))	→	app^#(D,x)	(31)
app^#(D,app(app(-,x),y))	→	app^#(D,x)	(28)
app^#(D,app(app(-,x),y))	→	app^#(D,y)	(27)
app^#(D,app(app(*,x),y))	→	app^#(D,x)	(22)
app^#(D,app(app(*,x),y))	→	app^#(D,y)	(20)
app^#(D,app(app(+,x),y))	→	app^#(D,x)	(17)
app^#(D,app(app(+,x),y))	→	app^#(D,y)	(16)

1.1.2.1 P is empty

There are no pairs anymore.