/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/dpqs.trs

The program

(COMMENT 

  This example is from Giesl & Ohlebusch (FroCoS'98).
  It provides a system which is DP-Quasi Simply Terminating
  but *not* DP-Simply Terminating.

)

(VAR x)
(RULES

f(f(x)) -> f(c(f(x))) 
f(f(x)) -> f(d(f(x))) 
g(c(x)) -> x 
g(d(x)) -> x 
g(c(0)) -> g(d(1)) 
g(c(1)) -> g(d(0)) 


)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend