CMP.13:4.4 - Recover the conclusion and examine a reported witness

Apply the requested observation to the closed result. If its represented states all satisfy the property, use that conclusion with its original input and transition assumptions. If the result overlaps an unwanted outcome, determine whether the overlap changes the next action. It may already be sufficient to retain the unresolved alternative.

When an actual path matters, reconstruct consecutive original states, starting from an admitted initial state. For abstract path a0, a1, ..., ak, propagate:

X0 = I ∩ gamma(a0);

X(i+1) = post(Xi) ∩ gamma(a(i+1)).

If some Xi is empty, the abstract path is spurious: its steps cannot be joined into one original execution. If the last set is nonempty and these sets were computed without adding possibilities, retained predecessors can recover a concrete path. If this reconstruction is itself approximate, qualify its result with that approximation’s direction; a nonempty overapproximation still leaves feasibility unresolved.

Loops and infinite-path properties require their own path and recurrence conditions. A finite prefix reaching a bad state settles finite reachability; repeating an abstract cycle does not by itself produce an infinite original execution.