(*
Title:  Allen's qualitative temporal calculus
Author:  Fadoua Ghourabi (fadouaghourabi@gmail.com)
Affiliation: Ochanomizu University, Japan
*)

section ‹Time interval relations›


theory allen

imports

  Main axioms 
  "HOL-Eisbach.Eisbach_Tools"


begin

section ‹Basic relations›

text‹We define 7 binary relations between time intervals.
  e, m, b, ov, d, s and f stand for equal, meets, before, overlaps, during, starts and finishes, respectively.›

class arelations = interval + 
 fixes 
  e::"('a×'a) set" and
  m::"('a×'a) set" and 
  b::"('a×'a) set" and
  ov::"('a×'a) set" and
  d::"('a×'a) set" and
  s::"('a×'a) set" and
  f::"('a×'a) set"  
assumes
  e:"(p,q) ∈ e = (p = q)" and
  m:"(p,q) ∈ m = p∥q" and
  b:"(p,q) ∈ b = (∃t::'a. p∥t ∧ t∥q)" and
  ov:"(p,q) ∈ ov = (∃k l u v t::'a.
                   (k∥p ∧ p∥u ∧ u∥v) ∧ (k∥l ∧ l∥q ∧ q∥v) ∧ (l∥t ∧ t∥u))" and
  s:"(p,q) ∈ s = (∃k u v::'a. k∥p ∧ p∥u ∧ u∥v ∧ k∥q ∧ q∥v)" and
  f:"(p,q) ∈ f = (∃k l u ::'a. k∥l ∧ l∥p ∧ p∥u ∧ k∥q ∧ q∥u)" and
  d:"(p,q) ∈ d = (∃k l u v::'a. k∥l ∧ l∥p ∧ p∥u ∧u∥v ∧ k∥q ∧ q∥v)" 
 

(** e compositions **)
subsection ‹e-composition›
text ‹Relation e is the identity relation for composition.›

lemma cer:
assumes  "r ∈ {e,m,b,ov,s,f,d,m^-1,b^-1,ov^-1,s^-1,f^-1,d^-1}" 
shows "e O r = r"
proof -
  { fix x y assume a:"(x,y) ∈ e O r" 
    then obtain z where "(x,z) ∈ e" and "(z,y) ∈ r" by auto
    from ‹(x,z) ∈ e› have "x = z" using e by auto
    with ‹(z,y)∈ r› have "(x,y) ∈ r" by simp} note c1 = this
  
 { fix x y assume a:"(x,y) ∈ r"
   have "(x,x) ∈ e" using e by auto
   with a have "(x,y) ∈ e O r" by blast} note c2 = this
 
 from c1 c2 show ?thesis by auto
qed

lemma cre:
assumes  "r ∈ {e,m,b,ov,s,f,d,m^-1,b^-1,ov^-1,s^-1,f^-1,d^-1}"
shows " r O e = r"
proof -
  { fix x y assume a:"(x,y) ∈ r O e" 
    then obtain z where "(x,z) ∈ r" and "(z,y) ∈ e" by auto
    from ‹(z,y) ∈ e› have "z = y" using e by auto
    with ‹(x,z)∈ r› have "(x,y) ∈ r" by simp} note c1 = this
  
 { fix x y assume a:"(x,y) ∈ r"
   have "(y,y) ∈ e" using e by auto
   with a have "(x,y) ∈ r O e" by blast} note c2 = this
 
 from c1 c2 show ?thesis by auto
qed

lemmas ceb = cer[of b]
lemmas cebi = cer[of "b^-1"]
lemmas cem = cer[of m]
lemmas cemi = cer[of "m^-1"]
lemmas cee = cer[of e]
lemmas ces = cer[of s]
lemmas cesi = cer[of "s^-1"]
lemmas cef = cer[of f]
lemmas cefi = cer[of "f^-1"]
lemmas ceov = cer[of ov]
lemmas ceovi = cer[of "ov^-1"]
lemmas ced = cer[of d]
lemmas cedi = cer[of "d^-1"]
lemmas cbe = cre[of b]
lemmas cbie = cre[of "b^-1"]
lemmas cme = cre[of m]
lemmas cmie = cre[of "m^-1"]
lemmas cse = cre[of s]
lemmas csie = cre[of "s^-1"]
lemmas cfe = cre[of f]
lemmas cfie = cre[of "f^-1"]
lemmas cove = cre[of ov]
lemmas covie = cre[of "ov^-1"]
lemmas cde = cre[of d]
lemmas cdie = cre[of "d^-1"]

(*******)

(* composition with single relation *)
subsection ‹r-composition›
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq r$, where $r$ is a basic relation.›

method (in arelations) r_compose uses r1 r2 r3 = ((auto, (subst (asm) r1 ), (subst (asm) r2), (subst r3)) ,  (meson M5exist_var))


lemma (in arelations) cbb:"b O b ⊆ b"
  by (r_compose r1:b r2:b r3:b)

lemma  (in arelations)  cbm:"b O m ⊆ b"
  by (r_compose r1:b r2:m r3:b)

lemma cbov:"b O ov ⊆ b"
  apply (auto simp:b ov)
  using M1 M5exist_var by blast

lemma cbfi:"b O f^-1 ⊆ b"
  apply (auto simp:b f)
  by (meson M1 M5exist_var)

lemma cbdi:"b O d^-1 ⊆ b"
  apply (auto simp: b d)
  by (meson M1 M5exist_var)
 
lemma cbs:"b O s ⊆ b"
  apply (auto simp: b s)
  by (meson M1 M5exist_var)

lemma cbsi:"b O s^-1 ⊆ b"
  apply (auto simp: b s)
  by (meson M1 M5exist_var)

lemma (in arelations) cmb:"m O b ⊆ b"
  by (r_compose r1:m r2:b r3:b)

lemma cmm:"m O m ⊆ b"
  by (auto simp: b m)

lemma cmov:"m O ov ⊆ b"
  apply (auto simp:b m ov)
  using M1 M5exist_var by blast

lemma cmfi:"m O f^-1 ⊆ b"
  apply (r_compose r1:m r2:f r3:b)
  by (meson M1)

lemma cmdi:"m O d^-1 ⊆ b"
  apply (auto simp add:m d b)
  using M1 by blast

lemma cms:"m O s ⊆ m"
  apply (auto simp add:m s)
  using M1 by auto

lemma cmsi:"m O s^-1 ⊆ m"
  apply (auto simp add:m s)
  using M1 by blast

lemma covb:"ov O b ⊆ b"
  apply (auto simp:ov b)
  using M1 M5exist_var by blast

lemma covm:"ov O m ⊆ b"
  apply (auto simp:ov m b)
  using M1 by blast

lemma covs:"ov O s ⊆ ov" 
proof
  fix p::"'a×'a" assume "p ∈ ov O s" then obtain x y z where p:"p = (x,z)" and xyov:"(x,y)∈ ov" and yzs:"(y,z) ∈ s" by auto
  from xyov obtain r u v t k where rx:"r∥x" and xu:"x∥u" and uv:"u∥v" and rt:"r∥t" and tk:"t∥k" and ty:"t∥y" and yv:"y∥v" and ku:"k∥u" using ov by blast
  from yzs obtain l1 l2 where yl1:"y∥l1" and l1l2:"l1∥l2" and zl2:"z∥l2" using s by blast
  from uv yl1 yv have "u∥l1" using M1 by blast
  with xu l1l2 obtain ul1 where xul1:"x∥ul1" and ul1l2:"ul1∥l2" using M5exist_var by blast
  from ku xu xul1 l1l2 have kul1:"k∥ul1" using M1 by blast
  from ty yzs have "t∥z" using s M1 by blast
  with rx rt xul1 ul1l2 zl2 tk kul1 have "(x,z) ∈ ov" using ov by blast
  with p show "p ∈ ov" by simp
qed

lemma cfib:"f^-1 O b ⊆ b" 
  apply (auto simp:f b)
  using M1 by blast

lemma cfim:"f^-1 O m ⊆ m"
  apply (auto simp:f m)
  using M1 by auto

lemma cfiov:"f^-1 O ov ⊆ ov" 
proof 
    fix p::"'a×'a" assume "p ∈ f^-1 O ov" then obtain x y z where p:"p = (x,z)" and xyfi:"(x,y)∈ f^-1" and yzov:"(y,z) ∈ ov" by auto
    from xyfi yzov obtain t' r u   where tpr:"t'∥r" and ry:"r∥y" and yu:"y∥u" and tpx:"t'∥x" and xu:"x∥u"  using f  by blast
    from yzov  ry  obtain v k t u' where yup:"y∥u'" and upv:"u'∥v" and rk:"r∥k" and kz:"k∥z" and zv:"z∥v" and kt:"k∥t" and tup:"t∥u'" 
    using ov using M1 by blast
    from yu xu yup have xup:"x∥u'" using M1 by blast
    from tpr rk kt obtain r' where tprp:"t'∥r'" and rpt:"r'∥t" using M5exist_var by blast
    from kt rpt kz have rpz:"r'∥z" using M1 by blast
    from tprp rpz rpt tpx xup zv upv tup have "(x,z) ∈ ov" using ov by blast
    with p show "p ∈ ov" by simp
qed

lemma cfifi:"f^-1 O f^-1 ⊆ f^-1"
proof
  fix x::"'a×'a" assume "x ∈ f^-1 O f^-1" then obtain p q z where x:"x = (p, q)" and "(p,z) ∈ f^-1" and "(z,q) ∈ f^-1" by auto
  from ‹(p,z) ∈ f^-1› obtain k l u  where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and pu:"p∥u" and zu:"z∥u"  using f  by blast
  from ‹(z,q) ∈ f^-1› obtain k' u' l' where kpz:"k'∥z" and kplp:"k'∥l'" and lpq:"l'∥q" and qup:"q∥u'" and zup:"z∥u'"  using f  by blast
  from zu zup pu have "p∥u'" using M1 by blast
  from lz kpz kplp have "l∥l'" using M1 by blast
  with kl lpq obtain ll where "k∥ll" and "ll∥q" using M5exist_var by blast
  with kp ‹p∥u'› qup show "x ∈ f^-1" using x f by blast
qed

lemma cfidi:"f^-1 O d^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x : f^-1 O d^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ f^-1" and "(z,q) ∈ d^-1" by auto
  then obtain k l u where kp:"k ∥ p" and kl:"k∥l" and lz:"l∥z" and pu:"p ∥u" and  zu:"z∥u" using f  by blast
  obtain k' l' u' v' where kpz:"k' ∥z" and kplp:"k' ∥l'" and lpq:"l' ∥q" and  qup:"q ∥u'" and  upvp:"u'∥v'" and zvp:"z∥v'" using d ‹(z,q)∈d^-1› by blast
  from lz kpz kplp have "l∥l'" using M1 by blast
  with kl lpq obtain ll where "k∥ll" and "ll∥q" using M5exist_var by blast
  moreover from zu zvp upvp have "u' ∥ u " using M1 by blast
  ultimately show "x ∈ d^-1" using x kp pu qup d  by blast
qed

lemma cfis:"f^-1 O s ⊆ ov"
proof
   fix x::"'a×'a" assume "x ∈ f^-1 O s" then obtain p q z where x:"x = (p,q)" and "(p,z)∈ f^-1" and "(z,q) ∈ s" by auto
   from ‹(p,z)∈ f^-1› obtain k l u where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and pu:"p∥u" and zu:"z∥u" using f by blast
   from ‹(z,q)∈ s› obtain k' u' v' where kpz:"k'∥z" and kpq:"k'∥q" and zup:"z∥u'" and upvp:"u'∥v'" and qvp:"q∥v'" using s M1 by blast
   from pu zu zup have pup:"p∥u'" using M1 by blast
   moreover from lz kpz kpq have lq:"l∥q" using M1 by blast
   ultimately show "x ∈ ov" using x lz zup kp kl upvp upvp ov qvp by blast
qed

lemma cfisi:"f^-1 O s^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ f^-1 O s^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ f^-1" and "(z,q) ∈ s^-1" by auto
  then obtain k l u where kp:"k ∥ p" and kl:"k∥l" and lz:"l∥z"  and pu:"p ∥u" and  zu:"z∥u" using f  by blast
  obtain k' u' v' where kpz:"k' ∥z" and kpq:"k' ∥q" and qup:"q ∥u'" and  upvp:"u'∥v'" and  zvp:"z∥v'" using s ‹(z,q): s^-1› by blast
  from zu zvp upvp have "u'∥u" using M1 by blast
  moreover from lz kpz kpq have "l ∥q " using M1 by blast
  ultimately show "x ∈ d^-1" using x d kl kp qup  pu  by blast
qed

lemma cdifi:"d^-1 O f^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x : d^-1 O f^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z,q) ∈ f^-1" by auto
  then obtain k l u v  where kp:"k ∥ p" and kl:"k∥l" and lz:"l∥z" and zu:"z ∥u" and uv:"u∥v" and pv:"p∥v" using d  by blast
  obtain k' l' u' where kpz:"k' ∥z" and kplp:"k' ∥l'" and lpq:"l' ∥q" and  qup:"q ∥u'" and zup:"z∥u'" using f ‹(z,q): f^-1› by blast
  from lz kpz kplp  have "l∥l'" using M1 by blast
  with kl lpq obtain ll where "k∥ll" and "ll∥q" using M5exist_var by blast
  moreover from zu qup zup have "q ∥ u " using M1 by blast
  ultimately show "x ∈ d^-1" using x d kp uv pv  by blast
qed

lemma cdidi:"d^-1 O d^-1 ⊆ d^-1" 
proof
  fix x::"'a×'a" assume "x : d^-1 O d^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z,q) ∈ d^-1" by auto
  then obtain k l u v where kp:"k ∥ p" and kl:"k∥l" and lz:"l∥z" and zu:"z ∥u" and uv:"u∥v" and pv:"p∥v" using d  by blast
  obtain k' l' u' v' where kpz:"k' ∥z" and kplp:"k' ∥l'" and lpq:"l' ∥q" and  qup:"q ∥u'" and upvp:"u' ∥v'" and zvp:"z ∥v'" using d ‹(z,q): d^-1› by blast
  from lz kpz kplp  have "l∥l'" using M1 by blast
  with kl lpq obtain ll where "k∥ll" and "ll∥q" using M5exist_var by blast
  moreover from zvp zu upvp have "u' ∥ u " using M1 by blast
  moreover with qup uv obtain uu where "q∥uu" and "uu∥v" using M5exist_var  by blast
  ultimately show "x ∈ d^-1" using x d kp pv   by blast
qed

lemma cdisi:"d^-1 O s^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x : d^-1 O s^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z,q) ∈ s^-1" by auto
  then obtain k l  u v where kp:"k ∥p" and kl:"k∥l"  and lz:"l∥z" and zu:"z∥u" and uv:"u∥v" and pv:"p∥v" using d by blast
  obtain k' u' v' where kpz:"k' ∥z" and kpq:"k' ∥q" and  qup:"q ∥u'" and upvp:"u' ∥v'" and zvp:"z ∥v'" using s ‹(z,q): s^-1› by blast
  from upvp zvp zu have "u'∥u" using M1 by blast
  with qup uv obtain uu where "q∥uu" and "uu∥v" using M5exist_var by blast
  moreover from kpz lz kpq have "l ∥q " using M1 by blast
  ultimately show "x ∈ d^-1" using x d kp kl pv  by blast
qed

lemma csb:"s O b ⊆ b"
apply (auto simp:s b)
using M1 M5exist_var by blast

lemma csm:"s O m ⊆ b"
apply (auto simp:s m b)
using M1 by blast

lemma css:"s O s ⊆ s"
proof
  fix x::"'a×'a" assume "x ∈ s O s" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s" and "(z,q) ∈ s" by auto
  from ‹(p,z) ∈ s› obtain k u v where kp:"k∥p" and kz:"k∥z" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v" using s by blast
  from ‹(z,q) ∈ s› obtain k' u' v' where kpq:"k'∥q" and kpz:"k'∥z" and zup:"z∥u'" and upvp:"u'∥v'" and qvp:"q∥v'" using s by blast
  from kp kpz kz have "k'∥p" using M1 by blast
  moreover from uv zup zv have "u∥u'" using M1 by blast
  moreover with pu upvp obtain uu where "p∥uu" and "uu∥v'" using M5exist_var by blast
  ultimately show "x ∈ s" using x s kpq qvp  by blast
qed

lemma csifi:"s^-1 O f^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x : s^-1 O f^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s^-1" and "(z,q) ∈ f^-1" by auto
  then obtain k u v where kp:"k ∥ p" and kz:"k∥z" and zu:"z ∥u" and uv:"u∥v" and pv:"p∥v" using s  by blast
  obtain k' l' u' where kpz:"k' ∥z" and kplp:"k' ∥l'" and lpq:"l' ∥q"  and zup:"z∥u'" and qup:"q∥u'" using f ‹(z,q): f^-1› by blast
  from kz kpz kplp have "k∥l'" using M1 by blast
  moreover from qup zup zu have "q ∥ u " using M1 by blast
  ultimately show "x ∈ d^-1" using x d kp lpq pv uv by blast
qed

lemma csidi:"s^-1 O d^-1 ⊆ d^-1"
proof
  fix x::"'a×'a" assume "x : s^-1 O d^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s^-1" and "(z,q) ∈ d^-1" by auto
  then obtain k u v where kp:"k ∥ p" and kz:"k∥z"  and zu:"z ∥u" and uv:"u∥v" and pv:"p∥v" using s  by blast
  obtain k' l' u' v' where kpz:"k' ∥z" and kplp:"k' ∥l'" and lpq:"l'∥q" and qup:"q ∥u'" and upvp:"u' ∥v'" and zvp:"z∥v'" using d ‹(z,q): d^-1› by blast
  from zvp upvp zu have "u'∥u" using M1 by blast
  with qup uv obtain uu where "q∥uu" and "uu∥v" using M5exist_var by blast
  moreover from kz kpz kplp have "k ∥l' " using M1 by blast
  ultimately show "x ∈ d^-1" using x d kp lpq pv  by blast
qed

lemma cdb:"d O b ⊆ b"
apply (auto simp:d b)
using M1 M5exist_var by blast

lemma cdm:"d O m ⊆ b"
apply (auto simp:d m b)
using M1 by blast

lemma cfb:"f O b ⊆ b"
apply (auto simp:f b)
using M1 by blast

lemma cfm:"f O m ⊆ m"
proof 
  fix x::"'a×'a" assume "x ∈ f O m" then obtain p q z where x:"x = (p,q)" and 1:"(p,z) ∈ f" and 2:"(z,q) ∈ m" by auto
  from 1 obtain u where pu:"p∥u" and zu:"z∥u" using f by auto
  with 2   have "(p,q) ∈ m" using M1 m by blast
  thus "x∈ m" using x by auto
qed


(* ========= $\alpah_1$ compositions ============ *)
subsection ‹$\alpha$-composition›
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq s \cup ov \cup d$.›


lemma (in arelations) cmd:"m O d ⊆ s ∪ ov ∪ d"
proof 
  fix x::"'a×'a" assume a:"x ∈ m O d" then obtain p q z where x:"x =(p,q)" and 1:"(p,z) ∈ m" and 2:"(z,q) ∈ d" by auto
  then obtain k l u v  where pz:"p∥z" and kq:"k∥q" and kl:"k∥l" and lz:"l∥z" and zu:"z∥u" and uv:"u∥v" and qv:"q∥v" using m d by blast
  obtain k' where kpp:"k'∥p" using M3 meets_wd pz by blast
  from pz zu uv obtain zu where pzu:"p∥zu" and zuv:"zu∥v" using M5exist_var  by blast
  from kpp kq have "k'∥q ⊕ ((∃t. k'∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast 
  then have "(?A∧¬?B∧¬?C)∨(¬?A∧?B∧¬?C)∨(¬?A∧¬?B∧?C)"  using local.meets_atrans xor_distr_L[of ?A ?B ?C]  by blast
  thus "x ∈ s ∪ ov ∪ d"    
  proof (elim disjE)
    {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp 
     then have "(p,q) ∈ s" using  s qv kpp pzu zuv by blast
     thus ?thesis using x by simp }
    next
    {assume "(¬?A∧?B∧¬?C)" then have "?B" by simp
     then obtain t where kpt:"k'∥t" and tq:"t∥q" by auto
     moreover from kq kl tq have "t∥l" using M1 by blast
     moreover from lz pz pzu have "l∥zu" using M1 by blast
     ultimately have "(p,q) ∈ ov" using ov kpp qv pzu zuv by blast
     thus ?thesis using x by simp}
    next
    {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
     then obtain t where kt:"k∥t" and tp:"t∥p" by auto
     with kq pzu zuv qv  have "(p,q)∈d" using d by blast
     thus ?thesis using x by simp}
  qed
qed

lemma (in arelations) cmf:"m O f ⊆ s ∪ ov ∪ d"
proof
  fix x::"'a×'a" assume a:"x ∈ m O f" then obtain p q z where x:"x =(p,q)" and 1:"(p,z) ∈ m" and 2:"(z,q) ∈ f" by auto
  then obtain k l u   where pz:"p∥z" and kq:"k∥q" and kl:"k∥l" and lz:"l∥z" and zu:"z∥u" and qu:"q∥u" using m f by blast
  obtain k' where kpp:"k'∥p" using M3 meets_wd pz by blast
  from kpp kq have "k'∥q ⊕ ((∃t. k'∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast 
  then have "(?A∧¬?B∧¬?C)∨(¬?A∧?B∧¬?C)∨(¬?A∧¬?B∧?C)" using local.meets_atrans xor_distr_L[of ?A ?B ?C]  by blast
  thus "x ∈ s ∪ ov ∪ d"    
  proof (elim disjE)
    {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp 
     then have "(p,q) ∈ s" using  s qu kpp pz zu by blast
     thus ?thesis using x by simp }
    next
    {assume "(¬?A∧?B∧¬?C)" then have "?B" by simp
     then obtain t where kpt:"k'∥t" and tq:"t∥q" by auto
     moreover from kq kl tq have "t∥l" using M1 by blast 
     moreover from lz pz pz have "l∥z" using M1 by blast
     ultimately have "(p,q) ∈ ov" using ov kpp qu pz zu by blast
     thus ?thesis using x by simp}
    next
    {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
     then obtain t where kt:"k∥t" and tp:"t∥p" by auto
     with kq pz zu qu  have "(p,q)∈d" using d by blast
     thus ?thesis using x by simp}
  qed
qed

lemma cmovi:"m O ov^-1 ⊆ s ∪ ov ∪ d"
proof 
  fix x::"'a×'a" assume a:"x ∈ m O ov^-1" then obtain p q z where x:"x =(p,q)" and 1:"(p,z) ∈ m" and 2:"(z,q) ∈ ov^-1" by auto
  then obtain k l c u v  where pz:"p∥z" and kq:"k∥q" and kl:"k∥l" and lz:"l∥z" and qu:"q∥u" and uv:"u∥v" and zv:"z∥v" and lc:"l∥c" and cu:"c∥u" using m ov by blast
  obtain k' where kpp:"k'∥p" using M3 meets_wd pz by blast
  from lz lc pz have pc:"p∥c" using M1 by auto
  from kpp kq have "k'∥q ⊕ ((∃t. k'∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast 
  then have "(?A∧¬?B∧¬?C)∨(¬?A∧?B∧¬?C)∨(¬?A∧¬?B∧?C)" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ s ∪ ov ∪ d"    
  proof (elim disjE)
    {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp 
     then have "(p,q) ∈ s" using s kpp qu cu pc by blast
     thus ?thesis using x by simp }
    next
    {assume "(¬?A∧?B∧¬?C)" then have "?B" by simp
     then obtain t where kpt:"k'∥t" and tq:"t∥q" by auto
     moreover from kq kl tq have "t∥l" using M1 by auto
     ultimately have "(p,q) ∈ ov" using ov kpp qu cu lc pc by blast
     thus ?thesis using x by simp}
    next
    {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
     then obtain t where kt:"k∥t" and tp:"t∥p" by auto
     then  have "(p,q)∈d" using d kq cu qu pc by blast
     thus ?thesis using x by simp}
  qed
qed

lemma covd:"ov O d ⊆ s ∪ ov ∪ d"
proof
  fix x::"'a×'a" assume "x ∈ ov O d" then obtain p q z where x:"x=(p,q)" and "(p,z) ∈ ov" and "(z,q) ∈ d" by auto
  from ‹(p,z) ∈ ov› obtain k u v l c where kp:"k∥p" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v" and lc:"l∥c" and cu:"c∥u" and kl:"k∥l" and lz:"l∥z" and cu:"c∥u" using ov by blast
  from ‹(z,q) ∈ d› obtain k' l' u' v' where kpq:"k'∥q" and kplp:"k'∥l'" and lpz:"l'∥z" and qvp:"q∥v'" and zup:"z∥u'" and upvp:"u'∥v'" using d by blast
  from uv zv zup have "u∥u'" using M1 by auto
  from pu upvp obtain uu where puu:"p∥uu" and uuvp:"uu∥v'" using ‹u∥u'› using M5exist_var by blast
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ s ∪ ov ∪ d"
  proof (elim disjE)
    { assume "?A∧¬?B∧¬?C" then have ?A by simp
      then have "(p,q) ∈ s" using s kp qvp puu uuvp by blast
      thus ?thesis using x by blast}
    next
    { assume "¬?A∧?B∧¬?C" then have ?B by simp
      then obtain t where kt:"k∥t" and tq:"t∥q" by auto
      from cu pu puu have "c∥uu" using M1 by auto
      moreover from kpq tq kplp have "t∥l'" using M1 by auto
      moreover from lpz lz lc have lpc:"l'∥c" using M1 by auto
      ultimately obtain lc where "t∥lc" and "lc∥uu" using M5exist_var by blast
      then have "(p,q) ∈ ov" using ov kp kt tq puu uuvp qvp  by blast
      thus ?thesis using x by auto}
    next
    { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
      then obtain t where "k'∥t" and "t∥p" by auto
      with puu uuvp qvp kpq have "(p,q) ∈ d" using d by blast
      thus ?thesis using x by auto}
  qed
