How to formalize "It doesn't matter how places the brackets" Let $X$ be a set and $X\times X\to X: (a, b)\mapsto a\cdot b$ an associative operation on $X$. Now one can prove by induction that it doesn't matter how one places the brackets in a product $x_1\cdot x_2\cdot\text{ }\dots\text{ } \cdot x_n$, the product always evaluates to the same value. This result justifies the notation of a product $x_1\cdot x_2\cdot\text{ }\dots\text{ } \cdot x_n$ without any brackets. But how can one formalize it?
One nice way to formalize the general associative law is via binary trees. For us, a tree of operations will be a finite tree, with a root node, where each node is either a leaf (no successors) or has exactly two successors (a left successor and a right successor), and each leaf is labelled with an element of $X$. 

The idea is that each leaf of the tree represents an input, and each non-leaf node is an instance of the operation $*$ applied to the values associated to the $*$-product of the left and right sub-trees of that node. So, for instance, $(a*b)*c$ is represented by a tree with one split at the root, and then the left side splits once more; and the leaves are labelled $a, b, c$, respectively.

A vauation of a tree of operations is a map $m$ from the nodes to $X$, satisfying $m(\sigma)$ is the label already on $\sigma$ - if $\sigma$ is a leaf - and $m(\sigma)=m(S_{left}(\sigma))*m(S_{right}(\sigma)),$ where $S_{left}$ and $S_{right}$ are the left and right successors of $\sigma$, if $\sigma$ is not a leaf.  We can prove by induction that each tree $T$ of operations has exactly one valuation; call this "$v(T)$."

Note that the leaves of a tree of operations are ordered in a natural way: one leaf $\sigma$ is before another leaf $\tau$ if it is "to the left" of $\tau$, that is, when $\rho$ is the furthest node of the tree above both $\sigma$ and $\tau$ we have that $\sigma$ goes left from $\rho$ while $\tau$ goes right. The general associative law is then:


  If $T_1, T_2$ are two trees of operations with the same leaf-labels occurring in the same left-right order, then $v(T_1)$ and $v(T_2)$ assign the same element of $X$ to the root of $T_1$ and $T_2$, respectively.
This is called the associative law which says precisely: $$\forall x,y,z [(x*(y*z))=((x*y)*z))] $$

That it extends to arbitrary finite products can then proven using induction.

Some more details: you will prove that every expresention is equivalent to the one with brackets on left e.g. to $(((x*y)*z)*w))$ (every expresion uses each variable only once). Then you can define complexity $C:\mathrm{EXP}\to\mathbb{N}$ of an expression recursively as : $C(x)=0$, and for composed expressions $C(e*f)=C(e)+C(f)+\mathrm{length}(f)-1$, where $e,f$ are expressions and $\mathrm{length}(f)$ is a number of variables in $f$. 

Examples:
 $C(x*y)=C(x)+C(y)+1-1=0$,

$C((x*y)*z))=C(x*y)+C(z)+1-1=0$, 

but $C(x*(y*z))=C(x)+C(y*z)+2-1=1$,

and use induction on the complexity. Calculate that any one application of associativity decreases the complexity.