Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup01)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[a45(x₁)]

x₁ +

[a46(x₁)]

x₁ +

19/2

[a56(x₁)]

x₁ +

[a16(x₁)]

x₁ +

19/2

[a15(x₁)]

x₁ +

19/2

[a14(x₁)]

x₁ +

19/2

[a13(x₁)]

x₁ +

19/2

[a12(x₁)]

x₁ +

[a23(x₁)]

x₁ +

[a26(x₁)]

x₁ +

19/2

[a24(x₁)]

x₁ +

19/2

[a25(x₁)]

x₁ +

19/2

[a35(x₁)]

x₁ +

19/2

[a34(x₁)]

x₁ +

[a36(x₁)]

x₁ +

19/2

all of the following rules can be deleted.

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

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a12^#(a12(a45(a45(x1))))	→	a12^#(x1)	(36)
a12^#(a12(a45(a45(x1))))	→	a12^#(a12(x1))	(37)
a12^#(a12(a56(a56(x1))))	→	a12^#(x1)	(38)
a12^#(a12(a56(a56(x1))))	→	a12^#(a12(x1))	(39)
a12^#(a12(a34(a34(x1))))	→	a12^#(x1)	(40)
a12^#(a12(a34(a34(x1))))	→	a12^#(a12(x1))	(41)
a12^#(a12(a34(a34(x1))))	→	a34^#(a12(a12(x1)))	(42)
a12^#(a12(a34(a34(x1))))	→	a34^#(a34(a12(a12(x1))))	(43)
a23^#(a23(a45(a45(x1))))	→	a23^#(x1)	(44)
a23^#(a23(a45(a45(x1))))	→	a23^#(a23(x1))	(45)
a23^#(a23(a56(a56(x1))))	→	a23^#(x1)	(46)
a23^#(a23(a56(a56(x1))))	→	a23^#(a23(x1))	(47)
a34^#(a34(a56(a56(x1))))	→	a34^#(x1)	(48)
a34^#(a34(a56(a56(x1))))	→	a34^#(a34(x1))	(49)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

[a45(x₁)]

x₁ +

[a56(x₁)]

x₁ +

[a12(x₁)]

x₁ +

[a23(x₁)]

x₁ +

[a34(x₁)]

x₁ +

[a12^#(x₁)]

x₁ +

[a23^#(x₁)]

x₁ +

[a34^#(x₁)]

x₁ +

together with the usable rules

a12(a12(a34(a34(x1))))	→	a34(a34(a12(a12(x1))))	(30)
a12(a12(a45(a45(x1))))	→	a45(a45(a12(a12(x1))))	(31)
a12(a12(a56(a56(x1))))	→	a56(a56(a12(a12(x1))))	(32)
a23(a23(a45(a45(x1))))	→	a45(a45(a23(a23(x1))))	(33)
a23(a23(a56(a56(x1))))	→	a56(a56(a23(a23(x1))))	(34)
a34(a34(a56(a56(x1))))	→	a56(a56(a34(a34(x1))))	(35)

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

a12^#(a12(a45(a45(x1))))	→	a12^#(x1)	(36)
a12^#(a12(a45(a45(x1))))	→	a12^#(a12(x1))	(37)
a12^#(a12(a56(a56(x1))))	→	a12^#(x1)	(38)
a12^#(a12(a56(a56(x1))))	→	a12^#(a12(x1))	(39)
a12^#(a12(a34(a34(x1))))	→	a12^#(x1)	(40)
a12^#(a12(a34(a34(x1))))	→	a12^#(a12(x1))	(41)
a12^#(a12(a34(a34(x1))))	→	a34^#(a12(a12(x1)))	(42)
a12^#(a12(a34(a34(x1))))	→	a34^#(a34(a12(a12(x1))))	(43)
a23^#(a23(a45(a45(x1))))	→	a23^#(x1)	(44)
a23^#(a23(a45(a45(x1))))	→	a23^#(a23(x1))	(45)
a23^#(a23(a56(a56(x1))))	→	a23^#(x1)	(46)
a23^#(a23(a56(a56(x1))))	→	a23^#(a23(x1))	(47)
a34^#(a34(a56(a56(x1))))	→	a34^#(x1)	(48)
a34^#(a34(a56(a56(x1))))	→	a34^#(a34(x1))	(49)

and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.