Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe11)

The rewrite relation of the following TRS is considered.

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)
quot(0,s(y))	→	0	(3)
quot(s(x),s(y))	→	s(quot(minus(x,y),s(y)))	(4)
plus(0,y)	→	y	(5)
plus(s(x),y)	→	s(plus(x,y))	(6)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)
app(nil,k)	→	k	(8)
app(l,nil)	→	l	(9)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
sum(cons(x,nil))	→	cons(x,nil)	(11)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)
plus(s(x),s(y))	→	s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))	(14)
plus(s(x),x)	→	plus(if(gt(x,x),id(x),id(x)),s(x))	(15)
plus(zero,y)	→	y	(16)
plus(id(x),s(y))	→	s(plus(x,if(gt(s(y),y),y,s(y))))	(17)
id(x)	→	x	(18)
if(true,x,y)	→	x	(19)
if(false,x,y)	→	y	(20)
not(x)	→	if(x,false,true)	(21)
gt(s(x),zero)	→	true	(22)
gt(zero,y)	→	false	(23)
gt(s(x),s(y))	→	gt(x,y)	(24)

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.

plus^#(s(x),y)	→	plus^#(x,y)	(25)
quot^#(s(x),s(y))	→	quot^#(minus(x,y),s(y))	(26)
gt^#(s(x),s(y))	→	gt^#(x,y)	(27)
plus^#(s(x),s(y))	→	not^#(gt(x,y))	(28)
plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(29)
plus^#(s(x),s(y))	→	gt^#(x,y)	(30)
plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(31)
not^#(x)	→	if^#(x,false,true)	(32)
plus^#(s(x),s(y))	→	if^#(not(gt(x,y)),id(x),id(y))	(33)
plus^#(s(x),s(y))	→	gt^#(x,y)	(30)
quot^#(s(x),s(y))	→	minus^#(x,y)	(34)
plus^#(s(x),x)	→	if^#(gt(x,x),id(x),id(x))	(35)
plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(36)
sum^#(cons(x,cons(y,l)))	→	sum^#(cons(plus(x,y),l))	(37)
plus^#(s(x),s(y))	→	if^#(gt(x,y),x,y)	(38)
sum^#(app(l,cons(x,cons(y,k))))	→	sum^#(cons(x,cons(y,k)))	(39)
plus^#(s(x),x)	→	id^#(x)	(40)
plus^#(id(x),s(y))	→	gt^#(s(y),y)	(41)
plus^#(s(x),x)	→	id^#(x)	(40)
minus^#(minus(x,y),z)	→	minus^#(x,plus(y,z))	(42)
app^#(cons(x,l),k)	→	app^#(l,k)	(43)
plus^#(s(x),x)	→	gt^#(x,x)	(44)
plus^#(id(x),s(y))	→	if^#(gt(s(y),y),y,s(y))	(45)
plus^#(s(x),s(y))	→	id^#(y)	(46)
sum^#(app(l,cons(x,cons(y,k))))	→	sum^#(app(l,sum(cons(x,cons(y,k)))))	(47)
minus^#(s(x),s(y))	→	minus^#(x,y)	(48)
sum^#(cons(x,cons(y,l)))	→	plus^#(x,y)	(49)
plus^#(s(x),s(y))	→	id^#(x)	(50)
sum^#(app(l,cons(x,cons(y,k))))	→	app^#(l,sum(cons(x,cons(y,k))))	(51)
minus^#(minus(x,y),z)	→	plus^#(y,z)	(52)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

sum^#(app(l,cons(x,cons(y,k))))

→

sum^#(app(l,sum(cons(x,cons(y,k)))))

