/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/Rubio-inn/muladd.trs

The program

(VAR X Y)
(RULES

*(X,+(Y,1))  -> +(*(X,+(Y,*(1,0))),X)
*(X,1) -> X
*(X,0) -> X
*(X,0) -> 0
)


Submit to AProVE Web Frontend

Edit in AProVE Web Frontend