The informal description of the semantics in the SRFI describes the lazy
version of the hygiene algorithm.  If I remember correctly, the original
syntax-case paper described the algorithm in the first few sections as if it
were eager, only introducing the lazy version in a later section for
efficiency.

Does the semantics depend on the laziness?  This is not clear to me, but if
not, the eager description may be easier to understand in the informal
decription.

Regards
Andre