the procedure returns 0 which is indeed x*y
inductive step: pass x+1,y
as x+1 is not 0, follow the else statement. return y plus whatever mult(x+1-1,y) returns. the nested mult() returns 0 so the parent procedure returns y which is y greater than what x*y returned in the base case.