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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from \<open>(p,z) \<in> s\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, z) \<in> s
[PROOF STEP]
obtain k u v where kp:"k\<parallel>p" and kz:"k\<parallel>z" and  pu:"p\<parallel>u" and uv:"u\<parallel>v" and zv:"z\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
(p, z) \<in> s

goal (1 subgoal):
 1. (\<And>k u v. \<lbrakk>k \<parallel> p; k \<parallel> z; p \<parallel> u; u \<parallel> v; z \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(p, z) \<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>k u v. \<lbrakk>k \<parallel> p; k \<parallel> z; p \<parallel> u; u \<parallel> v; z \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> z
p \<parallel> u
u \<parallel> v
z \<parallel> v

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from  \<open>(z,q) \<in> ov\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, q) \<in> ov
[PROOF STEP]
obtain k' l'  u' v'   where kpz:"k'\<parallel>z"  and kplp:"k'\<parallel>l'" and lpq:"l'\<parallel>q" and zup:"z\<parallel>u'"  and qvp:"q\<parallel>v'" and upvp:"u'\<parallel>v'"
[PROOF STATE]
proof (prove)
using this:
(z, q) \<in> ov

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from  kz kpz kplp
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> z
k' \<parallel> z
k' \<parallel> l'
[PROOF STEP]
have klp:"k\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> z
k' \<parallel> z
k' \<parallel> l'

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

goal (1 subgoal):
 1. k \<parallel> l'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> l'

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from  uv zv zup
[PROOF STATE]
proof (chain)
picking this:
u \<parallel> v
z \<parallel> v
z \<parallel> u'
[PROOF STEP]
have uup:"u\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
u \<parallel> v
z \<parallel> v
z \<parallel> u'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
with pu upvp
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
u' \<parallel> v'
u \<parallel> u'
[PROOF STEP]
obtain uu where puu:"p\<parallel>uu" and uuvp:"uu\<parallel>v'"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
u' \<parallel> v'
u \<parallel> u'

goal (1 subgoal):
 1. (\<And>uu. \<lbrakk>p \<parallel> uu; uu \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M5exist_var
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
u' \<parallel> v'
u \<parallel> u'
\<lbrakk>?x \<parallel> ?y; ?y \<parallel> ?z; ?z \<parallel> ?w\<rbrakk> \<Longrightarrow> \<exists>t. ?x \<parallel> t \<and> t \<parallel> ?w

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

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

goal (1 subgoal):
 1. p \<parallel> q \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
l' \<parallel> q
\<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> q \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> q \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. \<And>x. x \<in> s O ov \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> q \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. l' \<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> q \<oplus> ((\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u))

goal (1 subgoal):
 1. p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<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> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<or> \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u)

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 3. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> q
[PROOF STEP]
have "(p,q) \<in> m"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q

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

goal (1 subgoal):
 1. (p, q) \<in> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, q) \<in> m

goal (3 subgoals):
 1. p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 3. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> m

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> m
x = (p, q)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

goal (2 subgoals):
 1. \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. p \<parallel> t \<and> t \<parallel> q
[PROOF STEP]
have "(p,q) \<in> b"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> q

goal (1 subgoal):
 1. (p, q) \<in> b
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> q
((?p, ?q) \<in> b) = (\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?q)

goal (1 subgoal):
 1. (p, q) \<in> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, q) \<in> b

goal (2 subgoals):
 1. \<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> b

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> b
x = (p, q)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> q \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. l' \<parallel> t \<and> t \<parallel> u
[PROOF STEP]
obtain t where lpt:"l'\<parallel>t" and "t\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. l' \<parallel> t \<and> t \<parallel> u

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
with pu puu
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
p \<parallel> uu
l' \<parallel> t
t \<parallel> u
[PROOF STEP]
have "t\<parallel>uu"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
p \<parallel> uu
l' \<parallel> t
t \<parallel> u

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

goal (1 subgoal):
 1. t \<parallel> uu
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<parallel> uu

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
with lpt kp puu uuvp klp lpq qvp
[PROOF STATE]
proof (chain)
picking this:
l' \<parallel> t
k \<parallel> p
p \<parallel> uu
uu \<parallel> v'
k \<parallel> l'
l' \<parallel> q
q \<parallel> v'
t \<parallel> uu
[PROOF STEP]
have "(p,q) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
l' \<parallel> t
k \<parallel> p
p \<parallel> uu
uu \<parallel> v'
k \<parallel> l'
l' \<parallel> q
q \<parallel> v'
t \<parallel> uu

