I think the main problem people encounter understanding this thing is just parsing the expression tree for the rules. It isn't stated but all trees in question

I think the main problem people encounter understanding this thing is just parsing the expression tree for the rules. It isn't stated but all trees in question are binary trees. Even though the expression tree syntax is really easy E := t | E E The mental gymnastic needed to visualize that the string not = t ( t (t t) (t t t)) t correspond to the only tree drawn in https://treecalcul.us/specification/ https://treecalcul.us/specification/ is quite overwhelming. The left-associative notation to remove unneeded parenthesis makes it even harder. It could be explained so much better if the author made the 10 pictures corresponding to the transformation rules of the trees. Eventually highlighting the subtrees a, b, c, in the corresponding color before after. Brains are used to pattern matching images but not abstractly defined syntax unless you have been trained in grammar theory.