Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/s6)

The rewrite relation of the following TRS is considered.

a12(a12(x1))	→	x1	(1)
a13(a13(x1))	→	x1	(2)
a14(a14(x1))	→	x1	(3)
a15(a15(x1))	→	x1	(4)
a16(a16(x1))	→	x1	(5)
a23(a23(x1))	→	x1	(6)
a24(a24(x1))	→	x1	(7)
a25(a25(x1))	→	x1	(8)
a26(a26(x1))	→	x1	(9)
a34(a34(x1))	→	x1	(10)
a35(a35(x1))	→	x1	(11)
a36(a36(x1))	→	x1	(12)
a45(a45(x1))	→	x1	(13)
a46(a46(x1))	→	x1	(14)
a56(a56(x1))	→	x1	(15)
a13(x1)	→	a12(a23(a12(x1)))	(16)
a14(x1)	→	a12(a23(a34(a23(a12(x1)))))	(17)
a15(x1)	→	a12(a23(a34(a45(a34(a23(a12(x1)))))))	(18)
a16(x1)	→	a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))	(19)
a24(x1)	→	a23(a34(a23(x1)))	(20)
a25(x1)	→	a23(a34(a45(a34(a23(x1)))))	(21)
a26(x1)	→	a23(a34(a45(a56(a45(a34(a23(x1)))))))	(22)
a35(x1)	→	a34(a45(a34(x1)))	(23)
a36(x1)	→	a34(a45(a56(a45(a34(x1)))))	(24)
a46(x1)	→	a45(a56(a45(x1)))	(25)
a12(a23(a12(a23(a12(a23(x1))))))	→	x1	(26)
a23(a34(a23(a34(a23(a34(x1))))))	→	x1	(27)
a34(a45(a34(a45(a34(a45(x1))))))	→	x1	(28)
a45(a56(a45(a56(a45(a56(x1))))))	→	x1	(29)
a12(a34(x1))	→	a34(a12(x1))	(30)
a12(a45(x1))	→	a45(a12(x1))	(31)
a12(a56(x1))	→	a56(a12(x1))	(32)
a23(a45(x1))	→	a45(a23(x1))	(33)
a23(a56(x1))	→	a56(a23(x1))	(34)
a34(a56(x1))	→	a56(a34(x1))	(35)

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.

a34^#(a56(x1))	→	a34^#(x1)	(36)
a16^#(x1)	→	a56^#(a45(a34(a23(a12(x1)))))	(37)
a26^#(x1)	→	a23^#(x1)	(38)
a14^#(x1)	→	a23^#(a12(x1))	(39)
a16^#(x1)	→	a23^#(a12(x1))	(40)
a16^#(x1)	→	a45^#(a56(a45(a34(a23(a12(x1))))))	(41)
a16^#(x1)	→	a34^#(a45(a56(a45(a34(a23(a12(x1)))))))	(42)
a12^#(a56(x1))	→	a56^#(a12(x1))	(43)
a16^#(x1)	→	a12^#(x1)	(44)
a13^#(x1)	→	a12^#(a23(a12(x1)))	(45)
a25^#(x1)	→	a23^#(a34(a45(a34(a23(x1)))))	(46)
a15^#(x1)	→	a34^#(a45(a34(a23(a12(x1)))))	(47)
a15^#(x1)	→	a23^#(a12(x1))	(48)
a12^#(a56(x1))	→	a12^#(x1)	(49)
a36^#(x1)	→	a45^#(a34(x1))	(50)
a15^#(x1)	→	a45^#(a34(a23(a12(x1))))	(51)
a13^#(x1)	→	a12^#(x1)	(52)
a16^#(x1)	→	a23^#(a34(a45(a56(a45(a34(a23(a12(x1))))))))	(53)
a25^#(x1)	→	a34^#(a23(x1))	(54)
a12^#(a34(x1))	→	a34^#(a12(x1))	(55)
a35^#(x1)	→	a45^#(a34(x1))	(56)
a12^#(a45(x1))	→	a45^#(a12(x1))	(57)
a15^#(x1)	→	a23^#(a34(a45(a34(a23(a12(x1))))))	(58)
a26^#(x1)	→	a34^#(a45(a56(a45(a34(a23(x1))))))	(59)
a26^#(x1)	→	a23^#(a34(a45(a56(a45(a34(a23(x1)))))))	(60)
a16^#(x1)	→	a34^#(a23(a12(x1)))	(61)
a12^#(a45(x1))	→	a12^#(x1)	(62)
a23^#(a56(x1))	→	a23^#(x1)	(63)
a15^#(x1)	→	a12^#(a23(a34(a45(a34(a23(a12(x1)))))))	(64)
a12^#(a34(x1))	→	a12^#(x1)	(65)
a15^#(x1)	→	a12^#(x1)	(66)
a23^#(a56(x1))	→	a56^#(a23(x1))	(67)
a25^#(x1)	→	a23^#(x1)	(68)
a25^#(x1)	→	a34^#(a45(a34(a23(x1))))	(69)
a26^#(x1)	→	a45^#(a56(a45(a34(a23(x1)))))	(70)
a24^#(x1)	→	a23^#(x1)	(71)
a36^#(x1)	→	a34^#(x1)	(72)
a16^#(x1)	→	a12^#(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))	(73)
a35^#(x1)	→	a34^#(x1)	(74)
a14^#(x1)	→	a23^#(a34(a23(a12(x1))))	(75)
a36^#(x1)	→	a56^#(a45(a34(x1)))	(76)
a16^#(x1)	→	a45^#(a34(a23(a12(x1))))	(77)
a26^#(x1)	→	a34^#(a23(x1))	(78)
a23^#(a45(x1))	→	a23^#(x1)	(79)
a14^#(x1)	→	a34^#(a23(a12(x1)))	(80)
a26^#(x1)	→	a45^#(a34(a23(x1)))	(81)
a15^#(x1)	→	a34^#(a23(a12(x1)))	(82)
a46^#(x1)	→	a45^#(x1)	(83)
a14^#(x1)	→	a12^#(a23(a34(a23(a12(x1)))))	(84)
a24^#(x1)	→	a34^#(a23(x1))	(85)
a26^#(x1)	→	a56^#(a45(a34(a23(x1))))	(86)
a14^#(x1)	→	a12^#(x1)	(87)
a23^#(a45(x1))	→	a45^#(a23(x1))	(88)
a46^#(x1)	→	a56^#(a45(x1))	(89)
a36^#(x1)	→	a34^#(a45(a56(a45(a34(x1)))))	(90)
a34^#(a56(x1))	→	a56^#(a34(x1))	(91)
a13^#(x1)	→	a23^#(a12(x1))	(92)
a35^#(x1)	→	a34^#(a45(a34(x1)))	(93)
a46^#(x1)	→	a45^#(a56(a45(x1)))	(94)
a36^#(x1)	→	a45^#(a56(a45(a34(x1))))	(95)
a25^#(x1)	→	a45^#(a34(a23(x1)))	(96)
a24^#(x1)	→	a23^#(a34(a23(x1)))	(97)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

