Branches (if and while) on indeterminate values yield an Undef state.

This is needed for the (to be proven) progress theorem: a valid program can
either do a step, or is in an Undef or final state.

Also make the Undef states more detailed, this is useful for the interpreter
so we can see which subexpression failed.