[PATCH 12/12] formal/ppcmem: Fix label name for Fail1:

[SeongJae Park <sj@kernel.org>]

From: SeongJae Park <sj38.park@gmail.com>

A sentence is calling 'Fail1:' label as 'Fail:'.  Fix it.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 181ca7c6..10526bca 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -209,7 +209,7 @@ and \clnref{P1lwz} is equivalent to the C statement \co{r3=x}.
 	by setting non-zero status in the condition-code register,
 	which in turn is tested by the \co{bne} instruction.
 	Because actually modeling the loop would result in state-space
-	explosion, we instead branch to the \co{Fail:} label,
+	explosion, we instead branch to the \co{Fail1:} label,
 	terminating the model with the initial value of~2 in P0's \co{r3}
 	register, which will not trigger the exists assertion.
 
-- 
2.17.1