MAYBE
Termination Proof
Termination Proof
by ttt2 (version ttt2 1.15)
Input
The rewrite relation of the following TRS is considered.
a
(
x0
)
→
b
(
x0
)
a
(
b
(
c
(
x0
)))
→
c
(
c
(
a
(
a
(
x0
))))
c
(
c
(
x0
))
→
b
(
x0
)
Proof
1 Termination Assumption
We assume termination of the following TRS
a
(
x0
)
→
b
(
x0
)
a
(
b
(
c
(
x0
)))
→
c
(
c
(
a
(
a
(
x0
))))
c
(
c
(
x0
))
→
b
(
x0
)