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 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₁ +

[a56(x₁)]

x₁ +

[a16(x₁)]

x₁ +

[a15(x₁)]

x₁ +

[a14(x₁)]

x₁ +

[a13(x₁)]

x₁ +

[a12(x₁)]

x₁ +

[a23(x₁)]

x₁ +

[a26(x₁)]

x₁ +

[a24(x₁)]

x₁ +

[a25(x₁)]

x₁ +

[a35(x₁)]

x₁ +

[a34(x₁)]

x₁ +

[a36(x₁)]

x₁ +

all of the following rules can be deleted.

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)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a12^#(a45(x1))	→	a12^#(x1)	(36)
a12^#(a56(x1))	→	a12^#(x1)	(37)
a12^#(a34(x1))	→	a12^#(x1)	(38)
a12^#(a34(x1))	→	a34^#(a12(x1))	(39)
a23^#(a45(x1))	→	a23^#(x1)	(40)
a23^#(a56(x1))	→	a23^#(x1)	(41)
a34^#(a56(x1))	→	a34^#(x1)	(42)

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(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)

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

a12^#(a45(x1))	→	a12^#(x1)	(36)
a12^#(a56(x1))	→	a12^#(x1)	(37)
a12^#(a34(x1))	→	a12^#(x1)	(38)
a12^#(a34(x1))	→	a34^#(a12(x1))	(39)
a23^#(a45(x1))	→	a23^#(x1)	(40)
a23^#(a56(x1))	→	a23^#(x1)	(41)
a34^#(a56(x1))	→	a34^#(x1)	(42)

and no rules could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.