/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/gcd.trs

The program

(VAR X Y)
(RULES
	
minus(X,s(Y)) -> pred(minus(X,Y))
minus(X,0) -> X
pred(s(X)) -> X
le(s(X),s(Y)) -> le(X,Y)
le(s(X),0) -> false
le(0,Y) -> true
gcd(0,Y) -> 0
gcd(s(X),0) -> s(X)
gcd(s(X),s(Y)) -> if(le(Y,X),s(X),s(Y))
if(true,s(X),s(Y)) -> gcd(minus(X,Y),s(Y))
if(false,s(X),s(Y)) -> gcd(minus(Y,X),s(X))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend