Certification Problem

Input (TPDB SRS_Standard/Secret_06_SRS/aprove04)

The rewrite relation of the following TRS is considered.

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

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(sq(x1))	→	s(p(s(p(0(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))))))	(9)
s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
0(twice(x1))	→	s(p(s(p(s(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))))))))))))	(11)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)
s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)
0(p(x1))	→	s(s(s(s(s(s(s(s(s(s(s(0(x1))))))))))))	(15)
0(x1)	→	x1	(8)

1.1 Rule Removal

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

[twice(x₁)]	=	0 · x₁ + -∞
[sq(x₁)]	=	0 · x₁ + -∞
[p(x₁)]	=	0 · x₁ + -∞
[0(x₁)]	=	3 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + -∞

all of the following rules can be deleted.

0(x1)

→

(8)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

0^#(sq(x1))	→	s^#(p(x1))	(16)
0^#(sq(x1))	→	s^#(p(s(p(x1))))	(17)
0^#(sq(x1))	→	s^#(p(p(p(p(s(p(s(p(x1)))))))))	(18)
0^#(sq(x1))	→	s^#(s(p(p(p(p(s(p(s(p(x1))))))))))	(19)
0^#(sq(x1))	→	s^#(s(s(p(p(p(p(s(p(s(p(x1)))))))))))	(20)
0^#(sq(x1))	→	s^#(s(s(s(p(p(p(p(s(p(s(p(x1))))))))))))	(21)
0^#(sq(x1))	→	0^#(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))	(22)
0^#(sq(x1))	→	s^#(p(0(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))))	(23)
0^#(sq(x1))	→	s^#(p(s(p(0(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))))))	(24)
s^#(sq(x1))	→	s^#(x1)	(25)
s^#(sq(x1))	→	s^#(p(s(x1)))	(26)
s^#(sq(x1))	→	s^#(p(s(p(s(x1)))))	(27)
s^#(sq(x1))	→	s^#(p(p(s(p(s(p(s(x1))))))))	(28)
s^#(sq(x1))	→	s^#(s(p(p(s(p(s(p(s(x1)))))))))	(29)
s^#(sq(x1))	→	s^#(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))	(30)
s^#(sq(x1))	→	s^#(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))	(31)
s^#(sq(x1))	→	s^#(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))	(32)
s^#(sq(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))	(33)
s^#(sq(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))	(34)
s^#(sq(x1))	→	s^#(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))	(35)
s^#(sq(x1))	→	s^#(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))	(36)
s^#(sq(x1))	→	s^#(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))	(37)
s^#(sq(x1))	→	s^#(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))	(38)
s^#(sq(x1))	→	s^#(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))	(39)
s^#(sq(x1))	→	s^#(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(40)
0^#(twice(x1))	→	s^#(p(p(p(p(x1)))))	(41)
0^#(twice(x1))	→	s^#(s(p(p(p(p(x1))))))	(42)
0^#(twice(x1))	→	s^#(p(s(s(p(p(p(p(x1))))))))	(43)
0^#(twice(x1))	→	s^#(s(p(s(s(p(p(p(p(x1)))))))))	(44)
0^#(twice(x1))	→	s^#(s(s(p(s(s(p(p(p(p(x1))))))))))	(45)
0^#(twice(x1))	→	0^#(s(s(s(p(s(s(p(p(p(p(x1)))))))))))	(46)
0^#(twice(x1))	→	s^#(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))	(47)
0^#(twice(x1))	→	s^#(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1))))))))))))))))	(48)
0^#(twice(x1))	→	s^#(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))	(49)
0^#(twice(x1))	→	s^#(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1))))))))))))))))))))	(50)
0^#(twice(x1))	→	s^#(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))))))	(51)
0^#(twice(x1))	→	s^#(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))))))))	(52)
0^#(twice(x1))	→	s^#(p(s(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))))))))))	(53)
0^#(twice(x1))	→	s^#(p(s(p(s(p(s(s(p(p(s(s(s(p(p(p(0(s(s(s(p(s(s(p(p(p(p(x1)))))))))))))))))))))))))))	(54)
s^#(twice(x1))	→	s^#(p(p(x1)))	(55)
s^#(twice(x1))	→	s^#(s(p(p(x1))))	(56)
s^#(twice(x1))	→	s^#(s(s(p(p(x1)))))	(57)
s^#(twice(x1))	→	s^#(p(p(s(s(s(p(p(x1))))))))	(58)
s^#(twice(x1))	→	s^#(s(p(p(s(s(s(p(p(x1)))))))))	(59)
s^#(twice(x1))	→	s^#(s(s(p(p(s(s(s(p(p(x1))))))))))	(60)
s^#(twice(x1))	→	s^#(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))	(61)
s^#(twice(x1))	→	s^#(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(62)
0^#(p(x1))	→	0^#(x1)	(63)
0^#(p(x1))	→	s^#(0(x1))	(64)
0^#(p(x1))	→	s^#(s(0(x1)))	(65)
0^#(p(x1))	→	s^#(s(s(0(x1))))	(66)
0^#(p(x1))	→	s^#(s(s(s(0(x1)))))	(67)
0^#(p(x1))	→	s^#(s(s(s(s(0(x1))))))	(68)
0^#(p(x1))	→	s^#(s(s(s(s(s(0(x1)))))))	(69)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(0(x1))))))))	(70)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(s(0(x1)))))))))	(71)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(s(s(0(x1))))))))))	(72)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(s(s(s(0(x1)))))))))))	(73)
0^#(p(x1))	→	s^#(s(s(s(s(s(s(s(s(s(s(0(x1))))))))))))	(74)

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^#(s(s(s(p(s(s(p(p(p(p(x1)))))))))))	(46)
0^#(p(x1))	→	0^#(x1)	(63)
0^#(sq(x1))	→	0^#(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))	(22)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the

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

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