qed


lemma covf:"ov O f ⊆ s ∪ ov ∪ d"
proof
  fix x::"'a×'a" assume "x ∈ ov O f" then obtain p q z where x:"x=(p,q)" and "(p,z) ∈ ov" and "(z,q) ∈ f" by auto
  from ‹(p,z) ∈ ov› obtain k u v l c where kp:"k∥p" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v" and lc:"l∥c" and cu:"c∥u" and kl:"k∥l" and lz:"l∥z" and cu:"c∥u" using ov by blast
  from ‹(z,q) ∈ f› obtain k' l' u'  where kpq:"k'∥q" and kplp:"k'∥l'" and lpz:"l'∥z" and qup:"q∥u'" and zup:"z∥u'" using f by blast
  from uv zv zup have uu:"u∥u'" using M1 by auto
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ s ∪ ov ∪ d"
  proof (elim disjE)
    { assume "?A∧¬?B∧¬?C" then have ?A by simp
      then have "(p,q) ∈ s" using s kp qup uu pu by blast
      thus ?thesis using x by blast}
    next
    { assume "¬?A∧?B∧¬?C" then have ?B by simp
      then obtain t where kt:"k∥t" and tq:"t∥q" by auto
      moreover from kpq tq kplp have "t∥l'" using M1 by auto
      moreover from lpz lz lc have lpc:"l'∥c" using M1 by auto
      ultimately obtain lc where "t∥lc" and "lc∥u" using cu M5exist_var by blast
      then have "(p,q) ∈ ov" using ov kp kt tq pu uu qup  by blast
      thus ?thesis using x by auto}
    next
    { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
      then obtain t where "k'∥t" and "t∥p" by auto
      with pu uu qup kpq have "(p,q) ∈ d" using d by blast
      thus ?thesis using x by auto}
  qed
qed

lemma cfid:"f^-1 O d ⊆ s ∪ ov ∪ d"
proof
  fix x::"'a×'a" assume "x ∈ f^-1 O d" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ f^-1" and "(z,q)∈ d" by auto
  from ‹(p,z) ∈ f^-1› obtain k l u where "k∥l" and "l∥z" and kp:"k∥p" and pu:"p∥u" and zu:"z∥u" using f by blast
  from ‹(z,q) ∈ d› obtain k' l' u' v where kplp:"k'∥l'" and kpq:"k'∥q" and lpz:"l'∥z" and zup:"z∥u'" and upv:"u'∥v" and qv:"q∥v" using d by blast
  from pu zu zup have pup:"p∥u'" using M1 by blast
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ s ∪ ov ∪ d"
  proof (elim disjE)
    { assume "?A∧¬?B∧¬?C" then have ?A by simp
      with pup upv kp qv have "(p,q) ∈ s" using s by blast
      thus ?thesis using x by auto}
    next
    { assume "¬?A∧?B∧¬?C" then have ?B by simp
      then obtain t where kt:"k∥t" and tq:"t∥q" by auto
      from tq kpq kplp have "t∥l'" using M1 by blast
      with lpz zup obtain lpz where "t∥lpz" and "lpz∥u'" using M5exist_var by blast
      with kp pup upv kt tq qv have "(p,q)∈ov" using ov by blast
      thus ?thesis using x by blast}
       next
    { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
      then obtain t where "k'∥t" and "t∥p" by auto
      with pup upv kpq qv have "(p,q) ∈ d" using d by blast
      thus ?thesis using x by auto}
    qed
qed

lemma cfov:"f O ov ⊆ ov ∪ s ∪ d"
proof
    fix x::"'a×'a" assume "x ∈ f O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ f" and "(z,q)∈ ov" by auto
    from ‹(p,z) ∈ f› obtain  k l u where "k∥l" and kz:"k∥z" and lp:"l∥p" and pu:"p∥u" and zu:"z∥u" using f by blast
    from ‹(z,q) ∈ ov› obtain k' l' c  u' v where "k'∥l'" and kpz:"k'∥z" and lpq:"l'∥ q" and  zup:"z∥u'" and upv:"u'∥v" and qv:"q∥v" and lpc:"l'∥c" and cup:"c∥u'"  using  ov by blast
    from pu zu zup have pup:"p∥u'" using M1 by blast
    from lp lpq have "l∥q ⊕ ((∃t. l∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ ov ∪ s ∪ d"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with  lp pup upv qv have "(p,q) ∈ s" using s by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
      then obtain t where lt:"l∥t" and tq:"t∥q" by auto
      from tq lpq lpc have "t∥c" using M1 by blast
      with lp lt tq pup upv qv cup have "(p,q)∈ov" using ov by blast
      thus ?thesis using x by blast}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
      then obtain t where "l'∥t" and "t∥p" by auto
      with lpq pup upv qv have "(p,q) ∈ d" using d by blast
      thus ?thesis using x by auto}
    qed
qed

(* ========= $\alpha_2$ composition ========== *)
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq ov \cup f^{-1} \cup d^{-1}$.›

lemma covsi:"ov O s^-1 ⊆ ov ∪ f^-1 ∪ d^-1"
proof
    fix x::"'a×'a" assume "x ∈ ov O s^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov" and "(z,q) ∈ s^-1" by auto
    from ‹(p,z) ∈ ov› obtain k l c u  where kp:"k∥p" and pu:"p∥u" and kl:"k∥l" and lz:"l∥z" and lc:"l∥c" and cu:"c∥u" using ov by blast
    from ‹(z,q) ∈ s^-1› obtain k' u' v' where kpz:"k'∥z" and kpq:"k'∥q" and kpz:"k'∥z" and  zup:"z∥u'"  and qvp:"q∥v'" using s by blast
    from lz kpz kpq have lq:"l∥q" using M1 by blast
    from pu qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qvp kp kl lq have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where ptp:"p∥t" and "t∥v'" by auto
        moreover with pu cu have "c∥t" using M1 by blast
        ultimately have "(p,q)∈ ov" using kp kl lc cu lq qvp  ov by blast
        thus ?thesis using x by auto}        
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where qt:"q∥t" and "t∥u" by auto
        with kp kl lq pu  have "(p,q) ∈ d^-1" using d by blast 
        thus ?thesis using x by auto}
      qed
qed


lemma cdim:"d^-1 O m ⊆ ov ∪ d^-1 ∪ f^-1"
proof 
    fix x::"'a×'a" assume "x ∈ d^-1 O m" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z,q) ∈ m" by auto
    from ‹(p,z) ∈ d^-1› obtain k l u v where kp:"k∥p" and pv:"p∥v" and kl:"k∥l" and lz:"l∥z" and zu:"z∥u" and uv:"u∥v" using d by blast
    from ‹(z,q) ∈ m›  have zq:"z∥q" using m by blast
    obtain v' where qvp:"q∥v'" using M3 meets_wd zq by blast
    from kl lz zq obtain lz where klz:"k∥lz" and lzq:"lz∥q" using M5exist_var  by blast
    from pv qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ ov ∪ d^-1 ∪ f^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qvp kp klz lzq‹?A› have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from zq lzq zu have "lz∥u" using M1 by auto
        moreover from pt pv uv have "u∥t" using M1 by auto
        ultimately have "(p,q)∈ ov" using kp klz lzq pt tvp qvp ov by blast
        thus ?thesis using x by auto}        
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where qt:"q∥t" and "t∥v" by auto
        with kp klz lzq pv have "(p,q) ∈ d^-1" using d by blast 
        thus ?thesis using x by auto}
      qed
qed

lemma cdiov:"d^-1 O ov ⊆ ov ∪ f^-1 ∪ d^-1"
proof
    fix x::"'a×'a" assume "x ∈ d^-1 O ov" then obtain p q r where x:"x = (p,r)" and "(p,q) ∈ d^-1" and "(q,r) ∈ ov" by auto
    from ‹(p,q) ∈ d^-1› obtain u v k l  where kp:"k∥p" and pv:"p∥v" and kl:"k∥l" and lq:"l∥q"  and qu:"q∥u" and uv:"u∥v" using d by blast
    from ‹(q,r) ∈ ov› obtain k' l' t u' v' where lpr:"l'∥r" and kpq:"k'∥q" and kplp:"k'∥l'" and qup:"q∥u'" and "u'∥v'" and rvp:"r∥v'" and lpt:"l'∥t" and tup:"t∥u'" using ov by blast
    from lq kplp kpq have "l∥l'" using M1 by blast
    with kl lpr  obtain ll where  kll:"k∥ll" and llr:"ll∥r"  using M5exist_var by blast
    from pv rvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. r∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with rvp llr kp kll have "(p,r) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t' where ptp:"p∥t'" and tpvp:"t'∥v'" by auto
        moreover from lpt lpr llr have llt:"ll∥t" using M1 by blast
        moreover from ptp uv pv have utp:"u∥t'" using M1 by blast
        moreover from qu tup qup have "t∥u" using M1 by blast
        moreover with utp llt obtain tu where "ll∥tu" and "tu∥t'" using M5exist_var by blast
        with kp ptp tpvp kll llr rvp  have "(p,r)∈ ov" using  ov by blast
        thus ?thesis using x by auto}        
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t' where rtp:"r∥t'" and "t'∥v" by auto
        with kll llr kp pv have "(p,r) ∈ d^-1" using d by blast 
        thus ?thesis using x by auto}
      qed
qed

lemma cdis:"d^-1 O s ⊆ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ d^-1 O s" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z,q) ∈ s" by auto
  from ‹(p,z)∈d^-1› obtain k l u v where kl:"k∥l" and lz:"l∥z" and kp:"k∥p" and zu:"z∥u" and uv:"u∥v" and pv:"p∥v" using d by blast
  from ‹(z,q) ∈ s› obtain l'  v' where lpz:"l'∥z" and lpq:"l'∥q" and qvp:"q∥v'" using s by blast
  from lz lpz lpq have lq:"l∥q" using M1 by blast
  from pv qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with kl lq qvp kp have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt pv uv have "u∥t" using M1 by blast
        with lz zu obtain zu where "l∥zu" and "zu∥t" using M5exist_var by blast
        with kp pt tvp kl lq qvp have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with kl lq kp pv have "(p,q)∈d^-1" using d by blast
        thus ?thesis using x by auto}
      qed
qed

lemma csim:"s^-1 O m ⊆ ov ∪ f^-1 ∪ d^-1"
proof 
  fix x::"'a×'a" assume "x ∈ s^-1 O m" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s^-1" and "(z,q) ∈ m" by auto
  from ‹(p,z)∈s^-1› obtain k u v where kp:"k∥p" and kz:"k∥z" and zu:"z∥u" and uv:"u∥v" and pv:"p∥v" using s by blast
  from ‹(z,q) ∈ m› have zq:"z∥q" using m by auto
  obtain v' where qvp:"q∥v'" using M3 meets_wd zq by blast
  from pv qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with kp kz zq qvp have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt pv uv have "u∥t" using M1 by blast
        with kp pt tvp kz zq qvp zu  have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with kp kz zq pv have "(p,q)∈d^-1" using d by blast
        thus ?thesis using x by auto}
      qed
qed
 
lemma csiov:"s^-1 O ov ⊆ ov ∪ f^-1 ∪ d^-1"
proof 
  fix x::"'a×'a" assume "x ∈ s^-1 O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s^-1" and "(z,q) ∈ ov" by auto
  from ‹(p,z)∈s^-1› obtain k u v where kp:"k∥p" and kz:"k∥z" and zu:"z∥u" and uv:"u∥v" and pv:"p∥v" using s by blast
  from ‹(z,q) ∈ ov› obtain k' l' u' v' c where kpz:"k'∥z" and zup:"z∥u'" and upvp:"u'∥v'" and kplp:"k'∥l'" and lpq:"l'∥q" and qvp:"q∥v'" and lpc:"l'∥c" and cup:"c∥u'" using ov by blast
  from kz kpz kplp have klp:"k∥l'" using M1 by auto
  from pv qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with kp kplp lpq qvp klp have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt pv uv have "u∥t" using M1 by blast
        moreover from cup zup zu have cu:"c∥u" using M1 by auto
        ultimately obtain cu where "l'∥cu" and "cu∥t" using lpc M5exist_var by blast
        with kp pt tvp klp lpq qvp have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with kp klp lpq pv have "(p,q)∈d^-1" using d by blast
        thus ?thesis using x by auto}
      qed
qed

lemma covim:"ov^-1 O m ⊆ ov ∪ f^-1 ∪ d^-1"
proof
    fix x::"'a×'a" assume "x ∈ ov^-1 O m" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov^-1" and "(z,q) ∈ m" by auto
    from ‹(p,z) ∈ ov^-1› obtain k l c u v  where kz:"k∥z" and zu:"z∥u" and kl:"k∥l" and lp:"l∥p" and lc:"l∥c" and cu:"c∥u" and pv:"p∥v" and uv:"u∥v" using ov by blast
    from ‹(z,q) ∈ m›  have zq:"z∥q" using m by auto
    obtain v' where qvp:"q∥v'" using M3 meets_wd zq by blast
    from zu zq cu have cq:"c∥q" using M1 by blast
    from pv qvp have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ ov ∪ f^-1 ∪ d^-1"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with lp lc cq qvp have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where ptp:"p∥t" and "t∥v'" by auto
        moreover with pv uv have "u∥t" using M1 by blast
        ultimately have "(p,q)∈ ov" using lp lc cq qvp cu ov by blast
        thus ?thesis using x by auto}        
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where qt:"q∥t" and "t∥v" by auto
        with lp lc cq pv have "(p,q) ∈ d^-1" using d by blast 
        thus ?thesis using x by auto}
      qed
qed

(* =========$\alpha_3$ compositions========== *)
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq b \cup m \cup ov$.›

lemma covov:"ov O ov ⊆ b ∪ m ∪ ov"
proof
   fix x::"'a×'a" assume "x ∈ ov O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov" and "(z,q)∈ ov" by auto
   from ‹(p,z) ∈ ov› obtain k u l t v where kp:"k∥p" and pu:"p∥u" and kl:"k∥l" and lz:"l∥z" and "l∥t" and "t∥u" and uv:"u∥v" and zv:"z∥v" using ov by blast
   from  ‹(z,q) ∈ ov› obtain k' l' y u' v' where kplp:"k'∥l'" and kpz:"k'∥z" and lpq:"l'∥q" and lpy:"l'∥y" and "y∥u'" and zup:"z∥u'" and upvp:"u'∥v'" and qvp:"q∥v'" using ov by blast
   from lz kplp kpz have llp:"l∥l'" using M1 by blast
   from uv zv zup have "u∥u'" using M1 by blast
   with pu upvp obtain uu where puu:"p∥uu" and uuv:"uu∥v'" using M5exist_var by blast
   from puu lpq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. l'∥t' ∧ t'∥uu))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ b ∪ m ∪ ov"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        then have "(p,q) ∈ m" using m by auto
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then have "(p,q) ∈ b" using b by auto
        thus ?thesis using x by auto}
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t' where lptp:"l'∥t'" and "t'∥uu" by auto
        from kl llp lpq obtain ll where  kll:"k∥ll" and llq:"ll∥q" using M5exist_var by blast
        with lpq lptp  have "ll∥t'" using M1 by blast
        with kp puu uuv kll llq qvp ‹t'∥uu› have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      qed
qed

lemma covfi:"ov O f^-1 ⊆ b ∪ m ∪ ov"
proof
   fix x::"'a×'a" assume "x ∈ ov O f^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov" and "(z,q)∈ f^-1" by auto
   from ‹(p,z) ∈ ov› obtain k u l c v where kp:"k∥p" and pu:"p∥u" and kl:"k∥l" and lz:"l∥z" and "l∥c" and "c∥u" and uv:"u∥v" and zv:"z∥v" using ov by blast
   from  ‹(z,q) ∈ f^-1› obtain k' l' v'  where kplp:"k'∥l'" and kpz:"k'∥z" and lpq:"l'∥q"  and qvp:"q∥v'" and zvp:"z∥v'" using f by blast
   from lz kplp kpz have llp:"l∥l'" using M1 by blast
   from  zv qvp zvp have qv:"q∥v" using M1 by blast
   from pu lpq have "p∥q ⊕ ((∃t. p∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
    then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
    thus "x ∈ b ∪ m ∪ ov"
    proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        then have "(p,q) ∈ m" using m by auto
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then have "(p,q) ∈ b" using b by auto
        thus ?thesis using x by auto}
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where lptp:"l'∥t" and "t∥u" by auto
        from kl llp lpq obtain ll where  kll:"k∥ll" and llr:"ll∥q" using M5exist_var by blast
        with lpq lptp  have "ll∥t" using M1 by blast
        with kp pu uv kll llr qv ‹t∥u› have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      qed
qed


lemma csov:"s O ov ⊆ b ∪ m ∪ ov"
proof
   fix x::"'a×'a" assume "x ∈ s O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ s" and "(z,q)∈ ov" by auto
   from ‹(p,z) ∈ s› obtain k u v where kp:"k∥p" and kz:"k∥z" and  pu:"p∥u" and uv:"u∥v" and zv:"z∥v" using s by blast
   from  ‹(z,q) ∈ ov› obtain k' l'  u' v'   where kpz:"k'∥z"  and kplp:"k'∥l'" and lpq:"l'∥q" and zup:"z∥u'"  and qvp:"q∥v'" and upvp:"u'∥v'" using ov by blast
   from  kz kpz kplp have klp:"k∥l'" using M1 by blast
   from  uv zv zup  have uup:"u∥u'" using M1 by blast
   with pu upvp obtain uu where puu:"p∥uu" and uuvp:"uu∥v'" using M5exist_var by blast
   from pu lpq have "p∥q ⊕ ((∃t. p∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ b ∪ m ∪ ov"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        then have "(p,q) ∈ m" using m by auto
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then have "(p,q) ∈ b" using b by auto
        thus ?thesis using x by auto}
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where lpt:"l'∥t" and "t∥u" by auto
        with pu puu have "t∥uu" using M1 by blast
        with lpt kp puu uuvp klp lpq qvp  have "(p,q) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      qed
qed


lemma csfi:"s O f^-1 ⊆ b ∪ m ∪ ov"
proof
   fix x::"'a×'a" assume "x ∈ s O f^-1" then obtain p q r where x:"x = (p,r)" and "(p,q) ∈ s" and "(q,r)∈ f^-1" by auto
   from ‹(p,q) ∈ s› obtain k u v where kp:"k∥p" and kq:"k∥q" and  pu:"p∥u" and uv:"u∥v"  and qv:"q∥v"  using s by blast
   from  ‹(q,r) ∈ f^-1› obtain k' l  v'  where kpq:"k'∥q"  and kpl:"k'∥l" and lr:"l∥r"   and rvp:"r∥v'" and qvp:"q∥v'" using f by blast
   from kpq kpl kq have kl:"k∥l" using M1 by blast 
   from qvp qv uv have uvp:"u∥v'" using M1 by blast
   from pu lr have "p∥r ⊕ ((∃t'. p∥t' ∧ t'∥r) ⊕ (∃t'. l∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ b ∪ m ∪ ov"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        then have "(p,r) ∈ m" using m by auto
        thus ?thesis using x by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then have "(p,r) ∈ b" using b by auto
        thus ?thesis using x by auto}
     next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t' where ltp:"l∥t'" and "t'∥u" by auto
        with kp pu uvp kl lr rvp have "(p,r) ∈ ov" using ov by blast
        thus ?thesis using x by auto}
      qed
qed

(* =========$\alpha_4$ compositions========== *)
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq f \cup f^{-1} \cup e$.›

lemma cmmi:"m O m^-1 ⊆ f ∪ f^-1 ∪ e"
proof 
  fix x::"'a×'a" assume a:"x ∈ m O m^-1" then obtain p q z where x:"x =(p,q)" and 1:"(p,z) ∈ m" and 2:"(z,q) ∈ m^-1" by auto
  then have pz:"p∥z" and qz:"q∥z" using m by auto
  obtain k k' where kp:"k∥p" and kpq:"k'∥q" using M3 meets_wd qz pz by blast
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast 
  then have "(?A∧¬?B∧¬?C)∨(¬?A∧?B∧¬?C)∨(¬?A∧¬?B∧?C)" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈f ∪ f^-1 ∪ e"    
  proof (elim disjE)
    {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp 
     then have "p = q" using M4 kp pz qz by blast 
     then have "(p,q) ∈ e" using e by auto
     thus ?thesis using x by simp }
    next
    {assume "(¬?A∧?B∧¬?C)" then have "?B" by simp
     then obtain t where kt:"k∥t" and tq:"t∥q" by auto
     then have "(p,q) ∈ f^-1" using f qz pz kp by blast
     thus ?thesis using x by simp}
    next
    {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
     then obtain t where kt:"k'∥t" and tp:"t∥p" by auto
     with kpq pz qz have "(p,q)∈f" using f by blast
     thus ?thesis using x by simp}
  qed
qed
  

lemma cfif:"f^-1 O f ⊆ e ∪ f^-1 ∪ f"
proof
  fix x::"'a×'a" assume a:"x ∈ f^-1 O f" then obtain p q z where x:"x =(p,q)" and 1:"(p,z) ∈ f^-1" and 2:"(z,q) ∈ f" by auto
  from 1 obtain k l u where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and zu:"z∥u" and pu:"p∥u" using f by blast
  from 2 obtain k' l' u' where kpq:"k'∥q" and kplp:"k'∥l'" and lpz:"l'∥z" and zup:"z∥u'" and qup:"q∥u'" using f by blast
  from zu zup qup have qu:"q∥u" using M1 by auto
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast 
  then have "(?A∧¬?B∧¬?C)∨(¬?A∧?B∧¬?C)∨(¬?A∧¬?B∧?C)" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ e ∪ f^-1 ∪ f"    
  proof (elim disjE)
    {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp 
     then have "p = q" using M4 kp pu qu by blast 
     then have "(p,q) ∈ e" using e by auto
     thus ?thesis using x by simp }
    next
    {assume "(¬?A∧?B∧¬?C)" then have "?B" by simp
     then obtain t where kt:"k∥t" and tq:"t∥q" by auto
     then have "(p,q) ∈ f^-1" using f qu pu kp by blast
     thus ?thesis using x by simp}
    next
    {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
     then obtain t where kt:"k'∥t" and tp:"t∥p" by auto
     with kpq pu qu have "(p,q)∈f" using f by blast
     thus ?thesis using x by simp}
  qed
qed

lemma cffi:"f O f^-1 ⊆ e ∪ f ∪ f^-1"
proof
   fix x::"'a×'a" assume "x ∈ f O f^-1" then obtain p q r where x:"x = (p,r)" and "(p,q)∈f" and "(q,r) ∈f^-1" by auto
   from ‹(p,q)∈f› ‹(q,r) ∈ f^-1› obtain k k' where kp:"k∥p" and kpr:"k'∥r" using f by blast
   from ‹(p,q)∈f› ‹(q,r) ∈ f^-1› obtain u where pu:"p∥u" and "q∥u" and ru:"r∥u" using f M1 by blast
   from kp kpr have "k∥r ⊕ ((∃t. k∥t ∧ t∥r) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ e ∪ f ∪ f^-1"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with pu ru kp have "p = r" using M4 by auto
        thus ?thesis using x e by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where kt:"k∥t" and tr:"t∥r" by auto
        with ru kp pu show ?thesis using x f by blast}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where rtp:"k'∥t" and "t∥p" by auto
        with kpr ru pu show ?thesis using x f by blast}
    qed
qed

(* =========$\alpha_5$ composition========== *)
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq e \cup s \cup s^{-1}$.›

lemma cssi:"s O s^-1 ⊆ e ∪ s ∪ s^-1"
proof
   fix x::"'a×'a" assume "x ∈ s O s^-1" then obtain p q r where x:"x = (p,r)" and "(p,q)∈s" and "(q,r) ∈s^-1" by auto
   from ‹(p,q)∈s› ‹(q,r) ∈ s^-1› obtain k  where kp:"k∥p" and kr:"k∥r" and kq:"k∥q" using s M1  by blast
   from ‹(p,q)∈s› ‹(q,r) ∈ s^-1› obtain u u' where pu:"p∥u" and  rup:"r∥u'" using s by blast
   then have "p∥u' ⊕ ((∃t. p∥t ∧ t∥u') ⊕ (∃t. r∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ e ∪ s ∪ s^-1"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with rup kp kr have "p = r" using M4 by auto
        thus ?thesis using x e by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where kt:"p∥t" and tr:"t∥u'" by auto
        with rup kp kr  show ?thesis using x s by blast}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where rtp:"r∥t" and "t∥u" by auto
        with pu kp kr show ?thesis using x s  by blast}
    qed
qed

lemma csis:"s^-1 O s ⊆ e ∪ s ∪ s^-1"
proof
   fix x::"'a×'a" assume "x ∈ s^-1 O s" then obtain p q r where x:"x = (p,r)" and "(p,q)∈s^-1" and "(q,r) ∈s" by auto
   from ‹(p,q)∈s^-1› ‹(q,r) ∈ s› obtain k  where kp:"k∥p" and kr:"k∥r" and kq:"k∥q" using s M1  by blast
   from ‹(p,q)∈s^-1› ‹(q,r) ∈ s› obtain u u' where pu:"p∥u" and  rup:"r∥u'" using s by blast
   then have "p∥u' ⊕ ((∃t. p∥t ∧ t∥u') ⊕ (∃t. r∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ e ∪ s ∪ s^-1"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with rup kp kr have "p = r" using M4 by auto
        thus ?thesis using x e by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where kt:"p∥t" and tr:"t∥u'" by auto
        with rup kp kr  show ?thesis using x s by blast}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where rtp:"r∥t" and "t∥u" by auto
        with pu kp kr show ?thesis using x s  by blast}
    qed
qed

lemma cmim:"m^-1 O m ⊆ s ∪ s^-1 ∪ e"
proof
   fix x::"'a×'a" assume "x ∈ m^-1 O m" then obtain p q r where x:"x = (p,r)" and "(p,q)∈m^-1" and "(q,r) ∈m" by auto
   from ‹(p,q)∈m^-1› ‹(q,r) ∈ m›  have qp:"q∥p" and qr:"q∥r" using m  by auto
   obtain u u'  where pu:"p∥u" and  rup:"r∥u'" using M3 meets_wd qp qr by fastforce
   then have "p∥u' ⊕ ((∃t. p∥t ∧ t∥u') ⊕ (∃t. r∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ s ∪ s^-1 ∪ e"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with rup qp qr have "p = r" using M4 by auto
        thus ?thesis using x e by auto}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where kt:"p∥t" and tr:"t∥u'" by auto
        with rup qp qr  show ?thesis using x s by blast}
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where rtp:"r∥t" and "t∥u" by auto
        with pu qp qr show ?thesis using x s  by blast}
    qed
qed

(* =========$\beta_1$ composition========== *)
subsection ‹$\beta$-composition›
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq b \cup m \cup ov \cup s \cup d$.›

lemma cbd:"b O d ⊆ b ∪ m ∪ ov ∪ s ∪ d"
proof 
  fix x::"'a×'a" assume "x ∈ b O d" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ b" and "(z,q) ∈ d" by auto
  from ‹(p,z) ∈ b› obtain c where pc:"p∥c" and cz:"c∥z" using b by auto
  obtain a where ap:"a∥p" using M3 meets_wd pc by blast
  from ‹(z,q) ∈ d› obtain k l u v where "k∥l" and "l∥z" and kq:"k∥q" and zu:"z∥u" and uv:"u∥v" and qv:"q∥v" using d by blast
  from pc cz zu obtain cz where pcz:"p∥cz" and czu:"cz∥u" using M5exist_var by blast
  with uv obtain czu where pczu:"p∥czu" and czuv:"czu∥v" using M5exist_var by blast
  from ap kq  have "a∥q ⊕ ((∃t. a∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with ap pczu czuv uv qv have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where at:"a∥t" and tq:"t∥q" by auto
        from pc  tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where "t∥t'" and "t'∥c" by auto
             with pc pczu have "t'∥czu" using M1 by auto
             with at tq ap pczu czuv qv ‹t∥t'› have "(p,q)∈ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "k∥t" and "t∥p" by auto
        with kq pczu czuv uv qv have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cbf:"b O f ⊆ b ∪ m ∪ ov ∪ s ∪ d"
proof 
  fix x::"'a×'a" assume "x ∈ b O f" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ b" and "(z,q) ∈ f" by auto
  from ‹(p,z) ∈ b› obtain c where pc:"p∥c" and cz:"c∥z" using b by auto
  obtain a where ap:"a∥p" using M3 meets_wd pc by blast
  from ‹(z,q) ∈ f› obtain k l u  where "k∥l" and "l∥z" and kq:"k∥q" and zu:"z∥u" and qu:"q∥u" using f  by blast
  from pc cz zu obtain cz where pcz:"p∥cz" and czu:"cz∥u" using M5exist_var by blast
  from ap kq  have "a∥q ⊕ ((∃t. a∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with ap pcz czu  qu have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where at:"a∥t" and tq:"t∥q" by auto
        from pc  tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where "t∥t'" and "t'∥c" by auto
             with pc pcz have "t'∥cz" using M1 by auto
             with at tq ap pcz czu qu ‹t∥t'› have "(p,q)∈ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "k∥t" and "t∥p" by auto
        with kq pcz czu  qu have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cbovi:"b O ov^-1 ⊆ b ∪ m ∪ ov ∪ s ∪ d"
proof 
  fix x::"'a×'a" assume "x ∈ b O ov^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ b" and "(z,q) ∈ ov^-1" by auto
  from ‹(p,z) ∈ b› obtain c where pc:"p∥c" and cz:"c∥z" using b by auto
  obtain a where ap:"a∥p" using M3 meets_wd pc by blast
  from ‹(z,q) ∈ ov^-1› obtain k l u v w where "k∥l" and lz:"l∥z" and kq:"k∥q" and zv:"z∥v" and qu:"q∥u" and uv:"u∥v" and lw:"l∥w" and wu:"w∥u" using ov  by blast
  from cz lz lw have "c∥w" using M1 by auto
  with pc wu obtain cw where pcw:"p∥cw" and cwu:"cw∥u" using M5exist_var by blast
  from ap kq  have "a∥q ⊕ ((∃t. a∥t ∧ t∥q) ⊕ (∃t. k∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with ap qu pcw cwu  have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where at:"a∥t" and tq:"t∥q" by auto
        from pc  tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where "t∥t'" and "t'∥c" by auto
             with pc pcw have "t'∥cw" using M1 by auto
             with at tq ap pcw cwu qu ‹t∥t'› have "(p,q)∈ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "k∥t" and "t∥p" by auto
        with kq pcw cwu  qu have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cbmi:"b O m^-1 ⊆ b ∪ m ∪ ov ∪ s ∪ d"
proof 
   fix x::"'a×'a" assume "x ∈ b O m^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ b" and "(z,q) ∈ m^-1" by auto
   from ‹(p,z) ∈ b› obtain c where pc:"p∥c" and cz:"c∥z" using b by auto
   obtain k where kp:"k∥p" using M3 meets_wd pc by blast
   from ‹(z,q) ∈ m^-1› have qz:"q∥z" using m by auto
   obtain k' where kpq:"k'∥q" using M3 meets_wd qz by blast 
   from kp kpq  have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with kp pc cz qz  have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where kt:"k∥t" and tq:"t∥q" by auto
        from pc tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where "t∥t'" and "t'∥c" by auto
             with pc cz qz kt tq kp have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "k'∥t" and "t∥p" by auto
        with kpq pc cz qz have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cdov:"d O ov ⊆b ∪ m ∪ ov ∪ s ∪ d"
proof
   fix x::"'a×'a" assume "x ∈ d O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d" and "(z,q) ∈ ov" by auto
   from ‹(p,z) ∈ d› obtain k l u v where kl:"k∥l" and lp:"l∥p" and kz:"k∥z" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v" using d by blast
   from ‹(z,q) ∈ ov› obtain k' l' u' v' c where kplp:"k'∥l'" and kpz:"k'∥z" and lpq:"l'∥q" and zup:"z∥u'" and upvp:"u'∥v'" and qvp:"q∥v'" and "l'∥c" and "c∥u'" using ov by blast
   from zup zv uv have "u∥u'" using M1 by auto
   with pu upvp obtain uu where puu:"p∥uu" and uuvp:"uu∥v'" using M5exist_var by blast
   from lp lpq  have "l∥q ⊕ ((∃t. l∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with lp puu uuvp qvp  have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where lt:"l∥t" and tq:"t∥q" by auto
        from pu tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where ttp:"t∥t'" and "t'∥u" by auto
             with pu puu have "t'∥uu" using M1 by auto
             with lp puu qvp uuvp lt tq  ttp have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "l'∥t" and "t∥p" by auto
         with lpq puu uuvp qvp have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cdfi:"d O f^-1 ⊆ b ∪ m ∪ ov ∪ s ∪ d"
proof
   fix x::"'a×'a" assume "x ∈ d O f^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d" and "(z,q) ∈ f^-1" by auto
   from ‹(p,z) ∈ d› obtain k l u v where kl:"k∥l" and lp:"l∥p" and kz:"k∥z" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v" using d by blast
   from ‹(z,q) ∈ f^-1› obtain k' l' u'  where kpz:"k'∥z" and kplp:"k'∥l'" and lpq:"l'∥q" and zup:"z∥u'" and  qup:"q∥u'" using f by blast
   from zup zv uv have uup:"u∥u'" using M1 by auto
   from lp lpq  have "l∥q ⊕ ((∃t. l∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
   then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
   thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
   proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with lp pu uup qup  have "(p,q) ∈ s" using s by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where lt:"l∥t" and tq:"t∥q" by auto
        from pu tq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. t∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ s ∪ d"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where ttp:"t∥t'" and tpu:"t'∥u" by auto
             with lt tq lp pu uup qup  have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "l'∥t" and "t∥p" by auto
        with lpq pu uup qup  have "(p,q) ∈ d" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

(* =========$\beta_2$ composition ==========*)
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq b \cup m \cup ov \cup f^{-1} \cup d^{-1}$.›

lemma covdi:"ov O d^-1 ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ ov O d^-1" then obtain p q z where "(p,z) : ov" and "(z,q) : d^-1" and x:"x = (p,q)" by auto
  from ‹(p,z) : ov› obtain k l u v c  where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and pu:"p∥u" and uv:"u∥v"  and zv:"z∥v" and lc:"l∥c" and cu:"c∥u" using ov by blast
  from ‹(z,q) : d^-1› obtain l' k' u' v'  where lpq:"l'∥q" and kplp:"k'∥l'" and kpz:"k'∥z" and qup:"q∥u'" and upvp:"u'∥v'" and zvp:"z∥v'"  using d  by blast
  from lz kpz kplp have "l∥l'" using M1 by auto
  with kl lpq obtain ll where kll:"k∥ll" and llq:"ll∥q" using M5exist_var by blast
  from pu qup  have "p∥u' ⊕ ((∃t. p∥t ∧ t∥u') ⊕ (∃t. q∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qup kll llq kp  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tup:"t∥u'" by auto
        from pt lpq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. l'∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where lptp:"l'∥t'" and tpt:"t'∥t" by auto
             from lpq lptp llq have "ll∥t'" using M1 by auto
             with kp kll llq pt tup qup tpt  have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥u" by auto
        with pu kll llq kp   have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cdib:"d^-1 O b ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ d^-1 O b" then obtain p q z where "(p,z) : d^-1" and "(z,q) : b" and x:"x = (p,q)" by auto
  from ‹(p,z) : d^-1› obtain k l u v  where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and pv:"p∥v" and uv:"u∥v"  and zu:"z∥u"  using d by blast
  from ‹(z,q) : b› obtain c  where  zc:"z∥c" and cq:"c∥q"  using b by blast
  with kl lz obtain lzc where klzc:"k∥lzc" and lzcq:"lzc∥q" using M5exist_var by blast
  obtain v' where qvp:"q∥v'" using M3 meets_wd cq by blast
  from pv qvp  have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qvp kp klzc lzcq  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt cq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. c∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where ctp:"c∥t'" and tpt:"t'∥t" by auto
             from lzcq cq ctp have "lzc∥t'" using M1 by auto
             with pt tvp qvp kp klzc lzcq tpt have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with pv kp klzc lzcq  have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma csdi:"s O d^-1 ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ s O d^-1" then obtain p q z where "(p,z) : s" and "(z,q) : d^-1" and x:"x = (p,q)" by auto
  from ‹(p,z) : s› obtain k  u v  where kp:"k∥p" and kz:"k∥z" and pu:"p∥u" and uv:"u∥v"  and zv:"z∥v"  using s by blast
  from ‹(z,q) : d^-1› obtain l' k' u' v'  where lpq:"l'∥q" and kplp:"k'∥l'" and kpz:"k'∥z" and qup:"q∥u'" and upvp:"u'∥v'" and zvp:"z∥v'"  using d  by blast
  from kp kz kpz have kpp:"k'∥p" using M1 by auto
  from pu qup  have "p∥u' ⊕ ((∃t. p∥t ∧ t∥u') ⊕ (∃t. q∥t ∧ t∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qup kpp kplp lpq  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tup:"t∥u'" by auto
        from pt lpq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. l'∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where lptp:"l'∥t'" and tpt:"t'∥t" by auto
             with pt tup qup kpp kplp lpq  have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥u" by auto
        with pu kpp kplp lpq   have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma csib:"s^-1 O b ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ s^-1 O b" then obtain p q z where "(p,z) : s^-1" and "(z,q) : b" and x:"x = (p,q)" by auto
  from ‹(p,z) : s^-1› obtain k  u v  where kp:"k∥p" and kz:"k∥z" and zu:"z∥u" and uv:"u∥v"  and pv:"p∥v"  using s by blast
  from ‹(z,q) : b› obtain c  where  zc:"z∥c" and cq:"c∥q"  using b by blast
  from kz zc cq obtain zc where kzc:"k∥zc" and zcq:"zc∥q" using M5exist_var by blast
  obtain v' where qvp:"q∥v'" using M3 meets_wd cq by blast
  from pv qvp  have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qvp kp kzc zcq  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt cq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. c∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where ctp:"c∥t'" and tpt:"t'∥t" by auto
             from zcq cq ctp have "zc∥t'" using M1 by auto
             with zcq  pt tvp qvp kzc kp ctp tpt have "(p,q) ∈ ov" using ov by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with pv kp kzc zcq   have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma covib:"ov^-1 O b ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ ov^-1 O b" then obtain p q z where "(p,z) : ov^-1" and "(z,q) : b" and x:"x = (p,q)" by auto
  from ‹(p,z) : ov^-1› obtain k l u v c  where kz:"k∥z" and kl:"k∥l" and lp:"l∥p" and zu:"z∥u" and uv:"u∥v"  and pv:"p∥v" and lc:"l∥c" and cu:"c∥u" using ov by blast
  from ‹(z,q) : b› obtain w  where  zw:"z∥w" and wq:"w∥q"  using b by blast
  from cu zu zw have cw:"c∥w" using M1 by auto
  with lc wq obtain cw where lcw:"l∥cw" and cwq:"cw∥q" using M5exist_var by blast
  obtain v' where qvp:"q∥v'" using M3 meets_wd wq by blast
  from pv qvp  have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with qvp lp lcw cwq  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt wq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. w∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where wtp:"w∥t'" and tpt:"t'∥t" by auto
             moreover with wq cwq have "cw∥t'" using M1 by auto
             ultimately have "(p,q) ∈ ov" using ov cwq lp lcw pt tvp qvp by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with pv lp lcw cwq  have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

lemma cmib:"m^-1 O b ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
proof
  fix x::"'a×'a" assume "x ∈ m^-1 O b" then obtain p q z where "(p,z) : m^-1" and "(z,q) : b" and x:"x = (p,q)" by auto
  from ‹(p,z) : m^-1› have zp:"z∥p" using m by auto
  from ‹(z,q) : b› obtain w  where  zw:"z∥w" and wq:"w∥q"  using b by blast
  obtain v where pv:"p∥v" using M3 meets_wd zp  by blast
  obtain v' where qvp:"q∥v'" using M3 meets_wd wq by blast

  from pv qvp  have "p∥v' ⊕ ((∃t. p∥t ∧ t∥v') ⊕ (∃t. q∥t ∧ t∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have ?A by simp
        with zp zw wq qvp  have "(p,q) ∈ f^-1" using f by blast
        thus ?thesis using x  by auto} 
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp 
        then obtain t where pt:"p∥t" and tvp:"t∥v'" by auto
        from pt wq have "p∥q ⊕ ((∃t'. p∥t' ∧ t'∥q) ⊕ (∃t'. w∥t' ∧ t'∥t))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus "x ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
        proof (elim disjE)
           { assume "?A∧¬?B∧¬?C" then have ?A by simp
             thus ?thesis using x m by auto}
           next
           { assume "¬?A∧?B∧¬?C" then have ?B by simp
             thus ?thesis using x b by auto}
           next
           { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
             then obtain t' where wtp:"w∥t'" and tpt:"t'∥t" by auto
             with zp zw wq pt tvp qvp have "(p,q) ∈ ov" using ov  by blast
             thus ?thesis using x by auto}
        qed
        }  
      next
      { assume "¬?A ∧ ¬?B ∧ ?C" then have ?C by simp
        then obtain t where "q∥t" and "t∥v" by auto
        with zp zw wq pv   have "(p,q) ∈ d^-1" using d by blast
        thus ?thesis using x  by auto}
       qed
qed

(*==========$\gamma$ composition =======*)
subsection ‹$\gamma$-composition›
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq ov \cup s \cup d \cup f \cup e \cup f^{-1} \cup d^{-1} \cup s^{-1} \cup ov^{-1}$.›

lemma covovi:"ov O ov^-1 ⊆ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1 "
proof
  fix x::"'a×'a" assume "x ∈ ov O ov^-1" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov" and "(z, q) ∈ ov^-1" by auto
  from ‹(p,z) ∈ ov› obtain k l c u  where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and lc:"l∥c" and pu:"p∥u" and cu:"c∥u"  using ov by blast
  from ‹(z,q) ∈ ov^-1› obtain k' l' c' u'  where kpq:"k'∥q" and kplp:"k'∥l'" and lpz:"l'∥z" and lpcp:"l'∥c'" and qup:"q∥u'" and cpup:"c'∥u'"  using ov by blast

  from kp kpq  have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have kq:?A by simp
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with kq kp qup have "p = q" using M4 by auto
            thus ?thesis using x e by auto}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            with kq kp qup show ?thesis using x s by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with kq kp pu show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where kt:"k∥t" and tq:"t∥q" by auto
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with qup kp kt tq  show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where ptp:"p∥t'" and tpup:"t'∥u'" by auto
            from tq kpq kplp have "t∥l'" using M1 by auto
            moreover with lpz lz lc have "l'∥c" using M1 by auto
            moreover with cu pu ptp have "c∥t'" using M1 by auto
            ultimately obtain lc where "t∥lc" and "lc∥t'" using M5exist_var by blast
            with ptp tpup kp kt tq qup  show ?thesis using x ov by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with pu kp kt tq  show ?thesis using x d  by blast}

        qed}
      next
      {assume "¬?A∧¬?B∧?C" then have ?C by auto
       then obtain t where kpt:"k'∥t" and tp:"t∥p" by auto
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with kpq kpt tp qup show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where "p∥t'" and "t'∥u'" by auto
            with  kpq kpt tp qup show ?thesis using x d by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            then obtain t' where qtp:"q∥t'" and tpu:"t'∥u" by auto
            from tp kp kl have "t∥l" using M1 by auto
            moreover with lpcp lpz lz have "l∥c'" using M1 by auto
            moreover with cpup qup qtp have "c'∥t'" using M1 by auto
            ultimately obtain lc where "t∥lc" and "lc∥t'" using M5exist_var by blast
            with kpt tp kpq qtp tpu pu show ?thesis using x ov by blast}
          qed}
      qed
qed


lemma cdid:"d^-1 O d ⊆ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1 "
proof
  fix x::"'a×'a" assume "x ∈ d^-1 O d" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ d^-1" and "(z, q) ∈ d" by auto
  from ‹(p,z) ∈ d^-1› obtain k l u v where kp:"k∥p" and kl:"k∥l" and lz:"l∥z" and pv:"p∥v" and zu:"z∥u" and uv:"u∥v"  using d by blast
  from ‹(z,q) ∈ d› obtain k' l'  u' v'  where kpq:"k'∥q" and kplp:"k'∥l'" and lpz:"l'∥z"  and qvp:"q∥v'" and zup:"z∥u'" and upvp:"u'∥v'"  using d by blast

  from kp kpq  have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have kq:?A by simp
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with kq kp qvp have "p = q" using M4 by auto
            thus ?thesis using x e by auto}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            with kq kp qvp show ?thesis using x s by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with kq kp pv show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where kt:"k∥t" and tq:"t∥q" by auto
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with qvp kp kt tq  show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where ptp:"p∥t'" and tpvp:"t'∥v'" by auto
            from tq kpq kplp have "t∥l'" using M1 by auto
            moreover with ptp pv uv have "u∥t'" using M1 by auto
            moreover with lpz zu ‹t∥l'› obtain lzu where "t∥lzu" and "lzu∥t'" using  M5exist_var   by blast
            ultimately  show ?thesis using x ov kt tq kp ptp tpvp qvp by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with pv kp kt tq  show ?thesis using x d  by blast}

        qed}
      next
      {assume "¬?A∧¬?B∧?C" then have ?C by auto
       then obtain t where kpt:"k'∥t" and tp:"t∥p" by auto
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with kpq kpt tp qvp show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where "p∥t'" and "t'∥v'" by auto
            with  kpq kpt tp qvp show ?thesis using x d by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            then obtain t' where qtp:"q∥t'" and tpv:"t'∥v" by auto
            from tp kp kl have "t∥l" using M1 by auto
            moreover with qtp qvp upvp have "u'∥t'" using M1 by auto
            moreover with lz zup ‹t∥l› obtain lzu where "t∥lzu" and "lzu∥t'" using  M5exist_var by blast
            ultimately show ?thesis using x ov kpt tp kpq qtp tpv pv  by blast}
          qed}
      qed
qed

lemma coviov:"ov^-1 O ov ⊆ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1"
proof
  fix x::"'a×'a" assume "x ∈ ov^-1 O ov" then obtain p q z where x:"x = (p,q)" and "(p,z) ∈ ov^-1" and "(z, q) ∈ ov" by auto
  from ‹(p,z) ∈ ov^-1› obtain k l c u v where kz:"k∥z" and kl:"k∥l" and lp:"l∥p" and lc:"l∥c" and zu:"z∥u" and pv:"p∥v" and cu:"c∥u" and uv:"u∥v"  using ov by blast
  from ‹(z,q) ∈ ov› obtain k' l' c' u' v' where kpz:"k'∥z" and kplp:"k'∥l'" and lpq:"l'∥q" and lpcp:"l'∥c'" and qvp:"q∥v'" and zup:"z∥u'" and cpup:"c'∥u'" and upvp:"u'∥v'" using ov by blast

  from lp lpq  have "l∥q ⊕ ((∃t. l∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈ e ∪ ov ∪ ov^-1 ∪ d ∪ d^-1 ∪ s ∪ s^-1 ∪ f ∪ f^-1"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have lq:?A by simp
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with lq lp qvp have "p = q" using M4 by auto
            thus ?thesis using x e by auto}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            with lq lp qvp show ?thesis using x s by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with lq lp pv show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where lt:"l∥t" and tq:"t∥q" by auto
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with qvp lp lt tq  show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where ptp:"p∥t'" and tpvp:"t'∥v'" by auto
            from tq lpq lpcp have "t∥c'" using M1 by auto
            moreover with cpup zup zu have "c'∥u" using M1 by auto
            moreover with ptp pv uv have "u∥t'" using M1 by auto
            ultimately obtain cu where "t∥cu" and "cu∥t'" using M5exist_var by blast
            with lt tq lp ptp tpvp qvp  show ?thesis using x ov by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            with pv lp lt tq  show ?thesis using x d  by blast}

        qed}
      next
      {assume "¬?A∧¬?B∧?C" then have ?C by auto
       then obtain t where lpt:"l'∥t" and tp:"t∥p" by auto
        from pv qvp have "p∥v' ⊕ ((∃t'. p∥t' ∧ t'∥v') ⊕ (∃t'. q∥t' ∧ t'∥v))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          { assume "?A∧¬?B∧¬?C" then have ?A by simp
            with qvp lpq lpt tp show ?thesis using x f  by blast}
          next
          { assume "¬?A∧?B∧¬?C" then have ?B by simp
            then obtain t' where "p∥t'" and "t'∥v'" by auto
            with  qvp lpq lpt tp show ?thesis using x d by blast}
          next
          { assume "¬?A∧¬?B∧?C" then have ?C by simp
            then obtain t' where qtp:"q∥t'" and tpv:"t'∥v" by auto
            from tp lp lc have "t∥c" using M1 by auto
            moreover with cu zu zup have "c∥u'" using M1 by auto
            moreover with qtp qvp upvp have "u'∥t'" using M1 by auto
            ultimately obtain cu where "t∥cu" and "cu∥t'" using M5exist_var by blast
            with lpt tp lpq pv qtp tpv show ?thesis using x ov by blast}
          qed}
      qed
qed

(* ===========$\delta$ composition =========*)
subsection ‹$\gamma$-composition›
text ‹We prove compositions of the form $r_1 \circ r_2 \subseteq b \cup m \cup ov \cup s \cup d \cup f \cup e \cup f^{-1} \cup d^{-1} \cup s^{-1} \cup ov^{-1} \cup b^{-1} \cup m^{-1}$.›


lemma cbbi:"b O b^-1 ⊆ b ∪ b^-1 ∪ m ∪ m^-1 ∪ e ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ d ∪ d^-1 ∪ f ∪ f^-1" (is "b O b^-1 ⊆ ?R")
proof
  fix x::"'a×'a" assume "x ∈ b O b^-1" then obtain p q z::'a where x:"x = (p,q)" and "(p,z) ∈ b" and "(z,q) ∈ b^-1" by auto
  from ‹(p,z)∈b› obtain c where pc:"p∥c" and "c∥z" using b  by blast
  from ‹(z,q) ∈ b^-1› obtain c' where qcp:"q∥c'" and "c'∥z" using b  by blast
  obtain k k' where kp:"k∥p" and kpq:"k'∥q" using M3 meets_wd pc qcp by fastforce
  then have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈?R"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have kq:?A by simp
        from pc qcp have "p∥c' ⊕ ((∃t'. p∥t' ∧ t'∥c') ⊕ (∃t'. q∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp
           with kp kq qcp have "p = q" using M4 by auto
           thus ?thesis using x e  by auto}
          next
          {assume "¬?A∧?B∧¬?C" then have "?B" by simp
           with kq kp qcp show ?thesis using x s by blast}
          next
          {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
           with kq kp pc show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where kt:"k∥t" and tq:"t∥q" by auto
        from pc qcp have "p∥c' ⊕ ((∃t'. p∥t' ∧ t'∥c') ⊕ (∃t'. q∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with kp qcp kt tq show ?thesis using f x by blast}
          next
          {assume "¬?A∧?B∧¬?C"  then have ?B by simp
           then obtain t' where ptp:"p∥t'" and tpcp:"t'∥c'" by auto
           from pc tq  have "p∥q ⊕ ((∃t''. p∥t'' ∧ t''∥q) ⊕ (∃t''. t∥t'' ∧ t''∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then have ?C by simp
                then obtain g where "t∥g" and "g∥c" by auto
                moreover with pc ptp have "g∥t'" using M1 by blast
                ultimately  show ?thesis using x ov kt tq kp ptp tpcp qcp   by blast}
           qed}
         next
          {assume "¬?A∧¬?B∧?C" then have ?C by simp
           then obtain t' where "q∥t'" and "t'∥c" by auto
           with kp  kt tq pc show ?thesis using d x by blast}
         qed}
      next
      { assume "¬?A∧¬?B∧?C" then have ?C by simp
        then obtain t where kpt:"k'∥t" and tp:"t∥p" by auto
        from  pc qcp have "p∥c' ⊕ ((∃t'. p∥t' ∧ t'∥c') ⊕ (∃t'. q∥t' ∧ t'∥c))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qcp kpt tp kpq show ?thesis using x f by blast}
          next
          {assume "¬?A∧?B∧¬?C" then have ?B by simp
           with qcp kpt tp kpq show ?thesis using x d by blast}
          next
          {assume "¬?A∧¬?B∧?C" then obtain t' where qt':"q∥t'" and tpc:"t'∥c" by auto
           from qcp tp have "q∥p ⊕ ((∃t''. q∥t'' ∧ t''∥p) ⊕ (∃t''. t∥t'' ∧ t''∥c'))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then obtain g where tg:"t∥g" and "g∥c'" by auto
                with qcp qt' have "g∥t'" using M1 by blast
                with qt' tpc pc kpq kpt tp tg show ?thesis using x ov by blast}
          qed}
     qed}
 qed
qed
       


lemma cbib:"b^-1 O b ⊆ b ∪ b^-1 ∪ m ∪ m^-1 ∪ e ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ d ∪ d^-1 ∪ f ∪ f^-1" (is "b^-1 O b ⊆ ?R")
proof
  fix x::"'a×'a" assume "x ∈ b^-1 O b" then obtain p q z::'a where x:"x = (p,q)" and "(p,z) ∈ b^-1" and "(z,q) ∈ b" by auto
  from ‹(p,z)∈b^-1› obtain c where zc:"z∥c" and cp:"c∥p" using b  by blast
  from ‹(z,q) ∈ b› obtain c' where zcp:"z∥c'" and cpq:"c'∥q" using b  by blast
  obtain u u' where pu:"p∥u" and qup:"q∥u'" using M3 meets_wd cp cpq by fastforce
  from cp cpq have "c∥q ⊕ ((∃t. c∥t ∧ t∥q) ⊕ (∃t. c'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈?R"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have cq:?A by simp
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp
           with cq cp qup have "p = q" using M4 by auto
           thus ?thesis using x e  by auto}
          next
          {assume "¬?A∧?B∧¬?C" then have "?B" by simp
           with cq cp qup show ?thesis using x s by blast}
          next
          {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
           with pu cq cp show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where ct:"c∥t" and tq:"t∥q" by auto
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qup ct tq cp show ?thesis using f x by blast}
          next
          {assume "¬?A∧?B∧¬?C"  then have ?B by simp
           then obtain t' where ptp:"p∥t'" and tpup:"t'∥u'" by auto
           from pu tq  have "p∥q ⊕ ((∃t''. p∥t'' ∧ t''∥q) ⊕ (∃t''. t∥t'' ∧ t''∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then have ?C by simp
                then obtain g where "t∥g" and "g∥u" by auto
                moreover with pu ptp have "g∥t'" using M1 by blast
                ultimately  show ?thesis using x ov ct tq cp ptp tpup qup   by blast}
           qed}
         next
          {assume "¬?A∧¬?B∧?C" then have ?C by simp
           then obtain t' where "q∥t'" and "t'∥u" by auto
           with cp  ct tq pu  show ?thesis using d x by blast}
         qed}
      next
      { assume "¬?A∧¬?B∧?C" then have ?C by simp
        then obtain t where cpt:"c'∥t" and tp:"t∥p" by auto
        from  pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qup cpt tp cpq show ?thesis using x f by blast}
          next
          {assume "¬?A∧?B∧¬?C" then have ?B by simp
           with qup cpt tp cpq show ?thesis using x d by blast}
          next
          {assume "¬?A∧¬?B∧?C" then obtain t' where qt':"q∥t'" and tpc:"t'∥u" by auto
           from qup tp have "q∥p ⊕ ((∃t''. q∥t'' ∧ t''∥p) ⊕ (∃t''. t∥t'' ∧ t''∥u'))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then obtain g where tg:"t∥g" and "g∥u'" by auto
                with qup qt' have "g∥t'" using M1 by blast
                with qt' tpc pu cpq cpt tp tg show ?thesis using x ov by blast}
          qed}
     qed}
 qed
qed

lemma cddi:"d O d^-1 ⊆ b ∪ b^-1 ∪ m ∪ m^-1 ∪ e ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ d ∪ d^-1 ∪ f ∪ f^-1" (is "d O d^-1 ⊆ ?R")
proof
  fix x::"'a×'a" assume "x ∈ d O d^-1" then obtain p q z::'a where x:"x = (p,q)" and "(p,z) ∈ d" and "(z,q) ∈ d^-1" by auto
  from ‹(p,z) ∈ d› obtain k l u v where lp:"l∥p" and kl:"k∥l" and kz:"k∥z" and pu:"p∥u" and uv:"u∥v" and zv:"z∥v"  using d  by blast
  from ‹(z,q) ∈ d^-1› obtain k' l' u' v' where lpq:"l'∥q" and kplp:"k'∥l'" and kpz:"k'∥z" and qup:"q∥u'" and upvp:"u'∥v'" and zv':"z∥v'"  using d  by blast
  from lp lpq have "l∥q ⊕ ((∃t. l∥t ∧ t∥q) ⊕ (∃t. l'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus "x ∈?R"
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have lq:?A by simp
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp
           with lq lp qup have "p = q" using M4 by auto
           thus ?thesis using x e  by auto}
          next
          {assume "¬?A∧?B∧¬?C" then have "?B" by simp
           with lq lp qup show ?thesis using x s by blast}
          next
          {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
           with pu lq lp show ?thesis using x s by blast}
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where lt:"l∥t" and tq:"t∥q" by auto
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qup lt tq lp show ?thesis using f x by blast}
          next
          {assume "¬?A∧?B∧¬?C"  then have ?B by simp
           then obtain t' where ptp:"p∥t'" and tpup:"t'∥u'" by auto
           from pu tq  have "p∥q ⊕ ((∃t''. p∥t'' ∧ t''∥q) ⊕ (∃t''. t∥t'' ∧ t''∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then have ?C by simp
                then obtain g where "t∥g" and "g∥u" by auto
                moreover with pu ptp have "g∥t'" using M1 by blast
                ultimately  show ?thesis using x ov lt tq lp ptp tpup qup by blast}
           qed}
         next
          {assume "¬?A∧¬?B∧?C" then have ?C by simp
           then obtain t' where "q∥t'" and "t'∥u" by auto
           with lp  lt tq pu  show ?thesis using d x by blast}
         qed}
      next
      { assume "¬?A∧¬?B∧?C" then have ?C by simp
        then obtain t where lpt:"l'∥t" and tp:"t∥p" by auto
        from  pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qup lpt tp lpq show ?thesis using x f by blast}
          next
          {assume "¬?A∧?B∧¬?C" then have ?B by simp
           with qup lpt tp lpq show ?thesis using x d by blast}
          next
          {assume "¬?A∧¬?B∧?C" then obtain t' where qt':"q∥t'" and tpc:"t'∥u" by auto
           from qup tp have "q∥p ⊕ ((∃t''. q∥t'' ∧ t''∥p) ⊕ (∃t''. t∥t'' ∧ t''∥u'))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using x m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using x b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then obtain g where tg:"t∥g" and "g∥u'" by auto
                with qup qt' have "g∥t'" using M1 by blast
                with qt' tpc pu lpq lpt tp tg show ?thesis using x ov by blast}
          qed}
     qed}
 qed
qed


(* ========= inverse ========== *)
subsection ‹The rest of the composition table›
text ‹Because of the symmetry $(r_1 \circ r_2)^{-1} = r_2^{-1} \circ r_1^{-1} $, the rest of the compositions is easily deduced.›


lemma cmbi:"m O b^-1 ⊆ b^-1 ∪ m^-1 ∪ s^-1 ∪ ov^-1 ∪ d^-1"
  using cbmi by auto


lemma covmi:"ov O m^-1 ⊆ ov^-1 ∪ d^-1 ∪ s^-1"
  using  cmovi by auto

lemma covbi:"ov O b^-1 ⊆ b^-1 ∪ m^-1 ∪ s^-1 ∪ ov^-1 ∪ d^-1"
  using cbovi by auto

lemma cfiovi:"f^-1 O ov^-1 ⊆ ov^-1 ∪ s^-1 ∪ d^-1"
  using covf by auto

lemma cfimi:"(f^-1 O m^-1) ⊆ s^-1 ∪ ov^-1 ∪ d^-1"
  using cmf by auto

lemma cfibi:"f^-1 O b^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ s^-1 ∪ d^-1"
  using cbf by auto

lemma cdif:"d^-1 O f ⊆ ov^-1 ∪ s^-1 ∪ d^-1"
  using cfid by auto

lemma cdiovi:"d^-1 O ov ^-1 ⊆ ov^-1 ∪ s^-1 ∪ d^-1"
  using covd by auto

lemma cdimi:"d^-1 O m^-1 ⊆ s^-1 ∪ ov^-1 ∪ d^-1 "
  using cmd by auto

lemma cdibi:"d^-1 O b^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ s^-1 ∪ d^-1"
  using cbd by auto 

lemma csd:"s O d ⊆ d"
  using cdisi by auto

lemma csf:"s O f ⊆ d"
  using cfisi by auto

lemma csovi:"s O ov^-1 ⊆ ov^-1 ∪ f ∪ d"
  using covsi by auto

lemma csmi:"s O m^-1 ⊆ m^-1"
  using cmsi by auto

lemma csbi:"s O b^-1 ⊆ b^-1"
  using cbsi by auto

lemma csisi:"s^-1 O s^-1 ⊆ s^-1"
  using css by auto

lemma csid:"s^-1 O d ⊆ ov^-1 ∪ f ∪ d"
  using cdis by auto

lemma csif:"s^-1 O f ⊆ ov^-1"
  using cfis by auto

lemma csiovi:"s^-1 O ov^-1 ⊆ ov^-1"
  using covs by auto

lemma csimi:"s^-1 O m^-1 ⊆ m^-1"
  using cms by auto

lemma csibi:"s^-1 O b^-1 ⊆ b^-1"
  using cbs by auto

lemma cds:"d O s ⊆ d"
  using csidi by auto

lemma cdsi:"d O s^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using csdi by auto

lemma cdd:"d O d ⊆ d"
  using cdidi by auto

lemma cdf:"d O f ⊆ d" 
  using cfidi by auto

lemma cdovi:"d O ov^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using covdi by auto

lemma cdmi:"d O m^-1 ⊆ b^-1"
  using cmdi by auto

lemma cdbi:"d O b^-1 ⊆ b^-1"
  using cbdi by auto

lemma cfdi:"f O d^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ s^-1 ∪ d^-1 "
  using cdfi by auto

lemma cfs:"f O s ⊆ d"
  using csifi by auto

lemma cfsi:"f O s^-1 ⊆ b ^-1 ∪ m^-1 ∪ ov ^-1"
  using csfi by auto

lemma cfd:"f O d ⊆ d"
  using cdifi by auto


lemma cff:"f O f ⊆ f"
  using cfifi by auto

lemma cfovi:"f O ov^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1"
  using covfi by auto

lemma cfmi:"f O m^-1 ⊆ b^-1"
  using cmfi by auto

lemma cfbi:"f O b^-1 ⊆ b^-1"
  using cbfi by auto

lemma covifi:"ov^-1 O f^-1 ⊆ ov^-1 ∪ s^-1 ∪ d^-1"
  using cfov by auto

lemma covidi:"ov^-1 O d^-1 ⊆ b^-1 ∪ m^-1 ∪ s^-1 ∪ ov^-1 ∪ d^-1"
  using cdov by auto

lemma covis:"ov^-1 O s ⊆ ov^-1 ∪ f ∪ d"
  using csiov by auto

lemma covisi:"ov^-1 O s^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1"
  using csov by auto

lemma covid:"ov^-1 O d ⊆ ov^-1 ∪ f ∪ d"
  using cdiov by auto

lemma covif:"ov^-1 O f ⊆ ov^-1"
  using cfiov by auto

lemma coviovi:"ov^-1 O ov^-1 ⊆ b^-1 ∪ m^-1 ∪ ov^-1"
  using covov by auto

lemma covimi:"ov^-1 O m^-1 ⊆ b^-1"
  using cmov by auto

lemma covibi:"ov^-1 O b^-1 ⊆ b^-1"
  using cbov by auto

lemma cmiov:"m^-1 O ov ⊆ ov^-1 ∪ d ∪ f"
  using covim by auto

lemma cmifi:"m^-1 O f^-1 ⊆ m^-1"
  using cfm by auto

lemma cmidi:"m^-1 O d^-1 ⊆ b^-1"
  using cdm by auto

lemma cmis:"m^-1 O s ⊆ ov^-1 ∪ d ∪ f"
  using csim by auto

lemma cmisi:"m^-1 O s^-1 ⊆ b^-1"
  using csm by auto

lemma cmid:"m^-1 O d ⊆ ov^-1 ∪ d ∪ f"
  using cdim by auto

lemma cmif:"m^-1 O f ⊆ m^-1"
  using cfim by auto

lemma cmiovi:"m^-1 O ov^-1 ⊆ b^-1"
  using covm by auto

lemma cmimi:"m^-1 O m^-1 ⊆ b^-1"
  using cmm by auto

lemma cmibi:"m^-1 O b^-1 ⊆ b^-1"
  using cbm by auto

lemma cbim:"b^-1 O m ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using cmib by auto

lemma cbiov:"b^-1 O ov ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using covib by auto

lemma cbifi:"b^-1 O f^-1 ⊆ b^-1"
  using cfb by auto

lemma cbidi:"b^-1 O d^-1 ⊆ b^-1"
  using cdb by auto

lemma cbis:"b^-1 O s ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using csib by auto

lemma cbisi:"b^-1 O s^-1 ⊆ b^-1"
  using csb by auto

lemma cbid:"b^-1 O d ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d"
  using cdib by auto

lemma cbif:"b^-1 O f ⊆ b^-1"
  using cfib by auto

lemma cbiovi:"b^-1 O ov^-1 ⊆ b^-1"
  using covb by auto

lemma cbimi:"b^-1 O m^-1 ⊆ b^-1"
  using cmb by auto

lemma cbibi:"b^-1 O b^-1 ⊆ b^-1"
  using cbb by auto 

(****)

subsection ‹Composition rules›
named_theorems ce_rules declare cem[ce_rules] and ceb[ce_rules] and ceov[ce_rules] and ces[ce_rules] and cef[ce_rules] and ced[ce_rules] and 
cemi[ce_rules] and cebi[ce_rules] and ceovi[ce_rules] and cesi[ce_rules] and cefi[ce_rules] and cedi[ce_rules]

named_theorems cm_rules declare cme[cm_rules] and cmb[cm_rules] and cmm[cm_rules] and cmov[cm_rules] and cms [cm_rules] and cmd[cm_rules] and cmf[cm_rules] and
cmbi[cm_rules] and cmmi[cm_rules] and cmovi[cm_rules] and cmsi[cm_rules] and cmdi[cm_rules] and cmfi[cm_rules]

named_theorems cb_rules declare cbe[cb_rules] and cbm[cb_rules] and cbb[cb_rules] and cbov[cb_rules] and cbs [cb_rules] and cbd[cb_rules] and cbf[cb_rules] and
cbbi[cb_rules] and cbbi[cb_rules] and cbovi[cb_rules] and cbsi[cb_rules] and cbdi[cb_rules] and cbfi[cb_rules]

named_theorems cov_rules declare cove[cov_rules] and covb[cov_rules] and covb[cov_rules] and covov[cov_rules] and covs [cov_rules] and covd[cov_rules] and covf[cov_rules] and
covbi[cov_rules] and covbi[cov_rules] and covovi[cov_rules] and covsi[cov_rules] and covdi[cov_rules] and covfi[cov_rules]

named_theorems cs_rules declare cse[cs_rules] and csb[cs_rules] and csb[cs_rules] and csov[cs_rules] and css [cs_rules] and csd[cs_rules] and csf[cs_rules] and
csbi[cs_rules] and csbi[cs_rules] and csovi[cs_rules] and cssi[cs_rules] and csdi[cs_rules] and csfi[cs_rules]

named_theorems cf_rules declare cfe[cf_rules] and cfb[cf_rules] and cfb[cf_rules] and cfov[cf_rules] and cfs [cf_rules] and cfd[cf_rules] and cff[cf_rules] and
cfbi[cf_rules] and cfbi[cf_rules] and cfovi[cf_rules] and cfsi[cf_rules] and cfdi[cf_rules] and cffi[cf_rules]

named_theorems cd_rules declare cde[cd_rules] and cdb[cd_rules] and cdb[cd_rules] and cdov[cd_rules] and cds [cd_rules] and cdd[cd_rules] and cdf[cd_rules] and
cdbi[cd_rules] and cdbi[cd_rules] and cdovi[cd_rules] and cdsi[cd_rules] and cddi[cd_rules] and cdfi[cd_rules]

named_theorems cmi_rules declare cmie[cmi_rules] and cmib[cmi_rules] and cmib[cmi_rules] and cmiov[cmi_rules] and cmis [cmi_rules] and cmid[cmi_rules] and cmif[cmi_rules] and
cmibi[cmi_rules] and cmibi[cmi_rules] and cmiovi[cmi_rules] and cmisi[cmi_rules] and cmidi[cmi_rules] and cmifi[cmi_rules]

named_theorems cbi_rules declare cbie[cbi_rules] and cbim[cbi_rules] and cbib[cbi_rules] and cbiov[cbi_rules] and cbis [cbi_rules] and cbid[cbi_rules] and cbif[cbi_rules] and
cbimi[cbi_rules] and cbibi[cbi_rules] and cbiovi[cbi_rules] and cbisi[cbi_rules] and cbidi[cbi_rules] and cbifi[cbi_rules]

named_theorems covi_rules declare covie[covi_rules] and covib[covi_rules] and covib[covi_rules] and coviov[covi_rules] and covis [covi_rules] and covid[covi_rules] and covif[covi_rules] and
covibi[covi_rules] and covibi[covi_rules] and coviovi[covi_rules] and covisi[covi_rules] and covidi[covi_rules] and covifi[covi_rules]

named_theorems csi_rules declare csie[csi_rules] and csib[csi_rules] and csib[csi_rules] and csiov[csi_rules] and csis [csi_rules] and csid[csi_rules] and csif[csi_rules] and
csibi[csi_rules] and csibi[csi_rules] and csiovi[csi_rules] and csisi[csi_rules] and csidi[csi_rules] and csifi[csi_rules]

named_theorems cfi_rules declare cfie[cfi_rules] and cfib[cfi_rules] and cfib[cfi_rules] and cfiov[cfi_rules] and cfis [cfi_rules] and cfid[cfi_rules] and cfif[cfi_rules] and
cfibi[cfi_rules] and cfibi[cfi_rules] and cfiovi[cfi_rules] and cfisi[cfi_rules] and cfidi[cfi_rules] and cfifi[cfi_rules]

named_theorems cdi_rules declare cdie[cdi_rules] and cdib[cdi_rules] and cdib[cdi_rules] and cdiov[cdi_rules] and cdis [cdi_rules] and cdid[cdi_rules] and cdif[cdi_rules] and
cdibi[cdi_rules] and cdibi[cdi_rules] and cdiovi[cdi_rules] and cdisi[cdi_rules] and cdidi[cdi_rules] and cdifi[cdi_rules]
(**)
named_theorems cre_rules declare cee[cre_rules] and cme[cre_rules] and cbe[cre_rules] and cove[cre_rules] and cse[cre_rules] and cfe[cre_rules] and cde[cre_rules] and 
cmie[cre_rules] and cbie[cre_rules] and covie[cre_rules] and csie[cre_rules] and cfie[cre_rules] and cdie[cre_rules]

named_theorems crm_rules declare cem[crm_rules] and cbm[crm_rules] and cmm[crm_rules]  and covm[crm_rules] and csm[crm_rules] and cfm[crm_rules] and cdm[crm_rules] and 
cmim[crm_rules] and cbim[crm_rules] and covim[crm_rules] and csim[crm_rules] and cfim[crm_rules] and cdim[crm_rules]

named_theorems crmi_rules declare cemi[crmi_rules] and cbmi[crmi_rules] and cmmi[crmi_rules]  and covmi[crmi_rules] and csmi[crmi_rules] and cfmi[crmi_rules] and cdmi[crmi_rules] and 
cmimi[crmi_rules] and cbimi[crmi_rules] and covimi[crmi_rules] and csimi[crmi_rules] and cfimi[crmi_rules] and cdimi[crmi_rules]

named_theorems crs_rules declare ces[crs_rules] and cbs[crs_rules] and cms[crs_rules]  and covs[crs_rules] and css[crs_rules] and cfs[crs_rules] and cds[crs_rules] and 
cmis[crs_rules] and cbis[crs_rules] and covis[crs_rules] and csis[crs_rules] and cfis[crs_rules] and cdis[crs_rules]

named_theorems crsi_rules declare cesi[crsi_rules] and cbsi[crsi_rules] and cmsi[crsi_rules]  and covsi[crsi_rules] and cssi[crsi_rules] and cfsi[crsi_rules] and cdsi[crsi_rules] and 
cmisi[crsi_rules] and cbisi[crsi_rules] and covisi[crsi_rules] and csisi[crsi_rules] and cfisi[crsi_rules] and cdisi[crsi_rules]

named_theorems crb_rules declare ceb[crb_rules] and cbb[crb_rules] and cmb[crb_rules]  and covb[crb_rules] and csb[crb_rules] and cfb[crb_rules] and cdb[crb_rules] and 
cmib[crb_rules] and cbib[crb_rules] and covib[crb_rules] and csib[crb_rules] and cfib[crb_rules] and cdib[crb_rules]

named_theorems crbi_rules declare cebi[crbi_rules] and cbbi[crbi_rules] and cmbi[crbi_rules]  and covbi[crbi_rules] and csbi[crbi_rules] and cfbi[crbi_rules] and cdbi[crbi_rules] and 
cmibi[crbi_rules] and cbibi[crbi_rules] and covibi[crbi_rules] and csibi[crbi_rules] and cfibi[crbi_rules] and cdibi[crbi_rules]

named_theorems crov_rules declare ceov[crov_rules] and cbov[crov_rules] and cmov[crov_rules]  and covov[crov_rules] and csov[crov_rules] and cfov[crov_rules] and cdov[crov_rules] and 
cmiov[crov_rules] and cbiov[crov_rules] and coviov[crov_rules] and csiov[crov_rules] and cfiov[crov_rules] and cdiov[crov_rules]

named_theorems crovi_rules declare ceovi[crovi_rules] and cbovi[crovi_rules] and cmovi[crovi_rules]  and covovi[crovi_rules] and csovi[crovi_rules] and cfovi[crovi_rules] and cdovi[crovi_rules] and 
cmiovi[crovi_rules] and cbiovi[crovi_rules] and coviovi[crovi_rules] and csiovi[crovi_rules] and cfiovi[crovi_rules] and cdiovi[crovi_rules]

named_theorems crf_rules declare cef[crf_rules] and cbf[crf_rules] and cmf[crf_rules]  and covf[crf_rules] and csf[crf_rules] and cff[crf_rules] and cdf[crf_rules] and 
cmif[crf_rules] and cbif[crf_rules] and covif[crf_rules] and csif[crf_rules] and cfif[crf_rules] and cdif[crf_rules]

named_theorems crfi_rules declare cefi[crfi_rules] and cbfi[crfi_rules] and cmfi[crfi_rules]  and covfi[crfi_rules] and csfi[crfi_rules] and cffi[crfi_rules] and cdfi[crfi_rules] and 
cmifi[crfi_rules] and cbifi[crfi_rules] and covifi[crfi_rules] and csifi[crfi_rules] and cfifi[crfi_rules] and cdifi[crfi_rules]

named_theorems crd_rules declare ced[crd_rules] and cbd[crd_rules] and cmd[crd_rules]  and covd[crd_rules] and csd[crd_rules] and cfd[crd_rules] and cdd[crd_rules] and 
cmid[crd_rules] and cbid[crd_rules] and covid[crd_rules] and csid[crd_rules] and cfid[crd_rules] and cdid[crd_rules]

named_theorems crdi_rules declare cedi[crdi_rules] and cbdi[crdi_rules] and cmdi[crdi_rules]  and covdi[crdi_rules] and csdi[crdi_rules] and cfdi[crdi_rules] and cddi[crdi_rules] and 
cmidi[crdi_rules] and cbidi[crdi_rules] and covidi[crdi_rules] and csidi[crdi_rules] and cfidi[crdi_rules] and cdidi[crdi_rules]



end