/home/nowonder/forschung/aprove/TPDB05/TRS/secret2005/tpa1.trs

The program

(VAR x y)
(RULES
 min(x, 0) -> 0
 min(0, y) -> 0
 min(s(x), s(y)) -> s(min(x, y))
 max(x, 0) -> x
 max(0, y) -> y
 max(s(x), s(y)) -> s(max(x, y)) 
 -(x, 0) -> x
 -(s(x), s(y)) -> -(x, y) 
 gcd(s(x), s(y)) -> gcd(-(s(max(x, y)), s(min(x, y))), s(min(x, y)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend