Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 QTRS Reverse (⇔, 0 ms)

↳2 QTRS

↳3 RFCMatchBoundsTRSProof (⇔, 46 ms)

↳4 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Begin(b(c(a(b(c(x)))))) → Wait(Right1(x))
Begin(c(a(b(c(x))))) → Wait(Right2(x))
Begin(a(b(c(x)))) → Wait(Right3(x))
Begin(b(c(x))) → Wait(Right4(x))
Begin(c(x)) → Wait(Right5(x))
Right1(b(End(x))) → Left(a(b(b(c(b(c(a(End(x)))))))))
Right2(b(b(End(x)))) → Left(a(b(b(c(b(c(a(End(x)))))))))
Right3(b(b(c(End(x))))) → Left(a(b(b(c(b(c(a(End(x)))))))))
Right4(b(b(c(a(End(x)))))) → Left(a(b(b(c(b(c(a(End(x)))))))))
Right5(b(b(c(a(b(End(x))))))) → Left(a(b(b(c(b(c(a(End(x)))))))))
Right1(b(x)) → Ab(Right1(x))
Right2(b(x)) → Ab(Right2(x))
Right3(b(x)) → Ab(Right3(x))
Right4(b(x)) → Ab(Right4(x))
Right5(b(x)) → Ab(Right5(x))
Right1(c(x)) → Ac(Right1(x))
Right2(c(x)) → Ac(Right2(x))
Right3(c(x)) → Ac(Right3(x))
Right4(c(x)) → Ac(Right4(x))
Right5(c(x)) → Ac(Right5(x))
Right1(a(x)) → Aa(Right1(x))
Right2(a(x)) → Aa(Right2(x))
Right3(a(x)) → Aa(Right3(x))
Right4(a(x)) → Aa(Right4(x))
Right5(a(x)) → Aa(Right5(x))
Ab(Left(x)) → Left(b(x))
Ac(Left(x)) → Left(c(x))
Aa(Left(x)) → Left(a(x))
Wait(Left(x)) → Begin(x)
b(b(c(a(b(c(x)))))) → a(b(b(c(b(c(a(x)))))))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

