Termination w.r.t. Q of the following Term Rewriting System could be proven:

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

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.


QTRS
  ↳ RFCMatchBoundsTRSProof

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

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

Q is empty.

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

t(o(x1)) → m(a(x1))
t(e(x1)) → n(s(x1))
a(l(x1)) → a(t(x1))
o(m(a(x1))) → t(e(n(x1)))
s(a(x1)) → l(a(t(o(m(a(t(e(x1))))))))
n(s(x1)) → a(l(a(t(x1))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1, 2, 9, 5, 6, 8, 4, 7, 3, 10, 11, 12, 13, 14, 17, 16, 15, 18, 19, 20, 23, 21, 22, 24, 31, 27, 28, 30, 26, 29, 25, 32, 33, 34, 35, 36, 37, 40, 39, 38, 43, 42, 41, 46, 47, 50, 49, 45, 48, 44, 51, 52, 53, 54, 55, 56, 57, 60, 58, 59, 63, 61, 62, 64, 65, 66, 67, 68, 71, 70, 69, 74, 73, 72, 75, 76, 79, 77, 78, 80

Node 1 is start node and node 2 is final node.

Those nodes are connect through the following edges: