(1) 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:
active(f(f(a))) → mark(c(f(g(f(a)))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(c(X)) → active(c(X))
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
c(mark(X)) → c(X)
c(active(X)) → c(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
2340576, 2340577, 2340578, 2340579, 2340581, 2340582, 2340580, 2340583, 2340584, 2340585, 2340586, 2340587, 2340592, 2340589, 2340590, 2340588, 2340591, 2340593, 2340594, 2340595, 2340596, 2340597, 2340598, 2340599
Node 2340576 is start node and node 2340577 is final node.
Those nodes are connect through the following edges:
- 2340576 to 2340577 labelled g_1(0), f_1(0), c_1(0), g_1(1), c_1(1), f_1(1), c_1(2), f_1(2), g_1(2)
- 2340576 to 2340578 labelled mark_1(0), f_1(1), g_1(1), c_1(1)
- 2340576 to 2340583 labelled active_1(0), f_1(1), g_1(1), c_1(1)
- 2340576 to 2340576 labelled active_1(0), c_1(2), g_1(1), f_1(2), c_1(1), f_1(1), g_1(2)
- 2340576 to 2340582 labelled active_1(0), f_1(1), g_1(1), c_1(1)
- 2340576 to 2340585 labelled active_1(1), f_1(2), g_1(2), c_1(2)
- 2340576 to 2340588 labelled mark_1(1), f_1(2), g_1(2), c_1(1), f_1(1), c_1(2), g_1(1)
- 2340576 to 2340586 labelled c_1(2), g_1(1), f_1(2), c_1(1), f_1(1), g_1(2)
- 2340576 to 2340593 labelled active_1(2), f_1(3), g_1(3), f_1(2), g_1(2), c_1(2), c_1(3), c_1(1), f_1(1), g_1(1)
- 2340576 to 2340594 labelled f_1(3), g_1(3), f_1(2), c_1(1), f_1(1), g_1(2), g_1(1), c_1(2), c_1(3)
- 2340576 to 2340599 labelled f_1(3), g_1(3), f_1(2), c_1(1), f_1(1), g_1(2), g_1(1), c_1(2), c_1(3)
- 2340577 to 2340577 labelled #_1(0), mark_1(0), mark_1(1)
- 2340577 to 2340586 labelled active_1(1)
- 2340577 to 2340576 labelled active_1(1)
- 2340577 to 2340588 labelled mark_1(1)
- 2340577 to 2340593 labelled active_1(2)
- 2340577 to 2340594 labelled mark_1(2)
- 2340577 to 2340599 labelled active_1(3)
- 2340578 to 2340579 labelled c_1(0)
- 2340579 to 2340580 labelled f_1(0)
- 2340581 to 2340582 labelled f_1(0)
- 2340582 to 2340577 labelled a(0)
- 2340580 to 2340581 labelled g_1(0)
- 2340583 to 2340584 labelled g_1(0)
- 2340583 to 2340577 labelled g_1(1), g_1(2)
- 2340583 to 2340576 labelled g_1(2), g_1(1)
- 2340583 to 2340586 labelled g_1(1), g_1(2)
- 2340583 to 2340593 labelled g_1(3), g_1(2), g_1(1)
- 2340583 to 2340588 labelled g_1(2), g_1(1)
- 2340583 to 2340582 labelled g_1(1)
- 2340583 to 2340583 labelled g_1(1)
- 2340583 to 2340585 labelled g_1(2)
- 2340583 to 2340578 labelled g_1(1)
- 2340583 to 2340594 labelled g_1(1), g_1(3), g_1(2)
- 2340583 to 2340599 labelled g_1(1), g_1(3), g_1(2)
- 2340584 to 2340577 labelled mark_1(0)
- 2340584 to 2340586 labelled active_1(1)
- 2340584 to 2340576 labelled active_1(1)
- 2340584 to 2340588 labelled mark_1(1)
- 2340584 to 2340593 labelled active_1(2)
- 2340584 to 2340594 labelled mark_1(2)
- 2340584 to 2340599 labelled active_1(3)
- 2340585 to 2340579 labelled c_1(1)
- 2340586 to 2340587 labelled g_1(1)
- 2340586 to 2340577 labelled a(1), g_1(2), g_1(1)
- 2340586 to 2340576 labelled g_1(2), g_1(1)
- 2340586 to 2340588 labelled g_1(2)
- 2340586 to 2340586 labelled g_1(2)
- 2340586 to 2340594 labelled g_1(3), g_1(2)
- 2340586 to 2340593 labelled g_1(3), g_1(2)
- 2340586 to 2340582 labelled g_1(1)
- 2340586 to 2340583 labelled g_1(1)
- 2340586 to 2340585 labelled g_1(2)
- 2340586 to 2340578 labelled g_1(1)
- 2340586 to 2340599 labelled g_1(2), g_1(3)
- 2340587 to 2340577 labelled mark_1(1)
- 2340587 to 2340586 labelled active_1(1)
- 2340587 to 2340576 labelled active_1(1)
- 2340587 to 2340588 labelled mark_1(1)
- 2340587 to 2340594 labelled mark_1(2)
- 2340587 to 2340599 labelled active_1(3)
- 2340587 to 2340593 labelled active_1(2)
- 2340592 to 2340577 labelled a(1)
- 2340589 to 2340590 labelled f_1(1)
- 2340590 to 2340591 labelled g_1(1)
- 2340588 to 2340589 labelled c_1(1)
- 2340591 to 2340592 labelled f_1(1)
- 2340593 to 2340589 labelled c_1(2)
- 2340594 to 2340595 labelled c_1(2)
- 2340595 to 2340596 labelled f_1(2)
- 2340596 to 2340597 labelled g_1(2)
- 2340597 to 2340598 labelled f_1(2)
- 2340598 to 2340577 labelled a(2)
- 2340599 to 2340595 labelled c_1(3)