Proving Correctness Properties of a Replicated Synchronous Program