factorial: THEORY BEGIN n: VAR nat factorial(n): recursive posnat = (if n = 0 then 1 else n*factorial(n-1) endif) MEASURE n END factorial