I have a problem proving a logic equality in the context of the generation of verification condition for imperative non-deterministic programs. I have the following formulas that describe the change in the state of the program for certain constructs:
$R(havoc(x)) = \land_{v \in V \setminus \{x\} } v' = v$ where $V$ is the set of variables of the program.
$R(assume(F)) = F \land \land_{v \in V} v' = v$
$R(c_1;c_2) = \exists \overline{z}. R(c1)[\overline{x'}:=\overline{z}] \land R(c_2)[\overline{x}:=\overline{z}]$ where the $\overline{.}$ denotes possible vector values (a vector of variables) and in the first part of the conjunction $\overline{x'}$ refers to the output varaible states after $c_1$ and in the second part of the conjunction $\overline{x}$ refers to the input state for $c_2$.
The havoc primitive gives a non-specified value to variable x and the assume F stops any execution where F doesn't hold. The last primitive is normal sequential composition.
I should be able to proof with this primitives that $R(assume(f);c) ) = F \land R(c)$ and that $R(c;assume(F)) = R(c) \land F[\overline{x}:=\overline{x'}]$ however I'm not able to do it.
Take for instance the second case, I arrive to $\exists \overline{z}. R(c) [\overline{x'}:=\overline{z}] \land F[\overline{x} := \overline{z}] \land \overline{x'} := \overline{z}$ from here I'm supposed to use one-point rule to get to the expected equality $R(c) \land F[\overline{x}:=\overline{x'}]$. I understand the second part of the conjuction but why the first part can be simplied to $R(c)$?
The point here is than sequential composition rule must be rewritten or understood in the following manner:
$R(c_1;c_2) = \exists \overline{z}. R(c1)[\overline{x'}:=\overline{z}] \land R(c_2)[\overline{x}:=\overline{z}]$
So here $\overline{x'}$ in the first formula should be equal to $\overline{x}$ in the second formula because the output of the first command should be equal to the input of the second command.
Therefore, the rule should be rewritten in a convenient manner.