Given: \[\begin{split} Q &: n > 0\\ R &: res = n!\\ I &: (i \leq n + 1) {\ \land \ }(res = (i - 1)!)\\ B &: i \leq n\\ V &: n - i + 1\\ S &: \{ res := res * i; i := i + 1 \} \end{split}\]
We are proving that: \(Q \to {wp\left(S_1, I\right)}\), where \(S_1\) is the statement before the loop. \[\begin{split} & Q &\to {wp\left(S_1, I\right)}\\ {\ ({\mathbf{ยง1}})} \iff & Q &\to {wp\left(res, i := res * i, i + 1, (i \leq n + 1) {\ \land \ }(res = (i - 1)!)\right)}\\ \iff & Q &\to (2 \leq n + 1) {\ \land \ }(1 = 1!)\\ \iff & n > 0 &\to 2 \leq n + 1\\ \iff & {{\mathbf{\top}}}&\\ \end{split}\]