(47)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	0
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	3
[sum(x₁)]	=	65135
[not^#(x₁)]	=	0
[0]	=	36466
[if(x₁, x₂, x₃)]	=	x₂ + 5855
[quot(x₁, x₂)]	=	0
[nil]	=	32567
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 30988
[cons(x₁, x₂)]	=	x₂ + 32568
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	1
[quot^#(x₁, x₂)]	=	0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 31755

together with the usable rules

app(nil,k)	→	k	(8)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)

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

sum^#(app(l,cons(x,cons(y,k))))

→

sum^#(app(l,sum(cons(x,cons(y,k)))))

(47)

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^#(cons(x,l),k)

→

app^#(l,k)

(43)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 23974
[gt(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	0
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	3
[sum(x₁)]	=	2
[not^#(x₁)]	=	0
[0]	=	36466
[if(x₁, x₂, x₃)]	=	x₂ + 2
[quot(x₁, x₂)]	=	0
[nil]	=	1
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 14681
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	1
[quot^#(x₁, x₂)]	=	0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 31755

together with the usable rules

app(nil,k)	→	k	(8)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)

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

app^#(cons(x,l),k)

→

app^#(l,k)

(43)

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

sum^#(cons(x,cons(y,l)))

→

sum^#(cons(plus(x,y),l))

(37)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	0
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	3
[sum(x₁)]	=	2
[not^#(x₁)]	=	0
[0]	=	32869
[if(x₁, x₂, x₃)]	=	x₂ + 2
[quot(x₁, x₂)]	=	0
[nil]	=	1
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	1
[quot^#(x₁, x₂)]	=	0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 3287

together with the usable rules

app(nil,k)	→	k	(8)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)

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

sum^#(cons(x,cons(y,l)))

→

sum^#(cons(plus(x,y),l))

(37)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(26)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 51836
[gt(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	x₁ + 51835
[plus^#(x₁, x₂)]	=	0
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	3
[sum(x₁)]	=	29535
[not^#(x₁)]	=	0
[0]	=	32869
[if(x₁, x₂, x₃)]	=	x₂ + 2
[quot(x₁, x₂)]	=	0
[nil]	=	1
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 19496
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	1
[quot^#(x₁, x₂)]	=	x₁ + 0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 13324

together with the usable rules

app(nil,k)	→	k	(8)
minus(x,0)	→	x	(1)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(26)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

minus^#(s(x),s(y))	→	minus^#(x,y)	(48)
minus^#(minus(x,y),z)	→	minus^#(x,plus(y,z))	(42)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 51836
[gt(x₁, x₂)]	=	x₂ + 1
[minus(x₁, x₂)]	=	x₁ + 51835
[plus^#(x₁, x₂)]	=	0
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	3
[sum(x₁)]	=	82509
[not^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	x₂ + 2
[quot(x₁, x₂)]	=	0
[nil]	=	28716
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	x₁ + 0
[plus(x₁, x₂)]	=	x₁ + x₂ + 7630
[cons(x₁, x₂)]	=	x₂ + 53793
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	1
[quot^#(x₁, x₂)]	=	x₁ + 0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 25785

together with the usable rules

app(nil,k)	→	k	(8)
minus(x,0)	→	x	(1)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

minus^#(s(x),s(y))	→	minus^#(x,y)	(48)
minus^#(minus(x,y),z)	→	minus^#(x,plus(y,z))	(42)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(31)
plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(29)
plus^#(s(x),y)	→	plus^#(x,y)	(25)
plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(36)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	0
[s(x₁)]	=	x₁ + 8
[gt(x₁, x₂)]	=	max(x₂ + 1, 0)
[minus(x₁, x₂)]	=	max(0)
[plus^#(x₁, x₂)]	=	max(x₁ + 41064, x₂ + 41063, 0)
[false]	=	1
[id^#(x₁)]	=	0
[true]	=	1
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	max(x₁ + 3, x₂ + 1, x₃ + 0, 0)
[quot(x₁, x₂)]	=	max(0)
[nil]	=	0
[gt^#(x₁, x₂)]	=	max(0)
[app^#(x₁, x₂)]	=	max(0)
[minus^#(x₁, x₂)]	=	max(0)
[plus(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	x₁ + 1
[quot^#(x₁, x₂)]	=	max(0)
[sum^#(x₁)]	=	0
[not(x₁)]	=	x₁ + 3
[app(x₁, x₂)]	=	max(0)

together with the usable rules

id(x)	→	x	(18)
not(x)	→	if(x,false,true)	(21)
if(true,x,y)	→	x	(19)
gt(s(x),zero)	→	true	(22)
if(false,x,y)	→	y	(20)
gt(zero,y)	→	false	(23)
gt(s(x),s(y))	→	gt(x,y)	(24)

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

plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(31)
plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(29)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(36)
plus^#(s(x),y)	→	plus^#(x,y)	(25)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	x₁ + x₂ + 1
[minus(x₁, x₂)]	=	x₁ + 51835
[plus^#(x₁, x₂)]	=	x₁ + 0
[false]	=	1
[id^#(x₁)]	=	0
[true]	=	1
[sum(x₁)]	=	53794
[not^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[quot(x₁, x₂)]	=	0
[nil]	=	1
[gt^#(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 35873
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 1
[quot^#(x₁, x₂)]	=	x₁ + 0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 31251
[app(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

id(x)	→	x	(18)
app(nil,k)	→	k	(8)
minus(x,0)	→	x	(1)
not(x)	→	if(x,false,true)	(21)
if(true,x,y)	→	x	(19)
gt(s(x),zero)	→	true	(22)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)
if(false,x,y)	→	y	(20)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
gt(zero,y)	→	false	(23)
gt(s(x),s(y))	→	gt(x,y)	(24)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(36)
plus^#(s(x),y)	→	plus^#(x,y)	(25)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

gt^#(s(x),s(y))

→

gt^#(x,y)

(27)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	x₁ + x₂ + 35873
[minus(x₁, x₂)]	=	x₁ + 51835
[plus^#(x₁, x₂)]	=	x₁ + 0
[false]	=	1
[id^#(x₁)]	=	0
[true]	=	1
[sum(x₁)]	=	2
[not^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[quot(x₁, x₂)]	=	0
[nil]	=	1
[gt^#(x₁, x₂)]	=	x₂ + 0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 1
[quot^#(x₁, x₂)]	=	x₁ + 0
[sum^#(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 31251
[app(x₁, x₂)]	=	x₁ + x₂ + 37697

together with the usable rules

id(x)	→	x	(18)
app(nil,k)	→	k	(8)
minus(x,0)	→	x	(1)
not(x)	→	if(x,false,true)	(21)
if(true,x,y)	→	x	(19)
gt(s(x),zero)	→	true	(22)
app(cons(x,l),k)	→	cons(x,app(l,k))	(10)
minus(minus(x,y),z)	→	minus(x,plus(y,z))	(7)
if(false,x,y)	→	y	(20)
sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(12)
gt(zero,y)	→	false	(23)
gt(s(x),s(y))	→	gt(x,y)	(24)
sum(cons(x,nil))	→	cons(x,nil)	(11)
app(l,nil)	→	l	(9)
sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(13)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

gt^#(s(x),s(y))

→

gt^#(x,y)

(27)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.