fmod Naturale is
 protecting NAT .

 op spare : Nat -> Nat .
 op func : Nat Nat Nat -> Nat .

 var A : Nat .
 var B : Nat .
 var S : Nat .

 eq func(A, B, S) = if B >= A then S else func(A, B + 1, S + S + 2) fi .

 eq spare(A) = func(A, 0, 0) .

endfm


red spare(2) .
red spare(5) .
red spare(3) .