Evaluation
The evaluation of a path S R proceeds as follows. The source
S is evaluated, and, if the evaluation succeeds, the rest
R is evaluated.
The source S is considered to be at the zero level.
Env,0,St |- S => ,St'
Env,m,St'|- R => X,St''
-------------------------
Env,m,St |- S R => X,St''
Env,0,St |- S => $fail(k),St'
-------------------------------
Env,m,St |- S R => $fail(0),St'
Env,0,St |- S => $error(Ge),St'
---------------------------------
Env,m,St |- S R => $error(Ge),St'