# How to deal with missing variables when utilizing weakest precondition for verification?

I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following reinforcement learning equation and we want to constrain it across 2 timesteps -

$$v' = v + 0.1a + \epsilon$$

Based on a previous question that I asked [2], I modified the description given in that example to look more like a typical program with constraints (given by {}).

$$\{v_0 + 0.1a_0 + \epsilon_2 \le1 \land v_0 + 0.1a_0 + \epsilon_2 + 0.1a_1 + \epsilon_1 \le 1\}$$

$$v_1 = v_0 + 0.1a_0 + \epsilon_2$$

$$\{v_1 \le1 \land v_1 + 0.1a_1 + \epsilon_1 \le 1\}$$

$$v_2 = v_1 + 0.1a_1 + \epsilon_1$$

$$\{v_1 \le1 \land v_2 \le 1\}$$

My question is, how will the program check the first precondition ($$\{v_0 + 0.1a_0 + \epsilon_2 \le1 \land v_0 + 0.1a_0 + \epsilon_2 + 0.1a_1 + \epsilon_1 \le 1\}$$), since at time step 0, it won't know the value of $$a_1$$.

Please let me know if any clarification from my side is needed.

[1]. Anderson, Greg, Swarat Chaudhuri, and Isil Dillig. "Guiding Safe Exploration with Weakest Preconditions." International Conference on Learning Representations. 2023.