YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 RFCMatchBoundsTRSProof (⇔, 0 ms)
↳4 YES
f(n__f(n__a)) → f(n__g(f(n__a)))
f(X) → n__f(X)
a → n__a
g(X) → n__g(X)
activate(n__f(X)) → f(X)
activate(n__a) → a
activate(n__g(X)) → g(X)
activate(X) → X
n__a'(n__f(f(x))) → n__a'(f(n__g(f(x))))
f(X) → n__f(X)
a'(x) → n__a'(x)
g(X) → n__g(X)
n__f(activate(X)) → f(X)
n__a'(activate(x)) → a'(x)
n__g(activate(X)) → g(X)
activate(X) → X
n__a'(n__f(f(x))) → n__a'(f(n__g(f(x))))
f(X) → n__f(X)
a'(x) → n__a'(x)
g(X) → n__g(X)
n__f(activate(X)) → f(X)
n__a'(activate(x)) → a'(x)
n__g(activate(X)) → g(X)
activate(X) → X
The certificate consists of the following enumerated nodes:
1, 4, 8, 9, 10, 14, 15, 16
Node 1 is start node and node 4 is final node.
Those nodes are connected through the following edges: