Is there a program which shows set equality in steps? 
To show:
$(P(M),+,\cdot)$ is a commutative ring.
$A+B:= (A\cup B) \backslash (A\cap B)$ (or XOR)
$A\cdot B:=A\cap B$

First Ring axiom:
Addition is assiociative
$(A+B)+C=A+(B+C)$ for all $A,B,C\in P(M)$
Let $x\in ((A+B)+C)$
$\Leftrightarrow x\in (((A \cup B) \backslash (A \cap B))+C)$
$\Leftrightarrow x\in (((((A \cup B) \backslash (A \cap B)) \cup C) \backslash (((A \cup B) \backslash (A \cap B)) \cap C)))$
$\Leftrightarrow x\in (?)$
$\Leftrightarrow x\in (?)$
$\Leftrightarrow x\in (?)$
$\Leftrightarrow x\in (?)$
$\Leftrightarrow x\in (((A \cup ((B \cup C) \backslash (B \cap C))) \backslash (A \cap ((B \cup C) \backslash (B \cap C)))))$
$\Leftrightarrow x\in (A+((B \cup C) \backslash (B \cap C)))$
$\Leftrightarrow x\in (A+(B+C))$
Is there a program which can solve such things with steps to follow?
This is just tedious.
Or is my way in general stupid?
 A: $+$ is $\oplus$, which is the exclusive or.  Some identities for XOR are:
$$X\oplus Y = (X\cup Y)\cap (X\cap Y)^\complement= (X\cap Y^\complement)\cup(X^\complement\cap Y)\\ (X\oplus Y)^\complement = (X\oplus Y^\complement)=(X^\complement\oplus Y)=(X\cap Y)\cup(X^\complement\cap Y^\complement)$$
Then $(A+B)+C\\ = ((A\oplus B)\cup C)\cap ((A\oplus B)^\complement\cup C^\complement)\\= ((A\cap B^\complement)\cup (A^\complement\cap B)\cup C)\cap ((A\oplus B)^\complement\cup C^\complement) \\= ((A\cap B^\complement)\cup (A^\complement\cap B)\cup C)\cap ((A\cap B)\cup(A^\complement\cap B^\complement)\cup C^\complement) \\ = (A\cap B\cap C)\cup(A\cap B^\complement\cap C^\complement)\cup(A^\complement\cap B\cap C^\complement)\cup(A^\complement\cap B^\complement\cap C)$
By symmetry, then $(A+B)+C=A+(B+C)$

(Sigh) Like so $A+(B+C)\\ = (A\cup (B\oplus C))\cap (A^\complement\cup(B\oplus C)^\complement)\\= (A\cup(B\cap C^\complement)\cup (B^\complement\cap C))\cap (A^\complement\cup(B\oplus C)^\complement) \\= (A\cup(B\cap C^\complement)\cup (B^\complement\cap C))\cap (A^\complement\cup(B\cap C)\cup(B^\complement\cap C^\complement)) \\ = (A\cap B\cap C)\cup(A\cap B^\complement\cap C^\complement)\cup(A^\complement\cap B\cap C^\complement)\cup(A^\complement\cap B^\complement\cap C)$
The exclusive-disjunction of three sets consists of: everything that is either in exactly any one of the three sets, or in the union of all three sets.
