Well, I am embarrassed at how late I am in posting the solution to the puzzle I mentioned in my last post. It has been a busy summer with taking care of our sweet new baby at home, and running StarExec development at work. Anyhow, below is a graph with the minimum number of nodes which contains every legal possible combination of properties from termination (aka strong normalization), normalization (aka weak normalization), confluence (aka Church-Rosser), and local confluence (aka Weak Church-Rosser), and their negations. This graph was found by Hans Zantema, whom I asked about this puzzle by email (he agreed to let me share his solution here). Furthermore, he argues that 11 is the minimal number of nodes, as follows. Out of the 16 possible combinations of properties SN, WN, CR, and WCR and their negations, we exclude immediately the combinations with SN and ~WN (since SN implies WN) and CR and ~WCR (since CR implies WCR). So there are three legal possibilities for the values of CR and WCR, and three for the values of SN and WN. These are independent, so there are 9 legal combinations of properties. Now, Hans argues, since there is a node X which is SN and ~WCR, there must be two nodes which are SN and CR. For since X is SN but not WCR, it has two children (which are still SN) which cannot be joined. We may assume these children are themselves CR, otherwise we could repeat this observation and the graph would not be minimal. Similarly, since there is a node which is ~WN and ~WCR, there must be two nodes which are ~WN and CR. So there must be at least 11 nodes. And the graph below has 11 nodes. To test your knowledge, you can try to identify which combination of properties each node has! Fun!