YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 RFCMatchBoundsTRSProof (⇔, 0 ms)
↳4 YES
p(f(f(x))) → q(f(g(x)))
p(g(g(x))) → q(g(f(x)))
q(f(f(x))) → p(f(g(x)))
q(g(g(x))) → p(g(f(x)))
f(f(p(x))) → g(f(q(x)))
g(g(p(x))) → f(g(q(x)))
f(f(q(x))) → g(f(p(x)))
g(g(q(x))) → f(g(p(x)))
f(f(p(x))) → g(f(q(x)))
g(g(p(x))) → f(g(q(x)))
f(f(q(x))) → g(f(p(x)))
g(g(q(x))) → f(g(p(x)))
The certificate consists of the following enumerated nodes:
2, 4, 9, 10, 11, 12
Node 2 is start node and node 4 is final node.
Those nodes are connected through the following edges: