[STATEMENT]
lemma bind_assoc_SBE: "(y :\<equiv> (x :\<equiv> m; k); h) = (x :\<equiv> m; (y :\<equiv> k; h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( y :\<equiv>  x :\<equiv> m; k; h) = ( x :\<equiv> m;  y :\<equiv> k; h)
[PROOF STEP]
proof (rule ext, simp add: unit_SBE_def bind_SBE_def, rename_tac x,
    case_tac "m x", simp_all add: Let_def Set.image_iff, safe,goal_cases)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; (ac, bb) \<in> a; None = k bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 4. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 5. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 6. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (1 x a aa b ab ba a b)
[PROOF STATE]
proof (state)
this:
m x = Some a__
(aa, b__) \<in> a__
(ab, ba) \<in> the (k b__)
None = h ba
(a, b) \<in> a__
None = k b

goal (6 subgoals):
 1. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; (ac, bb) \<in> a; None = k bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 4. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 5. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 6. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a__
(aa, b__) \<in> a__
(ab, ba) \<in> the (k b__)
None = h ba
(a, b) \<in> a__
None = k b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a__
(aa, b__) \<in> a__
(ab, ba) \<in> the (k b__)
None = h ba
(a, b) \<in> a__
None = k b

goal (1 subgoal):
 1. \<exists>x\<in>a__. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
by(rule_tac x="(a, b)" in bexI, simp_all)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>a__. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (5 subgoals):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 4. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 5. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 4. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 5. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (2 x a aa b ab ba)
[PROOF STATE]
proof (state)
this:
m x = Some a
(aa, b) \<in> a
(ab, ba) \<in> the (k b)
None = h ba
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)

goal (5 subgoals):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 4. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 5. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a
(aa, b) \<in> a
(ab, ba) \<in> the (k b)
None = h ba
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a
(aa, b) \<in> a
(ab, ba) \<in> the (k b)
None = h ba
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)

goal (1 subgoal):
 1. \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>a. None \<noteq> k (snd x); m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba\<rbrakk> \<Longrightarrow> None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (erule_tac x="(aa,b)" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; None \<noteq> k (snd (aa, b))\<rbrakk> \<Longrightarrow> None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<lbrakk>m x = Some a; (aa, b) \<in> a; (ab, ba) \<in> the (k b); None = h ba; (aa, b) \<notin> a\<rbrakk> \<Longrightarrow> None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (auto simp: aux image_def split_def intro!: rev_bexI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (4 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 3. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 4. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 3. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 4. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (3 x a a b)
[PROOF STATE]
proof (state)
this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
(a, b) \<in> a__
None = k b

goal (4 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; None = k b\<rbrakk> \<Longrightarrow> \<exists>x\<in>a. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 3. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 4. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
(a, b) \<in> a__
None = k b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
(a, b) \<in> a__
None = k b

goal (1 subgoal):
 1. \<exists>x\<in>a__. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
by(rule_tac x="(a, b)" in bexI, simp_all)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>a__. None = (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (3 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 3. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 3. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (4 x a aa b)
[PROOF STATE]
proof (state)
this:
m x = Some a
\<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
(aa, b) \<in> a
None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (3 subgoals):
 1. \<And>x a aa b. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 3. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a
\<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
(aa, b) \<in> a
None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a
\<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
(aa, b) \<in> a
None = (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (erule_tac Q="None = X" for X in contrapos_pp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); (aa, b) \<in> a; \<not> False\<rbrakk> \<Longrightarrow> None \<noteq> (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (erule_tac x="(aa,b)" and P="\<lambda> x. None \<noteq> case_prod (\<lambda>out. k) x" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; \<not> False; None \<noteq> (case (aa, b) of (out, x) \<Rightarrow> k x)\<rbrakk> \<Longrightarrow> None \<noteq> (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (aa, b) \<in> a; \<not> False; (aa, b) \<notin> a\<rbrakk> \<Longrightarrow> None \<noteq> (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (auto simp: aux image_def split_def intro!: rev_bexI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 2. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 2. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (5 x a aa b ab ba a b)
[PROOF STATE]
proof (state)
this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(ab, ba) \<in> a__
(a, b) \<in> the (k ba)
(aa, b__) \<in> the (h b)

goal (2 subgoals):
 1. \<And>x a aa b ab ba ac bb. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (ac, bb) \<in> the (k ba); (aa, b) \<in> the (h bb)\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>a\<in>a. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
 2. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(ab, ba) \<in> a__
(a, b) \<in> the (k ba)
(aa, b__) \<in> the (h b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(ab, ba) \<in> a__
(a, b) \<in> the (k ba)
(aa, b__) \<in> the (h b)

goal (1 subgoal):
 1. (aa, b__) \<in> (\<Union>a\<in>a__. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some a__; \<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a__; (a, b) \<in> the (k ba); (aa, b__) \<in> the (h b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply ((erule_tac x="(ab,ba)" in ballE)+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m x = Some a__; (ab, ba) \<in> a__; (a, b) \<in> the (k ba); (aa, b__) \<in> the (h b); \<forall>x\<in>the (case (ab, ba) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); None \<noteq> (case (ab, ba) of (out, x) \<Rightarrow> k x); None \<noteq> (case (ab, ba) of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 2. \<lbrakk>m x = Some a__; (ab, ba) \<in> a__; (a, b) \<in> the (k ba); (aa, b__) \<in> the (h b); \<forall>x\<in>the (case (ab, ba) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); None \<noteq> (case (ab, ba) of (out, x) \<Rightarrow> k x); (ab, ba) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 3. \<lbrakk>m x = Some a__; \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a__; (a, b) \<in> the (k ba); (aa, b__) \<in> the (h b); \<forall>x\<in>the (case (ab, ba) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (ab, ba) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
 4. \<lbrakk>m x = Some a__; \<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a__; (a, b) \<in> the (k ba); (aa, b__) \<in> the (h b); (ab, ba) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (simp_all add: aux, (erule exE)+, simp add:split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>m x = Some a__; (ab, ba) \<in> a__; (a, b) \<in> y; (aa, b__) \<in> the (h b); \<forall>x\<in>y. \<exists>y. h (snd x) = Some y; k ba = Some y; (let S' = (\<lambda>x. h (snd x)) ` y in if None \<in> S' then None else Some (\<Union> (the ` S'))) = Some ya\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. (aa, b__) \<in> the (case k (snd x) of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
apply (erule rev_bexI, case_tac "None\<in>(\<lambda>p. h(snd p))`y",auto simp:split_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(aa, b__) \<in> (\<Union>a\<in>a__. the (case a of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))))

goal (1 subgoal):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
case (6 x a aa b a b)
[PROOF STATE]
proof (state)
this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(a, b) \<in> a__
(aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (1 subgoal):
 1. \<And>x a aa b ab ba. \<lbrakk>m x = Some a; \<forall>y\<in>a. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (ab, ba) \<in> a; (aa, b) \<in> the (case k ba of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> (aa, b) \<in> (\<Union>x\<in>a. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(a, b) \<in> a__
(aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m x = Some a__
\<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x)
\<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))
(a, b) \<in> a__
(aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))

goal (1 subgoal):
 1. (aa, b__) \<in> (\<Union>x\<in>a__. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some a__; \<forall>y\<in>a__. \<forall>x\<in>the (case y of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); \<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (a, b) \<in> a__; (aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (case x of (out, x) \<Rightarrow> k x). (aa, b__) \<in> the (case x of (out, x) \<Rightarrow> h x)
[PROOF STEP]
apply ((erule_tac x="(a,b)" in ballE)+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m x = Some a__; (a, b) \<in> a__; (aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); \<forall>x\<in>the (case (a, b) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); None \<noteq> (case (a, b) of (out, x) \<Rightarrow> k x); None \<noteq> (case (a, b) of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S')))\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (case x of (out, x) \<Rightarrow> k x). (aa, b__) \<in> the (case x of (out, x) \<Rightarrow> h x)
 2. \<lbrakk>m x = Some a__; (a, b) \<in> a__; (aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); \<forall>x\<in>the (case (a, b) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); None \<noteq> (case (a, b) of (out, x) \<Rightarrow> k x); (a, b) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (case x of (out, x) \<Rightarrow> k x). (aa, b__) \<in> the (case x of (out, x) \<Rightarrow> h x)
 3. \<lbrakk>m x = Some a__; \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (a, b) \<in> a__; (aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); \<forall>x\<in>the (case (a, b) of (out, x) \<Rightarrow> k x). None \<noteq> (case x of (out, x) \<Rightarrow> h x); (a, b) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (case x of (out, x) \<Rightarrow> k x). (aa, b__) \<in> the (case x of (out, x) \<Rightarrow> h x)
 4. \<lbrakk>m x = Some a__; \<forall>x\<in>a__. None \<noteq> (case x of (out, x) \<Rightarrow> k x); \<forall>x\<in>a__. None \<noteq> (case x of (out, \<sigma>') \<Rightarrow> case k \<sigma>' of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (a, b) \<in> a__; (aa, b__) \<in> the (case k b of None \<Rightarrow> None | Some S \<Rightarrow> let S' = (\<lambda>(out, y). h y) ` S in if None \<in> S' then None else Some (\<Union> (the ` S'))); (a, b) \<notin> a__\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (case x of (out, x) \<Rightarrow> k x). (aa, b__) \<in> the (case x of (out, x) \<Rightarrow> h x)
[PROOF STEP]
apply (simp_all add: aux, (erule exE)+, simp add:split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>m x = Some a__; (a, b) \<in> a__; (aa, b__) \<in> ya; \<forall>x\<in>y. \<exists>y. h (snd x) = Some y; k b = Some y; (let S' = (\<lambda>x. h (snd x)) ` y in if None \<in> S' then None else Some (\<Union> (the ` S'))) = Some ya\<rbrakk> \<Longrightarrow> \<exists>x\<in>a__. \<exists>x\<in>the (k (snd x)). (aa, b__) \<in> the (h (snd x))
[PROOF STEP]
apply (erule rev_bexI, case_tac "None\<in>(\<lambda>p. h(snd p))`y",auto simp:split_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(aa, b__) \<in> (\<Union>x\<in>a__. \<Union>a\<in>the (case x of (out, x) \<Rightarrow> k x). the (case a of (out, x) \<Rightarrow> h x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma src_tab_eq:
    shows "(\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0) \<cdot>
              TfTgh.composite_cell TTfgh_TfTgh.chine TTfgh_TfTgh.the_\<theta> \<cdot> TTfgh_TfTgh.the_\<nu> =
           TTfgh.tab"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
have "TfTgh.composite_cell TTfgh_TfTgh.chine TTfgh_TfTgh.the_\<theta> \<cdot> TTfgh_TfTgh.the_\<nu> =
            (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0) \<cdot> TTfgh.tab"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab
[PROOF STEP]
unfolding TTfgh.tab_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((f \<star> g \<star> h) \<star> arrow_of_spans_of_maps.the_\<theta> (\<cdot>) (\<star>) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h])) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h]] \<cdot> (TfTgh.tab \<star> arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h])) \<cdot> arrow_of_spans_of_maps.the_\<nu> (\<cdot>) (\<star>) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) (arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h]) = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> \<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)
[PROOF STEP]
using TTfgh_TfTgh.chine_is_induced_map TTfgh.tab_def TTfgh_TfTgh.\<Delta>_simps(4)
[PROOF STATE]
proof (prove)
using this:
TTfgh_TfTgh.is_induced_map TTfgh_TfTgh.chine
TTfgh.tab \<equiv> \<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)
local.dom ((\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab) = (tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1

goal (1 subgoal):
 1. (((f \<star> g \<star> h) \<star> arrow_of_spans_of_maps.the_\<theta> (\<cdot>) (\<star>) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h])) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h]] \<cdot> (TfTgh.tab \<star> arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h])) \<cdot> arrow_of_spans_of_maps.the_\<nu> (\<cdot>) (\<star>) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) (arrow_of_tabulations_in_maps.chine (\<cdot>) (\<star>) \<a> \<i> src trg (\<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)) (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) \<a>[f, g, h]) = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> \<a>\<^sup>-\<^sup>1[f \<star> g, h, tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0] \<cdot> ((f \<star> g) \<star> \<a>[h, tab\<^sub>0 h, fg\<^sub>0h\<^sub>1.p\<^sub>0]) \<cdot> ((f \<star> g) \<star> h.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> ((f \<star> g) \<star> fg\<^sub>0h\<^sub>1.\<phi>) \<cdot> \<a>[f \<star> g, tab\<^sub>0 g \<star> f\<^sub>0g\<^sub>1.p\<^sub>0, fg\<^sub>0h\<^sub>1.p\<^sub>1] \<cdot> (Tfg.\<rho>\<sigma>.tab \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
have "iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)
[PROOF STEP]
by (simp add: fg gh)
[PROOF STATE]
proof (state)
this:
local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
have "inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab
local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)
local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab
local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)
local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
using TTfgh_TfTgh.\<Delta>_simps(1)
              invert_side_of_triangle(1)
                [of "TfTgh.composite_cell TTfgh_TfTgh.chine TTfgh_TfTgh.the_\<theta> \<cdot> TTfgh_TfTgh.the_\<nu>"
                    "\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> TTfgh.p\<^sub>0" TTfgh.tab]
[PROOF STATE]
proof (prove)
using this:
(((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab
local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)
local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) = \<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0
seq (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) TTfgh.tab
\<lbrakk>seq (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) TTfgh_TfTgh.the_\<nu>; (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> TTfgh.tab = (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu>; local.iso (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)\<rbrakk> \<Longrightarrow> seq (local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0)) ((((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu>) \<and> TTfgh.tab = local.inv (\<a>[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu>

goal (1 subgoal):
 1. (\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(\<a>\<^sup>-\<^sup>1[f, g, h] \<star> tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<cdot> (((f \<star> g \<star> h) \<star> TTfgh_TfTgh.the_\<theta>) \<cdot> \<a>[f \<star> g \<star> h, (tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0, TTfgh_TfTgh.chine] \<cdot> (TfTgh.tab \<star> TTfgh_TfTgh.chine)) \<cdot> TTfgh_TfTgh.the_\<nu> = TTfgh.tab

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma single_row_inv:
  "j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
proof (induction j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j' < 0 \<Longrightarrow> fwi m n k i' 0 i' j' = fwi m n k i' j' i' j'
 2. \<And>j. \<lbrakk>j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'; j' < Suc j\<rbrakk> \<Longrightarrow> fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j' < 0

goal (2 subgoals):
 1. j' < 0 \<Longrightarrow> fwi m n k i' 0 i' j' = fwi m n k i' j' i' j'
 2. \<And>j. \<lbrakk>j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'; j' < Suc j\<rbrakk> \<Longrightarrow> fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
j' < 0

goal (1 subgoal):
 1. fwi m n k i' 0 i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fwi m n k i' 0 i' j' = fwi m n k i' j' i' j'

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'; j' < Suc j\<rbrakk> \<Longrightarrow> fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'; j' < Suc j\<rbrakk> \<Longrightarrow> fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'
j' < Suc j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'; j' < Suc j\<rbrakk> \<Longrightarrow> fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
j' < j \<Longrightarrow> fwi m n k i' j i' j' = fwi m n k i' j' i' j'
j' < Suc j

goal (1 subgoal):
 1. fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'
[PROOF STEP]
by (cases "j' = j") (simp add: fw_upd_def upd_def)+
[PROOF STATE]
proof (state)
this:
fwi m n k i' (Suc j) i' j' = fwi m n k i' j' i' j'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fwi_canonical_id:
  "fwi M n k i j = M" if "canonical_subs n {k} M" "i \<le> n" "j \<le> n" "k \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fwi M n k i j = M
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
canonical_subs n {k} M
i \<le> n
j \<le> n
k \<le> n

goal (1 subgoal):
 1. fwi M n k i j = M
[PROOF STEP]
proof (induction i arbitrary: j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>canonical_subs n {k} M; 0 \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k 0 j = M
 2. \<And>i j. \<lbrakk>\<And>j. \<lbrakk>canonical_subs n {k} M; i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i j = M; canonical_subs n {k} M; Suc i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k (Suc i) j = M
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
canonical_subs n {k} M
0 \<le> n
j \<le> n
k \<le> n

goal (2 subgoals):
 1. \<And>j. \<lbrakk>canonical_subs n {k} M; 0 \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k 0 j = M
 2. \<And>i j. \<lbrakk>\<And>j. \<lbrakk>canonical_subs n {k} M; i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i j = M; canonical_subs n {k} M; Suc i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k (Suc i) j = M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
canonical_subs n {k} M
0 \<le> n
j \<le> n
k \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
canonical_subs n {k} M
0 \<le> n
j \<le> n
k \<le> n

goal (1 subgoal):
 1. fwi M n k 0 j = M
[PROOF STEP]
by (induction j) (auto intro: fw_upd_canonical_subs_id)
[PROOF STATE]
proof (state)
this:
fwi M n k 0 j = M

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<And>j. \<lbrakk>canonical_subs n {k} M; i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i j = M; canonical_subs n {k} M; Suc i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k (Suc i) j = M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<And>j. \<lbrakk>canonical_subs n {k} M; i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i j = M; canonical_subs n {k} M; Suc i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k (Suc i) j = M
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
\<lbrakk>canonical_subs n {k} M; i_ \<le> n; ?j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i_ ?j = M
canonical_subs n {k} M
Suc i_ \<le> n
j \<le> n
k \<le> n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<And>j. \<lbrakk>canonical_subs n {k} M; i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i j = M; canonical_subs n {k} M; Suc i \<le> n; j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k (Suc i) j = M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>canonical_subs n {k} M; i_ \<le> n; ?j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i_ ?j = M
canonical_subs n {k} M
Suc i_ \<le> n
j \<le> n
k \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>canonical_subs n {k} M; i_ \<le> n; ?j \<le> n; k \<le> n\<rbrakk> \<Longrightarrow> fwi M n k i_ ?j = M
canonical_subs n {k} M
Suc i_ \<le> n
j \<le> n
k \<le> n

goal (1 subgoal):
 1. fwi M n k (Suc i_) j = M
[PROOF STEP]
by (induction j) (auto intro: fw_upd_canonical_subs_id)
[PROOF STATE]
proof (state)
this:
fwi M n k (Suc i_) j = M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Arden_removes_cl:
  "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rhss (Arden Y yrhs) = rhss yrhs - {Y}
[PROOF STEP]
apply (simp add:Arden_def append_rhs_preserves_cls)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rhss (yrhs - {Trn Y r |r. Trn Y r \<in> yrhs}) = rhss yrhs - {Y}
[PROOF STEP]
by (auto simp: rhss_def)


[STATEMENT]
lemma \<L>_epmty:
  "\<L> empty_reg = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<L> empty_reg = {}
[PROOF STEP]
by (auto simp: \<L>_def empty_gta_lang)


[STATEMENT]
lemma SBHReadUnbuffered':
  "\<lbrakk>buffered_val sb a = None;
    sb' = sb@[Read\<^sub>s\<^sub>b volatile a t (m a)]\<rbrakk>
   \<Longrightarrow>
   (Read volatile a t # is,\<theta>, sb, m, \<D>, \<O>,\<R>, \<S>) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h
          (is,\<theta> (t\<mapsto>m a), sb', m, \<D>, \<O>,\<R>, \<S>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>buffered_val sb a = None; sb' = sb @ [Read\<^sub>s\<^sub>b volatile a t (m a)]\<rbrakk> \<Longrightarrow> (Read volatile a t # is, \<theta>, sb, m, \<D>, \<O>, \<R>, \<S>) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h (is, \<theta>(t \<mapsto> m a), sb', m, \<D>, \<O>, \<R>, \<S>)
[PROOF STEP]
by (simp add: SBHReadUnbuffered)


[STATEMENT]
lemma ltl_Until_Release_con:
  "\<xi> \<Turnstile>\<^sub>c \<phi> R\<^sub>c \<psi> \<longleftrightarrow> (\<not> \<xi> \<Turnstile>\<^sub>c (not\<^sub>c \<phi>) U\<^sub>c (not\<^sub>c \<psi>))"
  "\<xi> \<Turnstile>\<^sub>c \<phi> U\<^sub>c \<psi> \<longleftrightarrow> (\<not> \<xi> \<Turnstile>\<^sub>c (not\<^sub>c \<phi>) R\<^sub>c (not\<^sub>c \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> \<Turnstile>\<^sub>c \<phi> R\<^sub>c \<psi> = (\<not> \<xi> \<Turnstile>\<^sub>c not\<^sub>c \<phi> U\<^sub>c not\<^sub>c \<psi>) &&& \<xi> \<Turnstile>\<^sub>c \<phi> U\<^sub>c \<psi> = (\<not> \<xi> \<Turnstile>\<^sub>c not\<^sub>c \<phi> R\<^sub>c not\<^sub>c \<psi>)
[PROOF STEP]
by auto


[STATEMENT]
lemma subfrmlsn_size:
  "\<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> size \<psi> < size \<phi> \<or> \<psi> = \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> size \<psi> < size \<phi> \<or> \<psi> = \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
lemma d_IN_0 [simp]: "d_IN (\<lambda>_. 0) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (\<lambda>_. 0) x = 0
[PROOF STEP]
by(simp add: d_IN_def)


[STATEMENT]
lemma degree0_coeffs: "degree p = 0 \<Longrightarrow>
  \<exists> a. p = [: a :]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree p = 0 \<Longrightarrow> \<exists>a. p = [:a:]
[PROOF STEP]
by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)


[STATEMENT]
lemma subst_ex_same' [usubst]:
  "mwb_lens x \<Longrightarrow> \<sigma>(x \<mapsto>\<^sub>s v) \<dagger> (\<exists> &x \<bullet> P) = \<sigma> \<dagger> (\<exists> &x \<bullet> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mwb_lens x \<Longrightarrow> \<sigma>(x \<mapsto>\<^sub>s v) \<dagger> (\<exists> &x \<bullet> P) = \<sigma> \<dagger> (\<exists> &x \<bullet> P)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma leftderives_rule_step:
  assumes ld: "leftderives a (u@[N]@v)"
  assumes rule: "(N, w) \<in> \<RR>"
  assumes is_word: "is_word u"
  assumes is_sentence: "is_sentence v"
  shows "leftderives a (u@w@v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
have N_w: "leftderives [N] w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leftderives [N] w
[PROOF STEP]
using rule leftderives_rule
[PROOF STATE]
proof (prove)
using this:
(N, w) \<in> \<RR>
(?N, ?w) \<in> \<RR> \<Longrightarrow> leftderives [?N] ?w

goal (1 subgoal):
 1. leftderives [N] w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
leftderives [N] w

goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leftderives [N] w
[PROOF STEP]
have "leftderives (u@[N]@v) (u@w@v)"
[PROOF STATE]
proof (prove)
using this:
leftderives [N] w

goal (1 subgoal):
 1. leftderives (u @ [N] @ v) (u @ w @ v)
[PROOF STEP]
using leftderives_pad is_word is_sentence
[PROOF STATE]
proof (prove)
using this:
leftderives [N] w
\<lbrakk>leftderives ?\<alpha> ?\<beta>; is_word ?u; is_sentence ?v\<rbrakk> \<Longrightarrow> leftderives (?u @ ?\<alpha> @ ?v) (?u @ ?\<beta> @ ?v)
is_word u
is_sentence v

goal (1 subgoal):
 1. leftderives (u @ [N] @ v) (u @ w @ v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
leftderives (u @ [N] @ v) (u @ w @ v)

goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leftderives (u @ [N] @ v) (u @ w @ v)
[PROOF STEP]
show "leftderives a (u@w@v)"
[PROOF STATE]
proof (prove)
using this:
leftderives (u @ [N] @ v) (u @ w @ v)

goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
using leftderives_trans ld
[PROOF STATE]
proof (prove)
using this:
leftderives (u @ [N] @ v) (u @ w @ v)
\<lbrakk>leftderives ?a ?b; leftderives ?b ?c\<rbrakk> \<Longrightarrow> leftderives ?a ?c
leftderives a (u @ [N] @ v)

goal (1 subgoal):
 1. leftderives a (u @ w @ v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
leftderives a (u @ w @ v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Prefixes_is_prefix: "q \<in> Prefixes p = is_prefix q p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q \<in> Prefixes p) = is_prefix q p
[PROOF STEP]
by (simp add: Prefixes_def)


[STATEMENT]
lemma wp_seq_var: "p \<le> wp x r \<Longrightarrow> r \<le> wp y q \<Longrightarrow> p \<le> wp (x \<cdot> y) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> wp x r; r \<le> wp y q\<rbrakk> \<Longrightarrow> p \<le> wp (x \<cdot> y) q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>p \<le> wp x r; r \<le> wp y q\<rbrakk> \<Longrightarrow> p \<le> wp (x \<cdot> y) q
[PROOF STEP]
assume a1: "p \<le> wp x r"
[PROOF STATE]
proof (state)
this:
p \<le> wp x r

goal (1 subgoal):
 1. \<lbrakk>p \<le> wp x r; r \<le> wp y q\<rbrakk> \<Longrightarrow> p \<le> wp (x \<cdot> y) q
[PROOF STEP]
assume a2: "r \<le> wp y q"
[PROOF STATE]
proof (state)
this:
r \<le> wp y q

goal (1 subgoal):
 1. \<lbrakk>p \<le> wp x r; r \<le> wp y q\<rbrakk> \<Longrightarrow> p \<le> wp (x \<cdot> y) q
[PROOF STEP]
have "\<forall>z. \<not> wp x r \<le> z \<or> p \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. \<not> wp x r \<le> z \<or> p \<le> z
[PROOF STEP]
using a1 dual_order.trans
[PROOF STATE]
proof (prove)
using this:
p \<le> wp x r
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. \<forall>z. \<not> wp x r \<le> z \<or> p \<le> z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>z. \<not> wp x r \<le> z \<or> p \<le> z

goal (1 subgoal):
 1. \<lbrakk>p \<le> wp x r; r \<le> wp y q\<rbrakk> \<Longrightarrow> p \<le> wp (x \<cdot> y) q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z. \<not> wp x r \<le> z \<or> p \<le> z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>z. \<not> wp x r \<le> z \<or> p \<le> z

goal (1 subgoal):
 1. p \<le> wp (x \<cdot> y) q
[PROOF STEP]
using a2 a_antitone mult_isol wp_def wp_seq
[PROOF STATE]
proof (prove)
using this:
\<forall>z. \<not> wp x r \<le> z \<or> p \<le> z
r \<le> wp y q
?x \<le> ?y \<Longrightarrow> ad ?y \<le> ad ?x
?x \<le> ?y \<Longrightarrow> ?z \<cdot> ?x \<le> ?z \<cdot> ?y
wp ?x ?p = ad (?x \<cdot> ad ?p)
wp (?x \<cdot> ?y) ?q = wp ?x (wp ?y ?q)

goal (1 subgoal):
 1. p \<le> wp (x \<cdot> y) q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<le> wp (x \<cdot> y) q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rev_H: "bidel_arc.H G M a' = H" (is ?t1)
    and rev_HM: "bidel_arc.HM G M a' = HM" (is ?t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bidel_arc.H G M a' = H &&& bidel_arc.HM G M a' = HM
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bidel_arc.H G M a' = H
 2. bidel_arc.HM G M a' = HM
[PROOF STEP]
interpret rev: bidel_arc G M a'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bidel_arc G M a'
[PROOF STEP]
using a_in
[PROOF STATE]
proof (prove)
using this:
a \<in> arcs G

goal (1 subgoal):
 1. bidel_arc G M a'
[PROOF STEP]
by unfold_locales simp
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rev.H = H
 2. rev.HM = HM
[PROOF STEP]
show ?t1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev.H = H
[PROOF STEP]
by (rule pre_digraph.equality) (auto simp: rev.verts_H verts_H rev.arcs_H arcs_H
        rev.tail_H tail_H rev.head_H head_H)
[PROOF STATE]
proof (state)
this:
rev.H = H

goal (1 subgoal):
 1. rev.HM = HM
[PROOF STEP]
show ?t2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev.HM = HM
[PROOF STEP]
using G.edge_succ_permutes
[PROOF STATE]
proof (prove)
using this:
edge_succ M permutes arcs G

goal (1 subgoal):
 1. rev.HM = HM
[PROOF STEP]
by (intro pre_map.equality) (auto simp: HM_def rev.HM_def insert_commute
        perm_rem_commutes permutes_conv_has_dom)
[PROOF STATE]
proof (state)
this:
rev.HM = HM

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_sccs_da: "card H.sccs = Suc (card G.sccs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H.sccs = Suc (card G.sccs)
[PROOF STEP]
using H_scc_of_a_not_in ends_in
[PROOF STATE]
proof (prove)
using this:
H.scc_of (tail G a) \<notin> G.sccs_verts
H.scc_of (head G a) \<notin> G.sccs_verts
{tail G a, head G a} \<subseteq> verts G

goal (1 subgoal):
 1. card H.sccs = Suc (card G.sccs)
[PROOF STEP]
unfolding G.card_sccs_verts[symmetric] H.card_sccs_verts[symmetric] scc_verts_da
[PROOF STATE]
proof (prove)
using this:
H.scc_of (tail G a) \<notin> G.sccs_verts
H.scc_of (head G a) \<notin> G.sccs_verts
{tail G a, head G a} \<subseteq> verts G

goal (1 subgoal):
 1. card (G.sccs_verts - {G.scc_of (tail G a)} \<union> {H.scc_of (tail G a), H.scc_of (head G a)}) = Suc (card G.sccs_verts)
[PROOF STEP]
by (simp add: card_insert_if G.finite_sccs_verts scc_of_tail_neq_head card_Suc_Diff1
      G.scc_of_in_sccs_verts del: card_Diff_insert)