goal (1 subgoal):
 1. (p, q) \<in> ov
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
l' \<parallel> t
k \<parallel> p
p \<parallel> uu
uu \<parallel> v'
k \<parallel> l'
l' \<parallel> q
q \<parallel> v'
t \<parallel> uu
((?p, ?q) \<in> ov) = (\<exists>k l u v t. (k \<parallel> ?p \<and> ?p \<parallel> u \<and> u \<parallel> v) \<and> (k \<parallel> l \<and> l \<parallel> ?q \<and> ?q \<parallel> v) \<and> l \<parallel> t \<and> t \<parallel> u)

goal (1 subgoal):
 1. (p, q) \<in> ov
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> ov

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov
x = (p, q)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> p \<parallel> q \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. (\<And>p r q. \<lbrakk>x = (p, r); (p, q) \<in> s; (q, r) \<in> f\<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> f\<inverse>

goal (1 subgoal):
 1. \<And>x. x \<in> s O f\<inverse> \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from \<open>(p,q) \<in> s\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> s
[PROOF STEP]
obtain k u v where kp:"k\<parallel>p" and kq:"k\<parallel>q" and  pu:"p\<parallel>u" and uv:"u\<parallel>v"  and qv:"q\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s

goal (1 subgoal):
 1. (\<And>k u v. \<lbrakk>k \<parallel> p; k \<parallel> q; p \<parallel> u; u \<parallel> v; q \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
(p, q) \<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>k u v. \<lbrakk>k \<parallel> p; k \<parallel> q; p \<parallel> u; u \<parallel> v; q \<parallel> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> q
p \<parallel> u
u \<parallel> v
q \<parallel> v

goal (1 subgoal):
 1. \<And>x. x \<in> s O f\<inverse> \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from  \<open>(q,r) \<in> f^-1\<close>
[PROOF STATE]
proof (chain)
picking this:
(q, r) \<in> f\<inverse>
[PROOF STEP]
obtain k' l  v'  where kpq:"k'\<parallel>q"  and kpl:"k'\<parallel>l" and lr:"l\<parallel>r"   and rvp:"r\<parallel>v'" and qvp:"q\<parallel>v'"
[PROOF STATE]
proof (prove)
using this:
(q, r) \<in> f\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O f\<inverse> \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from kpq kpl kq
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q
k' \<parallel> l
k \<parallel> q
[PROOF STEP]
have kl:"k\<parallel>l"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q
k' \<parallel> l
k \<parallel> q

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

goal (1 subgoal):
 1. k \<parallel> l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> l

goal (1 subgoal):
 1. \<And>x. x \<in> s O f\<inverse> \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
from qvp qv uv
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> v'
q \<parallel> v
u \<parallel> v
[PROOF STEP]
have uvp:"u\<parallel>v'"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> v'
q \<parallel> v
u \<parallel> v

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

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

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

goal (1 subgoal):
 1. p \<parallel> r \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<oplus> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
l \<parallel> r
\<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> r \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<oplus> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<parallel> r \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<oplus> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u))

goal (1 subgoal):
 1. \<And>x. x \<in> s O f\<inverse> \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> r \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<oplus> (\<exists>t'. l \<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> r \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<oplus> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u))

goal (1 subgoal):
 1. p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<or> \<not> p \<parallel> r \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<or> \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<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> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<or> \<not> p \<parallel> r \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<or> \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u)

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> r \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 3. \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> r
[PROOF STEP]
have "(p,r) \<in> m"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> r

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

goal (1 subgoal):
 1. (p, r) \<in> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, r) \<in> m

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

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, r) \<in> m
x = (p, r)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

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

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> r \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r
[PROOF STEP]
have "(p,r) \<in> b"
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r

goal (1 subgoal):
 1. (p, r) \<in> b
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r
((?p, ?q) \<in> b) = (\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?q)

goal (1 subgoal):
 1. (p, r) \<in> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, r) \<in> b

goal (2 subgoals):
 1. \<not> p \<parallel> r \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<nexists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
 2. \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, r) \<in> b

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, r) \<in> b
x = (p, r)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
with kp pu uvp kl lr rvp
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
p \<parallel> u
u \<parallel> v'
k \<parallel> l
l \<parallel> r
r \<parallel> v'
l \<parallel> t'
t' \<parallel> u
[PROOF STEP]
have "(p,r) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
p \<parallel> u
u \<parallel> v'
k \<parallel> l
l \<parallel> r
r \<parallel> v'
l \<parallel> t'
t' \<parallel> u

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

