src/HOL/HoareParallel/RG_Examples.thy
 author prensani Tue Mar 05 17:11:25 2002 +0100 (2002-03-05) changeset 13020 791e3b4c4039 child 13099 4bb592cdde0e permissions -rw-r--r--
HoareParallel Theories
```     1
```
```     2 header {* \section{Examples} *}
```
```     3
```
```     4 theory RG_Examples = RG_Syntax:
```
```     5
```
```     6 lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def
```
```     7
```
```     8 subsection {* Set Elements of an Array to Zero *}
```
```     9
```
```    10 lemma le_less_trans2: "\<lbrakk>(j::nat)<k; i\<le> j\<rbrakk> \<Longrightarrow> i<k"
```
```    11 by simp
```
```    12
```
```    13 lemma add_le_less_mono: "\<lbrakk> (a::nat) < c; b\<le>d \<rbrakk> \<Longrightarrow> a + b < c + d"
```
```    14 by simp
```
```    15
```
```    16 record Example1 =
```
```    17   A :: "nat list"
```
```    18
```
```    19 lemma Example1:
```
```    20  "\<turnstile> COBEGIN
```
```    21       SCHEME [0 \<le> i < n]
```
```    22      (\<acute>A := \<acute>A [i := 0],
```
```    23      \<lbrace> n < length \<acute>A \<rbrace>,
```
```    24      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>,
```
```    25      \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>,
```
```    26      \<lbrace> \<acute>A ! i = 0 \<rbrace>)
```
```    27     COEND
```
```    28  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>]"
```
```    29 apply(rule Parallel)
```
```    30     apply simp
```
```    31     apply clarify
```
```    32     apply simp
```
```    33     apply(erule disjE)
```
```    34      apply simp
```
```    35     apply clarify
```
```    36     apply simp
```
```    37    apply auto
```
```    38 apply(rule Basic)
```
```    39 apply auto
```
```    40 done
```
```    41
```
```    42 lemma Example1_parameterized:
```
```    43 "k < t \<Longrightarrow>
```
```    44   \<turnstile> COBEGIN
```
```    45     SCHEME [k*n\<le>i<(Suc k)*n] (\<acute>A:=\<acute>A[i:=0],
```
```    46    \<lbrace>t*n < length \<acute>A\<rbrace>,
```
```    47    \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and> \<ordmasculine>A!i = \<ordfeminine>A!i\<rbrace>,
```
```    48    \<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>,
```
```    49    \<lbrace>\<acute>A!i=0\<rbrace>)
```
```    50    COEND
```
```    51  SAT [\<lbrace>t*n < length \<acute>A\<rbrace>,
```
```    52       \<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>,
```
```    53       \<lbrace>t*n < length \<ordmasculine>A \<and> length \<ordmasculine>A=length \<ordfeminine>A \<and>
```
```    54       (\<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>,
```
```    55       \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
```
```    56 apply(rule Parallel)
```
```    57     apply simp
```
```    58     apply clarify
```
```    59     apply simp
```
```    60     apply(erule disjE)
```
```    61      apply clarify
```
```    62      apply simp
```
```    63     apply clarify
```
```    64     apply simp
```
```    65     apply clarify
```
```    66     apply simp
```
```    67     apply(erule_tac x="k*n +i" in allE)
```
```    68     apply(subgoal_tac "k*n+i <length (A b)")
```
```    69      apply force
```
```    70     apply(erule le_less_trans2)
```
```    71     apply(case_tac t,simp+)
```
```    72     apply (simp add:add_commute)
```
```    73     apply(rule add_le_mono)
```
```    74      apply simp
```
```    75     apply simp
```
```    76    apply simp
```
```    77    apply clarify
```
```    78    apply(rotate_tac -1)
```
```    79    apply force
```
```    80   apply force
```
```    81  apply force
```
```    82 apply simp
```
```    83 apply clarify
```
```    84 apply(rule Basic)
```
```    85    apply simp
```
```    86    apply clarify
```
```    87    apply (subgoal_tac "k*n+i< length (A x)")
```
```    88     apply simp
```
```    89    apply(erule le_less_trans2)
```
```    90    apply(case_tac t,simp+)
```
```    91    apply (simp add:add_commute)
```
```    92    apply(rule add_le_mono)
```
```    93     apply simp
```
```    94    apply simp
```
```    95   apply force+
```
```    96 done
```
```    97
```
```    98 subsection {* Increment a Variable in Parallel *}
```
```    99
```
```   100 subsubsection {* Two components *}
```
```   101
```
```   102 record Example2 =
```
```   103   x  :: nat
```
```   104   c_0 :: nat
```
```   105   c_1 :: nat
```
```   106
```
```   107 lemma Example2:
```
```   108  "\<turnstile>  COBEGIN
```
```   109     (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_0:=\<acute>c_0 + 1 \<rangle>,
```
```   110      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1  \<and> \<acute>c_0=0\<rbrace>,
```
```   111      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
```
```   112         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
```
```   113         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
```
```   114      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
```
```   115          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
```
```   116          \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
```
```   117      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_0=1 \<rbrace>)
```
```   118   \<parallel>
```
```   119       (\<langle> \<acute>x:=\<acute>x+1;; \<acute>c_1:=\<acute>c_1+1 \<rangle>,
```
```   120      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=0 \<rbrace>,
```
```   121      \<lbrace>\<ordmasculine>c_1 = \<ordfeminine>c_1 \<and>
```
```   122         (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
```
```   123         \<longrightarrow> \<ordfeminine>x = \<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
```
```   124      \<lbrace>\<ordmasculine>c_0 = \<ordfeminine>c_0 \<and>
```
```   125          (\<ordmasculine>x=\<ordmasculine>c_0 + \<ordmasculine>c_1
```
```   126         \<longrightarrow> \<ordfeminine>x =\<ordfeminine>c_0 + \<ordfeminine>c_1)\<rbrace>,
```
```   127      \<lbrace>\<acute>x=\<acute>c_0 + \<acute>c_1 \<and> \<acute>c_1=1\<rbrace>)
```
```   128  COEND
```
```   129  SAT [\<lbrace>\<acute>x=0 \<and> \<acute>c_0=0 \<and> \<acute>c_1=0\<rbrace>,
```
```   130       \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and>  \<ordmasculine>c_0= \<ordfeminine>c_0 \<and> \<ordmasculine>c_1=\<ordfeminine>c_1\<rbrace>,
```
```   131       \<lbrace>True\<rbrace>,
```
```   132       \<lbrace>\<acute>x=2\<rbrace>]"
```
```   133 apply(rule Parallel)
```
```   134    apply simp_all
```
```   135    apply clarify
```
```   136    apply(case_tac i)
```
```   137     apply simp
```
```   138     apply(erule disjE)
```
```   139      apply clarify
```
```   140      apply simp
```
```   141     apply clarify
```
```   142     apply simp
```
```   143     apply(case_tac j,simp)
```
```   144     apply simp
```
```   145    apply simp
```
```   146    apply(erule disjE)
```
```   147     apply clarify
```
```   148     apply simp
```
```   149    apply clarify
```
```   150    apply simp
```
```   151    apply(case_tac j,simp,simp)
```
```   152   apply clarify
```
```   153   apply(case_tac i,simp,simp)
```
```   154  apply clarify
```
```   155  apply simp
```
```   156  apply(erule_tac x=0 in all_dupE)
```
```   157  apply(erule_tac x=1 in allE,simp)
```
```   158 apply clarify
```
```   159 apply(case_tac i,simp)
```
```   160  apply(rule Await)
```
```   161   apply simp_all
```
```   162  apply(clarify)
```
```   163  apply(rule Seq)
```
```   164   prefer 2
```
```   165   apply(rule Basic)
```
```   166    apply simp_all
```
```   167   apply(rule subset_refl)
```
```   168  apply(rule Basic)
```
```   169  apply simp_all
```
```   170  apply clarify
```
```   171  apply simp
```
```   172 apply(rule Await)
```
```   173  apply simp_all
```
```   174 apply(clarify)
```
```   175 apply(rule Seq)
```
```   176  prefer 2
```
```   177  apply(rule Basic)
```
```   178   apply simp_all
```
```   179  apply(rule subset_refl)
```
```   180 apply(rule Basic)
```
```   181 apply simp_all
```
```   182 apply clarify
```
```   183 apply simp
```
```   184 done
```
```   185
```
```   186 subsubsection {* Parameterized *}
```
```   187
```
```   188 lemma Example2_lemma1: "j<n \<Longrightarrow> (\<Sum>i<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
```
```   189 apply(induct n)
```
```   190  apply simp_all
```
```   191 apply(force simp add: less_Suc_eq)
```
```   192 done
```
```   193
```
```   194 lemma Example2_lemma2_aux:
```
```   195  "j<n \<Longrightarrow> (\<Sum>i<n. (b i::nat)) = (\<Sum>i<j. b i) + b j + (\<Sum>i<n-(Suc j) . b (Suc j + i))"
```
```   196 apply(induct n)
```
```   197  apply simp_all
```
```   198 apply(simp add:less_Suc_eq)
```
```   199  apply(auto)
```
```   200 apply(subgoal_tac "n - j = Suc(n- Suc j)")
```
```   201   apply simp
```
```   202 apply arith
```
```   203 done
```
```   204
```
```   205 lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
```
```   206 apply(induct j)
```
```   207  apply simp_all
```
```   208 done
```
```   209
```
```   210 lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
```
```   211 apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
```
```   212 apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
```
```   213 apply(frule_tac b=b in Example2_lemma2_aux)
```
```   214 apply(erule_tac  t="Summation b n" in ssubst)
```
```   215 apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
```
```   216  apply(rotate_tac -1)
```
```   217  apply(erule ssubst)
```
```   218  apply(subgoal_tac "j\<le>j")
```
```   219   apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
```
```   220   apply(rotate_tac -1)
```
```   221   apply(erule ssubst)
```
```   222 apply simp_all
```
```   223 done
```
```   224
```
```   225 lemma Example2_lemma2_Suc0: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=Suc 0)) i)"
```
```   226 by(simp add:Example2_lemma2)
```
```   227
```
```   228 lemma Example2_lemma3: "\<forall>i< n. b i = 1 \<Longrightarrow> (\<Sum>i<n. b i)= n"
```
```   229 apply (induct n)
```
```   230 apply auto
```
```   231 done
```
```   232
```
```   233 record Example2_parameterized =
```
```   234   C :: "nat \<Rightarrow> nat"
```
```   235   y  :: nat
```
```   236
```
```   237 lemma Example2_parameterized: "0<n \<Longrightarrow>
```
```   238   \<turnstile> COBEGIN SCHEME  [0\<le>i<n]
```
```   239      (\<langle> \<acute>y:=\<acute>y+1;; \<acute>C:=\<acute>C (i:=1) \<rangle>,
```
```   240      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=0\<rbrace>,
```
```   241      \<lbrace>\<ordmasculine>C i = \<ordfeminine>C i \<and>
```
```   242       (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
```
```   243      \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>C j = \<ordfeminine>C j) \<and>
```
```   244        (\<ordmasculine>y=(\<Sum>i<n. \<ordmasculine>C i) \<longrightarrow> \<ordfeminine>y =(\<Sum>i<n. \<ordfeminine>C i))\<rbrace>,
```
```   245      \<lbrace>\<acute>y=(\<Sum>i<n. \<acute>C i) \<and> \<acute>C i=1\<rbrace>)
```
```   246     COEND
```
```   247  SAT [\<lbrace>\<acute>y=0 \<and> (\<Sum>i<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>]"
```
```   248 apply(rule Parallel)
```
```   249 apply force
```
```   250 apply force
```
```   251 apply(force elim:Example2_lemma1)
```
```   252 apply clarify
```
```   253 apply simp
```
```   254 apply(force intro:Example2_lemma3)
```
```   255 apply clarify
```
```   256 apply simp
```
```   257 apply(rule Await)
```
```   258 apply simp_all
```
```   259 apply clarify
```
```   260 apply(rule Seq)
```
```   261 prefer 2
```
```   262 apply(rule Basic)
```
```   263 apply(rule subset_refl)
```
```   264 apply simp+
```
```   265 apply(rule Basic)
```
```   266 apply simp
```
```   267 apply clarify
```
```   268 apply simp
```
```   269 apply(force elim:Example2_lemma2_Suc0)
```
```   270 apply simp+
```
```   271 done
```
```   272
```
```   273 subsection {* Find Least Element *}
```
```   274
```
```   275 text {* A previous lemma: *}
```
```   276
```
```   277 lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
```
```   278 apply(subgoal_tac "a=a div n*n + a mod n" )
```
```   279  prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
```
```   280 apply(subgoal_tac "j=j div n*n + j mod n")
```
```   281  prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
```
```   282 apply simp
```
```   283 apply(subgoal_tac "a div n*n < j div n*n")
```
```   284 prefer 2 apply arith
```
```   285 apply(subgoal_tac "j div n*n < (a div n + 1)*n")
```
```   286 prefer 2 apply simp
```
```   287 apply (simp only:mult_less_cancel2)
```
```   288 apply arith
```
```   289 done
```
```   290
```
```   291 record Example3 =
```
```   292   X :: "nat \<Rightarrow> nat"
```
```   293   Y :: "nat \<Rightarrow> nat"
```
```   294
```
```   295 lemma Example3: "m mod n=0 \<Longrightarrow>
```
```   296  \<turnstile> COBEGIN
```
```   297  SCHEME [0\<le>i<n]
```
```   298  (WHILE (\<forall>j<n. \<acute>X i < \<acute>Y j)  DO
```
```   299    IF P(B!(\<acute>X i)) THEN \<acute>Y:=\<acute>Y (i:=\<acute>X i)
```
```   300    ELSE \<acute>X:= \<acute>X (i:=(\<acute>X i)+ n) FI
```
```   301   OD,
```
```   302  \<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>,
```
```   303  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y j \<le> \<ordmasculine>Y j) \<and> \<ordmasculine>X i = \<ordfeminine>X i \<and>
```
```   304    \<ordmasculine>Y i = \<ordfeminine>Y i\<rbrace>,
```
```   305  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X j = \<ordfeminine>X j \<and> \<ordmasculine>Y j = \<ordfeminine>Y j) \<and>
```
```   306    \<ordfeminine>Y i \<le> \<ordmasculine>Y i\<rbrace>,
```
```   307  \<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>)
```
```   308  COEND
```
```   309  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>,
```
```   310   \<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>
```
```   311     (\<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>]"
```
```   312 apply(rule Parallel)
```
```   313 (*5*)
```
```   314 apply force+
```
```   315 apply clarify
```
```   316 apply simp
```
```   317 apply(rule While)
```
```   318     apply force
```
```   319    apply force
```
```   320   apply force
```
```   321  apply(rule_tac "pre'"="\<lbrace> \<acute>X i mod n = i \<and> (\<forall>j. j<\<acute>X i \<longrightarrow> j mod n = i \<longrightarrow> \<not>P(B!j)) \<and> (\<acute>Y i < n * q \<longrightarrow> P (B!(\<acute>Y i))) \<and> \<acute>X i<\<acute>Y i\<rbrace>" in Conseq)
```
```   322      apply force
```
```   323     apply(rule subset_refl)+
```
```   324  apply(rule Cond)
```
```   325     apply force
```
```   326    apply(rule Basic)
```
```   327       apply force
```
```   328      apply force
```
```   329     apply force
```
```   330    apply force
```
```   331   apply(rule Basic)
```
```   332      apply simp
```
```   333      apply clarify
```
```   334      apply simp
```
```   335      apply(case_tac "X x (j mod n)\<le> j")
```
```   336       apply(drule le_imp_less_or_eq)
```
```   337       apply(erule disjE)
```
```   338        apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
```
```   339         apply assumption+
```
```   340        apply simp+
```
```   341      apply(erule_tac x=j in allE)
```
```   342      apply force
```
```   343     apply simp
```
```   344     apply clarify
```
```   345     apply(rule conjI)
```
```   346      apply clarify
```
```   347      apply simp
```
```   348      apply(erule not_sym)
```
```   349     apply force
```
```   350 apply force+
```
```   351 done
```
```   352
```
```   353 text {* Same but with a list as auxiliary variable: *}
```
```   354
```
```   355 record Example3_list =
```
```   356   X :: "nat list"
```
```   357   Y :: "nat list"
```
```   358
```
```   359 lemma Example3_list: "m mod n=0 \<Longrightarrow> \<turnstile> (COBEGIN SCHEME [0\<le>i<n]
```
```   360  (WHILE (\<forall>j<n. \<acute>X!i < \<acute>Y!j)  DO
```
```   361      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
```
```   362   OD,
```
```   363  \<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>,
```
```   364  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordfeminine>Y!j \<le> \<ordmasculine>Y!j) \<and> \<ordmasculine>X!i = \<ordfeminine>X!i \<and>
```
```   365    \<ordmasculine>Y!i = \<ordfeminine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
```
```   366  \<lbrace>(\<forall>j<n. i\<noteq>j \<longrightarrow> \<ordmasculine>X!j = \<ordfeminine>X!j \<and> \<ordmasculine>Y!j = \<ordfeminine>Y!j) \<and>
```
```   367    \<ordfeminine>Y!i \<le> \<ordmasculine>Y!i \<and> length \<ordmasculine>X = length \<ordfeminine>X \<and> length \<ordmasculine>Y = length \<ordfeminine>Y\<rbrace>,
```
```   368  \<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)
```
```   369  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>,
```
```   370       \<lbrace>\<ordmasculine>X=\<ordfeminine>X \<and> \<ordmasculine>Y=\<ordfeminine>Y\<rbrace>,
```
```   371       \<lbrace>True\<rbrace>,
```
```   372       \<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>
```
```   373         (\<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>]"
```
```   374 apply(rule Parallel)
```
```   375 (*5*)
```
```   376 apply force+
```
```   377 apply clarify
```
```   378 apply simp
```
```   379 apply(rule While)
```
```   380     apply force
```
```   381    apply force
```
```   382   apply force
```
```   383  apply(rule_tac "pre'"="\<lbrace>n<length \<acute>X \<and> n<length \<acute>Y \<and> \<acute>X ! i mod n = i \<and> (\<forall>j. j < \<acute>X ! i \<longrightarrow> j mod n = i \<longrightarrow> \<not> P (B ! j)) \<and> (\<acute>Y ! i < n * q \<longrightarrow> P (B ! (\<acute>Y ! i))) \<and> \<acute>X!i<\<acute>Y!i\<rbrace>" in Conseq)
```
```   384      apply force
```
```   385     apply(rule subset_refl)+
```
```   386  apply(rule Cond)
```
```   387     apply force
```
```   388    apply(rule Basic)
```
```   389       apply force
```
```   390      apply force
```
```   391     apply force
```
```   392    apply force
```
```   393   apply(rule Basic)
```
```   394      apply simp
```
```   395      apply clarify
```
```   396      apply simp
```
```   397      apply(rule allI)
```
```   398      apply(rule impI)+
```
```   399      apply(case_tac "X x ! i\<le> j")
```
```   400       apply(drule le_imp_less_or_eq)
```
```   401       apply(erule disjE)
```
```   402        apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
```
```   403         apply assumption+
```
```   404        apply simp
```
```   405 apply force+
```
```   406 done
```
```   407
```
`   408 end`