A finite adaptive Euler–Maruyama budget returns a status

Before the first operation the counter is zero. Each operation increases it by exactly one, and no branch decreases it or runs without consuming a unit. Induction on the operation count therefore gives a counter between $0$ and $B$ throughout execution; the loop either reaches $T$ and returns complete, or reaches counter $B$ first and returns inconclusive by [F1].

Each trial state and finite queue is a measurable function of the initial data, Brownian increments and fresh Gaussian innovations: coefficient evaluation and the acceptance rule are Borel, and updates, splits and queue operations are measurable finite operations. Induction through the deterministic budget makes the event that trial $k$ is performed measurable for each $1\le k\le B$. Thus $C={\sum }_{k=1}^B{1}_{\{\text{trial }k\text{ is performed}\}}$ is a random variable. It satisfies $0\le C\le B$ pointwise by step 1.1, so it is integrable and $\mathbb{E}C\le B$. If $B=0$, no trial is performed and, since $T>0$, the status is inconclusive. This proves the claim without asserting that completion occurs with positive probability.