diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Sat Dec 27 19:51:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sat Dec 27 20:32:06 2014 +0100
@@ -1,12 +1,12 @@
-section {* Examples *}
+section \<open>Examples\<close>
 
 theory RG_Examples
 imports RG_Syntax
 begin
 
-lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def 
+lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def
 
-subsection {* Set Elements of an Array to Zero *}
+subsection \<open>Set Elements of an Array to Zero\<close>
 
 lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
 by simp
@@ -17,40 +17,40 @@
 record Example1 =
   A :: "nat list"
 
-lemma Example1: 
+lemma Example1:
  "\<turnstile> COBEGIN
       SCHEME [0 \<le> i < n]
-     (\<acute>A := \<acute>A [i := 0], 
-     \<lbrace> n < length \<acute>A \<rbrace>, 
-     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>, 
-     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>, 
-     \<lbrace> \<acute>A ! i = 0 \<rbrace>) 
+     (\<acute>A := \<acute>A [i := 0],
+     \<lbrace> n < length \<acute>A \<rbrace>,
+     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>,
+     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>,
+     \<lbrace> \<acute>A ! i = 0 \<rbrace>)
     COEND
  SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
 apply(rule Parallel)
-apply (auto intro!: Basic) 
+apply (auto intro!: Basic)
 done
 
-lemma Example1_parameterized: 
+lemma Example1_parameterized:
 "k < t \<Longrightarrow>
-  \<turnstile> COBEGIN 
-    SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0], 
-   \<lbrace>t*n < length \<acute>A\<rbrace>, 
-   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>, 
-   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>j<length \<ordmasculine>A . i\<noteq>j \<longrightarrow> \<ordmasculine>A!j = \<ordfeminine>A!j)\<rbrace>, 
-   \<lbrace>\<acute>A!i=0\<rbrace>) 
-   COEND  
- SAT [\<lbrace>t*n < length \<acute>A\<rbrace>, 
-      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>i<n. \<ordmasculine>A!(k*n+i)=\<ordfeminine>A!(k*n+i))\<rbrace>, 
-      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> 
-      (\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>, 
+  \<turnstile> COBEGIN
+    SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0],
+   \<lbrace>t*n < length \<acute>A\<rbrace>,
+   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>,
+   \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>j<length \<ordmasculine>A . i\<noteq>j \<longrightarrow> \<ordmasculine>A!j = \<ordfeminine>A!j)\<rbrace>,
+   \<lbrace>\<acute>A!i=0\<rbrace>)
+   COEND
+ SAT [\<lbrace>t*n < length \<acute>A\<rbrace>,
+      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> (\<forall>i<n. \<ordmasculine>A!(k*n+i)=\<ordfeminine>A!(k*n+i))\<rbrace>,
+      \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and>
+      (\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>,
       \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
 apply(rule Parallel)
     apply auto
   apply(erule_tac x="k*n +i" in allE)
   apply(subgoal_tac "k*n+i <length (A b)")
    apply force
-  apply(erule le_less_trans2) 
+  apply(erule le_less_trans2)
   apply(case_tac t,simp+)
   apply (simp add:add.commute)
   apply(simp add: add_le_mono)
@@ -66,38 +66,38 @@
 done
 
 
-subsection {* Increment a Variable in Parallel *}
+subsection \<open>Increment a Variable in Parallel\<close>
 
-subsubsection {* Two components *}
+subsubsection \<open>Two components\<close>
 
 record Example2 =
   x  :: nat
   c_0 :: nat
   c_1 :: nat
 
-lemma Example2: 
+lemma Example2:
  "\<turnstile>  COBEGIN
-    (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>, 
-     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>, 
-     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
-        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
-        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
-     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
-         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
+    (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>,
+     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>,
+     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
+        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
+        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
+     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
+         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
          \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
   \<parallel>
-      (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>, 
-     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>, 
-     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and> 
-        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
-        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,  
-     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and> 
-         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1 
+      (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>,
+     \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>,
+     \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
+        (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
+        \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
+     \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
+         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
  COEND
- SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>, 
+ SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>,
       \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
       \<lbrace>True\<rbrace>,
       \<lbrace>\<acute>x=2\<rbrace>]"
@@ -151,9 +151,9 @@
 apply(auto intro!: Basic)
 done
 
-subsubsection {* Parameterized *}
+subsubsection \<open>Parameterized\<close>
 
-lemma Example2_lemma2_aux: "j<n \<Longrightarrow> 
+lemma Example2_lemma2_aux: "j<n \<Longrightarrow>
  (\<Sum>i=0..<n. (b i::nat)) =
  (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
 apply(induct n)
@@ -165,11 +165,11 @@
 apply arith
 done
 
-lemma Example2_lemma2_aux2: 
+lemma Example2_lemma2_aux2:
   "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
   by (induct j) simp_all
 
-lemma Example2_lemma2: 
+lemma Example2_lemma2:
  "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
 apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
 apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
@@ -189,19 +189,19 @@
  Suc (\<Sum>i::nat=0..< n. b i)=(\<Sum>i=0..< n. (b (j:=Suc 0)) i)"
 by(simp add:Example2_lemma2)
 
-record Example2_parameterized =   
+record Example2_parameterized =
   C :: "nat \<Rightarrow> nat"
   y  :: nat
 
-lemma Example2_parameterized: "0<n \<Longrightarrow> 
+lemma Example2_parameterized: "0<n \<Longrightarrow>
   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
-     (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>, 
-     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>, 
-     \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and> 
-      (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,  
-     \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and> 
+     (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>,
+     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
+     \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and>
+      (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
+     \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and>
        (\<ordmasculine>y=(\<Sum>i=0..<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i=0..<n. \<ordfeminine>C i))\<rbrace>,
-     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>) 
+     \<lbrace>\<acute>y=(\<Sum>i=0..<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
     COEND
  SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i=0..<n. \<acute>C i)=0 \<rbrace>, \<lbrace>\<ordmasculine>C=\<ordfeminine>C \<and> \<ordmasculine>y=\<ordfeminine>y\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>\<acute>y=n\<rbrace>]"
 apply(rule Parallel)
@@ -229,9 +229,9 @@
 apply simp_all
 done
 
-subsection {* Find Least Element *}
+subsection \<open>Find Least Element\<close>
 
-text {* A previous lemma: *}
+text \<open>A previous lemma:\<close>
 
 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
 apply(subgoal_tac "a=a div n*n + a mod n" )
@@ -251,25 +251,25 @@
   X :: "nat \<Rightarrow> nat"
   Y :: "nat \<Rightarrow> nat"
 
-lemma Example3: "m mod n=0 \<Longrightarrow> 
- \<turnstile> COBEGIN 
+lemma Example3: "m mod n=0 \<Longrightarrow>
+ \<turnstile> COBEGIN
  SCHEME [0\<le>i<n]
- (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO 
-   IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i) 
-   ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI 
+ (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO
+   IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i)
+   ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI
   OD,
  \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i)\<rbrace>,
- \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and> 
+ \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and>
    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
- \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>   
+ \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>
    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
- \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i) \<rbrace>) 
+ \<lbrace>(\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i) \<rbrace>)
  COEND
  SAT [\<lbrace> \<forall>i<n. \<acute>X i=i \<and> \<acute>Y i=m+i \<rbrace>,\<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,\<lbrace>True\<rbrace>,
-  \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
+  \<lbrace>\<forall>i<n. (\<acute>X i) mod n=i \<and> (\<forall>j<\<acute>X i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
     (\<acute>Y i<m \<longrightarrow> P(B!(\<acute>Y i)) \<and> \<acute>Y i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y j \<le> \<acute>X i)\<rbrace>]"
 apply(rule Parallel)
---{*5 subgoals left *}
+--\<open>5 subgoals left\<close>
 apply force+
 apply clarify
 apply simp
@@ -298,29 +298,29 @@
      apply auto
 done
 
-text {* Same but with a list as auxiliary variable: *}
+text \<open>Same but with a list as auxiliary variable:\<close>
 
 record Example3_list =
   X :: "nat list"
   Y :: "nat list"
 
 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
- (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO 
-     IF P(B!(\<acute>X!i)) THEN \<acute>Y:=\<acute>Y[i:=\<acute>X!i] ELSE \<acute>X:= \<acute>X[i:=(\<acute>X!i)+ n] FI 
+ (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO
+     IF P(B!(\<acute>X!i)) THEN \<acute>Y:=\<acute>Y[i:=\<acute>X!i] ELSE \<acute>X:= \<acute>X[i:=(\<acute>X!i)+ n] FI
   OD,
  \<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i)\<rbrace>,
- \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and> 
+ \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and>
    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
- \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>   
+ \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>
    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
  \<lbrace>(\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i) \<rbrace>) COEND)
  SAT [\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> (\<forall>i<n. \<acute>X!i=i \<and> \<acute>Y!i=m+i) \<rbrace>,
       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
       \<lbrace>True\<rbrace>,
-      \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
+      \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
         (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
 apply (rule Parallel)
-apply (auto cong del: strong_INF_cong strong_SUP_cong) 
+apply (auto cong del: strong_INF_cong strong_SUP_cong)
 apply force
 apply (rule While)
     apply force