An operational semantics for lambda-calculus normal order evaluation strategy
You can use the following rules:

$\frac{t_1 \longrightarrow t_1'}{t_1 t_2 \longrightarrow t_1' t_2}$

$(λx. t_1) t_2 \longrightarrow [x \mapsto t_2]t_1$