diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index 26be616ced4b8919938e187cfc2188f7bc074ace..9a818d7201156062ccd5d4379e984753c3d1cf05 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/src/plugins/wp/doc/manual/wp_plugin.tex @@ -444,6 +444,18 @@ n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b \end{array} \] +\paragraph{Induction} Start a proof by integer induction \\ +The user select any integer expression $e$ in the proof and a base value $b$ (which defaults to +0). The tactic generates a proof by strong (integer) induction on $e$, that is, the base case +$e = b$ and then the cases $e < b$ and $b < e$. Formally: + +$\TACTIC{\Delta\models\,G}{% +\begin{array}[t]{llll} +\Delta, & G[e \leftarrow n], & n = b & \models G[e \leftarrow n] \\ +\Delta, & G[e \leftarrow i], & b \leq i < n & \models G[e \leftarrow n] \\ +\Delta, & G[e \leftarrow i], & n < i \leq b & \models G[e \leftarrow n] +\end{array}}$ + \paragraph{Overflow} Integer Conversions \\ This tactic rewrites machine integer conversions by identity, providing the converted value is in available range. The tactic applies on expression