c(b(a(c(b(Begin(x)))))) → Right1(Wait(x))
c(b(a(c(Begin(x))))) → Right2(Wait(x))
c(b(a(Begin(x)))) → Right3(Wait(x))
c(b(Begin(x))) → Right4(Wait(x))
c(Begin(x)) → Right5(Wait(x))
End(b(Right1(x))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(b(b(Right2(x)))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(c(b(b(Right3(x))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(a(c(b(b(Right4(x)))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(b(a(c(b(b(Right5(x))))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
Left(Ab(x)) → b(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Aa(x)) → a(Left(x))
Left(Wait(x)) → Begin(x)
c(b(a(c(b(b(x)))))) → a(c(b(c(b(b(a(x)))))))

Q is empty.

(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3. This implies Q-termination of R.
The following rules were used to construct the certificate:

c(b(a(c(b(Begin(x)))))) → Right1(Wait(x))
c(b(a(c(Begin(x))))) → Right2(Wait(x))
c(b(a(Begin(x)))) → Right3(Wait(x))
c(b(Begin(x))) → Right4(Wait(x))
c(Begin(x)) → Right5(Wait(x))
End(b(Right1(x))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(b(b(Right2(x)))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(c(b(b(Right3(x))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(a(c(b(b(Right4(x)))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
End(b(a(c(b(b(Right5(x))))))) → End(a(c(b(c(b(b(a(Left(x)))))))))
b(Right1(x)) → Right1(Ab(x))
b(Right2(x)) → Right2(Ab(x))
b(Right3(x)) → Right3(Ab(x))
b(Right4(x)) → Right4(Ab(x))
b(Right5(x)) → Right5(Ab(x))
c(Right1(x)) → Right1(Ac(x))
c(Right2(x)) → Right2(Ac(x))
c(Right3(x)) → Right3(Ac(x))
c(Right4(x)) → Right4(Ac(x))
c(Right5(x)) → Right5(Ac(x))
a(Right1(x)) → Right1(Aa(x))
a(Right2(x)) → Right2(Aa(x))
a(Right3(x)) → Right3(Aa(x))
a(Right4(x)) → Right4(Aa(x))
a(Right5(x)) → Right5(Aa(x))
Left(Ab(x)) → b(Left(x))
Left(Ac(x)) → c(Left(x))
Left(Aa(x)) → a(Left(x))
Left(Wait(x)) → Begin(x)
c(b(a(c(b(b(x)))))) → a(c(b(c(b(b(a(x)))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 42, 43, 44, 45, 46, 48, 63, 64, 65, 69, 76, 77, 78, 79, 80, 81, 82, 85, 86, 87, 88, 91, 92

Node 18 is start node and node 19 is final node.

Those nodes are connected through the following edges:

18 to 20 labelled Right1_1(0), Right2_1(0), Right3_1(0), Right4_1(0), Right5_1(0)
18 to 21 labelled End_1(0)
18 to 28 labelled b_1(0), c_1(0), a_1(0), a_1(1)
18 to 19 labelled Begin_1(0)
18 to 29 labelled a_1(0)
18 to 37 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
18 to 63 labelled Right5_1(2), Right4_1(2), Right3_1(2), Right2_1(2), Right1_1(2)
19 to 19 labelled #_1(0)
20 to 19 labelled Wait_1(0), Ab_1(0), Ac_1(0), Aa_1(0)
21 to 22 labelled a_1(0)
21 to 91 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
22 to 23 labelled c_1(0)
22 to 87 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
23 to 24 labelled b_1(0)
23 to 85 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
24 to 25 labelled c_1(0)
24 to 81 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
25 to 26 labelled b_1(0)
25 to 78 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
26 to 27 labelled b_1(0)
26 to 69 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
27 to 28 labelled a_1(0)
27 to 37 labelled Right5_1(1), Right4_1(1), Right3_1(1), Right2_1(1), Right1_1(1)
28 to 19 labelled Left_1(0), Begin_1(1)
28 to 35 labelled b_1(1), c_1(1), a_1(1)
28 to 39 labelled Right5_1(2), Right4_1(2), Right3_1(2), Right2_1(2), Right1_1(2)
28 to 42 labelled a_1(2)
28 to 63 labelled Right5_1(2), Right4_1(2), Right3_1(2), Right2_1(2), Right1_1(2)
28 to 92 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
29 to 30 labelled c_1(0)
29 to 79 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
30 to 31 labelled b_1(0)
30 to 76 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
31 to 32 labelled c_1(0)
31 to 65 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
32 to 33 labelled b_1(0)
32 to 40 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
33 to 34 labelled b_1(0)
33 to 38 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
34 to 19 labelled a_1(0)
34 to 36 labelled Right1_1(1), Right2_1(1), Right3_1(1), Right4_1(1), Right5_1(1)
35 to 19 labelled Left_1(1), Begin_1(1)
35 to 35 labelled b_1(1), c_1(1), a_1(1)
35 to 39 labelled Right5_1(2), Right4_1(2), Right3_1(2), Right2_1(2), Right1_1(2)
35 to 42 labelled a_1(2)
35 to 63 labelled Right5_1(2), Right4_1(2), Right3_1(2), Right2_1(2), Right1_1(2)
35 to 92 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
36 to 19 labelled Aa_1(1)
37 to 19 labelled Wait_1(1)
37 to 39 labelled Ab_1(1), Ac_1(1), Aa_1(1)
37 to 63 labelled Ab_1(1), Ac_1(1), Aa_1(1)
37 to 79 labelled Aa_1(1)
37 to 92 labelled Ab_1(1), Ac_1(1), Aa_1(1)
38 to 36 labelled Ab_1(1)
39 to 19 labelled Wait_1(2)
39 to 39 labelled Ab_1(2), Ac_1(2)
39 to 63 labelled Ab_1(2), Ac_1(2)
39 to 92 labelled Ab_1(2), Ac_1(2)
40 to 38 labelled Ab_1(1)
42 to 43 labelled c_1(2)
42 to 88 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
43 to 44 labelled b_1(2)
43 to 86 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
44 to 45 labelled c_1(2)
44 to 82 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
45 to 46 labelled b_1(2)
45 to 80 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
46 to 48 labelled b_1(2)
46 to 77 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
48 to 35 labelled a_1(2)
48 to 64 labelled Right5_1(3), Right4_1(3), Right3_1(3), Right2_1(3), Right1_1(3)
63 to 39 labelled Aa_1(2)
63 to 63 labelled Aa_1(2)
63 to 92 labelled Aa_1(2)
64 to 39 labelled Aa_1(3)
64 to 63 labelled Aa_1(3)
64 to 92 labelled Aa_1(3)
65 to 40 labelled Ac_1(1)
69 to 37 labelled Ab_1(1)
76 to 65 labelled Ab_1(1)
77 to 64 labelled Ab_1(3)
78 to 69 labelled Ab_1(1)
79 to 76 labelled Ac_1(1)
80 to 77 labelled Ab_1(3)
81 to 78 labelled Ac_1(1)
82 to 80 labelled Ac_1(3)
85 to 81 labelled Ab_1(1)
86 to 82 labelled Ab_1(3)
87 to 85 labelled Ac_1(1)
88 to 86 labelled Ac_1(3)
91 to 87 labelled Aa_1(1)
92 to 88 labelled Aa_1(3)

(0) Obligation:

(1) QTRS Reverse (EQUIVALENT transformation)

(2) Obligation:

(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

(4) YES