Platform claims not to support CPU time, falling back to wall time.
proof of /home/fs5/ayamada/tpdb/relative/Relative_05/rt1-3.trs
# AProVE Commit ID: 2b684c7cda508b1711f707cb42f127e64fe1df88 ffrohn 20140415 dirty
Termination of the given RelTRS could be proven:
(0) RelTRS
(1) RelTRStoQDPProof [SOUND, 0 ms]
(2) QDP
(3) DependencyGraphProof [EQUIVALENT, 0 ms]
(4) TRUE
----------------------------------------
(0)
Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
t(f(x), g(y), f(z)) -> t(z, g(x), g(y))
t(g(x), g(y), f(z)) -> t(f(y), f(z), x)
The relative TRS consists of the following S rules:
f(g(x)) -> g(f(x))
g(f(x)) -> f(g(x))
f(f(x)) -> g(g(x))
g(g(x)) -> f(f(x))
----------------------------------------
(1) RelTRStoQDPProof (SOUND)
The relative termination problem is root-restricted. We can therefore treat it as a dependency pair problem.
----------------------------------------
(2)
Obligation:
Q DP problem:
The TRS P consists of the following rules:
t(f(x), g(y), f(z)) -> t(z, g(x), g(y))
t(g(x), g(y), f(z)) -> t(f(y), f(z), x)
The TRS R consists of the following rules:
f(g(x)) -> g(f(x))
g(f(x)) -> f(g(x))
f(f(x)) -> g(g(x))
g(g(x)) -> f(f(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
----------------------------------------
(3) DependencyGraphProof (EQUIVALENT)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
----------------------------------------
(4)
TRUE