Answer set programming  is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper claims the correctness   of a number of interesting program rewritings. Notably, they  assume  programs with variables and  such important language features as choice, disjunction, and aggregates. We showcase the utility of some considered rewritings  by using them to argue that two different answer set programming  formalizations  of a planning module (for dynamic system descriptions expressed in action language AL) are essentially the same.  In addition, our findings provide the theoretical basis for possible future implementations of  tools for program rewritings, which is essential in a quest for automatic performance tuning.