diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index cc03c5dab638f25d8d7591b012f4e9b36fdd41ed..3f7683d84bd9c1575ea3333a47e93a00e47d7cd0 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/src/plugins/wp/doc/manual/wp_plugin.tex @@ -455,7 +455,7 @@ $G(n) \equiv P(n)\Longrightarrow\,Q(n)$: \[\TACTIC{\Delta\models\,G(n)}{% \begin{array}[t]{lll} \Delta', & n = b & \models G(n) \\ -\Delta', G(k), & b \leq i < n & \models G(n) \\ +\Delta',\; \forall i,\, b \leq i < n \Longrightarrow G(i) \;& \models G(n) \\ \Delta', G(k), & n < i \leq b & \models G(n) \end{array}} \]