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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

q1^#(0(x1))	→	q1^#(x1)	(17)
q3^#(1'(x1))	→	1'^#(q3(x1))	(18)
q2^#(0'(x1))	→	0'^#(q0(x1))	(19)
1'^#(q2(1'(x1)))	→	1'^#(1'(x1))	(20)
1'^#(q2(0(x1)))	→	1'^#(0(x1))	(21)
0'^#(q2(1'(x1)))	→	0'^#(1'(x1))	(22)
q1^#(1'(x1))	→	q1^#(x1)	(23)
q1^#(1'(x1))	→	1'^#(q1(x1))	(24)
1'^#(q2(1'(x1)))	→	q2^#(1'(1'(x1)))	(25)
0^#(q1(1(x1)))	→	q2^#(0(1'(x1)))	(26)
q0^#(1'(x1))	→	1'^#(q3(x1))	(27)
q3^#(1'(x1))	→	q3^#(x1)	(28)
q0^#(0(x1))	→	0'^#(q1(x1))	(29)
0'^#(q1(1(x1)))	→	q2^#(0'(1'(x1)))	(30)
q2^#(0'(x1))	→	q0^#(x1)	(31)
0'^#(q2(1'(x1)))	→	q2^#(0'(1'(x1)))	(32)
0^#(q1(1(x1)))	→	1'^#(x1)	(33)
1'^#(q1(1(x1)))	→	1'^#(x1)	(34)
0'^#(q2(0(x1)))	→	0'^#(0(x1))	(35)
0'^#(q1(1(x1)))	→	1'^#(x1)	(36)
0'^#(q2(0(x1)))	→	q2^#(0'(0(x1)))	(37)
0^#(q2(0(x1)))	→	0^#(0(x1))	(38)
0^#(q1(1(x1)))	→	0^#(1'(x1))	(39)
0^#(q2(1'(x1)))	→	0^#(1'(x1))	(40)
q0^#(0(x1))	→	q1^#(x1)	(41)
0'^#(q1(1(x1)))	→	0'^#(1'(x1))	(42)
0^#(q2(0(x1)))	→	q2^#(0(0(x1)))	(43)
1'^#(q1(1(x1)))	→	q2^#(1'(1'(x1)))	(44)
q1^#(0(x1))	→	0^#(q1(x1))	(45)
1'^#(q2(0(x1)))	→	q2^#(1'(0(x1)))	(46)
q0^#(1'(x1))	→	q3^#(x1)	(47)
1'^#(q1(1(x1)))	→	1'^#(1'(x1))	(48)
0^#(q2(1'(x1)))	→	q2^#(0(1'(x1)))	(49)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

