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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O f\<inverse> \<Longrightarrow> x \<in> f\<inverse>
[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 kp:"k\<parallel>p" and kl:"k\<parallel>l" and lz:"l\<parallel>z" 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> p; k \<parallel> l; l \<parallel> z; 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> p; k \<parallel> l; l \<parallel> z; p \<parallel> u; z \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> l
l \<parallel> z
p \<parallel> u
z \<parallel> u

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

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

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

goal (1 subgoal):
 1. p \<parallel> u'
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
z \<parallel> u
z \<parallel> u'
p \<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 f\<inverse> \<Longrightarrow> x \<in> f\<inverse>
[PROOF STEP]
from lz kpz kplp
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'
[PROOF STEP]
have "l\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O f\<inverse> \<Longrightarrow> x \<in> f\<inverse>
[PROOF STEP]
with kl lpq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'
[PROOF STEP]
obtain ll where "k\<parallel>ll" and "ll\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O f\<inverse> \<Longrightarrow> x \<in> f\<inverse>
[PROOF STEP]
with kp \<open>p\<parallel>u'\<close> qup
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> p
p \<parallel> u'
q \<parallel> u'
k \<parallel> ll
ll \<parallel> q
[PROOF STEP]
show "x \<in> f^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> p
p \<parallel> u'
q \<parallel> u'
k \<parallel> ll
ll \<parallel> q

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> f\<inverse>
(z, q) \<in> d\<inverse>
[PROOF STEP]
obtain k l u where kp:"k \<parallel> p" and kl:"k\<parallel>l" and lz:"l\<parallel>z" and pu:"p \<parallel>u" and  zu:"z\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> f\<inverse>
(z, q) \<in> d\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' l' u' v' where kpz:"k' \<parallel>z" and kplp:"k' \<parallel>l'" and lpq:"l' \<parallel>q" and  qup:"q \<parallel>u'" and  upvp:"u'\<parallel>v'" and zvp:"z\<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' l' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> l'; l' \<parallel> q; q \<parallel> u'; u' \<parallel> v'; z \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using d \<open>(z,q)\<in>d^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> d\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from lz kpz kplp
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'
[PROOF STEP]
have "l\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with kl lpq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'
[PROOF STEP]
obtain ll where "k\<parallel>ll" and "ll\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<parallel> ll
ll \<parallel> q

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from zu zvp upvp
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> u
z \<parallel> v'
u' \<parallel> v'
[PROOF STEP]
have "u' \<parallel> u "
[PROOF STATE]
proof (prove)
using this:
z \<parallel> u
z \<parallel> v'
u' \<parallel> v'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x kp pu qup d
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u
x = (p, q)
k \<parallel> p
p \<parallel> u
q \<parallel> u'
((?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> d\<inverse>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> d\<inverse>

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s \<Longrightarrow> x \<in> ov
[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 kp:"k\<parallel>p" and kl:"k\<parallel>l" and lz:"l\<parallel>z" 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> p; k \<parallel> l; l \<parallel> z; 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> p; k \<parallel> l; l \<parallel> z; p \<parallel> u; z \<parallel> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<parallel> p
k \<parallel> l
l \<parallel> z
p \<parallel> u
z \<parallel> u

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

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

goal (1 subgoal):
 1. (\<And>k' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> q; 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> z
k' \<parallel> q
z \<parallel> u'
u' \<parallel> v'
q \<parallel> v'

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s \<Longrightarrow> x \<in> ov
[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 s \<Longrightarrow> x \<in> ov
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<parallel> u'

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
from lz kpz kpq
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> q
[PROOF STEP]
have lq:"l\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> q

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s \<Longrightarrow> x \<in> ov
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<parallel> u'
l \<parallel> q
[PROOF STEP]
show "x \<in> ov"
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u'
l \<parallel> q

goal (1 subgoal):
 1. x \<in> ov
[PROOF STEP]
using x lz zup kp kl upvp upvp ov qvp
[PROOF STATE]
proof (prove)
using this:
p \<parallel> u'
l \<parallel> q
x = (p, q)
l \<parallel> z
z \<parallel> u'
k \<parallel> p
k \<parallel> l
u' \<parallel> v'
u' \<parallel> v'
((?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)
q \<parallel> v'

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> f\<inverse>
(z, q) \<in> s\<inverse>
[PROOF STEP]
obtain k l u where kp:"k \<parallel> p" and kl:"k\<parallel>l" and lz:"l\<parallel>z"  and pu:"p \<parallel>u" and  zu:"z\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> f\<inverse>
(z, q) \<in> s\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' u' v' where kpz:"k' \<parallel>z" and kpq:"k' \<parallel>q" and qup:"q \<parallel>u'" and  upvp:"u'\<parallel>v'" and  zvp:"z\<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> q; q \<parallel> u'; u' \<parallel> v'; z \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s \<open>(z,q): s^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> s\<inverse>

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u' \<parallel> u

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from lz kpz kpq
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> q
[PROOF STEP]
have "l \<parallel>q "
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> q

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u' \<parallel> u
l \<parallel> q
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
u' \<parallel> u
l \<parallel> q

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> f\<inverse>
[PROOF STEP]
obtain k l u v  where kp:"k \<parallel> p" and kl:"k\<parallel>l" and lz:"l\<parallel>z" and zu:"z \<parallel>u" and uv:"u\<parallel>v" and pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> f\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' l' u' where kpz:"k' \<parallel>z" and kplp:"k' \<parallel>l'" and lpq:"l' \<parallel>q" and  qup:"q \<parallel>u'" and zup:"z\<parallel>u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' l' u'. \<lbrakk>k' \<parallel> z; k' \<parallel> l'; l' \<parallel> q; q \<parallel> u'; z \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f \<open>(z,q): f^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> f\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from lz kpz kplp
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'
[PROOF STEP]
have "l\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with kl lpq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'
[PROOF STEP]
obtain ll where "k\<parallel>ll" and "ll\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<parallel> ll
ll \<parallel> q

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> ll
ll \<parallel> q
q \<parallel> u
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
q \<parallel> u

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x d kp uv pv
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
q \<parallel> u
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)
k \<parallel> p
u \<parallel> v
p \<parallel> v

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> d\<inverse>
[PROOF STEP]
obtain k l u v where kp:"k \<parallel> p" and kl:"k\<parallel>l" and lz:"l\<parallel>z" and zu:"z \<parallel>u" and uv:"u\<parallel>v" and pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> d\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' l' u' v' where kpz:"k' \<parallel>z" and kplp:"k' \<parallel>l'" and lpq:"l' \<parallel>q" and  qup:"q \<parallel>u'" and upvp:"u' \<parallel>v'" and zvp:"z \<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' l' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> l'; l' \<parallel> q; q \<parallel> u'; u' \<parallel> v'; z \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using d \<open>(z,q): d^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> d\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from lz kpz kplp
[PROOF STATE]
proof (chain)
picking this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'
[PROOF STEP]
have "l\<parallel>l'"
[PROOF STATE]
proof (prove)
using this:
l \<parallel> z
k' \<parallel> z
k' \<parallel> l'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with kl lpq
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'
[PROOF STEP]
obtain ll where "k\<parallel>ll" and "ll\<parallel>q"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l
l' \<parallel> q
l \<parallel> l'

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<parallel> ll
ll \<parallel> q

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from zvp zu upvp
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> v'
z \<parallel> u
u' \<parallel> v'
[PROOF STEP]
have "u' \<parallel> u "
[PROOF STATE]
proof (prove)
using this:
z \<parallel> v'
z \<parallel> u
u' \<parallel> v'

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u' \<parallel> u

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with qup uv
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u
[PROOF STEP]
obtain uu where "q\<parallel>uu" and "uu\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u
q \<parallel> uu
uu \<parallel> v
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u
q \<parallel> uu
uu \<parallel> v

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x d kp pv
[PROOF STATE]
proof (prove)
using this:
k \<parallel> ll
ll \<parallel> q
u' \<parallel> u
q \<parallel> uu
uu \<parallel> v
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)
k \<parallel> p
p \<parallel> v

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> s\<inverse>
[PROOF STEP]
obtain k l  u v where kp:"k \<parallel>p" and kl:"k\<parallel>l"  and lz:"l\<parallel>z" and zu:"z\<parallel>u" and uv:"u\<parallel>v" and pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> d\<inverse>
(z, q) \<in> s\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' u' v' where kpz:"k' \<parallel>z" and kpq:"k' \<parallel>q" and  qup:"q \<parallel>u'" and upvp:"u' \<parallel>v'" and zvp:"z \<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> q; q \<parallel> u'; u' \<parallel> v'; z \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s \<open>(z,q): s^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> s\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from upvp zvp zu
[PROOF STATE]
proof (chain)
picking this:
u' \<parallel> v'
z \<parallel> v'
z \<parallel> u
[PROOF STEP]
have "u'\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
u' \<parallel> v'
z \<parallel> v'
z \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with qup uv
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u
[PROOF STEP]
obtain uu where "q\<parallel>uu" and "uu\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<parallel> uu
uu \<parallel> v

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from kpz lz kpq
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> z
l \<parallel> z
k' \<parallel> q
[PROOF STEP]
have "l \<parallel>q "
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> z
l \<parallel> z
k' \<parallel> q

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> d\<inverse> O s\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> uu
uu \<parallel> v
l \<parallel> q
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> uu
uu \<parallel> v
l \<parallel> q

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x d kp kl pv
[PROOF STATE]
proof (prove)
using this:
q \<parallel> uu
uu \<parallel> v
l \<parallel> q
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)
k \<parallel> p
k \<parallel> l
p \<parallel> v

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma csb:"s O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O b \<subseteq> b
[PROOF STEP]
apply (auto simp:s b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k t u v. \<lbrakk>k \<parallel> x; y \<parallel> t; t \<parallel> z; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1 M5exist_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
\<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>x y z k t u v. \<lbrakk>k \<parallel> x; y \<parallel> t; t \<parallel> z; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma csm:"s O m \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O m \<subseteq> b
[PROOF STEP]
apply (auto simp:s m b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>y \<parallel> z; k \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k u v. \<lbrakk>y \<parallel> z; k \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>k' u' v'. \<lbrakk>k' \<parallel> q; k' \<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> q
k' \<parallel> z
z \<parallel> u'
u' \<parallel> v'
q \<parallel> v'

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O s \<Longrightarrow> x \<in> s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k' \<parallel> p

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O s \<Longrightarrow> x \<in> s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<parallel> u'

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s O s \<Longrightarrow> x \<in> s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k' \<parallel> p
u \<parallel> u'
p \<parallel> uu
uu \<parallel> v'
[PROOF STEP]
show "x \<in> s"
[PROOF STATE]
proof (prove)
using this:
k' \<parallel> p
u \<parallel> u'
p \<parallel> uu
uu \<parallel> v'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> s\<inverse>
(z, q) \<in> f\<inverse>
[PROOF STEP]
obtain k u v where kp:"k \<parallel> p" and kz:"k\<parallel>z" and zu:"z \<parallel>u" and uv:"u\<parallel>v" and pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> s\<inverse>
(z, q) \<in> f\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' l' u' where kpz:"k' \<parallel>z" and kplp:"k' \<parallel>l'" and lpq:"l' \<parallel>q"  and zup:"z\<parallel>u'" and qup:"q\<parallel>u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' l' u'. \<lbrakk>k' \<parallel> z; k' \<parallel> l'; l' \<parallel> q; z \<parallel> u'; q \<parallel> u'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f \<open>(z,q): f^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> f\<inverse>

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

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<parallel> l'

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

goal (1 subgoal):
 1. q \<parallel> u
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
q \<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. q \<parallel> u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<parallel> u

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O f\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k \<parallel> l'
q \<parallel> u
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l'
q \<parallel> u

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x d kp lpq pv uv
[PROOF STATE]
proof (prove)
using this:
k \<parallel> l'
q \<parallel> u
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)
k \<parallel> p
l' \<parallel> q
p \<parallel> v
u \<parallel> v

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (p, q)
(p, z) \<in> s\<inverse>
(z, q) \<in> d\<inverse>
[PROOF STEP]
obtain k u v where kp:"k \<parallel> p" and kz:"k\<parallel>z"  and zu:"z \<parallel>u" and uv:"u\<parallel>v" and pv:"p\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
x = (p, q)
(p, z) \<in> s\<inverse>
(z, q) \<in> d\<inverse>

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
obtain k' l' u' v' where kpz:"k' \<parallel>z" and kplp:"k' \<parallel>l'" and lpq:"l'\<parallel>q" and qup:"q \<parallel>u'" and upvp:"u' \<parallel>v'" and zvp:"z\<parallel>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' l' u' v'. \<lbrakk>k' \<parallel> z; k' \<parallel> l'; l' \<parallel> q; q \<parallel> u'; u' \<parallel> v'; z \<parallel> v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using d \<open>(z,q): d^-1\<close>
[PROOF STATE]
proof (prove)
using this:
((?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)
(z, q) \<in> d\<inverse>

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
from zvp upvp zu
[PROOF STATE]
proof (chain)
picking this:
z \<parallel> v'
u' \<parallel> v'
z \<parallel> u
[PROOF STEP]
have "u'\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
z \<parallel> v'
u' \<parallel> v'
z \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
with qup uv
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u
[PROOF STEP]
obtain uu where "q\<parallel>uu" and "uu\<parallel>v"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> u'
u \<parallel> v
u' \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<parallel> uu
uu \<parallel> v

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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> s\<inverse> O d\<inverse> \<Longrightarrow> x \<in> d\<inverse>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<parallel> uu
uu \<parallel> v
k \<parallel> l'
[PROOF STEP]
show "x \<in> d^-1"
[PROOF STATE]
proof (prove)
using this:
q \<parallel> uu
uu \<parallel> v
k \<parallel> l'

goal (1 subgoal):
 1. x \<in> d\<inverse>
[PROOF STEP]
using x d kp lpq pv
[PROOF STATE]
proof (prove)
using this:
q \<parallel> uu
uu \<parallel> v
k \<parallel> l'
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)
k \<parallel> p
l' \<parallel> q
p \<parallel> v

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdb:"d O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O b \<subseteq> b
[PROOF STEP]
apply (auto simp:d b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k t l u v. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1 M5exist_var
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s
\<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>x y z k t l u v. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cdm:"d O m \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O m \<subseteq> b
[PROOF STEP]
apply (auto simp:d m b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k l u v. \<lbrakk>y \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k l u v. \<lbrakk>y \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; u \<parallel> v; k \<parallel> y; y \<parallel> v\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


[STATEMENT]
lemma cfb:"f O b \<subseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O b \<subseteq> b
[PROOF STEP]
apply (auto simp:f b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z k t l u. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; k \<parallel> y; y \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
using M1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p \<parallel> ?q; ?p \<parallel> ?s; ?r \<parallel> ?q\<rbrakk> \<Longrightarrow> ?r \<parallel> ?s

goal (1 subgoal):
 1. \<And>x y z k t l u. \<lbrakk>y \<parallel> t; t \<parallel> z; k \<parallel> l; l \<parallel> x; x \<parallel> u; k \<parallel> y; y \<parallel> u\<rbrakk> \<Longrightarrow> \<exists>t. x \<parallel> t \<and> t \<parallel> z
[PROOF STEP]
by blast


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

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f O m \<Longrightarrow> x \<in> m
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
(p, z) \<in> f
[PROOF STEP]
obtain u where pu:"p\<parallel>u" and zu:"z\<parallel>u"
[PROOF STATE]
proof (prove)
using this:
(p, z) \<in> f

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

goal (1 subgoal):
 1. \<And>x. x \<in> f O m \<Longrightarrow> x \<in> m
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
(z, q) \<in> m
p \<parallel> u
z \<parallel> u
[PROOF STEP]
have "(p,q) \<in> m"
[PROOF STATE]
proof (prove)
using this:
(z, q) \<in> m
p \<parallel> u
z \<parallel> u

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> f O m \<Longrightarrow> x \<in> m
[PROOF STEP]
thus "x\<in> m"
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> m

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

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

goal:
No subgoals!
[PROOF STEP]
qed