Termination w.r.t. Q
of the given
QTRS
could be
proven
:
0 QTRS
↳
1 DirectTerminationProof (⇔)
↳
2 TRUE
(0)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f
(
x
) →
s
(
x
)
f
(
s
(
s
(
x
))) →
s
(
f
(
f
(
x
)))
Q is empty.
(1) DirectTerminationProof (EQUIVALENT transformation)
We use [DIRECT_TERMINATION] with the following order to prove termination.
Knuth-Bendix order [KBO] with precedence:
f
1
> s
1
and weight map:
f_1=1
s_1=1
The variable weight is 1
(2)
TRUE