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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> ov O f \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from \<open>(z,q) \<in> f\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, q) \<in> f
[PROOF STEP]
obtain k' l' u'  where kpq:"k'\<parallel>q" and kplp:"k'\<parallel>l'" and lpz:"l'\<parallel>z" and qup:"q\<parallel>u'" and zup:"z\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
(z, q) \<in> f

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> ov O f \<Longrightarrow> x \<in> s \<union> ov \<union> d
[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> ov O f \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus "x \<in>  s \<union> ov \<union> d"
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
have ?A
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p)

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

goal (3 subgoals):
 1. k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q
[PROOF STEP]
have "(p,q) \<in> s"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q

goal (1 subgoal):
 1. (p, q) \<in> s
[PROOF STEP]
using s kp qup uu pu
[PROOF STATE]
proof (prove)
using this:
k \<parallel> 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)
k \<parallel> p
q \<parallel> u'
u \<parallel> u'
p \<parallel> u

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
moreover
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
from kpq tq kplp
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> q
t \<parallel> q
k' \<parallel> l'
[PROOF STEP]
have "t\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> q
t \<parallel> q
k' \<parallel> l'

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<parallel> l'

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
from lpz lz lc
[PROOF STATE]
proof (chain)
picking this:
l' \<parallel> z
l \<parallel> z
l \<parallel> c
[PROOF STEP]
have lpc:"l'\<parallel>c"
[PROOF STATE]
proof (prove)
using this:
l' \<parallel> z
l \<parallel> z
l \<parallel> c

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

goal (1 subgoal):
 1. l' \<parallel> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> t
t \<parallel> q
t \<parallel> l'
l' \<parallel> c
[PROOF STEP]
obtain lc where "t\<parallel>lc" and "lc\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> t
t \<parallel> q
t \<parallel> l'
l' \<parallel> c

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> lc
lc \<parallel> u
[PROOF STEP]
have "(p,q) \<in> ov"
[PROOF STATE]
proof (prove)
using this:
t \<parallel> lc
lc \<parallel> u

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov

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

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

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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d

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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> p
[PROOF STEP]
obtain t where "k'\<parallel>t" and "t\<parallel>p"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> p

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

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

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

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

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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> d

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

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

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> s \<union> ov \<union> d

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from \<open>(p,z) \<in> f^-1\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, z) \<in> f\<inverse>
[PROOF STEP]
obtain k l u where "k\<parallel>l" and "l\<parallel>z" and kp:"k\<parallel>p" and pu:"p\<parallel>u" and zu:"z\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
(p, z) \<in> f\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from \<open>(z,q) \<in> d\<close>
[PROOF STATE]
proof (chain)
picking this:
(z, q) \<in> d
[PROOF STEP]
obtain k' l' u' v where kplp:"k'\<parallel>l'" and kpq:"k'\<parallel>q" and lpz:"l'\<parallel>z" and zup:"z\<parallel>u'" and upv:"u'\<parallel>v" and qv:"q\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
(z, q) \<in> d

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
from pu zu zup
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
z \<parallel> u
z \<parallel> u'
[PROOF STEP]
have pup:"p\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
z \<parallel> u
z \<parallel> u'

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[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> f\<inverse> O d \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
thus "x \<in> s \<union> ov \<union> d"
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p)
[PROOF STEP]
have ?A
[PROOF STATE]
proof (prove)
using this:
k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p)

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

goal (3 subgoals):
 1. k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
with pup upv kp qv
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u'
u' \<parallel> v
k \<parallel> p
q \<parallel> v
k \<parallel> q
[PROOF STEP]
have "(p,q) \<in> s"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u'
u' \<parallel> v
k \<parallel> p
q \<parallel> v
k \<parallel> q

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> s

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
from tq kpq kplp
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> q
k' \<parallel> q
k' \<parallel> l'
[PROOF STEP]
have "t\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
t \<parallel> q
k' \<parallel> q
k' \<parallel> l'

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
with lpz zup
[PROOF STATE]
proof (chain)
picking this:
l' \<parallel> z
z \<parallel> u'
t \<parallel> l'
[PROOF STEP]
obtain lpz where "t\<parallel>lpz" and "lpz\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
l' \<parallel> z
z \<parallel> u'
t \<parallel> l'

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
with kp pup upv kt tq qv
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
p \<parallel> u'
u' \<parallel> v
k \<parallel> t
t \<parallel> q
q \<parallel> v
t \<parallel> lpz
lpz \<parallel> u'
[PROOF STEP]
have "(p,q)\<in>ov"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
p \<parallel> u'
u' \<parallel> v
k \<parallel> t
t \<parallel> q
q \<parallel> v
t \<parallel> lpz
lpz \<parallel> u'

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

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

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> s \<union> ov \<union> d
 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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> ov

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

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

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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d

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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[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> s \<union> ov \<union> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> p
[PROOF STEP]
obtain t where "k'\<parallel>t" and "t\<parallel>p"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. k' \<parallel> t \<and> t \<parallel> p

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

goal (1 subgoal):
 1. \<not> k \<parallel> q \<and> (\<nexists>t. k \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. k' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> s \<union> ov \<union> d
[PROOF STEP]
with pup upv kpq qv
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u'
u' \<parallel> v
k' \<parallel> q
q \<parallel> v
k' \<parallel> t
t \<parallel> p
[PROOF STEP]
have "(p,q) \<in> d"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u'
u' \<parallel> v
k' \<parallel> q
q \<parallel> v
k' \<parallel> t
t \<parallel> p

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

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

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> s \<union> ov \<union> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> d

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

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

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> s \<union> ov \<union> d

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f O ov \<Longrightarrow> x \<in> ov \<union> s \<union> d
[PROOF STEP]
from pu zu zup
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u
z \<parallel> u
z \<parallel> u'
[PROOF STEP]
have pup:"p\<parallel>u'"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u
z \<parallel> u
z \<parallel> u'

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

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

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

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

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

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

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

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

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

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

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

goal (3 subgoals):
 1. l \<parallel> q \<and> (\<nexists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
 2. \<not> l \<parallel> q \<and> (\<exists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
 3. \<not> l \<parallel> q \<and> (\<nexists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
[PROOF STEP]
with  lp pup upv qv
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> p
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
l \<parallel> q
[PROOF STEP]
have "(p,q) \<in> s"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> p
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
l \<parallel> q

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

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

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

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<not> l \<parallel> q \<and> (\<exists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
 2. \<not> l \<parallel> q \<and> (\<nexists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
[PROOF STEP]
from tq lpq lpc
[PROOF STATE]
proof (chain)
picking this:
t \<parallel> q
l' \<parallel> q
l' \<parallel> c
[PROOF STEP]
have "t\<parallel>c"
[PROOF STATE]
proof (prove)
using this:
t \<parallel> q
l' \<parallel> q
l' \<parallel> c

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

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

goal (2 subgoals):
 1. \<not> l \<parallel> q \<and> (\<exists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<nexists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
 2. \<not> l \<parallel> q \<and> (\<nexists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
[PROOF STEP]
with lp lt tq pup upv qv cup
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> p
l \<parallel> t
t \<parallel> q
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
c \<parallel> u'
t \<parallel> c
[PROOF STEP]
have "(p,q)\<in>ov"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> p
l \<parallel> t
t \<parallel> q
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
c \<parallel> u'
t \<parallel> c

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> l \<parallel> q \<and> (\<nexists>t. l \<parallel> t \<and> t \<parallel> q) \<and> (\<exists>t. l' \<parallel> t \<and> t \<parallel> p) \<Longrightarrow> x \<in> ov \<union> s \<union> d
[PROOF STEP]
with lpq pup upv qv
[PROOF STATE]
proof (chain)
picking this:
l' \<parallel> q
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
l' \<parallel> t
t \<parallel> p
[PROOF STEP]
have "(p,q) \<in> d"
[PROOF STATE]
proof (prove)
using this:
l' \<parallel> q
p \<parallel> u'
u' \<parallel> v
q \<parallel> v
l' \<parallel> t
t \<parallel> p

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed