X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=report1%2Fmart.tex;h=b0eae6a98b3730a8cf1beb9311a5cc2ef7dfa0e7;hb=03c6e2f515f6516448ec39aa40a439b9fc20c4c8;hp=ee1d9b5f43a450dba68d30f5c56345de87b0bfb0;hpb=36c7bbee78dc35e2311cfe62ede14fa8c58debb6;p=mc1516pa.git

diff --git a/report1/mart.tex b/report1/mart.tex
index ee1d9b5..b0eae6a 100644
--- a/report1/mart.tex
+++ b/report1/mart.tex
@@ -56,7 +56,7 @@ $$
 When the goal state is reached the $movement$ variable should be set to
 $finished$ to be able to specify the CTL specification more easily. Via the
 following invariant the goal state is tied to the $movement$ variable:
-$$\left(\bigvee_{B`\in perm(B)}
+$$\left(\bigvee_{B`\in perms(B)}
 	\bigwedge_{b\in B`, i\in 0\ldots k}\left(
 		b_x=t^i_x \wedge b_y=t^i_y
 \right)\right)\leftrightarrow movement=finished$$