Theorem. Deterministic event folding gives replayable state [ftip-00C9]
✍️source

    For a materialization record in Definition [ftip-00C8], replaying the same initial state, event sequence, version sequence, and fold maps produces the same state \(h_n\).

    This finite result follows from the displayed hypotheses. It assumes exact equality of all recorded inputs and deterministic fold maps.

    Proof. 

      At step zero both replays have state \(h_0\). If their states agree at step \(i\), both apply the same function \(F_{v_i}\) to the same pair \((h_i,e_i)\), so their states agree at step \(i+1\). Finite induction gives equality at step \(n\).