Proof obligations, Hoare-logic I'm having trouble understanding why the proof obligations are valid.
When they write " F -> . = T" in the explanation, I assume they refer to ⊢ ⊤ ∧ (x=5) → ((( x=5 ) → (3=3)) ∧ ((x=3)→ (3=1))) but I still don't understand. Why would ⊤ ∧ (x=5)  be F ?
If someone could clarify I would really appreciate it!


 A: 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$.
