Termination w.r.t. Q
of the given
QTRS
could be
disproven
:
0 QTRS
↳
1 NonTerminationProof (⇔, 0 ms)
↳
2 NO
(0)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f
(
x
) →
f
(
x
)
Q is empty.
(1) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
f
→
f
f
→
f
by original rule (OC 1)
(2)
NO