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)