(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 5. This implies Q-termination of R.
The following rules were used to construct the certificate:
o(t(x)) → a(m(x))
e(t(x)) → s(n(x))
l(a(x)) → t(a(x))
a(m(o(x))) → n(e(t(x)))
a(s(x)) → e(t(a(m(o(t(a(l(x))))))))
s(n(x)) → t(a(l(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, 41, 43, 44, 45, 46, 47, 48, 49, 50, 51, 61, 62, 64, 65, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97
Node 18 is start node and node 19 is final node.
Those nodes are connected through the following edges:
- 18 to 20 labelled a_1(0)
- 18 to 21 labelled s_1(0)
- 18 to 22 labelled t_1(0)
- 18 to 23 labelled n_1(0)
- 18 to 25 labelled e_1(0)
- 18 to 32 labelled t_1(0)
- 18 to 35 labelled t_1(1)
- 18 to 41 labelled s_1(1)
- 18 to 43 labelled n_1(1)
- 18 to 68 labelled t_1(2)
- 19 to 19 labelled #_1(0)
- 20 to 19 labelled m_1(0)
- 21 to 19 labelled n_1(0)
- 22 to 19 labelled a_1(0)
- 22 to 43 labelled n_1(1)
- 22 to 45 labelled e_1(1)
- 22 to 71 labelled s_1(2)
- 22 to 80 labelled t_1(3)
- 23 to 24 labelled e_1(0)
- 23 to 61 labelled s_1(1)
- 23 to 72 labelled t_1(2)
- 24 to 19 labelled t_1(0)
- 25 to 26 labelled t_1(0)
- 26 to 27 labelled a_1(0)
- 26 to 64 labelled n_1(1)
- 27 to 28 labelled m_1(0)
- 28 to 29 labelled o_1(0)
- 28 to 62 labelled a_1(1)
- 29 to 30 labelled t_1(0)
- 30 to 31 labelled a_1(0)
- 31 to 19 labelled l_1(0)
- 31 to 37 labelled t_1(1)
- 32 to 33 labelled a_1(0)
- 33 to 34 labelled l_1(0)
- 33 to 37 labelled t_1(1)
- 34 to 19 labelled a_1(0)
- 34 to 43 labelled n_1(1)
- 34 to 45 labelled e_1(1)
- 34 to 71 labelled s_1(2)
- 34 to 80 labelled t_1(3)
- 35 to 36 labelled a_1(1)
- 36 to 37 labelled l_1(1)
- 36 to 74 labelled t_1(2)
- 37 to 19 labelled a_1(1)
- 37 to 43 labelled n_1(1)
- 37 to 45 labelled e_1(1)
- 37 to 71 labelled s_1(2)
- 37 to 80 labelled t_1(3)
- 41 to 26 labelled n_1(1)
- 43 to 44 labelled e_1(1)
- 43 to 75 labelled s_1(2)
- 43 to 83 labelled t_1(3)
- 44 to 19 labelled t_1(1)
- 45 to 46 labelled t_1(1)
- 46 to 47 labelled a_1(1)
- 46 to 78 labelled n_1(2)
- 47 to 48 labelled m_1(1)
- 48 to 49 labelled o_1(1)
- 48 to 76 labelled a_1(2)
- 49 to 50 labelled t_1(1)
- 50 to 51 labelled a_1(1)
- 51 to 19 labelled l_1(1)
- 51 to 37 labelled t_1(1)
- 61 to 19 labelled n_1(1)
- 62 to 30 labelled m_1(1)
- 64 to 65 labelled e_1(1)
- 64 to 77 labelled s_1(2)
- 64 to 86 labelled t_1(3)
- 65 to 29 labelled t_1(1)
- 68 to 69 labelled a_1(2)
- 69 to 70 labelled l_1(2)
- 69 to 89 labelled t_1(3)
- 70 to 26 labelled a_1(2)
- 71 to 46 labelled n_1(2)
- 72 to 73 labelled a_1(2)
- 73 to 74 labelled l_1(2)
- 73 to 85 labelled t_1(3)
- 74 to 19 labelled a_1(2)
- 74 to 43 labelled n_1(1)
- 74 to 45 labelled e_1(1)
- 74 to 71 labelled s_1(2)
- 74 to 80 labelled t_1(3)
- 75 to 19 labelled n_1(2)
- 76 to 50 labelled m_1(2)
- 77 to 29 labelled n_1(2)
- 78 to 79 labelled e_1(2)
- 78 to 90 labelled s_1(3)
- 78 to 91 labelled t_1(4)
- 79 to 49 labelled t_1(2)
- 80 to 81 labelled a_1(3)
- 81 to 82 labelled l_1(3)
- 81 to 94 labelled t_1(4)
- 82 to 46 labelled a_1(3)
- 83 to 84 labelled a_1(3)
- 84 to 85 labelled l_1(3)
- 84 to 95 labelled t_1(4)
- 85 to 19 labelled a_1(3)
- 85 to 43 labelled n_1(1)
- 85 to 45 labelled e_1(1)
- 85 to 71 labelled s_1(2)
- 85 to 80 labelled t_1(3)
- 86 to 87 labelled a_1(3)
- 87 to 88 labelled l_1(3)
- 87 to 96 labelled t_1(4)
- 88 to 29 labelled a_1(3)
- 89 to 26 labelled a_1(3)
- 90 to 49 labelled n_1(3)
- 91 to 92 labelled a_1(4)
- 92 to 93 labelled l_1(4)
- 92 to 97 labelled t_1(5)
- 93 to 49 labelled a_1(4)
- 94 to 46 labelled a_1(4)
- 95 to 19 labelled a_1(4)
- 95 to 43 labelled n_1(1)
- 95 to 45 labelled e_1(1)
- 95 to 71 labelled s_1(2)
- 95 to 80 labelled t_1(3)
- 96 to 29 labelled a_1(4)
- 97 to 49 labelled a_1(5)