Issue on page /chapters/interp/substitution.html

[Luv2C0d3]

This rules seem to be missing something, specifically a mention to e':

e -->* e

e -->* e''
  if e --> e' and e' -->* e''

The first step is basically saying that e "steps to itself in 0 or more steps". In fact as you shown previously it steps in 0 steps to itself, but the intent here seems to be to reinforce the role of e' being a single step, so possibly the rules are:

e --> e'

e -->* e''
  if e --> e' and e' -->* e''

Although, that would render the first one somewhat redundant.

[clarksmr]

Actually this is correct and as intended.

The first part, which is the one at issue here, is: e -->* e.

That simply says that -->* is reflexive.

By analogy, if we were defining an equivalent relation ==, we'd write x == x.