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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

app^#(app(app(app(filter2,true),f),x),xs)	→	app^#(app(filter,f),xs)	(47)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(f,x)),f),x),xs)	(71)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(67)
app^#(app(app(app(filter2,false),f),x),xs)	→	app^#(app(filter,f),xs)	(32)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(61)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(f,x)	(52)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	6
[ln]	=	1
[constant]	=	46959
[minus]	=	1
[pow]	=	1
[t]	=	1
[false]	=	39434
[div]	=	1
[D]	=	1
[true]	=	1
[filter2]	=	33215
[0]	=	46964
[nil]	=	23896
[-]	=	1
[app^#(x₁, x₂)]	=	x₂ + 0
[map]	=	1
[2]	=	35632
[cons]	=	1
[filter]	=	33216
[+]	=	1
[*]	=	1
[app(x₁, x₂)]	=	x₁ + x₂ + 3

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

app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(app(app(app(filter2,app(f,x)),f),x),xs)	(71)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(f,x)	(67)
app^#(app(map,f),app(app(cons,x),xs))	→	app^#(app(map,f),xs)	(61)
app^#(app(filter,f),app(app(cons,x),xs))	→	app^#(f,x)	(52)

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^#(D,app(app(+,x),y))	→	app^#(D,x)	(77)
app^#(D,app(ln,x))	→	app^#(D,x)	(73)
app^#(D,app(app(pow,x),y))	→	app^#(D,y)	(40)
app^#(D,app(app(div,x),y))	→	app^#(D,x)	(68)
app^#(D,app(app(*,x),y))	→	app^#(D,y)	(66)
app^#(D,app(app(+,x),y))	→	app^#(D,y)	(34)
app^#(D,app(app(pow,x),y))	→	app^#(D,x)	(63)
app^#(D,app(app(*,x),y))	→	app^#(D,x)	(28)
app^#(D,app(app(-,x),y))	→	app^#(D,y)	(24)
app^#(D,app(app(div,x),y))	→	app^#(D,y)	(22)
app^#(D,app(app(-,x),y))	→	app^#(D,x)	(20)
app^#(D,app(minus,x))	→	app^#(D,x)	(16)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	105200
[ln]	=	1
[constant]	=	14965
[minus]	=	54306
[pow]	=	34735
[t]	=	55152
[false]	=	37152
[div]	=	45734
[D]	=	32234
[true]	=	17811
[filter2]	=	53226
[0]	=	65013
[nil]	=	29231
[-]	=	18169
[app^#(x₁, x₂)]	=	x₂ + 0
[map]	=	16034
[2]	=	53742
[cons]	=	68706
[filter]	=	2332
[+]	=	20682
[*]	=	36718
[app(x₁, x₂)]	=	x₁ + x₂ + 17813

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

app^#(D,app(app(+,x),y))	→	app^#(D,x)	(77)
app^#(D,app(ln,x))	→	app^#(D,x)	(73)
app^#(D,app(app(pow,x),y))	→	app^#(D,y)	(40)
app^#(D,app(app(div,x),y))	→	app^#(D,x)	(68)
app^#(D,app(app(*,x),y))	→	app^#(D,y)	(66)
app^#(D,app(app(+,x),y))	→	app^#(D,y)	(34)
app^#(D,app(app(pow,x),y))	→	app^#(D,x)	(63)
app^#(D,app(app(*,x),y))	→	app^#(D,x)	(28)
app^#(D,app(app(-,x),y))	→	app^#(D,y)	(24)
app^#(D,app(app(div,x),y))	→	app^#(D,y)	(22)
app^#(D,app(app(-,x),y))	→	app^#(D,x)	(20)
app^#(D,app(minus,x))	→	app^#(D,x)	(16)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.