Both cases have to hold simultaneously.

I try to explain this part of the proof in other words:

We want to show that the Hoare triple holds with the computed precondition `pc s Q`

.

That is, we can prove (using the Hoare rules) `{pc s Q} s {Q}`

for any `s`

and `Q`

.

Note: We assume that all side conditions for while loops (`vc`

) hold.

To show this, we perform a case distinction about the shape of `s`

.

As some statements are composed of other statements, we need induction (as known from other basic courses like Programming 1).

One case is the condition `If`

.

Our proof obligation now is to show:

By induction we know

and

We have (by definition of `vc`

):

vc~(if(e)~s_1~else~s_2)~Q=(vc~s_1~Q) \cup(vc~s_2~Q)

Therefore, the conditions for the induction hypotheses are fulfilled.

To show

we can only apply the [Consequence] rule or [If] rule.

Lets try [If]:

We want to show this with P=pc~(if(e)~s_1~else~s_2)~Q.

Therefore, after applying the [If] rule, we are left to prove

\{e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_1~ \{Q\}

and

\{\lnot e\land pc~(if(e)~s_1~else~s_2)~Q\}~s_2~ \{Q\}

using our induction hypotheses.

The hypotheses (applied with the proof of the `vc`

conditions) look like:

\{pc~s_1~Q\}~s_1~ \{Q\}

and

\{pc~s_2~Q\}~s_2~ \{Q\}.

So if we can show

,

we can apply the consequence rule and proof the obligation using the hypothesis.

Put together in a nice clean tree:

So how do we obtain the proof of the implication?

It follows directly from the definition: