  One of the key steps in the proof of the Banach-Tarski Theorem is the
introduction of a free group of rotations. First, a free group of reduced words
is generated where each element of the set is represented as an ACL2 list. Then
we demonstrate that there is a one-to-one relation between the set of reduced
words and a set of 3D rotations. In this paper we present a way to generate
this set of reduced words and we prove group properties for this set. Then, we
show a way to generate a set of 3D matrices using the set of reduced words.
Finally we show a formalization of 3D rotations and prove that every element of
the 3D matrices set is a rotation.
