Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/aprove06)

The rewrite relation of the following TRS is considered.

tower(0(x1))	→	s(0(p(s(p(s(x1))))))	(1)
tower(s(x1))	→	p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))	(2)
twoto(0(x1))	→	s(0(x1))	(3)
twoto(s(x1))	→	p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))	(4)
twice(0(x1))	→	0(x1)	(5)
twice(s(x1))	→	p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))	(6)
p(p(s(x1)))	→	p(x1)	(7)
p(s(x1))	→	x1	(8)
p(0(x1))	→	0(s(s(s(s(s(s(s(s(x1)))))))))	(9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

0(tower(x1))	→	s(p(s(p(0(s(x1))))))	(10)
s(tower(x1))	→	s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(11)
0(twoto(x1))	→	0(s(x1))	(12)
s(twoto(x1))	→	s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(13)
0(twice(x1))	→	0(x1)	(14)
s(twice(x1))	→	s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(15)
s(p(p(x1)))	→	p(x1)	(16)
s(p(x1))	→	x1	(17)
0(p(x1))	→	s(s(s(s(s(s(s(s(0(x1)))))))))	(18)

1.1 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[twoto(x₁)]	=	0 · x₁ + -∞
[tower(x₁)]	=	5 · x₁ + -∞
[p(x₁)]	=	0 · x₁ + -∞
[twice(x₁)]	=	0 · x₁ + -∞
[0(x₁)]	=	0 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + -∞

all of the following rules can be deleted.

0(tower(x1))

→

s(p(s(p(0(s(x1))))))

(10)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

s^#(tower(x1))	→	s^#(p(x1))	(19)
s^#(tower(x1))	→	s^#(p(s(p(x1))))	(20)
s^#(tower(x1))	→	s^#(p(twoto(s(p(s(p(x1)))))))	(21)
s^#(tower(x1))	→	s^#(p(s(p(twoto(s(p(s(p(x1)))))))))	(22)
s^#(tower(x1))	→	s^#(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))	(23)
s^#(tower(x1))	→	s^#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(24)
0^#(twoto(x1))	→	s^#(x1)	(25)
0^#(twoto(x1))	→	0^#(s(x1))	(26)
s^#(twoto(x1))	→	s^#(p(p(x1)))	(27)
s^#(twoto(x1))	→	s^#(p(p(p(s(p(p(x1)))))))	(28)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(p(x1))))))))	(29)
s^#(twoto(x1))	→	s^#(p(s(s(p(p(p(s(p(p(x1))))))))))	(30)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(p(p(s(p(p(x1)))))))))))	(31)
s^#(twoto(x1))	→	s^#(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))	(32)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))	(33)
s^#(twoto(x1))	→	s^#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))	(34)
s^#(twoto(x1))	→	s^#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))	(35)
s^#(twoto(x1))	→	s^#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))	(36)
s^#(twoto(x1))	→	s^#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))	(37)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))	(38)
s^#(twoto(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))	(39)
s^#(twoto(x1))	→	s^#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))	(40)
s^#(twoto(x1))	→	s^#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(41)
0^#(twice(x1))	→	0^#(x1)	(42)
s^#(twice(x1))	→	s^#(p(p(p(x1))))	(43)
s^#(twice(x1))	→	s^#(s(p(p(p(x1)))))	(44)
s^#(twice(x1))	→	s^#(s(s(p(p(p(x1))))))	(45)
s^#(twice(x1))	→	s^#(s(s(s(p(p(p(x1)))))))	(46)
s^#(twice(x1))	→	s^#(s(s(s(s(p(p(p(x1))))))))	(47)
s^#(twice(x1))	→	s^#(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))	(48)
s^#(twice(x1))	→	s^#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))	(49)
s^#(twice(x1))	→	s^#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(50)
0^#(p(x1))	→	0^#(x1)	(51)
0^#(p(x1))	→	s^#(0(x1))	(52)
0^#(p(x1))	→	s^#(s(0(x1)))	(53)
0^#(p(x1))	→	s^#(s(s(0(x1))))	(54)
0^#(p(x1))	→	s^#(s(s(s(0(x1)))))	(55)
0^#(p(x1))	→	s^#(s(s(s(s(0(x1))))))	(56)
0^#(p(x1))	→	s^#(s(s(s(s(s(0(x1)))))))	(57)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(0(x1))))))))	(58)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(s(0(x1)))))))))	(59)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

0^#(twice(x1))	→	0^#(x1)	(42)
0^#(p(x1))	→	0^#(x1)	(51)
0^#(twoto(x1))	→	0^#(s(x1))	(26)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the

prec(0^#)	=	stat(0^#)	=	lex
prec(twice)	=	stat(twice)	=	lex
prec(twoto)	=	stat(twoto)	=	lex
prec(p)	=	stat(p)	=	lex
prec(s)	=	stat(s)	=	lex
prec(tower)	=	stat(tower)	=	lex

π(0^#)	=	1
π(twice)	=	1
π(twoto)	=	[1]
π(p)	=	1
π(s)	=	1
π(tower)	=	[]

together with the usable rules

s(tower(x1))	→	s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(11)
s(twoto(x1))	→	s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(13)
s(twice(x1))	→	s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(15)
s(p(p(x1)))	→	p(x1)	(16)
s(p(x1))	→	x1	(17)

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

0^#(twoto(x1))

→

0^#(s(x1))

(26)

could be deleted.

1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

0^#(twice(x1))	→	0^#(x1)	(42)

1	>	1
0^#(p(x1))	→	0^#(x1)	(51)

1	>	1

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

The 2^nd component contains the pair

s^#(twice(x1))	→	s^#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(50)
s^#(twice(x1))	→	s^#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))	(49)
s^#(twice(x1))	→	s^#(s(s(s(s(p(p(p(x1))))))))	(47)
s^#(twice(x1))	→	s^#(s(s(s(p(p(p(x1)))))))	(46)
s^#(twice(x1))	→	s^#(s(s(p(p(p(x1))))))	(45)
s^#(twice(x1))	→	s^#(s(p(p(p(x1)))))	(44)
s^#(twoto(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))	(39)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))	(38)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))	(33)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(p(p(s(p(p(x1)))))))))))	(31)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(p(x1))))))))	(29)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the

prec(s^#)	=	stat(s^#)	=	lex
prec(twice)	=	stat(twice)	=	lex
prec(twoto)	=	stat(twoto)	=	lex
prec(p)	=	stat(p)	=	lex
prec(s)	=	stat(s)	=	lex
prec(tower)	=	stat(tower)	=	lex

π(s^#)	=	1
π(twice)	=	1
π(twoto)	=	[1]
π(p)	=	1
π(s)	=	1
π(tower)	=	[]

together with the usable rules

s(p(p(x1)))	→	p(x1)	(16)
s(p(x1))	→	x1	(17)
s(tower(x1))	→	s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(11)
s(twoto(x1))	→	s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(13)
s(twice(x1))	→	s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(15)

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

s^#(twoto(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))	(39)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))	(38)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))	(33)
s^#(twoto(x1))	→	s^#(s(p(s(s(p(p(p(s(p(p(x1)))))))))))	(31)
s^#(twoto(x1))	→	s^#(s(p(p(p(s(p(p(x1))))))))	(29)

could be deleted.

1.1.1.1.2.1 Reduction Pair Processor with Usable Rules

Using the

prec(s^#)	=	stat(s^#)	=	lex
prec(twice)	=	stat(twice)	=	lex
prec(twoto)	=	stat(twoto)	=	lex
prec(p)	=	stat(p)	=	lex
prec(s)	=	stat(s)	=	lex
prec(tower)	=	stat(tower)	=	lex

π(s^#)	=	1
π(twice)	=	[1]
π(twoto)	=	[]
π(p)	=	1
π(s)	=	1
π(tower)	=	[]

together with the usable rules

s(p(p(x1)))	→	p(x1)	(16)
s(p(x1))	→	x1	(17)
s(tower(x1))	→	s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(11)
s(twoto(x1))	→	s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(13)
s(twice(x1))	→	s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(15)

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

s^#(twice(x1))	→	s^#(s(s(s(s(p(p(p(x1))))))))	(47)
s^#(twice(x1))	→	s^#(s(s(s(p(p(p(x1)))))))	(46)
s^#(twice(x1))	→	s^#(s(s(p(p(p(x1))))))	(45)
s^#(twice(x1))	→	s^#(s(p(p(p(x1)))))	(44)

could be deleted.

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[twoto(x₁)]	=	-3 · x₁ + 4
[tower(x₁)]	=	-∞ · x₁ + 1
[p(x₁)]	=	-1 · x₁ + 0
[twice(x₁)]	=	-∞ · x₁ + 6
[s^#(x₁)]	=	0 · x₁ + -16
[s(x₁)]	=	1 · x₁ + 2

together with the usable rules

s(p(p(x1)))	→	p(x1)	(16)
s(p(x1))	→	x1	(17)
s(tower(x1))	→	s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1))))))))))))))	(11)
s(twoto(x1))	→	s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))))))))	(13)
s(twice(x1))	→	s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(15)

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

s^#(twice(x1))	→	s^#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))))	(50)
s^#(twice(x1))	→	s^#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))	(49)

could be deleted.

1.1.1.1.2.1.1.1 P is empty

There are no pairs anymore.