NTH/UPDATE-NTH expressions
Major Section: MISCELLANEOUS
The rewriter contains special provisions for rewriting expressions
composed of nth, update-nth, update-nth-array, together
with let expressions and other applications of non-recursive
functions or lambda expressions. For details see the paper
``Rewriting for Symbolic Execution of State Machine Models'' by J
Strother Moore.
More will be written about this soon.