lambda calculus – PCF encoding and denotational semantics of simple recursive function


Let $f$ be the function:

$f(n: mathbb{N}) = text{if }(n > 0) text{ then } 0 text{ else } f(n-1)$

I encode it in PCF following the notations in a standard text in denotational semantics:

$f = Y_{sigma}(lambda f: nat to nat. lambda n: nat. text{ifz}(n,0,pred(n))$

Then I try to compute its semantics:

$((vdash f ))5 = mu(((lambda f. lambda n. text{ifz}(n,0,pred(n))))) = mu(Lambda (f vdash ((lambda n. text{ifz}(n,0,pred(n))))5))$

However, from here the computation seems confusing. For instance, what value should $f$ have according to the annotated environment (in this case $5$).

Denotational semantics rules:

enter image description here

enter image description here