[STATEMENT]
lemma cssi:"s O s^-1 \<subseteq> e \<union> s \<union> s^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O s\<inverse> \<subseteq> e \<union> s \<union> s\<inverse>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
fix x::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "x \<in> s O s^-1"
[PROOF STATE]
proof (state)
this:
x \<in> s O s\<inverse>

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> s O s\<inverse>
[PROOF STEP]
obtain p q r where x:"x = (p,r)" and "(p,q)\<in>s" and "(q,r) \<in>s^-1"
[PROOF STATE]
proof (prove)
using this:
x \<in> s O s\<inverse>

goal (1 subgoal):
 1. (\<And>p r q. \<lbrakk>x = (p, r); (p, q) \<in> s; (q, r) \<in> s\<inverse>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (p, r)
(p, q) \<in> s
(q, r) \<in> s\<inverse>

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
from \<open>(p,q)\<in>s\<close> \<open>(q,r) \<in> s^-1\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>
[PROOF STEP]
obtain k  where kp:"k\<parallel>p" and kr:"k\<parallel>r" and kq:"k\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<parallel> p; k \<parallel> r; k \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s M1
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<parallel> p; k \<parallel> r; k \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> r
k \<parallel> q

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
from \<open>(p,q)\<in>s\<close> \<open>(q,r) \<in> s^-1\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>
[PROOF STEP]
obtain u u' where pu:"p\<parallel>u" and  rup:"r\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s
(q, r) \<in> s\<inverse>
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
r \<parallel> u'
[PROOF STEP]
have "p\<parallel>u' \<oplus> ((\<exists>t. p\<parallel>t \<and> t\<parallel>u') \<oplus> (\<exists>t. r\<parallel>t \<and> t\<parallel>u))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?p \<parallel> ?s \<oplus> ((\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?s) \<oplus> (\<exists>t. ?r \<parallel> t \<and> t \<parallel> ?q))

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
have "(?A\<and>\<not>?B\<and>\<not>?C) \<or> ((\<not>?A\<and>?B\<and>\<not>?C) \<or> (\<not>?A\<and>\<not>?B\<and>?C))"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<And>x. x \<in> s O s\<inverse> \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
thus "x \<in> e \<union> s \<union> s^-1"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "?A\<and>\<not>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?A
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. p \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<parallel> u'

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with rup kp kr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'
[PROOF STEP]
have "p = r"
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'

goal (1 subgoal):
 1. p = r
[PROOF STEP]
using M4
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?q \<parallel> ?s; ?p \<parallel> ?r; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?q = ?r

goal (1 subgoal):
 1. p = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = r

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = r

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x e
[PROOF STATE]
proof (prove)
using this:
p = r
x = (p, r)
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "\<not>?A\<and>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?B
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
obtain t where kt:"p\<parallel>t" and tr:"t\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>p \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<parallel> t
t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with rup kp kr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "\<not>?A \<and> \<not>?B \<and> ?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?C
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
obtain t where rtp:"r\<parallel>t" and "t\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>r \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with pu kp kr
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma csis:"s^-1 O s \<subseteq> e \<union> s \<union> s^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O s \<subseteq> e \<union> s \<union> s\<inverse>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
fix x::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "x \<in> s^-1 O s"
[PROOF STATE]
proof (state)
this:
x \<in> s\<inverse> O s

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> s\<inverse> O s
[PROOF STEP]
obtain p q r where x:"x = (p,r)" and "(p,q)\<in>s^-1" and "(q,r) \<in>s"
[PROOF STATE]
proof (prove)
using this:
x \<in> s\<inverse> O s

goal (1 subgoal):
 1. (\<And>p r q. \<lbrakk>x = (p, r); (p, q) \<in> s\<inverse>; (q, r) \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (p, r)
(p, q) \<in> s\<inverse>
(q, r) \<in> s

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
from \<open>(p,q)\<in>s^-1\<close> \<open>(q,r) \<in> s\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s
[PROOF STEP]
obtain k  where kp:"k\<parallel>p" and kr:"k\<parallel>r" and kq:"k\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<parallel> p; k \<parallel> r; k \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s M1
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<parallel> p; k \<parallel> r; k \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> r
k \<parallel> q

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
from \<open>(p,q)\<in>s^-1\<close> \<open>(q,r) \<in> s\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s
[PROOF STEP]
obtain u u' where pu:"p\<parallel>u" and  rup:"r\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s\<inverse>
(q, r) \<in> s
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
r \<parallel> u'
[PROOF STEP]
have "p\<parallel>u' \<oplus> ((\<exists>t. p\<parallel>t \<and> t\<parallel>u') \<oplus> (\<exists>t. r\<parallel>t \<and> t\<parallel>u))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?p \<parallel> ?s \<oplus> ((\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?s) \<oplus> (\<exists>t. ?r \<parallel> t \<and> t \<parallel> ?q))

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
have "(?A\<and>\<not>?B\<and>\<not>?C) \<or> ((\<not>?A\<and>?B\<and>\<not>?C) \<or> (\<not>?A\<and>\<not>?B\<and>?C))"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O s \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
thus "x \<in> e \<union> s \<union> s^-1"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "?A\<and>\<not>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?A
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. p \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<parallel> u'

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with rup kp kr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'
[PROOF STEP]
have "p = r"
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'

goal (1 subgoal):
 1. p = r
[PROOF STEP]
using M4
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?q \<parallel> ?s; ?p \<parallel> ?r; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?q = ?r

goal (1 subgoal):
 1. p = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = r

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = r

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x e
[PROOF STATE]
proof (prove)
using this:
p = r
x = (p, r)
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "\<not>?A\<and>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?B
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
obtain t where kt:"p\<parallel>t" and tr:"t\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>p \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<parallel> t
t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with rup kp kr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
k \<parallel> p
k \<parallel> r
p \<parallel> t
t \<parallel> u'
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
assume "\<not>?A \<and> \<not>?B \<and> ?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?C
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
obtain t where rtp:"r\<parallel>t" and "t\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>r \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
with pu kp kr
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
k \<parallel> p
k \<parallel> r
r \<parallel> t
t \<parallel> u
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> e \<union> s \<union> s\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> s \<union> s\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmim:"m^-1 O m \<subseteq> s \<union> s^-1 \<union> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O m \<subseteq> s \<union> s\<inverse> \<union> e
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
fix x::"'a\<times>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
assume "x \<in> m^-1 O m"
[PROOF STATE]
proof (state)
this:
x \<in> m\<inverse> O m

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> m\<inverse> O m
[PROOF STEP]
obtain p q r where x:"x = (p,r)" and "(p,q)\<in>m^-1" and "(q,r) \<in>m"
[PROOF STATE]
proof (prove)
using this:
x \<in> m\<inverse> O m

goal (1 subgoal):
 1. (\<And>p r q. \<lbrakk>x = (p, r); (p, q) \<in> m\<inverse>; (q, r) \<in> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (p, r)
(p, q) \<in> m\<inverse>
(q, r) \<in> m

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
from \<open>(p,q)\<in>m^-1\<close> \<open>(q,r) \<in> m\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> m\<inverse>
(q, r) \<in> m
[PROOF STEP]
have qp:"q\<parallel>p" and qr:"q\<parallel>r"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> m\<inverse>
(q, r) \<in> m

goal (1 subgoal):
 1. q \<parallel> p &&& q \<parallel> r
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> m\<inverse>
(q, r) \<in> m
((?p, ?q) \<in> m) = ?p \<parallel> ?q

goal (1 subgoal):
 1. q \<parallel> p &&& q \<parallel> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<parallel> p
q \<parallel> r

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
obtain u u'  where pu:"p\<parallel>u" and  rup:"r\<parallel>u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3 meets_wd qp qr
[PROOF STATE]
proof (prove)
using this:
\<I> ?p \<Longrightarrow> \<exists>q r. q \<parallel> ?p \<and> ?p \<parallel> r
?p \<parallel> ?q \<Longrightarrow> \<I> ?p \<and> \<I> ?q
q \<parallel> p
q \<parallel> r

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>p \<parallel> u; r \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
r \<parallel> u'
[PROOF STEP]
have "p\<parallel>u' \<oplus> ((\<exists>t. p\<parallel>t \<and> t\<parallel>u') \<oplus> (\<exists>t. r\<parallel>t \<and> t\<parallel>u))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?p \<parallel> ?s \<oplus> ((\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?s) \<oplus> (\<exists>t. ?r \<parallel> t \<and> t \<parallel> ?q))

goal (1 subgoal):
 1. p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
have "(?A\<and>\<not>?B\<and>\<not>?C) \<or> ((\<not>?A\<and>?B\<and>\<not>?C) \<or> (\<not>?A\<and>\<not>?B\<and>?C))"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<oplus> (\<exists>t. r \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O m \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
thus "x \<in>  s \<union> s^-1 \<union> e"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
assume "?A\<and>\<not>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?A
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. p \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<parallel> u'

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
with rup qp qr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> u'
[PROOF STEP]
have "p = r"
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> u'

goal (1 subgoal):
 1. p = r
[PROOF STEP]
using M4
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> u'
\<lbrakk>?p \<parallel> ?q; ?q \<parallel> ?s; ?p \<parallel> ?r; ?r \<parallel> ?s\<rbrakk> \<Longrightarrow> ?q = ?r

goal (1 subgoal):
 1. p = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = r

goal (3 subgoals):
 1. p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 3. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = r

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
using x e
[PROOF STATE]
proof (prove)
using this:
p = r
x = (p, r)
((?p, ?q) \<in> e) = (?p = ?q)

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> s\<inverse> \<union> e

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
assume "\<not>?A\<and>?B\<and>\<not>?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?B
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'
[PROOF STEP]
obtain t where kt:"p\<parallel>t" and tr:"t\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> u'

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>p \<parallel> t; t \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<parallel> t
t \<parallel> u'

goal (2 subgoals):
 1. \<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
 2. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
with rup qp qr
[PROOF STATE]
proof (chain)
picking this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> t
t \<parallel> u'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> t
t \<parallel> u'

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
r \<parallel> u'
q \<parallel> p
q \<parallel> r
p \<parallel> t
t \<parallel> u'
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> s\<inverse> \<union> e

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<nexists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
assume "\<not>?A \<and> \<not>?B \<and> ?C"
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)
[PROOF STEP]
have ?C
[PROOF STATE]
proof (prove)
using this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. \<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
obtain t where rtp:"r\<parallel>t" and "t\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. r \<parallel> t \<and> t \<parallel> u

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>r \<parallel> t; t \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. \<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
with pu qp qr
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
q \<parallel> p
q \<parallel> r
r \<parallel> t
t \<parallel> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
q \<parallel> p
q \<parallel> r
r \<parallel> t
t \<parallel> u

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
using x s
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
q \<parallel> p
q \<parallel> r
r \<parallel> t
t \<parallel> u
x = (p, r)
((?p, ?q) \<in> s) = (\<exists>k u v. k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v \<and> k \<parallel> ?q \<and> ?q \<parallel> v)

goal (1 subgoal):
 1. x \<in> s \<union> s\<inverse> \<union> e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> s\<inverse> \<union> e

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> u' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> u') \<and> (\<exists>t. r \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> s \<union> s\<inverse> \<union> e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> s \<union> s\<inverse> \<union> e

goal:
No subgoals!
[PROOF STEP]
qed