An operational semantics for lambda-calculus normal order evaluation strategy TAPL book, page 56 reads:


  Under the normal order strategy, the leftmost, outermost redex is
  always reduced first.


I understand this as a restriction of the full beta-reduction evaluation strategy, whose reduction rules are given as follows:

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

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

$$\frac{t_1 \to t_1'}{λx. t_1 \to λx. t_1'}$$

$$\frac{(λx. t_1) t_2}{[x \to t_2] t_1}$$

My question is how to transform these rules so that the normal order strategy condition holds.
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$