goal (1 subgoal):
 1. (p, r) \<in> ov
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, r) \<in> ov

goal (1 subgoal):
 1. \<not> p \<parallel> r \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> r) \<and> (\<exists>t'. l \<parallel> t' \<and> t' \<parallel> u) \<Longrightarrow> x \<in> b \<union> m \<union> ov
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, r) \<in> ov

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(p, r) \<in> ov
x = (p, r)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> m O m\<inverse> \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> m\<inverse>
[PROOF STEP]
have pz:"p\<parallel>z" and qz:"q\<parallel>z"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> m
(z, q) \<in> m\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> m O m\<inverse> \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
obtain k k' where kp:"k\<parallel>p" and kpq:"k'\<parallel>q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k k'. \<lbrakk>k \<parallel> p; k' \<parallel> q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3 meets_wd qz pz
[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> z
p \<parallel> z

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

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

goal (1 subgoal):
 1. k \<parallel> q \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
k' \<parallel> q
\<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. k \<parallel> q \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> q \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))

goal (1 subgoal):
 1. \<And>x. x \<in> m O m\<inverse> \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[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:
k \<parallel> q \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))

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

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

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

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

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

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

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

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

goal (3 subgoals):
 1. k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
 2. \<not> k \<parallel> q \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
 3. \<not> k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q
[PROOF STEP]
have "(p,q) \<in> e"
[PROOF STATE]
proof (prove)
using this:
p = q

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

goal (1 subgoal):
 1. (p, q) \<in> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p, q) \<in> e

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<not> k \<parallel> q \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
 2. \<not> k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> t
t \<parallel> q
[PROOF STEP]
have "(p,q) \<in> f^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> t
t \<parallel> q

goal (1 subgoal):
 1. (p, q) \<in> f\<inverse>
[PROOF STEP]
using f qz pz kp
[PROOF STATE]
proof (prove)
using this:
k \<parallel> t
t \<parallel> q
((?p, ?q) \<in> f) = (\<exists>k l u. k \<parallel> l \<and> l \<parallel> ?p \<and> ?p \<parallel> u \<and> k \<parallel> ?q \<and> ?q \<parallel> u)
q \<parallel> z
p \<parallel> z
k \<parallel> p

goal (1 subgoal):
 1. (p, q) \<in> f\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> f\<inverse>

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
with kpq pz qz
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q
p \<parallel> z
q \<parallel> z
k' \<parallel> t
t \<parallel> p
[PROOF STEP]
have "(p,q)\<in>f"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q
p \<parallel> z
q \<parallel> z
k' \<parallel> t
t \<parallel> p

goal (1 subgoal):
 1. (p, q) \<in> f
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q
p \<parallel> z
q \<parallel> z
k' \<parallel> t
t \<parallel> p
((?p, ?q) \<in> f) = (\<exists>k l u. k \<parallel> l \<and> l \<parallel> ?p \<and> ?p \<parallel> u \<and> k \<parallel> ?q \<and> ?q \<parallel> u)

goal (1 subgoal):
 1. (p, q) \<in> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> f

goal (1 subgoal):
 1. \<not> k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> f \<union> f\<inverse> \<union> e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> f

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. k \<parallel> r \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
using M2
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
k' \<parallel> r
\<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. k \<parallel> r \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> r \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))

goal (1 subgoal):
 1. \<And>x. x \<in> f O f\<inverse> \<Longrightarrow> x \<in> e \<union> f \<union> f\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> r \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))
[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:
k \<parallel> r \<oplus> ((\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<oplus> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p))

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

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

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

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

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

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

goal (1 subgoal):
 1. p = r
[PROOF STEP]
using M4
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
r \<parallel> u
k \<parallel> p
k \<parallel> r
\<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. k \<parallel> r \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> r) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> e \<union> f \<union> f\<inverse>
 2. \<not> k \<parallel> r \<and> (\<exists>t. k \<parallel> t \<and> t \<parallel> r) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> e \<union> f \<union> f\<inverse>
 3. \<not> k \<parallel> r \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> r) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> e \<union> f \<union> f\<inverse>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = r

goal (1 subgoal):
 1. x \<in> e \<union> f \<union> f\<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> f \<union> f\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> e \<union> f \<union> f\<inverse>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed