Strong until ($\alpha \mathrm{U}\beta$)

In linear temporal logic, $\alpha \mathrm{U}\beta$ holds at position $i$ exactly when some $j\ge i$ satisfies $\beta$ and every position $k$ with $i\le k<j$ satisfies $\alpha$. The witness $j$ must exist. The case $j=i$ imposes no condition on $\alpha$.