ANSWER TO MOCK QUESTION 3: (i) satisfiable (A=emp), but invalid (A=x↦2). (ii) satisfiable (x=y), but invalid (x≠y) (iii) unsatisfiable. For any value v of x, heaps {v↦2} and {v↦2} are not disjoint) (iv) valid. Proof below. (v) satisfiable (A=emp), but invalid. Take A= x↦2 ∨ y↦3; B= x↦2; C= y↦3. Then heap {x↦2, y↦3} satisfies LHS, but no heap satisfies RHS since B∧C is false. (vi) satisfiable (C=emp), but invalid. Take A= true, B= x↦2, C=x↦2. The heap {x↦2} satisfies A⇒B, and it satisfies A*C, but it doesn't satisfy B*C, which is false. Proof of (iv): Suppose s,h ⊧ A*B ∨ A*C. Then s,h ⊧ A*B or s,h ⊧ A*C. So ∃h1 h2. h = h1+h2 ∧ s,h1⊧A ∧ s,h2⊧B or ∃h1 h2. h = h1+h2 ∧ s,h1⊧A ∧ s,h2⊧C Hence (since "or" distributes over ∃): ∃h1 h2. (h = h1+h2 ∧ s,h1⊧A ∧ s,h2⊧B) ∨ (h = h1+h2 ∧ s,h1⊧A ∧ s,h2⊧C) Hence: ∃h1 h2. h = h1+h2 ∧ s,h1⊧A ∧ (s,h2⊧B ∨ s,h2⊧C) Hence: ∃h1 h2. h = h1+h2 ∧ s,h1⊧A ∧ s,h2⊧B∨C Hence: s,h ⊧ A * (B∨C) as required.