operational semantics is incomplete?

I was trying to read docs/core-spec/core-spec.pdf to understand the operational semantics for core language. So I started off by playing with operational semantics rules manually.

But I found the following expression gets stuck:

v1 = let fix = \f -> let x = f x in x
         pf = \f x -> if x == 0
                          then x
                          else f (pred x)
     in (fix pf) 2
-- S_LETNONREC
v2 = ((\f -> let x = f x in x)
      (\f x -> if x == 0
                   then x
                   else f (pred x)))
     2
-- S_APP
v3 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in x) 2
-- S_APP; S_LETREC
v4 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in (\f x -> if x == 0
                      then x
                      else f (pred x)) x) 2
-- S_APP
v5 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in (\x1 -> if x1 == 0
                     then x1
                     else x (pred x1))) 2

at this point x is not a free variable so S_LETRECRETURN cannot be applied.

Did I make it wrong or some rules are missing for the operational semantics?

Trac metadata

Trac field	Value
Version	7.8.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Documentation
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture