Yes, I need the alphaRule here. When user wrote it, they suppose the alphaRules are not a part of their semantics. They are the rules for simulation only. The user wrote these rules to indicate that they are actually interested in the cell or variables by applying the rules. For example, let's say the whole configuration is w, then the alphaRule is a, then they user actually are interested in the cell or data in a(w). 
So, the basic idea of the simulation tool is two steps rewriting. First, I need to take two programs (a specification and a implementation), and use the rule set without alphaRule to rewrite the two programs to next step. Second, After I got the rewriting result as a Term, I apply alphaRule to the term to get the data which the users are insterested in and compare the specification side with the implementation side in order to determine if the two side are equivalent. 

I mean I did not need the rule during the execution of a program with its semantics. However, I need a way to distinguish the alpha rule and other semantics rules and I can use these two different things on different purpose.