- Before looking into how to prove these properties, we'll look at our
- transformation system from a graph perspective. The nodes of the graph are
- all possible Core expressions. The (directed) edges of the graph are
- transformations. When a transformation α applies to an expression \lam{A} to
- produce an expression \lam{B}, we add an edge from the node for \lam{A} to the
- node for \lam{B}, labeled α.
+ Before looking into how to prove these properties, we'll look at
+ transformation systems from a graph perspective. We will first define
+ the graph view and then illustrate it using a simple example from lambda
+ calculus (which is a different system than the Cλash normalization
+ system). The nodes of the graph are all possible Core expressions. The
+ (directed) edges of the graph are transformations. When a transformation
+ α applies to an expression \lam{A} to produce an expression \lam{B}, we
+ add an edge from the node for \lam{A} to the node for \lam{B}, labeled
+ α.