Certification Problem

Input (TPDB TRS_Standard/AProVE_06/tower)

The rewrite relation of the following TRS is considered.

plus(0,x)	→	x	(1)
plus(s(x),y)	→	s(plus(p(s(x)),y))	(2)
times(0,y)	→	0	(3)
times(s(x),y)	→	plus(y,times(p(s(x)),y))	(4)
exp(x,0)	→	s(0)	(5)
exp(x,s(y))	→	times(x,exp(x,y))	(6)
p(s(0))	→	0	(7)
p(s(s(x)))	→	s(p(s(x)))	(8)
tower(x,y)	→	towerIter(x,y,s(0))	(9)
towerIter(0,y,z)	→	z	(10)
towerIter(s(x),y,z)	→	towerIter(p(s(x)),y,exp(y,z))	(11)

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)	→	p^#(s(x))	(12)
towerIter^#(s(x),y,z)	→	towerIter^#(p(s(x)),y,exp(y,z))	(13)
p^#(s(s(x)))	→	p^#(s(x))	(14)
times^#(s(x),y)	→	times^#(p(s(x)),y)	(15)
times^#(s(x),y)	→	p^#(s(x))	(16)
towerIter^#(s(x),y,z)	→	p^#(s(x))	(17)
times^#(s(x),y)	→	plus^#(y,times(p(s(x)),y))	(18)
tower^#(x,y)	→	towerIter^#(x,y,s(0))	(19)
exp^#(x,s(y))	→	times^#(x,exp(x,y))	(20)
plus^#(s(x),y)	→	plus^#(p(s(x)),y)	(21)
towerIter^#(s(x),y,z)	→	exp^#(y,z)	(22)
exp^#(x,s(y))	→	exp^#(x,y)	(23)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

towerIter^#(s(x),y,z)

→

towerIter^#(p(s(x)),y,exp(y,z))

(13)

1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[tower(x₁, x₂)]

[s(x₁)]

1	1
1	1

· x₁ +

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

[towerIter(x₁, x₂, x₃)]

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

[p^#(x₁)]

[p(x₁)]

0	1
0	1

· x₁ +

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

[0]

[times(x₁, x₂)]

x₁ +

0	0
1	1

· x₂ +

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

[towerIter^#(x₁, x₂, x₃)]

x₁ +

[plus(x₁, x₂)]

0	1
1	1

· x₁ +

1	1
1	1

· x₂ +

[exp(x₁, x₂)]

together with the usable rules

p(s(s(x)))	→	s(p(s(x)))	(8)
p(s(0))	→	0	(7)

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

towerIter^#(s(x),y,z)

→

towerIter^#(p(s(x)),y,exp(y,z))

(13)

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

exp^#(x,s(y))

→

exp^#(x,y)

(23)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[tower(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 2
[plus^#(x₁, x₂)]	=	0
[towerIter(x₁, x₂, x₃)]	=	0
[exp^#(x₁, x₂)]	=	x₂ + 0
[p^#(x₁)]	=	0
[p(x₁)]	=	1
[times^#(x₁, x₂)]	=	0
[0]	=	5855
[times(x₁, x₂)]	=	x₁ + x₂ + 3
[tower^#(x₁, x₂)]	=	0
[towerIter^#(x₁, x₂, x₃)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 2
[exp(x₁, x₂)]	=	x₁ + x₂ + 1

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

exp^#(x,s(y))

→

exp^#(x,y)

(23)

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

times^#(s(x),y)

→

times^#(p(s(x)),y)

(15)

1.1.3 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[tower(x₁, x₂)]

[s(x₁)]

1	1
1	1

· x₁ +

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

[towerIter(x₁, x₂, x₃)]

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

[p^#(x₁)]

[p(x₁)]

0	1
0	1

· x₁ +

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

1	0
1	1

· x₁ +

[0]

[times(x₁, x₂)]

x₁ +

0	0
1	1

· x₂ +

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

[towerIter^#(x₁, x₂, x₃)]

x₁ +

[plus(x₁, x₂)]

0	1
1	1

· x₁ +

1	1
1	1

· x₂ +

24233

[exp(x₁, x₂)]

together with the usable rules

p(s(s(x)))	→	s(p(s(x)))	(8)
p(s(0))	→	0	(7)

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

times^#(s(x),y)

→

times^#(p(s(x)),y)

(15)

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

plus^#(s(x),y)

→

plus^#(p(s(x)),y)

(21)

1.1.4 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[tower(x₁, x₂)]

[s(x₁)]

1	1
1	1

· x₁ +

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

1	1
0	1

· x₁ +

[towerIter(x₁, x₂, x₃)]

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

[p^#(x₁)]

[p(x₁)]

0	1
0	1

· x₁ +

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

1	0
1	1

· x₁ +

[0]

35614

[times(x₁, x₂)]

x₁ +

0	0
1	1

· x₂ +

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

[towerIter^#(x₁, x₂, x₃)]

x₁ +

[plus(x₁, x₂)]

0	1
1	1

· x₁ +

1	1
1	1

· x₂ +

[exp(x₁, x₂)]

together with the usable rules

p(s(s(x)))	→	s(p(s(x)))	(8)
p(s(0))	→	0	(7)

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

plus^#(s(x),y)

→

plus^#(p(s(x)),y)

(21)

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

p^#(s(s(x)))

→

p^#(s(x))

(14)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[tower(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 2
[plus^#(x₁, x₂)]	=	0
[towerIter(x₁, x₂, x₃)]	=	0
[exp^#(x₁, x₂)]	=	0
[p^#(x₁)]	=	x₁ + 0
[p(x₁)]	=	2
[times^#(x₁, x₂)]	=	0
[0]	=	9728
[times(x₁, x₂)]	=	x₁ + x₂ + 3
[tower^#(x₁, x₂)]	=	0
[towerIter^#(x₁, x₂, x₃)]	=	0
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[exp(x₁, x₂)]	=	x₁ + x₂ + 1

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

p^#(s(s(x)))

→

p^#(s(x))

(14)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.