Revise eval relation to make proof simpler; prove correctness!

Revision does away with rule that turns

    Par (..... ++ [Done] ++ .....)

into

    Par (..... ++           .....)

Instead, the logical system now just leaves the Dones in place,
getting rid of the rule above entirely. The other change needed is to
say that (Par cs) moves to Done if every c ∈ cs is Done.

Also add a new rule that moves

    Par (..... ++ [Abort] ++ .....)

to

    Abort

just because it seems reasonable.