# HG changeset patch
# User wenzelm
# Date 1248731015 -7200
# Node ID a60f183eb63edd4a7dfca6116f97ff551ba81fb9
# Parent  6c394343360f382d21507acd567eac9d8197ec9e# Parent  2a3ffaf00de4ba1789c9a9c9cecddbedc4631627
merged

diff -r 6c394343360f -r a60f183eb63e NEWS
--- a/NEWS	Mon Jul 27 23:17:40 2009 +0200
+++ b/NEWS	Mon Jul 27 23:43:35 2009 +0200
@@ -67,6 +67,13 @@
 multiplicative monoids retains syntax "^" and is now defined generic
 in class power.  INCOMPATIBILITY.
 
+* Relation composition "R O S" now has a "more standard" argument order,
+i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
+INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
+may occationally break, since the O_assoc rule was not rewritten like this.
+Fix using O_assoc[symmetric].
+The same applies to the curried version "R OO S".
+
 * GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
 infinite sets. It is shown that they form a complete lattice.
 
diff -r 6c394343360f -r a60f183eb63e src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/FunDef.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -193,9 +193,9 @@
 subsection {* Reduction Pairs *}
 
 definition
-  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
+  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
 
-lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
 unfolding reduction_pair_def by auto
 
 lemma reduction_pair_lemma:
@@ -205,7 +205,7 @@
   assumes "wf S"
   shows "wf (R \<union> S)"
 proof -
-  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
+  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
     unfolding reduction_pair_def by auto
   with `wf S` have "wf (fst P \<union> S)" 
     by (auto intro: wf_union_compatible)
@@ -266,8 +266,8 @@
 text {* Reduction Pairs *}
 
 lemma max_ext_compat: 
-  assumes "S O R \<subseteq> R"
-  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
+  assumes "R O S \<subseteq> R"
+  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
 using assms 
 apply auto
 apply (elim max_ext.cases)
@@ -287,8 +287,8 @@
 by (auto simp: pair_less_def pair_leq_def)
 
 lemma min_ext_compat: 
-  assumes "S O R \<subseteq> R"
-  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
+  assumes "R O S \<subseteq> R"
+  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
 using assms 
 apply (auto simp: min_ext_def)
 apply (drule_tac x=ya in bspec, assumption)
diff -r 6c394343360f -r a60f183eb63e src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/IMP/Denotation.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -12,14 +12,14 @@
 
 definition
   Gamma :: "[bexp,com_den] => (com_den => com_den)" where
-  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+  "Gamma b cd = (\<lambda>phi. {(s,t). (s,t) \<in> (cd O phi) \<and> b s} \<union>
                        {(s,t). s=t \<and> \<not>b s})"
 
 primrec C :: "com => com_den"
 where
   C_skip:   "C \<SKIP>   = Id"
 | C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
-| C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
+| C_comp:   "C (c0;c1)   = C(c0) O C(c1)"
 | C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
 | C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
diff -r 6c394343360f -r a60f183eb63e src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/IMP/Machines.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -6,7 +6,7 @@
   "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
 apply(rule iffI)
  apply(blast elim:rel_pow_E2)
-apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
+apply (auto simp: rel_pow_commute[symmetric])
 done
 
 subsection "Instructions"
diff -r 6c394343360f -r a60f183eb63e src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Lambda/Eta.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -371,7 +371,7 @@
 
 theorem eta_postponement:
   assumes "(sup beta eta)\<^sup>*\<^sup>* s t"
-  shows "(eta\<^sup>*\<^sup>* OO beta\<^sup>*\<^sup>*) s t" using assms
+  shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms
 proof induct
   case base
   show ?case by blast
diff -r 6c394343360f -r a60f183eb63e src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -274,7 +274,19 @@
 oops
 
 lemma star_decomp: "star (a + b) = star a * star (b * star a)"
-oops
+proof (rule antisym)
+  have "1 + (a + b) * star a * star (b * star a) \<le>
+    1 + a * star a * star (b * star a) + b * star a * star (b * star a)"
+    by (metis add_commute add_left_commute eq_iff left_distrib mult_assoc)
+  also have "\<dots> \<le> star a * star (b * star a)"
+    by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
+  finally show "star (a + b) \<le> star a * star (b * star a)"
+    by (metis mult_1_right mult_assoc star3')
+next
+  show "star a * star (b * star a) \<le> star (a + b)"
+    by (metis add_assoc add_est1 add_est2 add_left_commute less_star mult_mono'
+      star_absorb_one star_absorb_one' star_idemp star_mono star_mult_idem zero_minimum)
+qed
 
 lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow>  star y * star x \<le> star x * star y"
 by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
diff -r 6c394343360f -r a60f183eb63e src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Library/RBT.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -916,9 +916,72 @@
   "alist_of Empty = []"
 | "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r"
 
+lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1"
+proof (rule ext)
+  fix x
+  assume ST: "st (Tr c t1 k v t2)"
+  let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x"
+
+  have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'"
+  proof -
+    fix k'
+    from ST have "t1 |\<guillemotleft> k" by simp
+    with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
+    moreover assume "k'\<in>dom (RBT.map_of t1)"
+    ultimately show "k>k'" using RBT.mapof_keys ST by auto
+  qed
+
+  have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'"
+  proof -
+    fix k'
+    from ST have "k \<guillemotleft>| t2" by simp
+    with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
+    moreover assume "k'\<in>dom (RBT.map_of t2)"
+    ultimately show "k<k'" using RBT.mapof_keys ST by auto
+  qed
+
+  {
+    assume C: "x<k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp
+    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+    moreover have "x\<notin>dom (RBT.map_of t2)" proof
+      assume "x\<in>dom (RBT.map_of t2)"
+      with DOM_T2 have "k<x" by blast
+      with C show False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } moreover {
+    assume [simp]: "x=k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp
+    moreover have "x\<notin>dom (RBT.map_of t1)" proof
+      assume "x\<in>dom (RBT.map_of t1)"
+      with DOM_T1 have "k>x" by blast
+      thus False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } moreover {
+    assume C: "x>k"
+    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x])
+    moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
+    moreover have "x\<notin>dom (RBT.map_of t1)" proof
+      assume "x\<in>dom (RBT.map_of t1)"
+      with DOM_T1 have "k>x" by simp
+      with C show False by simp
+    qed
+    ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
+  } ultimately show ?thesis using less_linear by blast
+qed
+
 lemma map_of_alist_of:
   shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t"
-  oops
+proof (induct t)
+  case Empty thus ?case by (simp add: RBT.map_of_Empty)
+next
+  case (Tr c t1 k v t2)
+  hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp
+  also note map_of_alist_of_aux[OF Tr.prems,symmetric]
+  finally show ?case .
+qed
 
 lemma fold_alist_fold:
   "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"
diff -r 6c394343360f -r a60f183eb63e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Map.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -307,6 +307,9 @@
 lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
 by (simp add: map_upds_def)
 
+lemma map_add_upd_left: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)"
+by (rule ext) (auto simp: map_add_def dom_def split: option.split)
+
 lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
 unfolding map_add_def
 apply (induct xs)
@@ -508,6 +511,12 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+lemma map_add_dom_app_simps:
+  "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+  "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
+  "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
+by (auto simp add: map_add_def split: option.split_asm)
+
 lemma dom_const [simp]:
   "dom (\<lambda>x. Some y) = UNIV"
   by auto
diff -r 6c394343360f -r a60f183eb63e src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Predicate.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -221,11 +221,11 @@
 subsubsection {* Composition  *}
 
 inductive
-  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
+  pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
     (infixr "OO" 75)
-  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
+  for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
 where
-  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
+  pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
 
 inductive_cases pred_compE [elim!]: "(r OO s) a c"
 
diff -r 6c394343360f -r a60f183eb63e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Relation.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -21,9 +21,9 @@
   converse  ("(_\<inverse>)" [1000] 999)
 
 definition
-  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"
+  rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
     (infixr "O" 75) where
-  "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
+  "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
 
 definition
   Image :: "[('a * 'b) set, 'a set] => 'b set"
@@ -140,15 +140,15 @@
 subsection {* Composition of two relations *}
 
 lemma rel_compI [intro]:
-  "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
+  "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
 by (unfold rel_comp_def) blast
 
 lemma rel_compE [elim!]: "xz : r O s ==>
