Evaluation
The evaluation of a rest = Q at a level m proceeds as
follows. The path Q is evaluated at the level 0. If the
result obtained is a failure $fail(k), then the whole construct returns the
failure $fail(m+1), which is so strong as to overcome all surrounding
fences that are not neutralized by cuts.
Env,0,St |- Q => Ge,St'
-------------------------
Env,m,St |- = Q => Ge,St'
Env,0,St |- Q => $fail(k),St'
---------------------------------
Env,m,St |- = Q => $fail(m+1),St'
Env,0,St |- Q => $error(Ge),St'
---------------------------------
Env,m,St |- = Q => $error(Ge),St'