Annotated type system problem about conditional branch

Question

I am reading the book "Principle of Program Analysis" by Flemming Nielson for annotated type systems. In the first chapter, section 1.6 they mentioned the simple type system for various statements(S). And S maps a state to a state, and may therefore to have type Σ --> Σ where Σ denotes the type of state. So they mentioned a system of axioms and inference rules like below for sequential statements and if-else block:

1. 
2. 

And later it is explained, an if-else statement in terms of Reaching Definition as below,

Also, I can visualize the sequencing rule seems natural, but they mentioned conditional rule is more dubious. I am not able to understand how this is dubious? As per my understanding reaching definition after after 'if' block execution will may execute then block or else block, then how this is even conflicting? S1 may have different statements and S2 will also have different statements but these two blocks would not execute at same time. I am not getting this scenario, can you please help me with this

Answer 1

With the above expression, two branches (if and else) have the same analysis information at their respective entry and exit points i.e. In simple terms we can say that then-branch gives rise to the same set of reaching definitions as the else-branch does.

So, this is dubious, depending on the condition of if-block it is decided control will go to then or else block which will become the exit of if-block. To follow this idea we can modify the equation like below.

We assume that if if-block gets executed as true then final(S1) is executed i.e. RD2 and for false statement final(S2) i.e. RD3 is executed. The exit of the if-block is the subset of the union of then-block and the else-block.