/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/2.21.trs

The program

(VAR x y z)
(RULES
bin(x,0) -> s(0)
bin(0,s(y)) -> 0
bin(s(x),s(y)) -> +(bin(x,s(y)),bin(x,y))
)
(COMMENT Example 2.21 (Binomial Coefficients) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend