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 
   can lead to state s2.

(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)