Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z092)

The rewrite relation of the following TRS is considered.

q0(0(x1))	→	0'(q1(x1))	(1)
q1(0(x1))	→	0(q1(x1))	(2)
q1(1'(x1))	→	1'(q1(x1))	(3)
0(q1(1(x1)))	→	q2(0(1'(x1)))	(4)
0'(q1(1(x1)))	→	q2(0'(1'(x1)))	(5)
1'(q1(1(x1)))	→	q2(1'(1'(x1)))	(6)
0(q2(0(x1)))	→	q2(0(0(x1)))	(7)
0'(q2(0(x1)))	→	q2(0'(0(x1)))	(8)
1'(q2(0(x1)))	→	q2(1'(0(x1)))	(9)
0(q2(1'(x1)))	→	q2(0(1'(x1)))	(10)
0'(q2(1'(x1)))	→	q2(0'(1'(x1)))	(11)
1'(q2(1'(x1)))	→	q2(1'(1'(x1)))	(12)
q2(0'(x1))	→	0'(q0(x1))	(13)
q0(1'(x1))	→	1'(q3(x1))	(14)
q3(1'(x1))	→	1'(q3(x1))	(15)
q3(b(x1))	→	b(q4(x1))	(16)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals

[q0(x₁)]	=	1 · x₁ + 2
[0(x₁)]	=	1 · x₁
[0'(x₁)]	=	1 · x₁
[q1(x₁)]	=	1 · x₁
[1'(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁ + 3
[q2(x₁)]	=	1 · x₁ + 3
[q3(x₁)]	=	1 · x₁ + 1
[b(x₁)]	=	1 · x₁
[q4(x₁)]	=	1 · x₁

all of the following rules can be deleted.

q0(0(x1))	→	0'(q1(x1))	(1)
q2(0'(x1))	→	0'(q0(x1))	(13)
q0(1'(x1))	→	1'(q3(x1))	(14)
q3(b(x1))	→	b(q4(x1))	(16)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[q1(x₁)]	=	1 · x₁
[0(x₁)]	=	1 · x₁
[1'(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁ + 1
[q2(x₁)]	=	1 · x₁
[0'(x₁)]	=	1 · x₁
[q3(x₁)]	=	1 · x₁

all of the following rules can be deleted.

0(q1(1(x1)))	→	q2(0(1'(x1)))	(4)
0'(q1(1(x1)))	→	q2(0'(1'(x1)))	(5)
1'(q1(1(x1)))	→	q2(1'(1'(x1)))	(6)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

q1^#(0(x1))	→	0^#(q1(x1))	(17)
q1^#(0(x1))	→	q1^#(x1)	(18)
q1^#(1'(x1))	→	1'^#(q1(x1))	(19)
q1^#(1'(x1))	→	q1^#(x1)	(20)
0^#(q2(0(x1)))	→	0^#(0(x1))	(21)
0'^#(q2(0(x1)))	→	0'^#(0(x1))	(22)
1'^#(q2(0(x1)))	→	1'^#(0(x1))	(23)
0^#(q2(1'(x1)))	→	0^#(1'(x1))	(24)
0'^#(q2(1'(x1)))	→	0'^#(1'(x1))	(25)
1'^#(q2(1'(x1)))	→	1'^#(1'(x1))	(26)
q3^#(1'(x1))	→	1'^#(q3(x1))	(27)
q3^#(1'(x1))	→	q3^#(x1)	(28)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

q1^#(1'(x1)) → q1^#(x1) (20)

q1^#(0(x1)) → q1^#(x1) (18)

1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[1'(x₁)] = 1 · x₁

[0(x₁)] = 1 · x₁

[q1^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule 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.

q1^#(1'(x1)) → q1^#(x1) (20)

1 > 1

q1^#(0(x1)) → q1^#(x1) (18)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
q3^#(1'(x1)) → q3^#(x1) (28)

1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[1'(x₁)] = 1 · x₁

[q3^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.2.1 Size-Change Termination

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

q3^#(1'(x1)) → q3^#(x1) (28)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair

0^#(q2(1'(x1))) → 0^#(1'(x1)) (24)

0^#(q2(0(x1))) → 0^#(0(x1)) (21)

1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[0(x₁)] = 1 · x₁

[q2(x₁)] = 1 · x₁

[1'(x₁)] = 1 · x₁

[0^#(x₁)] = 1 · x₁

together with the usable rules

0(q2(0(x1))) → q2(0(0(x1))) (7)

0(q2(1'(x1))) → q2(0(1'(x1))) (10)

1'(q2(0(x1))) → q2(1'(0(x1))) (9)

1'(q2(1'(x1))) → q2(1'(1'(x1))) (12)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.3.1 Size-Change Termination

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

0^#(q2(1'(x1))) → 0^#(1'(x1)) (24)

1 > 1

0^#(q2(0(x1))) → 0^#(0(x1)) (21)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair

0'^#(q2(1'(x1))) → 0'^#(1'(x1)) (25)

0'^#(q2(0(x1))) → 0'^#(0(x1)) (22)

1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[0(x₁)] = 1 · x₁

[q2(x₁)] = 1 · x₁

[1'(x₁)] = 1 · x₁

[0'^#(x₁)] = 1 · x₁

together with the usable rules

0(q2(0(x1))) → q2(0(0(x1))) (7)

0(q2(1'(x1))) → q2(0(1'(x1))) (10)

1'(q2(0(x1))) → q2(1'(0(x1))) (9)

1'(q2(1'(x1))) → q2(1'(1'(x1))) (12)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.4.1 Size-Change Termination

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

0'^#(q2(1'(x1))) → 0'^#(1'(x1)) (25)

1 > 1

0'^#(q2(0(x1))) → 0'^#(0(x1)) (22)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 5^th component contains the pair

1'^#(q2(1'(x1))) → 1'^#(1'(x1)) (26)

1'^#(q2(0(x1))) → 1'^#(0(x1)) (23)

1.1.1.1.5 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[0(x₁)] = 1 · x₁

[q2(x₁)] = 1 · x₁

[1'(x₁)] = 1 · x₁

[1'^#(x₁)] = 1 · x₁

together with the usable rules

0(q2(0(x1))) → q2(0(0(x1))) (7)

0(q2(1'(x1))) → q2(0(1'(x1))) (10)

1'(q2(0(x1))) → q2(1'(0(x1))) (9)

1'(q2(1'(x1))) → q2(1'(1'(x1))) (12)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.5.1 Size-Change Termination

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

1'^#(q2(1'(x1))) → 1'^#(1'(x1)) (26)

1 > 1

1'^#(q2(0(x1))) → 1'^#(0(x1)) (23)

1 > 1

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

Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z092)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

1.1 Rule Removal

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.1.1 Size-Change Termination

1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.2.1 Size-Change Termination

1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.3.1 Size-Change Termination

1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.4.1 Size-Change Termination

1.1.1.1.5 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.5.1 Size-Change Termination