lambda calculus, normal order, normal form,

In lambda calculus, if a term has normal form, normal order reduction strategy will always produce it.

I just wonder how to prove the above proposition strictly?

The result you mention is a corollary of the so called standardization theorem, stating that for any reduction sequence M->N there is another "standard" one between the same terms M and N, where you execute redexes in leftmost outermost order. The proof is not so trivial, and there are several different approaches in the literature. I add a short bibliography below.

The recent proof by Kashima 5 (see also 1) has the advantage of not using the notion of residual and of being based on purely inductive techniques. It is also good for formalization 2, but unless you are not already confident with the subject, it is not particularly instructive.

The general idea behind standardization is the following. Suppose to have two redexes R and S, where S is in leftmost outermost position with respect to R, and consider the following reduction:

                R      S
             M  ->  P  ->  N

Then, you can start firing S, instead, but in this way you can possibly duplicate (or erase) the redex R. These redexes, that are essentially what remains of R after firing S, are called residuals, and are usually indicated as R/S (read: residuals of R after S). So, the basic lemma is that

             R S = S (R/S)

In order to use it for standardization, we need to generalize R to an arbitrary sequence ρ (that we may assume to be standard, with no redex in leftmost outermost position w.r.t. S). It is still true that

         (*) ρS = S (ρ/S)

but what is not so evident is the standardization of (ρ/S). To this aim, let us observe that ρ was performed before firing S = C[\x.M N], that essentially splits the term in three disconnected regions: the context C, M, and N. This induces a repartition of ρ in three consecutive sequences:

           ρ1   inside M
           ρ2   inside N
           ρ3   inside C

(remember that no redex was in leftmost outermost position w.r.t. S). The only part that can be duplicated (or erased) is ρ2, and the residuals ρ2-0 ... ρ2-k are easily ordered according to the different positions of the k copies of N created by the firing of S. So

   S ρ1 ρ2-0 ... ρ2-k ρ_3

is the standard version of (*).

Basic bibliography.

1 A.Asperti, JJ. Levy. The cost of usage in the lambda-calculus. LICS 2013.

3 H. P. Barendregt. The Lambda Calculus, North-Holland (1984).

4 G.Gonthier, JJ. Levy, PA. Mellies. An abstract standardisation theorem. LICS ’92.

2 F.Guidi. Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. Journal of Formalized Reasoning 5(1):1–25, 2012.

5 R.Kashima. A proof of the standardization theorem in lambda-calculus. Technical Report C-145,, Tokyo Institute of Technology, 2000.

[6] JW. Klop. Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, 1980.

[7] G.Mitschke. The standardisation theorem for the lambda-calculus. Z. Math.Logik. Grundlag. Math, 25:29–31, 1979

[8] M.Takahashi. Parallel reductions in lambda-calculus. Information and Computation 118, pp.120-127, 1995.

[9] H. Xi, Upper bounds for standardizations and an application. Journal of Symboloc Logic 64, pp.291-303, 1999.