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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O b \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
from \<open>(p,z) : m^-1\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, z) \<in> m\<inverse>
[PROOF STEP]
have zp:"z\<parallel>p"
[PROOF STATE]
proof (prove)
using this:
(p, z) \<in> m\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O b \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
from \<open>(z,q) : b\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, q) \<in> b
[PROOF STEP]
obtain w  where  zw:"z\<parallel>w" and wq:"w\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
(z, q) \<in> b

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O b \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
obtain v where pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. p \<parallel> v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3 meets_wd zp
[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
z \<parallel> p

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

goal (1 subgoal):
 1. \<And>x. x \<in> m\<inverse> O b \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
obtain v' where qvp:"q\<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v'. q \<parallel> v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M3 meets_wd wq
[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
w \<parallel> q

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

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

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

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

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

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> v' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 3. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
with zp zw wq qvp
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
q \<parallel> v'
p \<parallel> v'
[PROOF STEP]
have "(p,q) \<in> f^-1"
[PROOF STATE]
proof (prove)
using this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
q \<parallel> v'
p \<parallel> v'

goal (1 subgoal):
 1. (p, q) \<in> f\<inverse>
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
q \<parallel> v'
p \<parallel> v'
((?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\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(p, q) \<in> f\<inverse>

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> v' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. p \<parallel> t \<and> t \<parallel> v'
[PROOF STEP]
obtain t where pt:"p\<parallel>t" and tvp:"t\<parallel>v'"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. p \<parallel> t \<and> t \<parallel> v'

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

goal (2 subgoals):
 1. \<not> p \<parallel> v' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
from pt wq
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> t
w \<parallel> q
[PROOF STEP]
have "p\<parallel>q \<oplus> ((\<exists>t'. p\<parallel>t' \<and> t'\<parallel>q) \<oplus> (\<exists>t'. w\<parallel>t' \<and> t'\<parallel>t))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> t
w \<parallel> q

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

goal (2 subgoals):
 1. \<not> p \<parallel> v' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t))
[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'. w \<parallel> t' \<and> t' \<parallel> t))

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

goal (2 subgoals):
 1. \<not> p \<parallel> v' \<and> (\<exists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<nexists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
thus "x \<in> b \<union> m \<union> ov \<union> f^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<or> \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<or> \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t)

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 3. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 3. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)

goal (3 subgoals):
 1. p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 3. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)
[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'. w \<parallel> t' \<and> t' \<parallel> t)

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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 3. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<parallel> q

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)

goal (2 subgoals):
 1. \<not> p \<parallel> q \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<nexists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)
[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'. w \<parallel> t' \<and> t' \<parallel> t)

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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q

goal (1 subgoal):
 1. x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
using x b
[PROOF STATE]
proof (prove)
using this:
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> q
x = (p, q)
((?p, ?q) \<in> b) = (\<exists>t. ?p \<parallel> t \<and> t \<parallel> ?q)

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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'. w \<parallel> t' \<and> t' \<parallel> t)
[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'. w \<parallel> t' \<and> t' \<parallel> t)

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> q) \<and> (\<exists>t'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
with zp zw wq pt tvp qvp
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
p \<parallel> t
t \<parallel> v'
q \<parallel> v'
w \<parallel> t'
t' \<parallel> t
[PROOF STEP]
have "(p,q) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
p \<parallel> t
t \<parallel> v'
q \<parallel> v'
w \<parallel> t'
t' \<parallel> t

goal (1 subgoal):
 1. (p, q) \<in> ov
[PROOF STEP]
using ov
[PROOF STATE]
proof (prove)
using this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
p \<parallel> t
t \<parallel> v'
q \<parallel> v'
w \<parallel> t'
t' \<parallel> t
((?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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[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 \<union> f\<inverse> \<union> d\<inverse>
[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 \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

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'. w \<parallel> t' \<and> t' \<parallel> t) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> v' \<and> (\<nexists>t. p \<parallel> t \<and> t \<parallel> v') \<and> (\<exists>t. q \<parallel> t \<and> t \<parallel> v) \<Longrightarrow> x \<in> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>
[PROOF STEP]
with zp zw wq pv
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
p \<parallel> v
q \<parallel> t
t \<parallel> v
[PROOF STEP]
have "(p,q) \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
z \<parallel> p
z \<parallel> w
w \<parallel> q
p \<parallel> v
q \<parallel> t
t \<parallel> v

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed