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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> b O b\<inverse> \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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 pc qcp
[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
p \<parallel> c
q \<parallel> c'

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

goal (1 subgoal):
 1. \<And>x. x \<in> b O b\<inverse> \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
then
[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> b O b\<inverse> \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b O b\<inverse> \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
thus "x \<in>?R"
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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 kq:?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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
from pc qcp
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c
q \<parallel> c'
[PROOF STEP]
have "p\<parallel>c' \<oplus> ((\<exists>t'. p\<parallel>t' \<and> t'\<parallel>c') \<oplus> (\<exists>t'. q\<parallel>t' \<and> t'\<parallel>c))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> c
q \<parallel> c'

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

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))
[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> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))

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

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> c' \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 3. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with kp kq qcp
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
k \<parallel> q
q \<parallel> c'
p \<parallel> c'
[PROOF STEP]
have "p = q"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
k \<parallel> q
q \<parallel> c'
p \<parallel> c'

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> c' \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with kq kp qcp
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q
k \<parallel> p
q \<parallel> c'
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
k \<parallel> p
q \<parallel> c'
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c'

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with kq kp pc
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q
k \<parallel> p
p \<parallel> c
\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q
k \<parallel> p
p \<parallel> c
\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
from pc qcp
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c
q \<parallel> c'
[PROOF STEP]
have "p\<parallel>c' \<oplus> ((\<exists>t'. p\<parallel>t' \<and> t'\<parallel>c') \<oplus> (\<exists>t'. q\<parallel>t' \<and> t'\<parallel>c))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> c
q \<parallel> c'

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

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))
[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> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))

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

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> c' \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 3. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with kp qcp kt tq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
q \<parallel> c'
k \<parallel> t
t \<parallel> q
p \<parallel> c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
q \<parallel> c'
k \<parallel> t
t \<parallel> q
p \<parallel> c'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using f x
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
q \<parallel> c'
k \<parallel> t
t \<parallel> q
p \<parallel> c'
((?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)
x = (p, q)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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''. t \<parallel> t'' \<and> t'' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> q \<and> (\<nexists>t''. p \<parallel> t'' \<and> t'' \<parallel> q) \<and> (\<exists>t''. t \<parallel> t'' \<and> t'' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<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> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<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> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t''. p \<parallel> t'' \<and> t'' \<parallel> q) \<and> (\<exists>t''. t \<parallel> t'' \<and> t'' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with pc ptp
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c
p \<parallel> t'
t \<parallel> g
g \<parallel> c
[PROOF STEP]
have "g\<parallel>t'"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> c
p \<parallel> t'
t \<parallel> g
g \<parallel> c

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> q \<and> (\<nexists>t''. p \<parallel> t'' \<and> t'' \<parallel> q) \<and> (\<exists>t''. t \<parallel> t'' \<and> t'' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> g
g \<parallel> c
g \<parallel> t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<parallel> g
g \<parallel> c
g \<parallel> t'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using x ov kt tq kp ptp tpcp qcp
[PROOF STATE]
proof (prove)
using this:
t \<parallel> g
g \<parallel> c
g \<parallel> t'
x = (p, q)
((?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)
k \<parallel> t
t \<parallel> q
k \<parallel> p
p \<parallel> t'
t' \<parallel> c'
q \<parallel> c'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<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''. t \<parallel> t'' \<and> t'' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with kp  kt tq pc
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
k \<parallel> t
t \<parallel> q
p \<parallel> c
q \<parallel> t'
t' \<parallel> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
k \<parallel> t
t \<parallel> q
p \<parallel> c
q \<parallel> t'
t' \<parallel> c

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using d x
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
k \<parallel> t
t \<parallel> q
p \<parallel> c
q \<parallel> t'
t' \<parallel> c
((?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)
x = (p, q)

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

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

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

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<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 kpt:"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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
from  pc qcp
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c
q \<parallel> c'
[PROOF STEP]
have "p\<parallel>c' \<oplus> ((\<exists>t'. p\<parallel>t' \<and> t'\<parallel>c') \<oplus> (\<exists>t'. q\<parallel>t' \<and> t'\<parallel>c))" (is "?A \<oplus> (?B \<oplus> ?C)")
[PROOF STATE]
proof (prove)
using this:
p \<parallel> c
q \<parallel> c'

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

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))
[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> c' \<oplus> ((\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<oplus> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c))

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

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

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

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

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

goal (3 subgoals):
 1. p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> c' \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 3. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with qcp kpt tp kpq
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
p \<parallel> c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
p \<parallel> c'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using x f
[PROOF STATE]
proof (prove)
using this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
p \<parallel> c'
x = (p, 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)

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

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

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

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

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

goal (2 subgoals):
 1. \<not> p \<parallel> c' \<and> (\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<nexists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
 2. \<not> p \<parallel> c' \<and> (\<nexists>t'. p \<parallel> t' \<and> t' \<parallel> c') \<and> (\<exists>t'. q \<parallel> t' \<and> t' \<parallel> c) \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with qcp kpt tp kpq
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using x d
[PROOF STATE]
proof (prove)
using this:
q \<parallel> c'
k' \<parallel> t
t \<parallel> p
k' \<parallel> q
\<exists>t'. p \<parallel> t' \<and> t' \<parallel> c'
x = (p, q)
((?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. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> q \<parallel> p \<and> (\<nexists>t''. q \<parallel> t'' \<and> t'' \<parallel> p) \<and> (\<exists>t''. t \<parallel> t'' \<and> t'' \<parallel> c') \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with qcp qt'
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> c'
q \<parallel> t'
t \<parallel> g
g \<parallel> c'
[PROOF STEP]
have "g\<parallel>t'"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> c'
q \<parallel> t'
t \<parallel> g
g \<parallel> c'

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

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

goal (1 subgoal):
 1. \<not> q \<parallel> p \<and> (\<nexists>t''. q \<parallel> t'' \<and> t'' \<parallel> p) \<and> (\<exists>t''. t \<parallel> t'' \<and> t'' \<parallel> c') \<Longrightarrow> x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
with qt' tpc pc kpq kpt tp tg
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> t'
t' \<parallel> c
p \<parallel> c
k' \<parallel> q
k' \<parallel> t
t \<parallel> p
t \<parallel> g
g \<parallel> t'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<parallel> t'
t' \<parallel> c
p \<parallel> c
k' \<parallel> q
k' \<parallel> t
t \<parallel> p
t \<parallel> g
g \<parallel> t'

goal (1 subgoal):
 1. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
using x ov
[PROOF STATE]
proof (prove)
using this:
q \<parallel> t'
t' \<parallel> c
p \<parallel> c
k' \<parallel> q
k' \<parallel> t
t \<parallel> p
t \<parallel> g
g \<parallel> t'
x = (p, q)
((?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. x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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

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

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

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

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> b \<union> b\<inverse> \<union> m \<union> m\<inverse> \<union> e \<union> ov \<union> ov\<inverse> \<union> s \<union> s\<inverse> \<union> d \<union> d\<inverse> \<union> f \<union> f\<inverse>

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

goal:
No subgoals!
[PROOF STEP]
qed