Theorem 1: Scanning the Rules

Now we will show that for every rule R, if A2 $\wedge$ A3 $\wedge$ A4 $\wedge$ A5 and the enabling predicate hold, then Theorem 1 will hold after the rule's action.
Rules 1 to 3 do not change relation $\ensuremath{\rightarrow}$ , so they trivially verify the induction step.
The following conventions are used to represent graphically the $\ensuremath{\rightarrow}$ graph: $\includegraphics [width=0.8\textwidth]{conventions.eps}$