 The uncompleted program does not yet rule out intervening events. It is, for example, consistent with an Unload event occurring at time instant 9. The completion of the program should tell us that (46) and (47) were the only events. The completion is computed according to the following  procedure.[7]  We start with the facts in (46) and (47). Both of these are Happens formulae. The completion of the program intuitively corresponds to an assertion that, given this program, Happens\((e, t)\) can only mean Load occurring at 1 or Shoot occurring at 10. We therefore first substitute variables for the constants and write the following disjunction: 