κ) = (Lam lam, ρ', σ, κ) where Clo (lam, ρ') = σ!(ρ!x) step (f :@ e, ρ, σ, κ) = (f, ρ, σ, Ar(e, ρ, κ)) step (Lam lam,ρ,σ,Ar(e, ρ', κ)) = (e, ρ', σ, Fn(lam, ρ, κ)) step (Lam lam,ρ,σ,Fn(x :=> e, ρ', κ)) = (e, ρ' // [x ==> a'], σ // [a' ==> Clo (lam, ρ)], κ) where a' = alloc(σ)