0^#(q2(1'(x1)))	→	q2^#(0(1'(x1)))	(49)
q0^#(0(x1))	→	0'^#(q1(x1))	(29)
1'^#(q1(1(x1)))	→	1'^#(1'(x1))	(48)
q3^#(1'(x1))	→	q3^#(x1)	(28)
q0^#(1'(x1))	→	1'^#(q3(x1))	(27)
q0^#(1'(x1))	→	q3^#(x1)	(47)
0^#(q1(1(x1)))	→	q2^#(0(1'(x1)))	(26)
1'^#(q2(1'(x1)))	→	q2^#(1'(1'(x1)))	(25)
1'^#(q2(0(x1)))	→	q2^#(1'(0(x1)))	(46)
q1^#(0(x1))	→	0^#(q1(x1))	(45)
q1^#(1'(x1))	→	1'^#(q1(x1))	(24)
1'^#(q1(1(x1)))	→	q2^#(1'(1'(x1)))	(44)
q1^#(1'(x1))	→	q1^#(x1)	(23)
0^#(q2(0(x1)))	→	q2^#(0(0(x1)))	(43)
0'^#(q1(1(x1)))	→	0'^#(1'(x1))	(42)
q0^#(0(x1))	→	q1^#(x1)	(41)
0'^#(q2(1'(x1)))	→	0'^#(1'(x1))	(22)
1'^#(q2(0(x1)))	→	1'^#(0(x1))	(21)
1'^#(q2(1'(x1)))	→	1'^#(1'(x1))	(20)
0^#(q1(1(x1)))	→	0^#(1'(x1))	(39)
0^#(q2(1'(x1)))	→	0^#(1'(x1))	(40)
0^#(q2(0(x1)))	→	0^#(0(x1))	(38)
q2^#(0'(x1))	→	0'^#(q0(x1))	(19)
0'^#(q2(0(x1)))	→	q2^#(0'(0(x1)))	(37)
0'^#(q1(1(x1)))	→	1'^#(x1)	(36)
0'^#(q2(0(x1)))	→	0'^#(0(x1))	(35)
1'^#(q1(1(x1)))	→	1'^#(x1)	(34)
0^#(q1(1(x1)))	→	1'^#(x1)	(33)
0'^#(q2(1'(x1)))	→	q2^#(0'(1'(x1)))	(32)
q2^#(0'(x1))	→	q0^#(x1)	(31)
q3^#(1'(x1))	→	1'^#(q3(x1))	(18)
q1^#(0(x1))	→	q1^#(x1)	(17)
0'^#(q1(1(x1)))	→	q2^#(0'(1'(x1)))	(30)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	19431
[1(x₁)]	=	1
[0'^#(x₁)]	=	19433
[1'(x₁)]	=	18589
[b(x₁)]	=	2
[q3(x₁)]	=	1
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	18590
[q0^#(x₁)]	=	19433
[0(x₁)]	=	2
[0'(x₁)]	=	19433
[q1(x₁)]	=	1
[q2(x₁)]	=	x₁ + 0
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 19431
[q2^#(x₁)]	=	x₁ + 0

together with the usable rules

0(q1(1(x1)))	→	q2(0(1'(x1)))	(4)
0'(q2(0(x1)))	→	q2(0'(0(x1)))	(8)
q0(0(x1))	→	0'(q1(x1))	(1)
0'(q1(1(x1)))	→	q2(0'(1'(x1)))	(5)
0(q2(1'(x1)))	→	q2(0(1'(x1)))	(10)
0(q2(0(x1)))	→	q2(0(0(x1)))	(7)
q0(1'(x1))	→	1'(q3(x1))	(14)
1'(q2(1'(x1)))	→	q2(1'(1'(x1)))	(12)
0'(q2(1'(x1)))	→	q2(0'(1'(x1)))	(11)
1'(q2(0(x1)))	→	q2(1'(0(x1)))	(9)
q2(0'(x1))	→	0'(q0(x1))	(13)
1'(q1(1(x1)))	→	q2(1'(1'(x1)))	(6)

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

0^#(q2(1'(x1)))	→	q2^#(0(1'(x1)))	(49)
q0^#(1'(x1))	→	1'^#(q3(x1))	(27)
q0^#(1'(x1))	→	q3^#(x1)	(47)
0^#(q1(1(x1)))	→	q2^#(0(1'(x1)))	(26)
1'^#(q2(1'(x1)))	→	q2^#(1'(1'(x1)))	(25)
1'^#(q2(0(x1)))	→	q2^#(1'(0(x1)))	(46)
q1^#(0(x1))	→	0^#(q1(x1))	(45)
q1^#(1'(x1))	→	1'^#(q1(x1))	(24)
1'^#(q1(1(x1)))	→	q2^#(1'(1'(x1)))	(44)
0^#(q2(0(x1)))	→	q2^#(0(0(x1)))	(43)
q0^#(0(x1))	→	q1^#(x1)	(41)
0'^#(q1(1(x1)))	→	1'^#(x1)	(36)
0^#(q1(1(x1)))	→	1'^#(x1)	(33)
q3^#(1'(x1))	→	1'^#(q3(x1))	(18)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

q3^#(1'(x1))

→

q3^#(x1)

(28)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	19431
[1(x₁)]	=	x₁ + 1
[0'^#(x₁)]	=	19433
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 0
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	18590
[q0^#(x₁)]	=	19433
[0(x₁)]	=	1
[0'(x₁)]	=	19433
[q1(x₁)]	=	x₁ + 0
[q2(x₁)]	=	x₁ + 0
[q3^#(x₁)]	=	x₁ + 18591
[q0(x₁)]	=	x₁ + 19432
[q2^#(x₁)]	=	x₁ + 0

together with the usable rules

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

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

q3^#(1'(x1))

→

q3^#(x1)

(28)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

0^#(q1(1(x1)))	→	0^#(1'(x1))	(39)
0^#(q2(1'(x1)))	→	0^#(1'(x1))	(40)
0^#(q2(0(x1)))	→	0^#(0(x1))	(38)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 19431
[1(x₁)]	=	x₁ + 2
[0'^#(x₁)]	=	19433
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 0
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	18590
[q0^#(x₁)]	=	19433
[0(x₁)]	=	1
[0'(x₁)]	=	19433
[q1(x₁)]	=	x₁ + 0
[q2(x₁)]	=	x₁ + 0
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 19432
[q2^#(x₁)]	=	x₁ + 0

together with the usable rules

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

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

0^#(q1(1(x1)))

→

0^#(1'(x1))

(39)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

0^#(q2(1'(x1)))	→	0^#(1'(x1))	(40)
0^#(q2(0(x1)))	→	0^#(0(x1))	(38)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 19431
[1(x₁)]	=	x₁ + 24389
[0'^#(x₁)]	=	19433
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 12280
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	18590
[q0^#(x₁)]	=	19433
[0(x₁)]	=	x₁ + 1
[0'(x₁)]	=	x₁ + 24389
[q1(x₁)]	=	x₁ + 5017
[q2(x₁)]	=	x₁ + 29405
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 29405
[q2^#(x₁)]	=	x₁ + 0

together with the usable rules

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

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

0^#(q2(1'(x1)))	→	0^#(1'(x1))	(40)
0^#(q2(0(x1)))	→	0^#(0(x1))	(38)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

0'^#(q2(0(x1)))	→	0'^#(0(x1))	(35)
0'^#(q2(0(x1)))	→	q2^#(0'(0(x1)))	(37)
q0^#(0(x1))	→	0'^#(q1(x1))	(29)
0'^#(q1(1(x1)))	→	0'^#(1'(x1))	(42)
0'^#(q1(1(x1)))	→	q2^#(0'(1'(x1)))	(30)
0'^#(q2(1'(x1)))	→	0'^#(1'(x1))	(22)
0'^#(q2(1'(x1)))	→	q2^#(0'(1'(x1)))	(32)
q2^#(0'(x1))	→	q0^#(x1)	(31)
q2^#(0'(x1))	→	0'^#(q0(x1))	(19)

1.1.1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 19431
[1(x₁)]	=	x₁ + 3
[0'^#(x₁)]	=	x₁ + 0
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 1
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	18590
[q0^#(x₁)]	=	x₁ + 1
[0(x₁)]	=	x₁ + 1
[0'(x₁)]	=	x₁ + 1
[q1(x₁)]	=	x₁ + 1
[q2(x₁)]	=	x₁ + 3
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 1
[q2^#(x₁)]	=	x₁ + 1

together with the usable rules

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

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

0'^#(q2(0(x1)))	→	0'^#(0(x1))	(35)
0'^#(q2(0(x1)))	→	q2^#(0'(0(x1)))	(37)
q0^#(0(x1))	→	0'^#(q1(x1))	(29)
0'^#(q1(1(x1)))	→	0'^#(1'(x1))	(42)
0'^#(q1(1(x1)))	→	q2^#(0'(1'(x1)))	(30)
0'^#(q2(1'(x1)))	→	0'^#(1'(x1))	(22)
0'^#(q2(1'(x1)))	→	q2^#(0'(1'(x1)))	(32)
q2^#(0'(x1))	→	q0^#(x1)	(31)
q2^#(0'(x1))	→	0'^#(q0(x1))	(19)

could be deleted.

1.1.1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

1'^#(q2(1'(x1)))	→	1'^#(1'(x1))	(20)
1'^#(q2(0(x1)))	→	1'^#(0(x1))	(21)
1'^#(q1(1(x1)))	→	1'^#(x1)	(34)
1'^#(q1(1(x1)))	→	1'^#(1'(x1))	(48)

1.1.1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 19431
[1(x₁)]	=	x₁ + 2914
[0'^#(x₁)]	=	x₁ + 0
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 1
[q4(x₁)]	=	1
[q1^#(x₁)]	=	19432
[1'^#(x₁)]	=	x₁ + 18590
[q0^#(x₁)]	=	1
[0(x₁)]	=	x₁ + 1
[0'(x₁)]	=	x₁ + 508
[q1(x₁)]	=	x₁ + 240
[q2(x₁)]	=	x₁ + 3153
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 793
[q2^#(x₁)]	=	x₁ + 1

together with the usable rules

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

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

1'^#(q2(1'(x1)))	→	1'^#(1'(x1))	(20)
1'^#(q2(0(x1)))	→	1'^#(0(x1))	(21)
1'^#(q1(1(x1)))	→	1'^#(x1)	(34)
1'^#(q1(1(x1)))	→	1'^#(1'(x1))	(48)

could be deleted.

1.1.1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

q1^#(1'(x1))	→	q1^#(x1)	(23)
q1^#(0(x1))	→	q1^#(x1)	(17)

1.1.1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 19431
[1(x₁)]	=	x₁ + 625
[0'^#(x₁)]	=	x₁ + 0
[1'(x₁)]	=	x₁ + 1
[b(x₁)]	=	35102
[q3(x₁)]	=	x₁ + 25536
[q4(x₁)]	=	1
[q1^#(x₁)]	=	x₁ + 19432
[1'^#(x₁)]	=	x₁ + 18590
[q0^#(x₁)]	=	1
[0(x₁)]	=	x₁ + 1
[0'(x₁)]	=	x₁ + 625
[q1(x₁)]	=	x₁ + 24912
[q2(x₁)]	=	x₁ + 25536
[q3^#(x₁)]	=	18591
[q0(x₁)]	=	x₁ + 25536
[q2^#(x₁)]	=	x₁ + 1

together with the usable rules

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

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

q1^#(1'(x1))	→	q1^#(x1)	(23)
q1^#(0(x1))	→	q1^#(x1)	(17)

could be deleted.

1.1.1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.