together with the usable rules

s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)
s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)

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

0^#(sq(x1))

→

0^#(s(s(s(s(p(p(p(p(s(p(s(p(x1)))))))))))))

(22)

could be deleted.

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the

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

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

together with the usable rules

s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)
s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)

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

0^#(twice(x1))

→

0^#(s(s(s(p(s(s(p(p(p(p(x1)))))))))))

(46)

could be deleted.

1.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^#(p(x1))	→	0^#(x1)	(63)

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(p(p(s(s(s(p(p(x1)))))))))	(59)
s^#(twice(x1))	→	s^#(s(s(p(p(s(s(s(p(p(x1))))))))))	(60)
s^#(twice(x1))	→	s^#(s(s(p(p(x1)))))	(57)
s^#(twice(x1))	→	s^#(s(p(p(x1))))	(56)
s^#(sq(x1))	→	s^#(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(40)
s^#(sq(x1))	→	s^#(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))	(39)
s^#(sq(x1))	→	s^#(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))	(38)
s^#(sq(x1))	→	s^#(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))	(37)
s^#(sq(x1))	→	s^#(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))	(36)
s^#(sq(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))	(34)
s^#(sq(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))	(33)
s^#(sq(x1))	→	s^#(s(p(p(s(p(s(p(s(x1)))))))))	(29)
s^#(sq(x1))	→	s^#(x1)	(25)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the

prec(s^#)	=	stat(s^#)	=	lex
prec(twice)	=	stat(twice)	=	lex
prec(p)	=	stat(p)	=	lex
prec(s)	=	stat(s)	=	lex
prec(sq)	=	stat(sq)	=	lex

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

together with the usable rules

s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)
s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)

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

s^#(sq(x1))	→	s^#(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))	(34)
s^#(sq(x1))	→	s^#(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))	(33)
s^#(sq(x1))	→	s^#(s(p(p(s(p(s(p(s(x1)))))))))	(29)
s^#(sq(x1))	→	s^#(x1)	(25)

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(p)	=	stat(p)	=	lex
prec(s)	=	stat(s)	=	lex
prec(sq)	=	stat(sq)	=	lex

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

together with the usable rules

s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)
s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)

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

s^#(twice(x1))	→	s^#(s(p(p(s(s(s(p(p(x1)))))))))	(59)
s^#(twice(x1))	→	s^#(s(s(p(p(s(s(s(p(p(x1))))))))))	(60)
s^#(twice(x1))	→	s^#(s(s(p(p(x1)))))	(57)
s^#(twice(x1))	→	s^#(s(p(p(x1))))	(56)

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

[twice(x₁)]	=	-∞ · x₁ + 6
[sq(x₁)]	=	0 · x₁ + 5
[p(x₁)]	=	-1 · x₁ + 0
[s^#(x₁)]	=	0 · x₁ + 0
[s(x₁)]	=	1 · x₁ + 0

together with the usable rules

s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)
s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)

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

s^#(sq(x1))	→	s^#(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))))	(39)
s^#(sq(x1))	→	s^#(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))	(38)
s^#(sq(x1))	→	s^#(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1))))))))))))))))))))))))))))))	(37)
s^#(sq(x1))	→	s^#(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))	(36)

could be deleted.

1.1.1.1.2.1.1.1 Reduction Pair Processor with Usable Rules

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

[twice(x₁)]	=	-∞ · x₁ + 0
[sq(x₁)]	=	-∞ · x₁ + 6
[p(x₁)]	=	-1 · x₁ + 0
[s^#(x₁)]	=	0 · x₁ + 0
[s(x₁)]	=	1 · x₁ + 0

together with the usable rules

s(sq(x1))	→	s(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))	(10)
s(twice(x1))	→	s(p(s(p(twice(s(s(s(p(p(s(s(s(p(p(x1)))))))))))))))	(12)
s(p(p(x1)))	→	p(x1)	(13)
s(p(x1))	→	x1	(14)

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

s^#(sq(x1))

→

s^#(s(s(s(s(s(p(p(p(p(p(p(sq(s(s(s(p(p(p(s(p(s(p(twice(s(s(p(p(s(p(s(p(s(x1)))))))))))))))))))))))))))))))))

(40)

could be deleted.

1.1.1.1.2.1.1.1.1 P is empty

There are no pairs anymore.