Abstract: In this paper, we give a formal treatment of the reduction idea in Lipton's paper, and investigate its application in proving correctness of asynchronous systems. In a complex system, it is both tempting and convenient to assume that certain sequences of actions behave like single indivisible or instantaneous actions. Such conceptual reduction of sequences of relatively small actions to single occurrences of relatively large actions is encountered very often in computer science. For asynchronous systems, reduction is particularly appealing because it helps to reduce the amount of interleaving of actions involved and also the complexity of the systems, thereby making correctness proofs more tractable. However, reduction is also very dangerous for it could easily lead to erroneous and disastrous conclusions about systems. We establish, in this paper, simple and general sufficient conditions for reduction under which correctness is preserved, and any conclusions obtained about the correctness of the reduced systems are also valid for the original systems, as far as deadlock-freedom, homing, determinacy and the Church-Rosser property are concerned. We also show that the results in Lipton's paper are special cases of some of our results here.