[STATEMENT]
lemma (in det_while_algo) while_proof:
  assumes inv_imp: "\<And>s. \<lbrakk>s\<in>dwa_invar WA; \<not> dwa_cond WA s\<rbrakk> \<Longrightarrow> Q s"
  shows "Q loop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q loop
[PROOF STEP]
apply (unfold loop_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (while (dwa_cond WA) (dwa_step WA) (dwa_initial WA))
[PROOF STEP]
apply (rule_tac P="\<lambda>x. x\<in>dwa_invar WA" and
                  r="{ (dwa_step WA s,s) | s. s\<in>dwa_invar WA \<and> dwa_cond WA s }"
                  in while_rule)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. dwa_initial WA \<in> dwa_invar WA
 2. \<And>s. \<lbrakk>s \<in> dwa_invar WA; dwa_cond WA s\<rbrakk> \<Longrightarrow> dwa_step WA s \<in> dwa_invar WA
 3. \<And>s. \<lbrakk>s \<in> dwa_invar WA; \<not> dwa_cond WA s\<rbrakk> \<Longrightarrow> Q s
 4. wf {(dwa_step WA s, s) |s. s \<in> dwa_invar WA \<and> dwa_cond WA s}
 5. \<And>s. \<lbrakk>s \<in> dwa_invar WA; dwa_cond WA s\<rbrakk> \<Longrightarrow> (dwa_step WA s, s) \<in> {(dwa_step WA s, s) |s. s \<in> dwa_invar WA \<and> dwa_cond WA s}
[PROOF STEP]
apply (simp_all add: step_invar initial_invar step_wf inv_imp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done

  \<comment> \<open>This version is useful when using transferred correctness lemmas\<close>


[STATEMENT]
lemma (in det_while_algo) while_proof':
  assumes inv_imp:
    "\<forall>s. s\<in>wa_invar (det_wa_wa WA) \<and> s\<notin>wa_cond (det_wa_wa WA) \<longrightarrow> Q s"
  shows "Q loop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q loop
[PROOF STEP]
using inv_imp
[PROOF STATE]
proof (prove)
using this:
\<forall>s. s \<in> wa_invar (det_wa_wa WA) \<and> s \<notin> wa_cond (det_wa_wa WA) \<longrightarrow> Q s

goal (1 subgoal):
 1. Q loop
[PROOF STEP]
apply (simp add: det_wa_wa_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. s \<in> dwa_invar WA \<and> \<not> dwa_cond WA s \<longrightarrow> Q s \<Longrightarrow> Q loop
[PROOF STEP]
apply (blast intro: while_proof)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in det_while_algo) loop_invar:
  "loop \<in> dwa_invar WA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loop \<in> dwa_invar WA
[PROOF STEP]
by (rule while_proof) simp


[STATEMENT]
lemma mk_inject [iff]:
  assumes "(f, length ss) \<in> F" and "(g, length ts) \<in> F"
  shows "mk f ss = mk g ts \<longleftrightarrow> f = g \<and> ss = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
assume "mk f ss = mk g ts"
[PROOF STATE]
proof (state)
this:
mk f ss = mk g ts

goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mk f ss = mk g ts
[PROOF STEP]
have "root (mk f ss) = root (mk g ts)"
      and "args (mk f ss) = args (mk g ts)"
[PROOF STATE]
proof (prove)
using this:
mk f ss = mk g ts

goal (1 subgoal):
 1. root (mk f ss) = root (mk g ts) &&& args (mk f ss) = args (mk g ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root (mk f ss) = root (mk g ts)
args (mk f ss) = args (mk g ts)

goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
mk f ss = mk g ts \<Longrightarrow> root (mk f ss) = root (mk g ts)
mk f ss = mk g ts \<Longrightarrow> args (mk f ss) = args (mk g ts)

goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
using root_mk [OF assms(1)] and root_mk [OF assms(2)]
      and args_mk [OF assms(1)] and args_mk [OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
root (mk f ss) = (f, length ss)
root (mk g ts) = (g, length ts)
args (mk f ss) = ss
args (mk g ts) = ts

goal (1 subgoal):
 1. (mk f ss = mk g ts) = (f = g \<and> ss = ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mk f ss = mk g ts) = (f = g \<and> ss = ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma almost_full_on_trees:
  assumes "almost_full_on P F"
  shows "almost_full_on (emb P) trees" (is "almost_full_on ?P ?A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_full_on (emb P) trees
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
interpret mbs ?A
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> almost_full_on (emb P) trees

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
from mbs' [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<in>BAD (emb P). \<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g
[PROOF STEP]
obtain m
    where bad: "m \<in> BAD ?P"
    and min: "\<forall>g. (m, g) \<in> gseq \<longrightarrow> good ?P g"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<in>BAD (emb P). \<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<in> BAD (emb P); \<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
m \<in> BAD (emb P)
\<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> BAD (emb P)
\<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g
[PROOF STEP]
have trees: "\<And>i. m i \<in> trees"
[PROOF STATE]
proof (prove)
using this:
m \<in> BAD (emb P)
\<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g

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

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
define r where "r i = root (m i)" for i
[PROOF STATE]
proof (state)
this:
r ?i = root (m ?i)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
define a where "a i = args (m i)" for i
[PROOF STATE]
proof (state)
this:
a ?i = args (m ?i)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
define S where "S = \<Union>{set (a i) | i. True}"
[PROOF STATE]
proof (state)
this:
S = \<Union> {set (a i) |i. True}

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have m: "\<And>i. m i = mk (fst (r i)) (a i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. m i = mk (fst (r i)) (a i)
[PROOF STEP]
by (simp add: r_def a_def mk_root_args [OF trees])
[PROOF STATE]
proof (state)
this:
m ?i = mk (fst (r ?i)) (a ?i)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have lists: "\<forall>i. a i \<in> lists S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. a i \<in> lists S
[PROOF STEP]
by (auto simp: a_def S_def)
[PROOF STATE]
proof (state)
this:
\<forall>i. a i \<in> lists S

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have arity: "\<And>i. length (a i) = snd (r i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. length (a i) = snd (r i)
[PROOF STEP]
using trees_arity [OF trees]
[PROOF STATE]
proof (prove)
using this:
length (args (m ?i1)) = snd (root (m ?i1))

goal (1 subgoal):
 1. \<And>i. length (a i) = snd (r i)
[PROOF STEP]
by (auto simp: r_def a_def)
[PROOF STATE]
proof (state)
this:
length (a ?i) = snd (r ?i)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (a ?i) = snd (r ?i)
[PROOF STEP]
have sig: "\<And>i. (fst (r i), length (a i)) \<in> F"
[PROOF STATE]
proof (prove)
using this:
length (a ?i) = snd (r ?i)

goal (1 subgoal):
 1. \<And>i. (fst (r i), length (a i)) \<in> F
[PROOF STEP]
using trees_root [OF trees]
[PROOF STATE]
proof (prove)
using this:
length (a ?i) = snd (r ?i)
root (m ?i1) \<in> F

goal (1 subgoal):
 1. \<And>i. (fst (r i), length (a i)) \<in> F
[PROOF STEP]
by (auto simp: a_def r_def)
[PROOF STATE]
proof (state)
this:
(fst (r ?i), length (a ?i)) \<in> F

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have a_trees: "\<And>i. \<forall>t \<in> set (a i). t \<in> trees"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<forall>t\<in>set (a i). t \<in> trees
[PROOF STEP]
by (auto simp: a_def trees_args [OF trees])
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set (a ?i). t \<in> trees

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have "almost_full_on ?P S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_full_on (emb P) S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> almost_full_on (emb P) S

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> almost_full_on (emb P) S
[PROOF STEP]
obtain s :: "nat \<Rightarrow> 'a"
      where S: "\<And>i. s i \<in> S" and bad_s: "bad ?P s"
[PROOF STATE]
proof (prove)
using this:
\<not> almost_full_on (emb P) S

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>\<And>i. s i \<in> S; bad (emb P) s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: almost_full_on_def)
[PROOF STATE]
proof (state)
this:
s ?i \<in> S
bad (emb P) s

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
define n where "n = (LEAST n. \<exists>k. s k \<in> set (a n))"
[PROOF STATE]
proof (state)
this:
n = (LEAST n. \<exists>k. s k \<in> set (a n))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have "\<exists>n. \<exists>k. s k \<in> set (a n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n k. s k \<in> set (a n)
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
s ?i \<in> S

goal (1 subgoal):
 1. \<exists>n k. s k \<in> set (a n)
[PROOF STEP]
by (force simp: S_def)
[PROOF STATE]
proof (state)
this:
\<exists>n k. s k \<in> set (a n)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
from LeastI_ex [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. s k \<in> set (a (LEAST n. \<exists>k. s k \<in> set (a n)))
[PROOF STEP]
obtain k
      where sk: "s k \<in> set (a n)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. s k \<in> set (a (LEAST n. \<exists>k. s k \<in> set (a n)))

goal (1 subgoal):
 1. (\<And>k. s k \<in> set (a n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
s k \<in> set (a n)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have args: "\<And>k. \<exists>m \<ge> n. s k \<in> set (a m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<exists>m\<ge>n. s k \<in> set (a m)
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
s ?i \<in> S

goal (1 subgoal):
 1. \<And>k. \<exists>m\<ge>n. s k \<in> set (a m)
[PROOF STEP]
by (auto simp: S_def) (metis Least_le n_def)
[PROOF STATE]
proof (state)
this:
\<exists>m\<ge>n. s ?k \<in> set (a m)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
define m' where "m' i = (if i < n then m i else s (k + (i - n)))" for i
[PROOF STATE]
proof (state)
this:
m' ?i = (if ?i < n then m ?i else s (k + (?i - n)))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have m'_less: "\<And>i. i < n \<Longrightarrow> m' i = m i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> m' i = m i
[PROOF STEP]
by (simp add: m'_def)
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> m' ?i = m ?i

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have m'_geq: "\<And>i. i \<ge> n \<Longrightarrow> m' i = s (k + (i - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. n \<le> i \<Longrightarrow> m' i = s (k + (i - n))
[PROOF STEP]
by (simp add: m'_def)
[PROOF STATE]
proof (state)
this:
n \<le> ?i \<Longrightarrow> m' ?i = s (k + (?i - n))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have "bad ?P m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bad (emb P) m'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
assume "good ?P m'"
[PROOF STATE]
proof (state)
this:
good (emb P) m'

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
good (emb P) m'
[PROOF STEP]
obtain i j where "i < j" and emb: "?P (m' i) (m' j)"
[PROOF STATE]
proof (prove)
using this:
good (emb P) m'

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; emb P (m' i) (m' j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < j
emb P (m' i) (m' j)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i < j
emb P (m' i) (m' j)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
assume "j < n"
[PROOF STATE]
proof (state)
this:
j < n

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with \<open>i < j\<close> and emb
[PROOF STATE]
proof (chain)
picking this:
i < j
emb P (m' i) (m' j)
j < n
[PROOF STEP]
have "?P (m i) (m j)"
[PROOF STATE]
proof (prove)
using this:
i < j
emb P (m' i) (m' j)
j < n

goal (1 subgoal):
 1. emb P (m i) (m j)
[PROOF STEP]
by (auto simp: m'_less)
[PROOF STATE]
proof (state)
this:
emb P (m i) (m j)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with \<open>i < j\<close> and bad
[PROOF STATE]
proof (chain)
picking this:
i < j
m \<in> BAD (emb P)
emb P (m i) (m j)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
i < j
m \<in> BAD (emb P)
emb P (m i) (m j)

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

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j < n \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < n \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j < n \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
assume "n \<le> i"
[PROOF STATE]
proof (state)
this:
n \<le> i

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with \<open>i < j\<close> and emb
[PROOF STATE]
proof (chain)
picking this:
i < j
emb P (m' i) (m' j)
n \<le> i
[PROOF STEP]
have "?P (s (k + (i - n))) (s (k + (j - n)))"
          and "k + (i - n) < k + (j - n)"
[PROOF STATE]
proof (prove)
using this:
i < j
emb P (m' i) (m' j)
n \<le> i

goal (1 subgoal):
 1. emb P (s (k + (i - n))) (s (k + (j - n))) &&& k + (i - n) < k + (j - n)
[PROOF STEP]
by (auto simp: m'_geq)
[PROOF STATE]
proof (state)
this:
emb P (s (k + (i - n))) (s (k + (j - n)))
k + (i - n) < k + (j - n)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with bad_s
[PROOF STATE]
proof (chain)
picking this:
bad (emb P) s
emb P (s (k + (i - n))) (s (k + (j - n)))
k + (i - n) < k + (j - n)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
bad (emb P) s
emb P (s (k + (i - n))) (s (k + (j - n)))
k + (i - n) < k + (j - n)

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

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
n \<le> i \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<le> i \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n \<le> i \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
assume "i < n" and "n \<le> j"
[PROOF STATE]
proof (state)
this:
i < n
n \<le> j

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with \<open>i < j\<close> and emb
[PROOF STATE]
proof (chain)
picking this:
i < j
emb P (m' i) (m' j)
i < n
n \<le> j
[PROOF STEP]
have *: "?P (m i) (s (k + (j - n)))"
[PROOF STATE]
proof (prove)
using this:
i < j
emb P (m' i) (m' j)
i < n
n \<le> j

goal (1 subgoal):
 1. emb P (m i) (s (k + (j - n)))
[PROOF STEP]
by (auto simp: m'_less m'_geq)
[PROOF STATE]
proof (state)
this:
emb P (m i) (s (k + (j - n)))

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
with args
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<ge>n. s ?k \<in> set (a m)
emb P (m i) (s (k + (j - n)))
[PROOF STEP]
obtain l where "l \<ge> n" and **: "s (k + (j - n)) \<in> set (a l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<ge>n. s ?k \<in> set (a m)
emb P (m i) (s (k + (j - n)))

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>n \<le> l; s (k + (j - n)) \<in> set (a l)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<le> l
s (k + (j - n)) \<in> set (a l)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
from emb.arg [OF sig [of l] _ a_trees [of l] ** *]
[PROOF STATE]
proof (chain)
picking this:
length (a l) = length (a l) \<Longrightarrow> emb P (m i) (mk (fst (r l)) (a l))
[PROOF STEP]
have "?P (m i) (m l)"
[PROOF STATE]
proof (prove)
using this:
length (a l) = length (a l) \<Longrightarrow> emb P (m i) (mk (fst (r l)) (a l))

goal (1 subgoal):
 1. emb P (m i) (m l)
[PROOF STEP]
by (simp add: m)
[PROOF STATE]
proof (state)
this:
emb P (m i) (m l)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emb P (m i) (m l)

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
have "i < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < l
[PROOF STEP]
using \<open>i < n\<close> and \<open>n \<le> l\<close>
[PROOF STATE]
proof (prove)
using this:
i < n
n \<le> l

goal (1 subgoal):
 1. i < l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < l

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
emb P (m i) (m l)
i < l
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
emb P (m i) (m l)
i < l

goal (1 subgoal):
 1. False
[PROOF STEP]
using bad
[PROOF STATE]
proof (prove)
using this:
emb P (m i) (m l)
i < l
m \<in> BAD (emb P)

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

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < n; n \<le> j\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. good (emb P) m' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < n \<Longrightarrow> False
n \<le> i \<Longrightarrow> False
\<lbrakk>i < n; n \<le> j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
j < n \<Longrightarrow> False
n \<le> i \<Longrightarrow> False
\<lbrakk>i < n; n \<le> j\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>i < j\<close>
[PROOF STATE]
proof (prove)
using this:
j < n \<Longrightarrow> False
n \<le> i \<Longrightarrow> False
\<lbrakk>i < n; n \<le> j\<rbrakk> \<Longrightarrow> False
i < j

goal (1 subgoal):
 1. False
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bad (emb P) m'

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bad (emb P) m'

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
have "(m, m') \<in> gseq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
have "m \<in> SEQ ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> SEQ trees
[PROOF STEP]
using trees
[PROOF STATE]
proof (prove)
using this:
m ?i \<in> trees

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

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<in> SEQ trees

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
have "m' \<in> SEQ ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> SEQ trees
[PROOF STEP]
using trees and S and trees_args [OF trees]
[PROOF STATE]
proof (prove)
using this:
m ?i \<in> trees
s ?i \<in> S
?s \<in> set (args (m ?i1)) \<Longrightarrow> ?s \<in> trees

goal (1 subgoal):
 1. m' \<in> SEQ trees
[PROOF STEP]
by (auto simp: m'_def a_def S_def)
[PROOF STATE]
proof (state)
this:
m' \<in> SEQ trees

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m' \<in> SEQ trees

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
have "\<forall>i < n. m i = m' i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. m i = m' i
[PROOF STEP]
by (auto simp: m'_less)
[PROOF STATE]
proof (state)
this:
\<forall>i<n. m i = m' i

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<n. m i = m' i

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
have "size (m' n) < size (m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (m' n) < size (m n)
[PROOF STEP]
using sk and size_arg [OF trees, unfolded m]
[PROOF STATE]
proof (prove)
using this:
s k \<in> set (a n)
?s \<in> set (args (mk (fst (r ?i1)) (a ?i1))) \<Longrightarrow> size ?s < size (mk (fst (r ?i1)) (a ?i1))

goal (1 subgoal):
 1. size (m' n) < size (m n)
[PROOF STEP]
by (auto simp: m m'_geq root_mk [OF sig] args_mk [OF sig])
[PROOF STATE]
proof (state)
this:
size (m' n) < size (m n)

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<in> SEQ trees
m' \<in> SEQ trees
\<forall>i<n. m i = m' i
size (m' n) < size (m n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<in> SEQ trees
m' \<in> SEQ trees
\<forall>i<n. m i = m' i
size (m' n) < size (m n)

goal (1 subgoal):
 1. (m, m') \<in> gseq
[PROOF STEP]
by (auto simp: gseq_def)
[PROOF STATE]
proof (state)
this:
(m, m') \<in> gseq

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(m, m') \<in> gseq

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) S \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bad (emb P) m'
(m, m') \<in> gseq
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
bad (emb P) m'
(m, m') \<in> gseq

goal (1 subgoal):
 1. False
[PROOF STEP]
using min
[PROOF STATE]
proof (prove)
using this:
bad (emb P) m'
(m, m') \<in> gseq
\<forall>g. (m, g) \<in> gseq \<longrightarrow> good (emb P) g

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
almost_full_on (emb P) S

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
from almost_full_on_lists [OF this, THEN almost_full_on_imp_homogeneous_subseq, OF lists]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<phi>. \<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j \<and> list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))
[PROOF STEP]
obtain \<phi> :: "nat \<Rightarrow> nat"
    where less: "\<And>i j. i < j \<Longrightarrow> \<phi> i < \<phi> j"
      and lemb: "\<And>i j. i < j \<Longrightarrow> list_emb ?P (a (\<phi> i)) (a (\<phi> j))"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<phi>. \<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j \<and> list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i j. i < j \<Longrightarrow> \<phi> i < \<phi> j; \<And>i j. i < j \<Longrightarrow> list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?i < ?j \<Longrightarrow> \<phi> ?i < \<phi> ?j
?i < ?j \<Longrightarrow> list_emb (emb P) (a (\<phi> ?i)) (a (\<phi> ?j))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
have roots: "\<And>i. r (\<phi> i) \<in> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. r (\<phi> i) \<in> F
[PROOF STEP]
using trees [THEN trees_root]
[PROOF STATE]
proof (prove)
using this:
root (m ?i1) \<in> F

goal (1 subgoal):
 1. \<And>i. r (\<phi> i) \<in> F
[PROOF STEP]
by (auto simp: r_def)
[PROOF STATE]
proof (state)
this:
r (\<phi> ?i) \<in> F

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r (\<phi> ?i) \<in> F
[PROOF STEP]
have "r \<circ> \<phi> \<in> SEQ F"
[PROOF STATE]
proof (prove)
using this:
r (\<phi> ?i) \<in> F

goal (1 subgoal):
 1. r \<circ> \<phi> \<in> SEQ F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<circ> \<phi> \<in> SEQ F

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
almost_full_on P F
r \<circ> \<phi> \<in> SEQ F
[PROOF STEP]
have "good P (r \<circ> \<phi>)"
[PROOF STATE]
proof (prove)
using this:
almost_full_on P F
r \<circ> \<phi> \<in> SEQ F

goal (1 subgoal):
 1. good P (r \<circ> \<phi>)
[PROOF STEP]
by (auto simp: almost_full_on_def)
[PROOF STATE]
proof (state)
this:
good P (r \<circ> \<phi>)

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
good P (r \<circ> \<phi>)
[PROOF STEP]
obtain i j
    where "i < j" and "P (r (\<phi> i)) (r (\<phi> j))"
[PROOF STATE]
proof (prove)
using this:
good P (r \<circ> \<phi>)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; P (r (\<phi> i)) (r (\<phi> j))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < j
P (r (\<phi> i)) (r (\<phi> j))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
with lemb [OF \<open>i < j\<close>]
[PROOF STATE]
proof (chain)
picking this:
list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))
i < j
P (r (\<phi> i)) (r (\<phi> j))
[PROOF STEP]
have "?P (m (\<phi> i)) (m (\<phi> j))"
[PROOF STATE]
proof (prove)
using this:
list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))
i < j
P (r (\<phi> i)) (r (\<phi> j))

goal (1 subgoal):
 1. emb P (m (\<phi> i)) (m (\<phi> j))
[PROOF STEP]
using sig and arity and a_trees
[PROOF STATE]
proof (prove)
using this:
list_emb (emb P) (a (\<phi> i)) (a (\<phi> j))
i < j
P (r (\<phi> i)) (r (\<phi> j))
(fst (r ?i), length (a ?i)) \<in> F
length (a ?i) = snd (r ?i)
\<forall>t\<in>set (a ?i). t \<in> trees

goal (1 subgoal):
 1. emb P (m (\<phi> i)) (m (\<phi> j))
[PROOF STEP]
by (auto simp: m intro!: emb.list_emb)
[PROOF STATE]
proof (state)
this:
emb P (m (\<phi> i)) (m (\<phi> j))

goal (1 subgoal):
 1. \<not> almost_full_on (emb P) trees \<Longrightarrow> False
[PROOF STEP]
with less [OF \<open>i < j\<close>] and bad
[PROOF STATE]
proof (chain)
picking this:
\<phi> i < \<phi> j
m \<in> BAD (emb P)
emb P (m (\<phi> i)) (m (\<phi> j))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<phi> i < \<phi> j
m \<in> BAD (emb P)
emb P (m (\<phi> i)) (m (\<phi> j))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_emb_trans_right:
  assumes "list_emb P xs ys" and "list_emb (\<lambda>y z. P y z \<and> (\<forall>x. P x y \<longrightarrow> P x z)) ys zs"
  shows "list_emb P xs zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_emb P xs zs
[PROOF STEP]
using assms(2, 1)
[PROOF STATE]
proof (prove)
using this:
list_emb (\<lambda>y z. P y z \<and> (\<forall>x. P x y \<longrightarrow> P x z)) ys zs
list_emb P xs ys

goal (1 subgoal):
 1. list_emb P xs zs
[PROOF STEP]
by (induct arbitrary: xs) (auto elim!: list_emb_Nil2_cases list_emb_Cons_cases)


[STATEMENT]
lemma emb_trans:
  assumes trans: "\<And>f g h. f \<in> F \<Longrightarrow> g \<in> F \<Longrightarrow> h \<in> F \<Longrightarrow> P f g \<Longrightarrow> P g h \<Longrightarrow> P f h"
  assumes "emb P s t" and "emb P t u"
  shows "emb P s u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emb P s u
[PROOF STEP]
using assms(3, 2)
[PROOF STATE]
proof (prove)
using this:
emb P t u
emb P s t

goal (1 subgoal):
 1. emb P s u
[PROOF STEP]
proof (induct arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f m ts t s sa. \<lbrakk>(f, m) \<in> F; length ts = m; \<forall>t\<in>set ts. t \<in> trees; t \<in> set ts; emb P s t; \<And>sa. emb P sa s \<Longrightarrow> emb P sa t; emb P sa s\<rbrakk> \<Longrightarrow> emb P sa (mk f ts)
 2. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
case (arg f m ts v)
[PROOF STATE]
proof (state)
this:
(f, m) \<in> F
length ts = m
\<forall>t\<in>set ts. t \<in> trees
v \<in> set ts
emb P s_ v
emb P ?s s_ \<Longrightarrow> emb P ?s v
emb P s s_

goal (2 subgoals):
 1. \<And>f m ts t s sa. \<lbrakk>(f, m) \<in> F; length ts = m; \<forall>t\<in>set ts. t \<in> trees; t \<in> set ts; emb P s t; \<And>sa. emb P sa s \<Longrightarrow> emb P sa t; emb P sa s\<rbrakk> \<Longrightarrow> emb P sa (mk f ts)
 2. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f, m) \<in> F
length ts = m
\<forall>t\<in>set ts. t \<in> trees
v \<in> set ts
emb P s_ v
emb P ?s s_ \<Longrightarrow> emb P ?s v
emb P s s_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(f, m) \<in> F
length ts = m
\<forall>t\<in>set ts. t \<in> trees
v \<in> set ts
emb P s_ v
emb P ?s s_ \<Longrightarrow> emb P ?s v
emb P s s_

goal (1 subgoal):
 1. emb P s (mk f ts)
[PROOF STEP]
by (auto intro: emb.arg)
[PROOF STATE]
proof (state)
this:
emb P s (mk f ts)

goal (1 subgoal):
 1. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
case (list_emb f m g n ss ts)
[PROOF STATE]
proof (state)
this:
(f, m) \<in> F
(g, n) \<in> F
length ss = m
length ts = n
\<forall>s\<in>set ss. s \<in> trees
\<forall>t\<in>set ts. t \<in> trees
P (f, m) (g, n)
list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts
emb P s (mk f ss)

goal (1 subgoal):
 1. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
note IH = this
[PROOF STATE]
proof (state)
this:
(f, m) \<in> F
(g, n) \<in> F
length ss = m
length ts = n
\<forall>s\<in>set ss. s \<in> trees
\<forall>t\<in>set ts. t \<in> trees
P (f, m) (g, n)
list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts
emb P s (mk f ss)

goal (1 subgoal):
 1. \<And>f m g n ss ts s. \<lbrakk>(f, m) \<in> F; (g, n) \<in> F; length ss = m; length ts = n; \<forall>s\<in>set ss. s \<in> trees; \<forall>t\<in>set ts. t \<in> trees; P (f, m) (g, n); list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts; emb P s (mk f ss)\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
from \<open>emb P s (mk f ss)\<close>
[PROOF STATE]
proof (chain)
picking this:
emb P s (mk f ss)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
emb P s (mk f ss)

goal (1 subgoal):
 1. emb P s (mk g ts)
[PROOF STEP]
proof (cases rule: emb_mk2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa tsa t. \<lbrakk>mk f ss = mk fa tsa; (fa, length tsa) \<in> F; \<forall>t\<in>set tsa. t \<in> trees; t \<in> set tsa; emb P s t\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
 2. \<And>fa ga ssa tsa. \<lbrakk>s = mk fa ssa; mk f ss = mk ga tsa; (fa, length ssa) \<in> F; (ga, length tsa) \<in> F; \<forall>s\<in>set ssa. s \<in> trees; \<forall>t\<in>set tsa. t \<in> trees; P (fa, length ssa) (ga, length tsa); list_emb (emb P) ssa tsa\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
case arg
[PROOF STATE]
proof (state)
this:
mk f ss = mk f_ ts_
(f_, length ts_) \<in> F
\<forall>t\<in>set ts_. t \<in> trees
t_ \<in> set ts_
emb P s t_

goal (2 subgoals):
 1. \<And>fa tsa t. \<lbrakk>mk f ss = mk fa tsa; (fa, length tsa) \<in> F; \<forall>t\<in>set tsa. t \<in> trees; t \<in> set tsa; emb P s t\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
 2. \<And>fa ga ssa tsa. \<lbrakk>s = mk fa ssa; mk f ss = mk ga tsa; (fa, length ssa) \<in> F; (ga, length tsa) \<in> F; \<forall>s\<in>set ssa. s \<in> trees; \<forall>t\<in>set tsa. t \<in> trees; P (fa, length ssa) (ga, length tsa); list_emb (emb P) ssa tsa\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mk f ss = mk f_ ts_
(f_, length ts_) \<in> F
\<forall>t\<in>set ts_. t \<in> trees
t_ \<in> set ts_
emb P s t_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mk f ss = mk f_ ts_
(f_, length ts_) \<in> F
\<forall>t\<in>set ts_. t \<in> trees
t_ \<in> set ts_
emb P s t_

goal (1 subgoal):
 1. emb P s (mk g ts)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
mk f ss = mk f_ ts_
(f_, length ts_) \<in> F
\<forall>t\<in>set ts_. t \<in> trees
t_ \<in> set ts_
emb P s t_
(f, m) \<in> F
(g, n) \<in> F
length ss = m
length ts = n
\<forall>s\<in>set ss. s \<in> trees
\<forall>t\<in>set ts. t \<in> trees
P (f, m) (g, n)
list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts
emb P s (mk f ss)

goal (1 subgoal):
 1. emb P s (mk g ts)
[PROOF STEP]
by (auto elim!: list_emb_set intro: emb.arg)
[PROOF STATE]
proof (state)
this:
emb P s (mk g ts)

goal (1 subgoal):
 1. \<And>fa ga ssa tsa. \<lbrakk>s = mk fa ssa; mk f ss = mk ga tsa; (fa, length ssa) \<in> F; (ga, length tsa) \<in> F; \<forall>s\<in>set ssa. s \<in> trees; \<forall>t\<in>set tsa. t \<in> trees; P (fa, length ssa) (ga, length tsa); list_emb (emb P) ssa tsa\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa ga ssa tsa. \<lbrakk>s = mk fa ssa; mk f ss = mk ga tsa; (fa, length ssa) \<in> F; (ga, length tsa) \<in> F; \<forall>s\<in>set ssa. s \<in> trees; \<forall>t\<in>set tsa. t \<in> trees; P (fa, length ssa) (ga, length tsa); list_emb (emb P) ssa tsa\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
case list_emb
[PROOF STATE]
proof (state)
this:
s = mk f_ ss_
mk f ss = mk g_ ts_
(f_, length ss_) \<in> F
(g_, length ts_) \<in> F
\<forall>s\<in>set ss_. s \<in> trees
\<forall>t\<in>set ts_. t \<in> trees
P (f_, length ss_) (g_, length ts_)
list_emb (emb P) ss_ ts_

goal (1 subgoal):
 1. \<And>fa ga ssa tsa. \<lbrakk>s = mk fa ssa; mk f ss = mk ga tsa; (fa, length ssa) \<in> F; (ga, length tsa) \<in> F; \<forall>s\<in>set ssa. s \<in> trees; \<forall>t\<in>set tsa. t \<in> trees; P (fa, length ssa) (ga, length tsa); list_emb (emb P) ssa tsa\<rbrakk> \<Longrightarrow> emb P s (mk g ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = mk f_ ss_
mk f ss = mk g_ ts_
(f_, length ss_) \<in> F
(g_, length ts_) \<in> F
\<forall>s\<in>set ss_. s \<in> trees
\<forall>t\<in>set ts_. t \<in> trees
P (f_, length ss_) (g_, length ts_)
list_emb (emb P) ss_ ts_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = mk f_ ss_
mk f ss = mk g_ ts_
(f_, length ss_) \<in> F
(g_, length ts_) \<in> F
\<forall>s\<in>set ss_. s \<in> trees
\<forall>t\<in>set ts_. t \<in> trees
P (f_, length ss_) (g_, length ts_)
list_emb (emb P) ss_ ts_

goal (1 subgoal):
 1. emb P s (mk g ts)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
s = mk f_ ss_
mk f ss = mk g_ ts_
(f_, length ss_) \<in> F
(g_, length ts_) \<in> F
\<forall>s\<in>set ss_. s \<in> trees
\<forall>t\<in>set ts_. t \<in> trees
P (f_, length ss_) (g_, length ts_)
list_emb (emb P) ss_ ts_
(f, m) \<in> F
(g, n) \<in> F
length ss = m
length ts = n
\<forall>s\<in>set ss. s \<in> trees
\<forall>t\<in>set ts. t \<in> trees
P (f, m) (g, n)
list_emb (\<lambda>x1 x2. emb P x1 x2 \<and> (\<forall>x. emb P x x1 \<longrightarrow> emb P x x2)) ss ts
emb P s (mk f ss)

goal (1 subgoal):
 1. emb P s (mk g ts)
[PROOF STEP]
by (auto intro: emb.intros dest: trans list_emb_trans_right)
[PROOF STATE]
proof (state)
this:
emb P s (mk g ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emb P s (mk g ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transp_on_emb:
  assumes "transp_on P F"
  shows "transp_on (emb P) trees"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transp_on (emb P) trees
[PROOF STEP]
using assms and emb_trans [of P]
[PROOF STATE]
proof (prove)
using this:
transp_on P F
\<lbrakk>\<And>f g h. \<lbrakk>f \<in> F; g \<in> F; h \<in> F; P f g; P g h\<rbrakk> \<Longrightarrow> P f h; emb P ?s ?t; emb P ?t ?u\<rbrakk> \<Longrightarrow> emb P ?s ?u

goal (1 subgoal):
 1. transp_on (emb P) trees
[PROOF STEP]
unfolding transp_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>F. \<forall>y\<in>F. \<forall>z\<in>F. P x y \<and> P y z \<longrightarrow> P x z
\<lbrakk>\<And>f g h. \<lbrakk>f \<in> F; g \<in> F; h \<in> F; P f g; P g h\<rbrakk> \<Longrightarrow> P f h; emb P ?s ?t; emb P ?t ?u\<rbrakk> \<Longrightarrow> emb P ?s ?u

goal (1 subgoal):
 1. \<forall>x\<in>trees. \<forall>y\<in>trees. \<forall>z\<in>trees. emb P x y \<and> emb P y z \<longrightarrow> emb P x z
[PROOF STEP]
by blast


[STATEMENT]
lemma kruskal:
  assumes "wqo_on P F"
  shows "wqo_on (emb P) trees"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wqo_on (emb P) trees
[PROOF STEP]
using almost_full_on_trees [of P] and assms
[PROOF STATE]
proof (prove)
using this:
almost_full_on P F \<Longrightarrow> almost_full_on (emb P) trees
wqo_on P F

goal (1 subgoal):
 1. wqo_on (emb P) trees
[PROOF STEP]
by (metis transp_on_emb wqo_on_def)


[STATEMENT]
lemma eff_sound:
  assumes \<open>eff r (A, B) = Some ss\<close> \<open>\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>(E :: _ \<Rightarrow> 'a). sc (E, F, G) (A, B))\<close>
  shows \<open>sc (E, F, G) (A, B)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eff r (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
proof (induct r \<open>(A, B)\<close> rule: eff.induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpL p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 8. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
case (5 p q)
[PROOF STATE]
proof (state)
this:
eff (ImpL p q) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (8 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpL p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 8. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eff (ImpL p q) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))
[PROOF STEP]
have \<open>sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)\<close> \<open>sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)\<close>
[PROOF STATE]
proof (prove)
using this:
eff (ImpL p q) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (1 subgoal):
 1. sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B) &&& sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)
[PROOF STEP]
by (metis eff.simps(5) finsertCI option.inject option.simps(3))+
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)
sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)

goal (8 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpL p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 8. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)
sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)
sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
using "5.prems"(1)
[PROOF STATE]
proof (prove)
using this:
sc (E, F, G) (A [\<div>] (p \<^bold>\<longrightarrow> q), p # B)
sc (E, F, G) (q # A [\<div>] (p \<^bold>\<longrightarrow> q), B)
eff (ImpL p q) (A, B) = Some ss

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
by (force split: if_splits)
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A, B)

goal (7 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
case (7 t p)
[PROOF STATE]
proof (state)
this:
eff (UniL t p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (7 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eff (UniL t p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))
[PROOF STEP]
have \<open>sc (E, F, G) (\<langle>t\<rangle>p # A, B)\<close>
[PROOF STATE]
proof (prove)
using this:
eff (UniL t p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (1 subgoal):
 1. sc (E, F, G) (\<langle>t\<rangle> p # A, B)
[PROOF STEP]
by (metis eff.simps(7) finsert_iff option.inject option.simps(3))
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (\<langle>t\<rangle> p # A, B)

goal (7 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>t p. \<lbrakk>eff (UniL t p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 7. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sc (E, F, G) (\<langle>t\<rangle> p # A, B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sc (E, F, G) (\<langle>t\<rangle> p # A, B)

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
using "7.prems"(1)
[PROOF STATE]
proof (prove)
using this:
sc (E, F, G) (\<langle>t\<rangle> p # A, B)
eff (UniL t p) (A, B) = Some ss

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
by (fastforce split: if_splits)
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A, B)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
case (8 p)
[PROOF STATE]
proof (state)
this:
eff (UniR p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
let ?n = \<open>fresh (A @ B)\<close>
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
have A: \<open>\<forall>p [\<in>] A. max_list (vars_fm p) < ?n\<close> and B: \<open>\<forall>p [\<in>] B. max_list (vars_fm p) < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set A. max_list (vars_fm p) < fresh (A @ B) &&& \<forall>p\<in>set B. max_list (vars_fm p) < fresh (A @ B)
[PROOF STEP]
unfolding fresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set A. max_list (vars_fm p) < Suc (max_list (vars_fms (A @ B))) &&& \<forall>p\<in>set B. max_list (vars_fm p) < Suc (max_list (vars_fms (A @ B)))
[PROOF STEP]
using max_list_vars_fms max_list_mono vars_fms_member
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>max_list (vars_fms ?A) \<le> ?n; ?p [\<in>] ?A\<rbrakk> \<Longrightarrow> max_list (vars_fm ?p) \<le> ?n
?A [\<subseteq>] ?B \<Longrightarrow> max_list ?A \<le> max_list ?B
?p [\<in>] ?A \<Longrightarrow> vars_fm ?p [\<subseteq>] vars_fms ?A

goal (1 subgoal):
 1. \<forall>p\<in>set A. max_list (vars_fm p) < Suc (max_list (vars_fms (A @ B))) &&& \<forall>p\<in>set B. max_list (vars_fm p) < Suc (max_list (vars_fms (A @ B)))
[PROOF STEP]
by (metis Un_iff le_imp_less_Suc set_append)+
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set A. max_list (vars_fm p) < fresh (A @ B)
\<forall>p\<in>set B. max_list (vars_fm p) < fresh (A @ B)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
from 8
[PROOF STATE]
proof (chain)
picking this:
eff (UniR p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))
[PROOF STEP]
have \<open>sc (E(?n := x), F, G) (A, \<langle>\<^bold>#?n\<rangle>p # B [\<div>] \<^bold>\<forall>p)\<close> for x
[PROOF STATE]
proof (prove)
using this:
eff (UniR p) (A, B) = Some ss
\<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))

goal (1 subgoal):
 1. sc (E(fresh (A @ B) := x), F, G) (A, \<langle>\<^bold># (fresh (A @ B))\<rangle> p # B [\<div>] \<^bold>\<forall> p)
[PROOF STEP]
by (metis eff.simps(8) finsert_iff option.inject option.simps(3))
[PROOF STATE]
proof (state)
this:
sc (E(fresh (A @ B) := ?x), F, G) (A, \<langle>\<^bold># (fresh (A @ B))\<rangle> p # B [\<div>] \<^bold>\<forall> p)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sc (E(fresh (A @ B) := ?x), F, G) (A, \<langle>\<^bold># (fresh (A @ B))\<rangle> p # B [\<div>] \<^bold>\<forall> p)
[PROOF STEP]
have \<open>(\<forall>p [\<in>] A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow>
      (\<forall>x. \<lbrakk>(x \<Zsemi> \<lambda>m. (E(?n := x)) m), F, G\<rbrakk> p) \<or> (\<exists>q [\<in>] B [\<div>] \<^bold>\<forall>p. \<lbrakk>E, F, G\<rbrakk> q)\<close>
[PROOF STATE]
proof (prove)
using this:
sc (E(fresh (A @ B) := ?x), F, G) (A, \<langle>\<^bold># (fresh (A @ B))\<rangle> p # B [\<div>] \<^bold>\<forall> p)

goal (1 subgoal):
 1. (\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>x \<Zsemi> E(fresh (A @ B) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
[PROOF STEP]
using A B upd_vars_fm
[PROOF STATE]
proof (prove)
using this:
sc (E(fresh (A @ B) := ?x), F, G) (A, \<langle>\<^bold># (fresh (A @ B))\<rangle> p # B [\<div>] \<^bold>\<forall> p)
\<forall>p\<in>set A. max_list (vars_fm p) < fresh (A @ B)
\<forall>p\<in>set B. max_list (vars_fm p) < fresh (A @ B)
max_list (vars_fm ?p) < ?n \<Longrightarrow> \<lbrakk>?E(?n := ?x), ?F, ?G\<rbrakk> ?p = \<lbrakk>?E, ?F, ?G\<rbrakk> ?p

goal (1 subgoal):
 1. (\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>x \<Zsemi> E(fresh (A @ B) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>x \<Zsemi> E(fresh (A @ B) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>x \<Zsemi> E(fresh (A @ B) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
[PROOF STEP]
have \<open>(\<forall>p [\<in>] A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow>
      (\<forall>x. \<lbrakk>((x \<Zsemi> E)(Suc ?n := x)), F, G\<rbrakk> p) \<or> (\<exists>q [\<in>] B [\<div>] \<^bold>\<forall>p. \<lbrakk>E, F, G\<rbrakk> q)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>x \<Zsemi> E(fresh (A @ B) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)

goal (1 subgoal):
 1. (\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
[PROOF STEP]
unfolding add_upd_commute
[PROOF STATE]
proof (prove)
using this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)

goal (1 subgoal):
 1. (\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
have \<open>max_list (vars_fm p) < ?n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (vars_fm p) < fresh (A @ B)
[PROOF STEP]
using B "8.prems"(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set B. max_list (vars_fm p) < fresh (A @ B)
eff (UniR p) (A, B) = Some ss

goal (1 subgoal):
 1. max_list (vars_fm p) < fresh (A @ B)
[PROOF STEP]
by (metis eff.simps(8) option.distinct(1) vars_fm.simps(4))
[PROOF STATE]
proof (state)
this:
max_list (vars_fm p) < fresh (A @ B)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
max_list (vars_fm p) < fresh (A @ B)
[PROOF STEP]
have \<open>sc (E, F, G) (A, \<^bold>\<forall>p # (B [\<div>] \<^bold>\<forall>p))\<close>
[PROOF STATE]
proof (prove)
using this:
(\<forall>p\<in>set A. \<lbrakk>E, F, G\<rbrakk> p) \<longrightarrow> (\<forall>x. \<lbrakk>(x \<Zsemi> E)(Suc (fresh (A @ B)) := x), F, G\<rbrakk> p) \<or> (\<exists>q\<in>set (B [\<div>] \<^bold>\<forall> p). \<lbrakk>E, F, G\<rbrakk> q)
max_list (vars_fm p) < fresh (A @ B)

goal (1 subgoal):
 1. sc (E, F, G) (A, \<^bold>\<forall> p # B [\<div>] \<^bold>\<forall> p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A, \<^bold>\<forall> p # B [\<div>] \<^bold>\<forall> p)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A, \<^bold>\<forall> p # B [\<div>] \<^bold>\<forall> p)

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
have \<open>\<^bold>\<forall>p [\<in>] B\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<forall> p [\<in>] B
[PROOF STEP]
using "8.prems"(1)
[PROOF STATE]
proof (prove)
using this:
eff (UniR p) (A, B) = Some ss

goal (1 subgoal):
 1. \<^bold>\<forall> p [\<in>] B
[PROOF STEP]
by (simp split: if_splits)
[PROOF STATE]
proof (state)
this:
\<^bold>\<forall> p [\<in>] B

goal (6 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 6. \<And>p. \<lbrakk>eff (UniR p) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sc (E, F, G) (A, \<^bold>\<forall> p # B [\<div>] \<^bold>\<forall> p)
\<^bold>\<forall> p [\<in>] B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sc (E, F, G) (A, \<^bold>\<forall> p # B [\<div>] \<^bold>\<forall> p)
\<^bold>\<forall> p [\<in>] B

goal (1 subgoal):
 1. sc (E, F, G) (A, B)
[PROOF STEP]
by (metis (full_types) Diff_iff sc.simps set_ConsD set_removeAll)
[PROOF STATE]
proof (state)
this:
sc (E, F, G) (A, B)

goal (5 subgoals):
 1. \<lbrakk>eff Idle (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 2. \<And>P ts. \<lbrakk>eff (Axiom P ts) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 3. \<lbrakk>eff FlsL (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 4. \<lbrakk>eff FlsR (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
 5. \<And>p q. \<lbrakk>eff (ImpR p q) (A, B) = Some ss; \<forall>A B. (A, B) |\<in>| ss \<longrightarrow> (\<forall>E. sc (E, F, G) (A, B))\<rbrakk> \<Longrightarrow> sc (E, F, G) (A, B)
[PROOF STEP]
qed (fastforce split: if_splits)+


[STATEMENT]
theorem prover_soundness:
  assumes \<open>tfinite t\<close> and \<open>wf t\<close>
  shows \<open>sc (E, F, G) (fst (root t))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc (E, F, G) (fst (tree.root t))
[PROOF STEP]
using assms soundness
[PROOF STATE]
proof (prove)
using this:
tfinite t
Prover.wf t
\<lbrakk>tfinite ?t; Prover.wf ?t\<rbrakk> \<Longrightarrow> \<forall>S\<in>UNIV. sc S (fst (tree.root ?t))

goal (1 subgoal):
 1. sc (E, F, G) (fst (tree.root t))
[PROOF STEP]
by fast


[STATEMENT]
lemma lemSqrt:
    assumes "x \<ge> 0"
      and   "r = sqrt x"
    shows   "r \<ge> 0  \<and>  r*r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
have rootExists: "(\<exists>r. sqrtTest x r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. sqrtTest x r
[PROOF STEP]
by (metis AxEuclidean assms(1))
[PROOF STATE]
proof (state)
this:
\<exists>r. sqrtTest x r

goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
hence "sqrtTest x (sqrt x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. sqrtTest x r

goal (1 subgoal):
 1. sqrtTest x (sqrt x)
[PROOF STEP]
by (metis lemSomeFunc)
[PROOF STATE]
proof (state)
this:
sqrtTest x (sqrt x)

goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sqrtTest x (sqrt x)

goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
sqrtTest x (sqrt x)
r = sqrt x

goal (1 subgoal):
 1. (0::'a) \<le> r \<and> r * r = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> r \<and> r * r = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemCProps:
  assumes "IOb m"
     and  "v = c m"
  shows "(v > 0) \<and> (\<forall>x y.((\<exists>p. (Ph p \<and> W m p x \<and> W m p y))
                      \<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
have vExists: "(\<exists>v. cTest m v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. cTest m v
[PROOF STEP]
by (metis AxPh assms(1))
[PROOF STATE]
proof (state)
this:
\<exists>v. cTest m v

goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
hence "cTest m (c m)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. cTest m v

goal (1 subgoal):
 1. cTest m (c m)
[PROOF STEP]
by (metis lemSomeFunc)
[PROOF STATE]
proof (state)
this:
cTest m (c m)

goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cTest m (c m)

goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
cTest m (c m)
v = c m

goal (1 subgoal):
 1. (0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) < v \<and> (\<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemCCone:
  assumes "IOb m"
    and   "onCone y (lightcone m x)"
  shows   "\<exists>p. (Ph p \<and> W m p x \<and> W m p y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
have "(\<exists>p.(Ph p \<and> W m p x \<and> W m p y))
                      \<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y)
[PROOF STEP]
by (smt assms(1) lemCProps)
[PROOF STATE]
proof (state)
this:
(\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y)

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
hence ph_exists: "(space2 x y = (c m * c m)*time2 x y) \<longrightarrow> (\<exists>p.(Ph p \<and> W m p x \<and> W m p y))"
[PROOF STATE]
proof (prove)
using this:
(\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y)

goal (1 subgoal):
 1. space2 x y = c m * c m * time2 x y \<longrightarrow> (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
space2 x y = c m * c m * time2 x y \<longrightarrow> (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y)

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
define lcmx where "lcmx = lightcone m x"
[PROOF STATE]
proof (state)
this:
lcmx = lightcone m x

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
have lcmx_vertex: "vertex lcmx = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex lcmx = x
[PROOF STEP]
by (simp add: lcmx_def)
[PROOF STATE]
proof (state)
this:
vertex lcmx = x

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
have lcmx_slope: "slope lcmx = c m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slope lcmx = c m
[PROOF STEP]
by (simp add: lcmx_def)
[PROOF STATE]
proof (state)
this:
slope lcmx = c m

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
have "onCone y lcmx \<longrightarrow> (space2 x y = (c m * c m)*time2 x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. onCone y lcmx \<longrightarrow> space2 x y = c m * c m * time2 x y
[PROOF STEP]
by (metis lcmx_vertex lcmx_slope onCone.simps)
[PROOF STATE]
proof (state)
this:
onCone y lcmx \<longrightarrow> space2 x y = c m * c m * time2 x y

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
hence "space2 x y = (c m * c m)*time2 x y"
[PROOF STATE]
proof (prove)
using this:
onCone y lcmx \<longrightarrow> space2 x y = c m * c m * time2 x y

goal (1 subgoal):
 1. space2 x y = c m * c m * time2 x y
[PROOF STEP]
by (metis lcmx_def assms(2))
[PROOF STATE]
proof (state)
this:
space2 x y = c m * c m * time2 x y

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
space2 x y = c m * c m * time2 x y

goal (1 subgoal):
 1. \<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y
[PROOF STEP]
by (metis ph_exists)
[PROOF STATE]
proof (state)
this:
\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lemCPos:
  assumes "IOb m"
  shows   "c m > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < c m
[PROOF STEP]
by (metis assms(1) lemCProps)


[STATEMENT]
lemma lemCPhoton:
  assumes "IOb m"
  shows "\<forall>x y. (\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (c m * c m)*(time2 x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (\<exists>p. Ph p \<and> m sees p at x \<and> m sees p at y) = (space2 x y = c m * c m * time2 x y)
[PROOF STEP]
by (metis assms(1) lemCProps)


[STATEMENT]
lemma measurable_\<iota>'[measurable (raw)]:
  "f \<in> measurable M (count_space UNIV) \<Longrightarrow> g \<in> measurable M (count_space UNIV) \<Longrightarrow>
    (\<lambda>x. \<iota> (f x) (g x)) \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> M \<rightarrow>\<^sub>M count_space UNIV; g \<in> M \<rightarrow>\<^sub>M count_space UNIV\<rbrakk> \<Longrightarrow> (\<lambda>x. \<iota> (f x) (g x)) \<in> borel_measurable M
[PROOF STEP]
using measurable_compose[OF _ measurable_\<iota>, of "\<lambda>x. (f x, g x)" M]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f x, g x)) \<in> M \<rightarrow>\<^sub>M count_space UNIV \<Otimes>\<^sub>M count_space UNIV \<Longrightarrow> (\<lambda>x. case (f x, g x) of (a, b) \<Rightarrow> \<iota> a b) \<in> borel_measurable M

goal (1 subgoal):
 1. \<lbrakk>f \<in> M \<rightarrow>\<^sub>M count_space UNIV; g \<in> M \<rightarrow>\<^sub>M count_space UNIV\<rbrakk> \<Longrightarrow> (\<lambda>x. \<iota> (f x) (g x)) \<in> borel_measurable M
[PROOF STEP]
by simp


[STATEMENT]
lemma measurable_\<rho>[measurable]: "\<rho> \<in> borel_measurable (count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<in> borel_measurable (count_space UNIV)
[PROOF STEP]
by simp


[STATEMENT]
lemma single_l:
  fixes s and x :: real assumes "s \<in> S"
  shows "(\<Sum>s'\<in>S. (if s' = s then 1 else 0) * l s') = x \<longleftrightarrow> l s = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Sum>s'\<in>S. (if s' = s then 1 else 0) * l s') = x) = (l s = x)
[PROOF STEP]
by (simp add: assms if_distrib [of "\<lambda>x. x * a" for a] cong: if_cong)


[STATEMENT]
lemma order_Ex:
  assumes "s \<in> S" obtains i where "i < card S" "s = order i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < card S; s = order i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < card S; s = order i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
have "s \<in> order ` {..<card S}"
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. s \<in> order ` {..<card S}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> order ` {..<card S}

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < card S; s = order i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i1 < card S; s = order ?i1\<rbrakk> \<Longrightarrow> thesis
s \<in> order ` {..<card S}
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < card S; s = order ?i1\<rbrakk> \<Longrightarrow> thesis
s \<in> order ` {..<card S}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp del: image_order)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_iorder: "bij_betw iorder S {..<card S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw iorder S {..<card S}
[PROOF STEP]
unfolding iorder_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (the_inv_into {..<card S} order) S {..<card S}
[PROOF STEP]
by (rule bij_betw_the_inv_into bij_order)+


[STATEMENT]
lemma iorder_image_eq: "iorder ` S = {..<card S}"
  and inj_iorder: "inj_on iorder S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iorder ` S = {..<card S} &&& inj_on iorder S
[PROOF STEP]
using bij_iorder
[PROOF STATE]
proof (prove)
using this:
bij_betw iorder S {..<card S}

goal (1 subgoal):
 1. iorder ` S = {..<card S} &&& inj_on iorder S
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on iorder S \<and> iorder ` S = {..<card S}

goal (1 subgoal):
 1. iorder ` S = {..<card S} &&& inj_on iorder S
[PROOF STEP]
by auto


[STATEMENT]
lemma order_iorder: "\<And>s. s \<in> S \<Longrightarrow> order (iorder s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> order (iorder s) = s
[PROOF STEP]
unfolding iorder_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> order (the_inv_into {..<card S} order s) = s
[PROOF STEP]
using bij_order
[PROOF STATE]
proof (prove)
using this:
bij_betw order {..<card S} S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> order (the_inv_into {..<card S} order s) = s
[PROOF STEP]
by (intro f_the_inv_into_f) (auto simp: bij_betw_def)


[STATEMENT]
lemma gauss_jordan'_correct:
  assumes "gauss_jordan' M a = Some f"
  shows "\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
note \<open>gauss_jordan' M a = Some f\<close>
[PROOF STATE]
proof (state)
this:
gauss_jordan' M a = Some f

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gauss_jordan' M a = Some f

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
define M' where "M' = (\<lambda>i j. if j = card S then
    a (order i) else M (order i) (order j))"
[PROOF STATE]
proof (state)
this:
M' = (\<lambda>i j. if j = card S then a (order i) else M (order i) (order j))

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gauss_jordan' M a = Some f
M' = (\<lambda>i j. if j = card S then a (order i) else M (order i) (order j))
[PROOF STEP]
obtain sol where sol: "gauss_jordan M' (card S) = Some sol"
    and f: "f = (\<lambda>i. sol (iorder i) (card S))"
[PROOF STATE]
proof (prove)
using this:
gauss_jordan' M a = Some f
M' = (\<lambda>i j. if j = card S then a (order i) else M (order i) (order j))

goal (1 subgoal):
 1. (\<And>sol. \<lbrakk>gauss_jordan M' (card S) = Some sol; f = (\<lambda>i. sol (iorder i) (card S))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: gauss_jordan'_def Let_def split: bind_split_asm)
[PROOF STATE]
proof (state)
this:
gauss_jordan M' (card S) = Some sol
f = (\<lambda>i. sol (iorder i) (card S))

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
from gauss_jordan_correct[OF sol]
[PROOF STATE]
proof (chain)
picking this:
solution M' (card S) (\<lambda>j. sol j (card S))
[PROOF STEP]
have "\<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)"
[PROOF STATE]
proof (prove)
using this:
solution M' (card S) (\<lambda>j. sol j (card S))

goal (1 subgoal):
 1. \<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)
[PROOF STEP]
unfolding solution_def M'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i<card S. (\<Sum>j = 0..<card S. (if j = card S then a (order i) else M (order i) (order j)) * sol j (card S)) = (if card S = card S then a (order i) else M (order i) (order (card S)))

goal (1 subgoal):
 1. \<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)
[PROOF STEP]
by (simp add: atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{..<card S}. (\<Sum>j<card S. M (order i) (order j) * sol j (card S)) = a (order i)

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s
[PROOF STEP]
unfolding iorder_image_eq[symmetric] f
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>iorder ` S. (\<Sum>j\<in>iorder ` S. M (order i) (order j) * sol j (card S)) = a (order i)

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * sol (iorder s') (card S)) = a s
[PROOF STEP]
using inj_iorder
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>iorder ` S. (\<Sum>j\<in>iorder ` S. M (order i) (order j) * sol j (card S)) = a (order i)
inj_on iorder S

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * sol (iorder s') (card S)) = a s
[PROOF STEP]
by (subst (asm) sum.reindex) (auto simp: order_iorder)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * f s') = a s

goal:
No subgoals!
[PROOF STEP]
qed