Proof obligations, Hoare-logic

Solution 1:

The two hints do not refer to the top level of the formula. $\top\land(x=5)$ is indeed not equivalent to $\bot$. Below are two ways to argue that the implication resulting from the then-branch is valid. In both cases, the most "difficult" arguments are ex falso quodlibet (false implies everything, $\bot\rightarrow X$ is valid) and verum ex quodlibet (true is implied by everything, $X\rightarrow\top$ is valid). This is what the authors try to point out.

$$(\top ∧ x=5) → ((x=5 → 3=3) ∧ (x=3 → 3=1))$$ simplifies to $$ x=5 → ((x=5 → \top) ∧ (x=3 → \bot))$$ because $\top∧X\equiv X$, $(3=3) \equiv \top$, and $(3=1) \equiv \bot$, which simplifies to $$x=5 → (\top ∧ x\neq3)$$ because $X→\top\equiv\top$ and $X\rightarrow\bot\equiv\lnot X$, which simplifies to $$x=5 → x\neq3$$ because $\top\land X\equiv X$. The last formula is valid over the integers.

Another way to argue might use that $$A\rightarrow(B\land C)\equiv(A\rightarrow B)\land(A\rightarrow C)\quad\text{and}\quad A\rightarrow( B\rightarrow C)\equiv (A\land B)\rightarrow C$$ With these equivalences, the top formula becomes $$((x=5\land x=5) → 3=3) ∧ ((x=5\land x=3) → 3=1))$$ which simplifies to $$(x=5 → \top) ∧ (\bot → \bot))$$ This formula is valid, since $X\rightarrow\top\equiv\top$ and $\bot\rightarrow X\equiv\top$.