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

The program

(VAR X Y)
(RULES

min(X,0) -> X
min(s(X),s(Y)) -> min(X,Y)
quot(0,s(Y)) -> 0
quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X,s(s(0))))))


)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend