The goal of this interactive is to see how the more general versions of rules are connected with their binary versions. For instance, you can see that the general version of associativity (the ability to freely shuffle parentheses around sums) follows from the binary version (a+b)+c = a+(b+c) and a convention regarding long sums. Here we use the left-associativity convention that abc means (ab)c, the same as lambda calculus.

To get started, click on a subexpression of the formula at the bottom of the screen. If there are rules you can apply, a menu should pop up with a list of possibilities. You can also see a full list of rules this interactive knows about by changing the "show rules" option to include the "sidebar". Your first move should be to select the entire expression a+b+c below and apply the left-associativity "convention" to rewrite it as (a+b)+c. You can try problems that require a sequence of moves by using the "level select" menu below.