-  (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
+  (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s  ==> P) ==> P"
 by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
 
 lemma rel_compEpair:
-  "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
+  "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
 by (iprover elim: rel_compE Pair_inject ssubst)
 
 lemma R_O_Id [simp]: "R O Id = R"
@@ -173,7 +173,7 @@
 by blast
 
 lemma rel_comp_subset_Sigma:
-    "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
+    "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
 by blast
 
 lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
diff -r 6c394343360f -r a60f183eb63e src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -159,7 +159,7 @@
   apply (erule asm_rl exE disjE conjE base step)+
   done
 
-lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
+lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
   apply (rule subsetI)
   apply (rule_tac p="x" in PairE, clarify)
   apply (erule rtrancl_induct, auto) 
@@ -291,7 +291,7 @@
   by (blast elim: rtranclE converse_rtranclE
     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
 
-lemma rtrancl_unfold: "r^* = Id Un r O r^*"
+lemma rtrancl_unfold: "r^* = Id Un r^* O r"
   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
 
 lemma rtrancl_Un_separatorE:
@@ -384,7 +384,7 @@
   | (step) c where "(a, c) : r^+" and "(c, b) : r"
   using assms by cases simp_all
 
-lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
+lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
   apply (rule subsetI)
   apply (rule_tac p = x in PairE)
   apply clarify
@@ -392,7 +392,7 @@
    apply auto
   done
 
-lemma trancl_unfold: "r^+ = r Un r O r^+"
+lemma trancl_unfold: "r^+ = r Un r^+ O r"
   by (auto intro: trancl_into_trancl elim: tranclE)
 
 text {* Transitivity of @{term "r^+"} *}
@@ -676,7 +676,7 @@
 
 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     "relpow 0 R = Id"
-  | "relpow (Suc n) R = R O (R ^^ n)"
+  | "relpow (Suc n) R = (R ^^ n) O R"
 
 end
 
@@ -734,11 +734,11 @@
   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   done
 
-lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
+lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
 by(induct n) auto
 
 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
-  by (induct n) (simp, simp add: O_assoc [symmetric])
+by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"
diff -r 6c394343360f -r a60f183eb63e src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -117,7 +117,7 @@
 (*Lemma proving transitivity and more*)
 lemma genPrefix_trans_O [rule_format]: 
      "(x, y) : genPrefix r  
-      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
+      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
 apply (erule genPrefix.induct)
   prefer 3 apply (blast dest: append_genPrefix)
  prefer 2 apply (blast intro: genPrefix.prepend, blast)
@@ -134,13 +134,15 @@
 lemma prefix_genPrefix_trans [rule_format]: 
      "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
 apply (unfold prefix_def)
-apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
+apply (drule genPrefix_trans_O, assumption)
+apply simp
 done
 
 lemma genPrefix_prefix_trans [rule_format]: 
      "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
 apply (unfold prefix_def)
-apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
+apply (drule genPrefix_trans_O, assumption)
+apply simp
 done
 
 lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"
diff -r 6c394343360f -r a60f183eb63e src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Jul 27 23:17:40 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Jul 27 23:43:35 2009 +0200
@@ -239,7 +239,7 @@
 
 lemma wf_union_compatible:
   assumes "wf R" "wf S"
-  assumes "S O R \<subseteq> R"
+  assumes "R O S \<subseteq> R"
   shows "wf (R \<union> S)"
 proof (rule wfI_min)
   fix x :: 'a and Q 
@@ -258,8 +258,8 @@
       assume "y \<in> Q"
       with `y \<notin> ?Q'` 
       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
-      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
-      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
+      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
+      with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
       with `z \<in> ?Q'` have "w \<notin> Q" by blast 
       with `w \<in> Q` show False by contradiction
     qed
@@ -312,7 +312,7 @@
   by (auto simp: Un_ac)
 
 lemma wf_union_merge: 
-  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
+  "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B")
 proof
   assume "wf ?A"
   with wf_trancl have wfT: "wf (?A^+)" .
@@ -331,7 +331,7 @@
     obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
       by (erule wfE_min)
     then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
-      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
+      and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
       and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
       by auto
     
@@ -353,7 +353,7 @@
           with A1 show "y \<notin> Q" .
         next
           assume "(y, z') \<in> S" 
-          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
+          then have "(y, z) \<in> S O R" using  `(z', z) \<in> R` ..
           with A2 show "y \<notin> Q" .
         qed
       qed