a12^#(a34(x1))	→	a12^#(x1)	(65)
a12^#(a45(x1))	→	a12^#(x1)	(62)
a12^#(a56(x1))	→	a12^#(x1)	(49)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a15^#(x₁)]	=	0
[a24^#(x₁)]	=	0
[a36(x₁)]	=	0
[a25(x₁)]	=	0
[a23^#(x₁)]	=	0
[a16^#(x₁)]	=	0
[a16(x₁)]	=	0
[a24(x₁)]	=	0
[a36^#(x₁)]	=	0
[a45(x₁)]	=	x₁ + 1
[a34(x₁)]	=	x₁ + 1
[a26(x₁)]	=	0
[a56(x₁)]	=	x₁ + 1
[a13(x₁)]	=	0
[a25^#(x₁)]	=	0
[a12^#(x₁)]	=	x₁ + 0
[a15(x₁)]	=	0
[a14(x₁)]	=	0
[a23(x₁)]	=	0
[a46^#(x₁)]	=	0
[a14^#(x₁)]	=	0
[a26^#(x₁)]	=	0
[a12(x₁)]	=	0
[a45^#(x₁)]	=	0
[a35(x₁)]	=	0
[a13^#(x₁)]	=	0
[a34^#(x₁)]	=	0
[a35^#(x₁)]	=	0
[a46(x₁)]	=	0
[a56^#(x₁)]	=	0

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

a12^#(a34(x1))	→	a12^#(x1)	(65)
a12^#(a45(x1))	→	a12^#(x1)	(62)
a12^#(a56(x1))	→	a12^#(x1)	(49)

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

a34^#(a56(x1))

→

a34^#(x1)

(36)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a15^#(x₁)]	=	0
[a24^#(x₁)]	=	0
[a36(x₁)]	=	0
[a25(x₁)]	=	0
[a23^#(x₁)]	=	0
[a16^#(x₁)]	=	0
[a16(x₁)]	=	0
[a24(x₁)]	=	0
[a36^#(x₁)]	=	0
[a45(x₁)]	=	1
[a34(x₁)]	=	1
[a26(x₁)]	=	0
[a56(x₁)]	=	x₁ + 1
[a13(x₁)]	=	0
[a25^#(x₁)]	=	0
[a12^#(x₁)]	=	0
[a15(x₁)]	=	0
[a14(x₁)]	=	0
[a23(x₁)]	=	0
[a46^#(x₁)]	=	0
[a14^#(x₁)]	=	0
[a26^#(x₁)]	=	0
[a12(x₁)]	=	0
[a45^#(x₁)]	=	0
[a35(x₁)]	=	0
[a13^#(x₁)]	=	0
[a34^#(x₁)]	=	x₁ + 0
[a35^#(x₁)]	=	0
[a46(x₁)]	=	0
[a56^#(x₁)]	=	0

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

a34^#(a56(x1))

→

a34^#(x1)

(36)

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

a23^#(a56(x1))	→	a23^#(x1)	(63)
a23^#(a45(x1))	→	a23^#(x1)	(79)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a15^#(x₁)]	=	0
[a24^#(x₁)]	=	0
[a36(x₁)]	=	0
[a25(x₁)]	=	0
[a23^#(x₁)]	=	x₁ + 0
[a16^#(x₁)]	=	0
[a16(x₁)]	=	0
[a24(x₁)]	=	0
[a36^#(x₁)]	=	0
[a45(x₁)]	=	x₁ + 1
[a34(x₁)]	=	1
[a26(x₁)]	=	0
[a56(x₁)]	=	x₁ + 1
[a13(x₁)]	=	0
[a25^#(x₁)]	=	0
[a12^#(x₁)]	=	0
[a15(x₁)]	=	0
[a14(x₁)]	=	0
[a23(x₁)]	=	0
[a46^#(x₁)]	=	0
[a14^#(x₁)]	=	0
[a26^#(x₁)]	=	0
[a12(x₁)]	=	0
[a45^#(x₁)]	=	0
[a35(x₁)]	=	0
[a13^#(x₁)]	=	0
[a34^#(x₁)]	=	0
[a35^#(x₁)]	=	0
[a46(x₁)]	=	0
[a56^#(x₁)]	=	0

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

a23^#(a56(x1))	→	a23^#(x1)	(63)
a23^#(a45(x1))	→	a23^#(x1)	(79)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.