+ * This method computes the result `v.w'` as needed (viz. only if `v ~_[E] w`
+ * with respect to this execution `E`). The implementation takes advantage
+ * of the fact that determining whether `v ~_[E] w` yields "for free" the
+ * the shortest such `w'` we are looking for; if we ultimately determine
+ * that `v ~_[E] w`, the work we did to do so leaves us precisely with `w'`,
+ * so we can simply prepend `v` to it and call it a day
+ *
+ * @precondition: This method assumes that `E.v` is a valid execution, viz.