```ANSWER TO MOCK QUESTION 5:

|= {P}C{Q} means:

∀s1 s2. Ssem P s1 ∧ Csem C s1 s2 ⇒ Ssem Q s2

where

- Ssem P s is the meaning of first order logic statement P in state s

- Csem C s1 s2 means that executing command C in state s1

(a) The validity of the conjunction rule is thus:

((∀s1 s2. Ssem P1 s1 ∧ Csem C s1 s2 ⇒ Ssem Q1 s2)
∧
(∀s1 s2. Ssem P2 s1 ∧ Csem C s1 s2 ⇒ Ssem Q2 s2))
⇒
(∀s1 s2. Ssem (P1 ∧ P2) s1 ∧ Csem C s1 s2 ⇒ Ssem (Q1 ∧ Q2) s2)

This follows by pure logical reasoning because Ssem is defined so that:

- Ssem (P1 ∧ P2) s = (Ssem P1 s) ∧ (Ssem P2 s)

- Ssem (Q1 ∧ Q2) s = (Ssem Q1 s) ∧ (Ssem Q2 s)

and so abbreviating:

- A1 s    = (Ssem P1 s)
- A2 s    = (Ssem P2 s)
- B1 s    = (Ssem Q1 s)
- B2 s    = (Ssem Q2 s)
- C s1 s2 = (Csem C s1 s2)

the soundness of the rule is equivalent to the truth of:

((∀s1 s2. A1 s ∧ C s1 s2 ⇒ B1 s)
∧
(∀s1 s2. A2 s ∧ C s1 s2 ⇒ B2 s))
⇒
(∀s1 s2. (A1 s1 ∧ A2 s1) ∧ C s1 s2 ⇒ (B1 s2 ∧ B2 s2)

which is true by first order reasoning (details omitted).

(b) The proof of the validity of the disjunction rule is similar. It
relies instead on the truth of:

((∀s1 s2. A1 s ∧ C s1 s2 ⇒ B1 s)
∧
(∀s1 s2. A2 s ∧ C s1 s2 ⇒ B2 s))
⇒
(∀s1 s2. (A1 s1 ∨ A2 s1) ∧ C s1 s2 ⇒ (B1 s2 ∨ B2 s2)
```