Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors