[STATEMENT]
lemma compute_less_pp[code]:
  "xs < (ys :: 'a :: linorder \<Rightarrow>\<^sub>0 'b :: {zero, linorder}) \<longleftrightarrow>
    (\<exists>i\<in>keys xs \<union> keys ys. lookup xs i < lookup ys i \<and>
    (\<forall>j\<in>keys xs \<union> keys ys. j < i \<longrightarrow> lookup xs j = lookup ys j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs < ys) = (\<exists>i\<in>keys xs \<union> keys ys. lookup xs i < lookup ys i \<and> (\<forall>j\<in>keys xs \<union> keys ys. j < i \<longrightarrow> lookup xs j = lookup ys j))
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
fix f g :: "'a \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
let ?dom = "{i. f i \<noteq> 0} \<union> {i. g i \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
have "less_fun f g \<longleftrightarrow> (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_fun f g = (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k'))
[PROOF STEP]
unfolding less_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k')) = (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k'))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
less_fun f g = (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k'))

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
less_fun f g = (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k'))

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists>i. f i < g i \<and> (i \<in> ?dom \<and> (\<forall>j\<in>?dom. j < i \<longrightarrow> f j = g j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k')) = (\<exists>i. f i < g i \<and> i \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))
[PROOF STEP]
proof (intro iff_exI conj_cong refl)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
assume "f k < g k"
[PROOF STATE]
proof (state)
this:
f k < g k

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
hence k: "k \<in> ?dom"
[PROOF STATE]
proof (prove)
using this:
f k < g k

goal (1 subgoal):
 1. k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
have "(\<forall>k'<k. f k' = g k') = (\<forall>k'\<in>{..<k}. f k' = g k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>k'<k. f k' = g k') = (\<forall>k'\<in>{..<k}. f k' = g k')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>k'<k. f k' = g k') = (\<forall>k'\<in>{..<k}. f k' = g k')

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>k'<k. f k' = g k') = (\<forall>k'\<in>{..<k}. f k' = g k')

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<forall>j\<in>({k. f k \<noteq> 0} \<union> {k. g k \<noteq> 0}) \<inter> {..<k}. f j = g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>k'\<in>{..<k}. f k' = g k') = (\<forall>j\<in>({k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}) \<inter> {..<k}. f j = g j)
[PROOF STEP]
by (intro Ball_subset_right) auto
[PROOF STATE]
proof (state)
this:
(\<forall>k'\<in>{..<k}. f k' = g k') = (\<forall>j\<in>({k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}) \<inter> {..<k}. f j = g j)

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>k'\<in>{..<k}. f k' = g k') = (\<forall>j\<in>({k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}) \<inter> {..<k}. f j = g j)

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<forall>j\<in>({k. f k \<noteq> 0} \<union> {k. g k \<noteq> 0}). j < k \<longrightarrow> f j = g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<in>({k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}) \<inter> {..<k}. f j = g j) = (\<forall>j\<in>{k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>j\<in>({k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}) \<inter> {..<k}. f j = g j) = (\<forall>j\<in>{k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j)

goal (1 subgoal):
 1. \<And>k. f k < g k \<Longrightarrow> (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<forall>k'<k. f k' = g k') = (\<forall>j\<in>{k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j)
[PROOF STEP]
show "(\<forall>k'<k. f k' = g k') \<longleftrightarrow> k \<in> ?dom \<and> (\<forall>j\<in>?dom. j < k \<longrightarrow> f j = g j)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>k'<k. f k' = g k') = (\<forall>j\<in>{k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j)

goal (1 subgoal):
 1. (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
(\<forall>k'<k. f k' = g k') = (\<forall>j\<in>{k. f k \<noteq> (0::'b)} \<union> {k. g k \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j)
k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}

goal (1 subgoal):
 1. (\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>k'<k. f k' = g k') = (k \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < k \<longrightarrow> f j = g j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k')) = (\<exists>i. f i < g i \<and> i \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k')) = (\<exists>i. f i < g i \<and> i \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists>i\<in>?dom. f i < g i \<and> (\<forall>j\<in>?dom. j < i \<longrightarrow> f j = g j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>i. f i < g i \<and> i \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j)) = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))
[PROOF STEP]
by (simp add: Bex_def conj_ac)
[PROOF STATE]
proof (state)
this:
(\<exists>i. f i < g i \<and> i \<in> {i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)} \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j)) = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>finite {x. xs x \<noteq> (0::'b)}; finite {x. ys x \<noteq> (0::'b)}\<rbrakk> \<Longrightarrow> less_fun xs ys = (\<exists>i\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. xs i < ys i \<and> (\<forall>j\<in>{k. xs k \<noteq> (0::'b)} \<union> {k. ys k \<noteq> (0::'b)}. j < i \<longrightarrow> xs j = ys j))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
less_fun f g = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))
[PROOF STEP]
show "less_fun f g \<longleftrightarrow> (\<exists>i\<in>?dom. f i < g i \<and> (\<forall>j\<in>?dom. j < i \<longrightarrow> f j = g j))"
[PROOF STATE]
proof (prove)
using this:
less_fun f g = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))

goal (1 subgoal):
 1. less_fun f g = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
less_fun f g = (\<exists>i\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. f i < g i \<and> (\<forall>j\<in>{i. f i \<noteq> (0::'b)} \<union> {i. g i \<noteq> (0::'b)}. j < i \<longrightarrow> f j = g j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_le_pp[code]:
  "xs \<le> ys \<longleftrightarrow> xs = ys \<or> xs < (ys :: _ \<Rightarrow>\<^sub>0 _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<le> ys) = (xs = ys \<or> xs < ys)
[PROOF STEP]
by (auto simp: order.order_iff_strict)


[STATEMENT]
lemma vars_code [code]:
  "vars (MPoly p) = (\<Union>m\<in>keys p. keys m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly p) = \<Union> (keys ` keys p)
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (MPoly p))) = \<Union> (keys ` keys p)
[PROOF STEP]
by transfer' simp


[STATEMENT]
lemma mpoly_coeff_code [code]: "coeff (MPoly p) = lookup p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly p) = lookup p
[PROOF STEP]
by transfer' simp


[STATEMENT]
lemma sym_mpoly_code [code]:
  "sym_mpoly (set xs) k = (\<Sum>X\<in>Set.filter (\<lambda>X. card X = k) (Pow (set xs)). monom (monom_of_set X) 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_mpoly (set xs) k = (\<Sum>X\<in>Set.filter (\<lambda>X. card X = k) (Pow (set xs)). MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
by (simp add: sym_mpoly_altdef Set.filter_def)


[STATEMENT]
lemma monom_of_set_code [code]:
  "monom_of_set (set xs) = Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_of_set (set xs) = Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))
[PROOF STEP]
proof (intro poly_mapping_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (monom_of_set (set xs)) k = lookup (Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))) k
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (monom_of_set (set xs)) k = lookup (Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))) k
[PROOF STEP]
show "lookup ?lhs k = lookup ?rhs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (monom_of_set (set xs)) k = lookup (Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))) k
[PROOF STEP]
by (induction xs) (auto simp: lookup_monom_of_set fmlookup_default_def)
[PROOF STATE]
proof (state)
this:
lookup (monom_of_set (set xs)) k = lookup (Pm_fmap (fmap_of_list (map (\<lambda>x. (x, 1)) xs))) k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma restrictpm_code [code]:
  "restrictpm A (Pm_fmap m) = Pm_fmap (fmrestrict_set A m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (Pm_fmap m) = Pm_fmap (fmrestrict_set A m)
[PROOF STEP]
by (intro poly_mapping_eqI) (auto simp: lookup_restrictpm fmlookup_default_def)


[STATEMENT]
lemma textbook_invalid: "I\<lbrakk>invalid\<rbrakk>\<tau> = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>invalid\<rbrakk> \<tau> = UML_Types.bot_class.bot
[PROOF STEP]
by(simp add: invalid_def Sem_def)


[STATEMENT]
lemma textbook_null_fun: "I\<lbrakk>null::('\<AA>,'\<alpha>::null) val\<rbrakk> \<tau> = (null::('\<alpha>::null))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<lbrakk>null\<rbrakk> \<tau> = null
[PROOF STEP]
by(simp add: null_fun_def Sem_def)


[STATEMENT]
lemma PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> subst P t xx \<in> fmla
[PROOF STEP]
by auto


[STATEMENT]
lemma Fvars_PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> trm \<Longrightarrow> Fvars (subst P t xx) = FvarsT t
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]:
"n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n"
"n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n) &&& (n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n)
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<in> num \<Longrightarrow> subst (subst P (Var yy) xx) n yy = subst P n xx) &&& (n \<in> num \<Longrightarrow> subst (subst P (Var xx) xx) n xx = subst P n xx)
[PROOF STEP]
by auto


[STATEMENT]
lemma HBL1_PP:
"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>)
[PROOF STEP]
using HBL1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> bprv (subst P \<langle>?\<phi>\<rangle> xx)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>)
[PROOF STEP]
unfolding PP_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prv ?\<phi>\<rbrakk> \<Longrightarrow> bprv (subst P \<langle>?\<phi>\<rangle> xx)

goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> fmla; Fvars \<phi> = {}; prv \<phi>\<rbrakk> \<Longrightarrow> bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
by auto


[STATEMENT]
lemma P[simp,intro!]: "P \<in> fmla" and Fvars_P[simp]: "Fvars P = {xx}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> fmla &&& Fvars P = {xx}
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exi yy (PPf (Var yy) (Var xx)) \<in> fmla &&& Fvars (exi yy (PPf (Var yy) (Var xx))) = {xx}
[PROOF STEP]
by (auto simp: PPf_def2)


[STATEMENT]
lemma HBL1:
assumes \<phi>: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p\<phi>: "prv \<phi>"
shows "bprv (subst P \<langle>\<phi>\<rangle> xx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
obtain "prf" where pf: "prf \<in> proof" and "prfOf prf \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prf. \<lbrakk>prf \<in> proof; prfOf prf \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prv_prfOf assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}\<rbrakk> \<Longrightarrow> prv ?\<phi> = (\<exists>prf\<in>proof. prfOf prf ?\<phi>)
\<phi> \<in> fmla
Fvars \<phi> = {}
prv \<phi>

goal (1 subgoal):
 1. (\<And>prf. \<lbrakk>prf \<in> proof; prfOf prf \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prf \<in> proof
prfOf prf \<phi>

goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
hence 0: "bprv (PPf (encPf prf) (enc \<phi>))"
[PROOF STATE]
proof (prove)
using this:
prf \<in> proof
prfOf prf \<phi>

goal (1 subgoal):
 1. bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)
[PROOF STEP]
using prfOf_PPf \<phi>
[PROOF STATE]
proof (prove)
using this:
prf \<in> proof
prfOf prf \<phi>
\<lbrakk>?prf \<in> proof; ?\<phi> \<in> fmla; Fvars ?\<phi> = {}; prfOf ?prf ?\<phi>\<rbrakk> \<Longrightarrow> bprv (PPf (encPf ?prf) \<langle>?\<phi>\<rangle>)
\<phi> \<in> fmla
Fvars \<phi> = {}

goal (1 subgoal):
 1. bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)

goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
have 1: "subst (subst Pf (encPf prf) yy) \<langle>\<phi>\<rangle> xx = subst (subst Pf \<langle>\<phi>\<rangle> xx) (substT (encPf prf) \<langle>\<phi>\<rangle> xx) yy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst Pf (encPf prf) yy) \<langle>\<phi>\<rangle> xx = subst (subst Pf \<langle>\<phi>\<rangle> xx) (substT (encPf prf) \<langle>\<phi>\<rangle> xx) yy
[PROOF STEP]
using assms pf
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
Fvars \<phi> = {}
prv \<phi>
prf \<in> proof

goal (1 subgoal):
 1. subst (subst Pf (encPf prf) yy) \<langle>\<phi>\<rangle> xx = subst (subst Pf \<langle>\<phi>\<rangle> xx) (substT (encPf prf) \<langle>\<phi>\<rangle> xx) yy
[PROOF STEP]
by (intro subst_compose_diff) auto
[PROOF STATE]
proof (state)
this:
subst (subst Pf (encPf prf) yy) \<langle>\<phi>\<rangle> xx = subst (subst Pf \<langle>\<phi>\<rangle> xx) (substT (encPf prf) \<langle>\<phi>\<rangle> xx) yy

goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)

goal (1 subgoal):
 1. bprv (subst P \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)

goal (1 subgoal):
 1. bprv (subst (exi yy (PPf (Var yy) (Var xx))) \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)
\<phi> \<in> fmla
Fvars \<phi> = {}
prv \<phi>

goal (1 subgoal):
 1. bprv (subst (exi yy (PPf (Var yy) (Var xx))) \<langle>\<phi>\<rangle> xx)
[PROOF STEP]
by (auto simp: PPf_def2 1 pf intro!: B.prv_exiI[of _ _ "encPf prf"])
[PROOF STATE]
proof (state)
this:
bprv (subst P \<langle>\<phi>\<rangle> xx)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_prv_prv_neg_PPf:
assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "\<not> prv \<phi>" and n[simp]: "n \<in> num"
shows "bprv (neg (PPf n \<langle>\<phi>\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
have "\<forall>prf\<in>proof. \<not> prfOf prf \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>prf\<in>proof. \<not> prfOf prf \<phi>
[PROOF STEP]
using prv_prfOf p
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}\<rbrakk> \<Longrightarrow> prv ?\<phi> = (\<exists>prf\<in>proof. prfOf prf ?\<phi>)
\<not> prv \<phi>

goal (1 subgoal):
 1. \<forall>prf\<in>proof. \<not> prfOf prf \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>prf\<in>proof. \<not> prfOf prf \<phi>

goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
hence "\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>prf\<in>proof. \<not> prfOf prf \<phi>

goal (1 subgoal):
 1. \<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))
[PROOF STEP]
using not_prfOf_PPf
[PROOF STATE]
proof (prove)
using this:
\<forall>prf\<in>proof. \<not> prfOf prf \<phi>
\<lbrakk>?prf \<in> proof; ?\<phi> \<in> fmla; Fvars ?\<phi> = {}; \<not> prfOf ?prf ?\<phi>\<rbrakk> \<Longrightarrow> bprv (neg (PPf (encPf ?prf) \<langle>?\<phi>\<rangle>))

goal (1 subgoal):
 1. \<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
using not_prfOf_PPf
[PROOF STATE]
proof (prove)
using this:
\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))
\<lbrakk>?prf \<in> proof; ?\<phi> \<in> fmla; Fvars ?\<phi> = {}; \<not> prfOf ?prf ?\<phi>\<rbrakk> \<Longrightarrow> bprv (neg (PPf (encPf ?prf) \<langle>?\<phi>\<rangle>))

goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
using Clean_PPf_encPf
[PROOF STATE]
proof (prove)
using this:
\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))
\<lbrakk>?prf \<in> proof; ?\<phi> \<in> fmla; Fvars ?\<phi> = {}; \<not> prfOf ?prf ?\<phi>\<rbrakk> \<Longrightarrow> bprv (neg (PPf (encPf ?prf) \<langle>?\<phi>\<rangle>))
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; ?p \<in> num; ?p \<notin> encPf ` proof\<rbrakk> \<Longrightarrow> bprv (neg (PPf ?p \<langle>?\<phi>\<rangle>))

goal (1 subgoal):
 1. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
by (cases "n \<in> encPf ` proof") auto
[PROOF STATE]
proof (state)
this:
bprv (neg (PPf n \<langle>\<phi>\<rangle>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma consistent_not_prv_not_prv_PPf:
assumes c: consistent
and 0[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" "\<not> prv \<phi>" "n \<in> num"
shows "\<not> bprv (PPf n \<langle>\<phi>\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bprv (PPf n \<langle>\<phi>\<rangle>)
[PROOF STEP]
using not_prv_prv_neg_PPf[OF 0] c[THEN dwf_dwfd.consistent_B_consistent]
[PROOF STATE]
proof (prove)
using this:
bprv (neg (PPf n \<langle>\<phi>\<rangle>))
B.consistent

goal (1 subgoal):
 1. \<not> bprv (PPf n \<langle>\<phi>\<rangle>)
[PROOF STEP]
unfolding B.consistent_def3
[PROOF STATE]
proof (prove)
using this:
bprv (neg (PPf n \<langle>\<phi>\<rangle>))
\<forall>\<phi>\<in>fmla. \<not> (bprv \<phi> \<and> bprv (neg \<phi>))

goal (1 subgoal):
 1. \<not> bprv (PPf n \<langle>\<phi>\<rangle>)
[PROOF STEP]
by auto


[STATEMENT]
lemma PP_PPf:
assumes "\<phi> \<in> fmla"
shows "wrepr.PP \<langle>\<phi>\<rangle> = exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrepr.PP \<langle>\<phi>\<rangle> = exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)
[PROOF STEP]
unfolding wrepr.PP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst P \<langle>\<phi>\<rangle> xx = exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla

goal (1 subgoal):
 1. subst P \<langle>\<phi>\<rangle> xx = exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)
[PROOF STEP]
by (auto simp: PPf_def2 P_def)


[STATEMENT]
lemma \<omega>consistentStd1_HBL1_rev:
assumes oc: "B.\<omega>consistentStd1"
and \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
and iPP: "bprv (wrepr.PP \<langle>\<phi>\<rangle>)"
shows "prv \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
have 0: "bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
using iPP
[PROOF STATE]
proof (prove)
using this:
bprv (wrepr.PP \<langle>\<phi>\<rangle>)

goal (1 subgoal):
 1. bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
by (simp add: PP_PPf)
[PROOF STATE]
proof (state)
this:
bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
assume "\<not> prv \<phi>"
[PROOF STATE]
proof (state)
this:
\<not> prv \<phi>

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
hence "\<forall>n \<in> num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
\<not> prv \<phi>

goal (1 subgoal):
 1. \<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
using not_prv_prv_neg_PPf
[PROOF STATE]
proof (prove)
using this:
\<not> prv \<phi>
\<lbrakk>?\<phi> \<in> fmla; Fvars ?\<phi> = {}; \<not> prv ?\<phi>; ?n \<in> num\<rbrakk> \<Longrightarrow> bprv (neg (PPf ?n \<langle>?\<phi>\<rangle>))

goal (1 subgoal):
 1. \<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
hence "\<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. \<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
using oc
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
B.\<omega>consistentStd1

goal (1 subgoal):
 1. \<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
unfolding B.\<omega>consistentStd1_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. bprv (neg (subst \<phi> n x))) \<longrightarrow> \<not> bprv (exi x \<phi>)

goal (1 subgoal):
 1. \<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))
\<forall>\<phi>\<in>fmla. \<forall>x\<in>var. Fvars \<phi> = {x} \<longrightarrow> (\<forall>n\<in>num. bprv (neg (subst \<phi> n x))) \<longrightarrow> \<not> bprv (exi x \<phi>)
\<phi> \<in> fmla
Fvars \<phi> = {}

goal (1 subgoal):
 1. \<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))

goal (1 subgoal):
 1. False
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))
bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))

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

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> prv \<phi> \<Longrightarrow> False

goal (1 subgoal):
 1. prv \<phi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> prv \<phi> \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HBL2_imp:
 "\<And>\<phi> \<chi>. \<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> Fvars \<chi> = {} \<Longrightarrow>
  bprv (imp (PP \<langle>imp \<phi> \<chi>\<rangle>) (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi> \<chi>. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; Fvars \<phi> = {}; Fvars \<chi> = {}\<rbrakk> \<Longrightarrow> bprv (imp (PP \<langle>imp \<phi> \<chi>\<rangle>) (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>)))
[PROOF STEP]
using HBL2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<phi> \<in> fmla; ?\<chi> \<in> fmla; Fvars ?\<phi> = {}; Fvars ?\<chi> = {}\<rbrakk> \<Longrightarrow> bprv (imp (cnj (PP \<langle>?\<phi>\<rangle>) (PP \<langle>imp ?\<phi> ?\<chi>\<rangle>)) (PP \<langle>?\<chi>\<rangle>))

goal (1 subgoal):
 1. \<And>\<phi> \<chi>. \<lbrakk>\<phi> \<in> fmla; \<chi> \<in> fmla; Fvars \<phi> = {}; Fvars \<chi> = {}\<rbrakk> \<Longrightarrow> bprv (imp (PP \<langle>imp \<phi> \<chi>\<rangle>) (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>)))
[PROOF STEP]
by (simp add: B.prv_cnj_imp B.prv_imp_com)


[STATEMENT]
lemma HBL2_imp2:
assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" "Fvars \<phi> = {}" "Fvars \<chi> = {}"
assumes "bprv (PP \<langle>imp \<phi> \<chi>\<rangle>)"
shows "bprv (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bprv (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<chi> \<in> fmla
Fvars \<phi> = {}
Fvars \<chi> = {}
bprv (PP \<langle>imp \<phi> \<chi>\<rangle>)

goal (1 subgoal):
 1. bprv (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>))
[PROOF STEP]
by (meson HBL2_imp PP enc imp num B.prv_imp_mp subsetCE)


[STATEMENT]
lemma add_env_semantics [simp]: \<open>\<lparr>E, F\<rparr> ((t \<Zsemi> s) n) = (\<lparr>E, F\<rparr> t \<Zsemi> \<lambda>m. \<lparr>E, F\<rparr> (s m)) n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>E, F\<rparr> ((t \<Zsemi> s) n) = (\<lparr>E, F\<rparr> t \<Zsemi> \<lambda>m. \<lparr>E, F\<rparr> (s m)) n
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma lift_lemma [simp]: \<open>\<lparr>x \<Zsemi> E, F\<rparr> (lift_tm t) = \<lparr>E, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>x \<Zsemi> E, F\<rparr> (lift_tm t) = \<lparr>E, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma sub_tm_semantics [simp]: \<open>\<lparr>E, F\<rparr> (sub_tm s t) = \<lparr>\<lambda>n. \<lparr>E, F\<rparr> (s n), F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>E, F\<rparr> (sub_tm s t) = \<lparr>\<lambda>n. \<lparr>E, F\<rparr> (s n), F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma sub_fm_semantics [simp]: \<open>\<lbrakk>E, F, G\<rbrakk> (sub_fm s p) = \<lbrakk>\<lambda>n. \<lparr>E, F\<rparr> (s n), F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> (sub_fm s p) = \<lbrakk>\<lambda>n. \<lparr>E, F\<rparr> (s n), F, G\<rbrakk> p
[PROOF STEP]
by (induct p arbitrary: E s) (auto cong: map_cong)


[STATEMENT]
lemma upd_vars_tm [simp]: \<open>n [\<notin>] vars_tm t \<Longrightarrow> \<lparr>E(n := x), F\<rparr> t = \<lparr>E, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n [\<notin>] vars_tm t \<Longrightarrow> \<lparr>E(n := x), F\<rparr> t = \<lparr>E, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma add_upd_commute [simp]: \<open>(y \<Zsemi> E(n := x)) m = ((y \<Zsemi> E)(Suc n := x)) m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<Zsemi> E(n := x)) m = ((y \<Zsemi> E)(Suc n := x)) m
[PROOF STEP]
by (induct m) simp_all


[STATEMENT]
lemma upd_vars_fm [simp]: \<open>max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
proof (induct p arbitrary: E n)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
case (Pre P ts)
[PROOF STATE]
proof (state)
this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>max_list (concat (map vars_tm ts)) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
using Pre.prems max_list_concat
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
?xs [\<in>] ?xss \<Longrightarrow> max_list ?xs \<le> max_list (concat ?xss)

goal (1 subgoal):
 1. max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_list (concat (map vars_tm ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
have \<open>n [\<notin>] concat (map vars_tm ts)\<close>
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_tm ts)) < n

goal (1 subgoal):
 1. n [\<notin>] concat (map vars_tm ts)
[PROOF STEP]
using max_list_in
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_tm ts)) < n
max_list ?xs < ?n \<Longrightarrow> ?n [\<notin>] ?xs

goal (1 subgoal):
 1. n [\<notin>] concat (map vars_tm ts)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n [\<notin>] concat (map vars_tm ts)

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n [\<notin>] concat (map vars_tm ts)
[PROOF STEP]
have \<open>\<forall>t [\<in>] ts. n [\<notin>] vars_tm t\<close>
[PROOF STATE]
proof (prove)
using this:
n [\<notin>] concat (map vars_tm ts)

goal (1 subgoal):
 1. \<forall>t\<in>set ts. n [\<notin>] vars_tm t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. n [\<notin>] vars_tm t

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n [\<notin>] vars_tm t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n [\<notin>] vars_tm t

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
using upd_vars_tm
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n [\<notin>] vars_tm t
?n [\<notin>] vars_tm ?t \<Longrightarrow> \<lparr>?E(?n := ?x), ?F\<rparr> ?t = \<lparr>?E, ?F\<rparr> ?t

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
by (metis list.map_cong semantics_fm.simps(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
case (Uni p)
[PROOF STATE]
proof (state)
this:
max_list (vars_fm p) < ?n \<Longrightarrow> \<lbrakk>?E(?n := x), F, G\<rbrakk> p = \<lbrakk>?E, F, G\<rbrakk> p
max_list (vars_fm (\<^bold>\<forall> p)) < n

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>?case = ((\<forall>y. \<lbrakk>\<lambda>m. (y \<Zsemi> E(n := x)) m, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>y \<Zsemi> E(n := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))
[PROOF STEP]
by (simp add: fun_upd_def)
[PROOF STATE]
proof (state)
this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>y \<Zsemi> E(n := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>y \<Zsemi> E(n := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>y \<Zsemi> E(n := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
using Uni
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>y \<Zsemi> E(n := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>y \<Zsemi> E, F, G\<rbrakk> p))
max_list (vars_fm p) < ?n \<Longrightarrow> \<lbrakk>?E(?n := x), F, G\<rbrakk> p = \<lbrakk>?E, F, G\<rbrakk> p
max_list (vars_fm (\<^bold>\<forall> p)) < n

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)

goal (2 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
[PROOF STEP]
qed (auto simp: max_list_append cong: map_cong)


[STATEMENT]
lemma dom_combination_dom_union: "dom (\<tau>;;\<tau>') = dom \<tau> \<union> dom \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<tau>;;\<tau>') = dom \<tau> \<union> dom \<tau>'
[PROOF STEP]
by auto


[STATEMENT]
lemma injective_cntxt [simp]: "(\<E>[e1] = \<E>[e2]) = (e1 = e2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<E> [e1] = \<E> [e2]) = (e1 = e2)
[PROOF STEP]
by (induction \<E>) auto


[STATEMENT]
lemma VE_empty_cntxt [simp]: "(VE v = \<E>[e]) = (\<E> = \<box> \<and> VE v = e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (VE v = \<E> [e]) = (\<E> = \<box> \<and> VE v = e)
[PROOF STEP]
by (cases \<E>, auto)


[STATEMENT]
lemma plugged_redex_not_val [simp]: "redex r \<Longrightarrow> (\<E> \<lhd> r) \<noteq> (VE t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redex r \<Longrightarrow> \<E> [r] \<noteq> VE t
[PROOF STEP]
by (cases \<E>) auto


[STATEMENT]
lemma plug_decomposition_equivalence: "redex r \<Longrightarrow> decompose e \<E> r = (\<E>[r] = e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. redex r \<Longrightarrow> decompose e \<E> r = (\<E> [r] = e)
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>redex r; decompose e \<E> r\<rbrakk> \<Longrightarrow> \<E> [r] = e
 2. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
assume x: "decompose e \<E> r"
[PROOF STATE]
proof (state)
this:
decompose e \<E> r

goal (2 subgoals):
 1. \<lbrakk>redex r; decompose e \<E> r\<rbrakk> \<Longrightarrow> \<E> [r] = e
 2. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
show "\<E>[r] = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E> [r] = e
[PROOF STEP]
proof (use x in \<open>induct rule: decompose.induct\<close>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>e. redex e \<Longrightarrow> \<box> [e] = e
 2. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 3. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 4. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 6. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 7. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 8. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 9. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
case (top_redex e)
[PROOF STATE]
proof (state)
this:
redex e

goal (9 subgoals):
 1. \<And>e. redex e \<Longrightarrow> \<box> [e] = e
 2. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 3. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 4. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 6. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 7. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 8. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 9. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
thus "\<box>[e] = e"
[PROOF STATE]
proof (prove)
using this:
redex e

goal (1 subgoal):
 1. \<box> [e] = e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<box> [e] = e

goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
case (lapply e\<^sub>1 e\<^sub>2 \<E> r)
[PROOF STATE]
proof (state)
this:
\<not> redex (Apply e\<^sub>1 e\<^sub>2)
decompose e\<^sub>1 \<E> r
\<E> [r] = e\<^sub>1

goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
have "(ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply (\<E>[r]) e\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply (\<E> [r]) e\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply (\<E> [r]) e\<^sub>2

goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply (\<E> [r]) e\<^sub>2

goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
have "... = Apply e\<^sub>1 e\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Apply (\<E> [r]) e\<^sub>2 = Apply e\<^sub>1 e\<^sub>2
[PROOF STEP]
using \<open>\<E>[r] = e\<^sub>1\<close>
[PROOF STATE]
proof (prove)
using this:
\<E> [r] = e\<^sub>1

goal (1 subgoal):
 1. Apply (\<E> [r]) e\<^sub>2 = Apply e\<^sub>1 e\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Apply (\<E> [r]) e\<^sub>2 = Apply e\<^sub>1 e\<^sub>2

goal (8 subgoals):
 1. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Apply e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
 2. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 3. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 5. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 6. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 7. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 8. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Apply (\<E> [r]) e\<^sub>2 = Apply e\<^sub>1 e\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Apply (\<E> [r]) e\<^sub>2 = Apply e\<^sub>1 e\<^sub>2

goal (1 subgoal):
 1. (ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ApplyL\<^sub>\<E> \<E> e\<^sub>2) [r] = Apply e\<^sub>1 e\<^sub>2

goal (7 subgoals):
 1. \<And>v e \<E> r. \<lbrakk>\<not> redex (Apply (VE v) e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (ApplyR\<^sub>\<E> v \<E>) [r] = Apply (VE v) e
 2. \<And>e\<^sub>1 e\<^sub>2 e\<^sub>3 \<E> r. \<lbrakk>\<not> redex (Ite e\<^sub>1 e\<^sub>2 e\<^sub>3); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (Ite\<^sub>\<E> \<E> e\<^sub>2 e\<^sub>3) [r] = Ite e\<^sub>1 e\<^sub>2 e\<^sub>3
 3. \<And>e \<E> r. \<lbrakk>\<not> redex (Ref e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Ref\<^sub>\<E> \<E>) [r] = Ref e
 4. \<And>e \<E> r. \<lbrakk>\<not> redex (Read e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Read\<^sub>\<E> \<E>) [r] = Read e
 5. \<And>e\<^sub>1 e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign e\<^sub>1 e\<^sub>2); decompose e\<^sub>1 \<E> r; \<E> [r] = e\<^sub>1\<rbrakk> \<Longrightarrow> (AssignL\<^sub>\<E> \<E> e\<^sub>2) [r] = Assign e\<^sub>1 e\<^sub>2
 6. \<And>l e\<^sub>2 \<E> r. \<lbrakk>\<not> redex (Assign (VE (Loc l)) e\<^sub>2); decompose e\<^sub>2 \<E> r; \<E> [r] = e\<^sub>2\<rbrakk> \<Longrightarrow> (AssignR\<^sub>\<E> l \<E>) [r] = Assign (VE (Loc l)) e\<^sub>2
 7. \<And>e \<E> r. \<lbrakk>\<not> redex (Rjoin e); decompose e \<E> r; \<E> [r] = e\<rbrakk> \<Longrightarrow> (Rjoin\<^sub>\<E> \<E>) [r] = Rjoin e
[PROOF STEP]
qed simp+
[PROOF STATE]
proof (state)
this:
\<E> [r] = e

goal (1 subgoal):
 1. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
assume red: "redex r" and  eq: "\<E>[r] = e"
[PROOF STATE]
proof (state)
this:
redex r
\<E> [r] = e

goal (1 subgoal):
 1. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
have "decompose (\<E>[r]) \<E> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decompose (\<E> [r]) \<E> r
[PROOF STEP]
by (induct \<E>) (use red in \<open>auto intro: decompose.intros\<close>)
[PROOF STATE]
proof (state)
this:
decompose (\<E> [r]) \<E> r

goal (1 subgoal):
 1. \<lbrakk>redex r; \<E> [r] = e\<rbrakk> \<Longrightarrow> decompose e \<E> r
[PROOF STEP]
thus "decompose e \<E> r"
[PROOF STATE]
proof (prove)
using this:
decompose (\<E> [r]) \<E> r

goal (1 subgoal):
 1. decompose e \<E> r
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
decompose e \<E> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique_decomposition: "decompose e \<E>\<^sub>1 r\<^sub>1 \<Longrightarrow> decompose e \<E>\<^sub>2 r\<^sub>2 \<Longrightarrow> \<E>\<^sub>1 = \<E>\<^sub>2 \<and> r\<^sub>1 = r\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>decompose e \<E>\<^sub>1 r\<^sub>1; decompose e \<E>\<^sub>2 r\<^sub>2\<rbrakk> \<Longrightarrow> \<E>\<^sub>1 = \<E>\<^sub>2 \<and> r\<^sub>1 = r\<^sub>2
[PROOF STEP]
by (induct arbitrary: \<E>\<^sub>2 rule: decompose.induct) auto


[STATEMENT]
lemma completion_eq [simp]:
  assumes
    red_e: "redex r" and
    red_e': "redex r'"
  shows "(\<E>[r] = \<E>'[r']) = (\<E> = \<E>' \<and> r = r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<E> [r] = \<E>' [r']) = (\<E> = \<E>' \<and> r = r')
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>' \<and> r = r'
 2. \<E> = \<E>' \<and> r = r' \<Longrightarrow> \<E> [r] = \<E>' [r']
[PROOF STEP]
show "\<E>[r] = \<E>'[r'] \<Longrightarrow> \<E> = \<E>' \<and> r = r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>' \<and> r = r'
[PROOF STEP]
proof (rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>'
 2. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
assume eq: "\<E>[r] = \<E>'[r']"
[PROOF STATE]
proof (state)
this:
\<E> [r] = \<E>' [r']

goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>'
 2. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
have "decompose (\<E>[r]) \<E> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decompose (\<E> [r]) \<E> r
[PROOF STEP]
using plug_decomposition_equivalence red_e
[PROOF STATE]
proof (prove)
using this:
redex ?r \<Longrightarrow> decompose ?e ?\<E> ?r = (?\<E> [?r] = ?e)
redex r

goal (1 subgoal):
 1. decompose (\<E> [r]) \<E> r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
decompose (\<E> [r]) \<E> r

goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>'
 2. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
hence fst_decomp:"decompose (\<E>'[r']) \<E> r"
[PROOF STATE]
proof (prove)
using this:
decompose (\<E> [r]) \<E> r

goal (1 subgoal):
 1. decompose (\<E>' [r']) \<E> r
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
decompose (\<E>' [r']) \<E> r

goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>'
 2. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
have snd_decomp: "decompose (\<E>'[r']) \<E>' r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decompose (\<E>' [r']) \<E>' r'
[PROOF STEP]
using plug_decomposition_equivalence red_e'
[PROOF STATE]
proof (prove)
using this:
redex ?r \<Longrightarrow> decompose ?e ?\<E> ?r = (?\<E> [?r] = ?e)
redex r'

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

goal (2 subgoals):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>'
 2. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
show cntxts_eq: "\<E> = \<E>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E> = \<E>'
[PROOF STEP]
using fst_decomp snd_decomp unique_decomposition
[PROOF STATE]
proof (prove)
using this:
decompose (\<E>' [r']) \<E> r
decompose (\<E>' [r']) \<E>' r'
\<lbrakk>decompose ?e ?\<E>\<^sub>1 ?r\<^sub>1; decompose ?e ?\<E>\<^sub>2 ?r\<^sub>2\<rbrakk> \<Longrightarrow> ?\<E>\<^sub>1 = ?\<E>\<^sub>2 \<and> ?r\<^sub>1 = ?r\<^sub>2

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

goal (1 subgoal):
 1. \<E> [r] = \<E>' [r'] \<Longrightarrow> r = r'
[PROOF STEP]
show "r = r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = r'
[PROOF STEP]
using cntxts_eq eq
[PROOF STATE]
proof (prove)
using this:
\<E> = \<E>'
\<E> [r] = \<E>' [r']

goal (1 subgoal):
 1. r = r'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = r'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<E> [r] = \<E>' [r'] \<Longrightarrow> \<E> = \<E>' \<and> r = r'

goal (1 subgoal):
 1. \<E> = \<E>' \<and> r = r' \<Longrightarrow> \<E> [r] = \<E>' [r']
[PROOF STEP]
qed simp


[STATEMENT]
lemma fusion_partially_correct:
  assumes wrap_unwrap: "wrap oo unwrap = ID"
  assumes work: "work = fix\<cdot>(unwrap oo body oo wrap)"
  assumes body': "unwrap oo body oo wrap = body' oo unwrap oo wrap"
  shows "fix\<cdot>body' \<sqsubseteq> work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>body' \<sqsubseteq> work
[PROOF STEP]
proof(rule fix_least)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "work = (unwrap oo body oo wrap)\<cdot>work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. work = (unwrap oo body oo wrap)\<cdot>work
[PROOF STEP]
using work
[PROOF STATE]
proof (prove)
using this:
work = fix\<cdot>(unwrap oo body oo wrap)

goal (1 subgoal):
 1. work = (unwrap oo body oo wrap)\<cdot>work
[PROOF STEP]
by (simp add: fix_eq[symmetric])
[PROOF STATE]
proof (state)
this:
work = (unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
work = (unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "... = (body' oo unwrap oo wrap)\<cdot>work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>work
[PROOF STEP]
using body'
[PROOF STATE]
proof (prove)
using this:
unwrap oo body oo wrap = body' oo unwrap oo wrap

goal (1 subgoal):
 1. (unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>work
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "... = (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body' oo unwrap oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work)
[PROOF STEP]
using work
[PROOF STATE]
proof (prove)
using this:
work = fix\<cdot>(unwrap oo body oo wrap)

goal (1 subgoal):
 1. (body' oo unwrap oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work)
[PROOF STEP]
by (simp add: fix_eq[symmetric])
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work)

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap)\<cdot>work = (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work)

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "... = (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work) = (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work) = (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap)\<cdot>((unwrap oo body oo wrap)\<cdot>work) = (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "... = (body' oo unwrap oo body oo wrap)\<cdot>work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo body oo wrap)\<cdot>work
[PROOF STEP]
using wrap_unwrap
[PROOF STATE]
proof (prove)
using this:
wrap oo unwrap = ID

goal (1 subgoal):
 1. (body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo body oo wrap)\<cdot>work
[PROOF STEP]
by (simp add: assoc_oo)
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo wrap oo unwrap oo body oo wrap)\<cdot>work = (body' oo unwrap oo body oo wrap)\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
have "... = body'\<cdot>work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body' oo unwrap oo body oo wrap)\<cdot>work = body'\<cdot>work
[PROOF STEP]
using work
[PROOF STATE]
proof (prove)
using this:
work = fix\<cdot>(unwrap oo body oo wrap)

goal (1 subgoal):
 1. (body' oo unwrap oo body oo wrap)\<cdot>work = body'\<cdot>work
[PROOF STEP]
by (simp add: fix_eq[symmetric])
[PROOF STATE]
proof (state)
this:
(body' oo unwrap oo body oo wrap)\<cdot>work = body'\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
work = body'\<cdot>work
[PROOF STEP]
show "body'\<cdot>work = work"
[PROOF STATE]
proof (prove)
using this:
work = body'\<cdot>work

goal (1 subgoal):
 1. body'\<cdot>work = work
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
body'\<cdot>work = work

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wrap_strict[simp]: "wrap\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma wrap_unwrap: "wrap oo unwrap = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrap oo unwrap = ID
[PROOF STEP]
by (simp add: cfun_eq_iff)


[STATEMENT]
lemma body'_strict[simp]: "body'\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. body'\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma body_body': "unwrap oo body oo wrap = body' oo unwrap oo wrap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrap oo body oo wrap = body' oo unwrap oo wrap
[PROOF STEP]
by (simp add: cfun_eq_iff)


[STATEMENT]
lemma "fix\<cdot>body' \<sqsubseteq> fix\<cdot>(unwrap oo body oo wrap)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>body' \<sqsubseteq> fix\<cdot>(unwrap oo body oo wrap)
[PROOF STEP]
by (rule fusion_partially_correct[OF wrap_unwrap refl body_body'])


[STATEMENT]
lemma "\<not> fix\<cdot>(unwrap oo body oo wrap) \<sqsubseteq> fix\<cdot>body'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'
[PROOF STEP]
have l: "fix\<cdot>(unwrap oo body oo wrap) = B\<cdot>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) = B\<cdot>A
[PROOF STEP]
by (subst fix_eq) simp
[PROOF STATE]
proof (state)
this:
fix\<cdot>(unwrap oo body oo wrap) = B\<cdot>A

goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'
[PROOF STEP]
have r: "fix\<cdot>body' = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>body' = \<bottom>
[PROOF STEP]
by (simp add: fix_strict)
[PROOF STATE]
proof (state)
this:
fix\<cdot>body' = \<bottom>

goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'
[PROOF STEP]
from l r
[PROOF STATE]
proof (chain)
picking this:
fix\<cdot>(unwrap oo body oo wrap) = B\<cdot>A
fix\<cdot>body' = \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fix\<cdot>(unwrap oo body oo wrap) = B\<cdot>A
fix\<cdot>body' = \<bottom>

goal (1 subgoal):
 1. fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fix\<cdot>(unwrap oo body oo wrap) \<notsqsubseteq> fix\<cdot>body'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quality_increasesI [intro!]:
  assumes "\<And>dip. dip \<in> kD(rt \<xi>) \<Longrightarrow> dip \<in> kD(rt \<xi>')"
      and "\<And>dip. \<lbrakk> dip \<in> kD(rt \<xi>); dip \<in> kD(rt \<xi>') \<rbrakk> \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>'"
      and "\<And>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip"
    shows "quality_increases \<xi> \<xi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quality_increases \<xi> \<xi>'
[PROOF STEP]
unfolding quality_increases_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>dip\<in>kD (rt \<xi>). dip \<in> kD (rt \<xi>') \<and> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>') \<and> (\<forall>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?dip \<in> kD (rt \<xi>) \<Longrightarrow> ?dip \<in> kD (rt \<xi>')
\<lbrakk>?dip \<in> kD (rt \<xi>); ?dip \<in> kD (rt \<xi>')\<rbrakk> \<Longrightarrow> rt \<xi> \<sqsubseteq>\<^bsub>?dip\<^esub> rt \<xi>'
sqn (rt \<xi>) ?dip \<le> sqn (rt \<xi>') ?dip

goal (1 subgoal):
 1. (\<forall>dip\<in>kD (rt \<xi>). dip \<in> kD (rt \<xi>') \<and> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>') \<and> (\<forall>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip)
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma quality_increasesE [elim]:
    fixes dip
  assumes "quality_increases \<xi> \<xi>'"
      and "dip\<in>kD(rt \<xi>)"
      and "\<lbrakk> dip \<in> kD(rt \<xi>'); rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>'; sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip \<rbrakk> \<Longrightarrow> R dip \<xi> \<xi>'"
    shows "R dip \<xi> \<xi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quality_increases \<xi> \<xi>'
dip \<in> kD (rt \<xi>)
\<lbrakk>dip \<in> kD (rt \<xi>'); rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>'; sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip\<rbrakk> \<Longrightarrow> R dip \<xi> \<xi>'

goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
unfolding quality_increases_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>dip\<in>kD (rt \<xi>). dip \<in> kD (rt \<xi>') \<and> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>') \<and> (\<forall>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip)
dip \<in> kD (rt \<xi>)
\<lbrakk>dip \<in> kD (rt \<xi>'); rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>'; sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip\<rbrakk> \<Longrightarrow> R dip \<xi> \<xi>'

goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma quality_increases_rt_fresherD [dest]:
    fixes ip
  assumes "quality_increases \<xi> \<xi>'"
      and "ip\<in>kD(rt \<xi>)"
    shows "rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> rt \<xi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> rt \<xi>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quality_increases \<xi> \<xi>'
ip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. rt \<xi> \<sqsubseteq>\<^bsub>ip\<^esub> rt \<xi>'
[PROOF STEP]
by auto


[STATEMENT]
lemma quality_increases_sqnE [elim]:
    fixes dip
  assumes "quality_increases \<xi> \<xi>'"
      and "sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip \<Longrightarrow> R dip \<xi> \<xi>'"
    shows "R dip \<xi> \<xi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quality_increases \<xi> \<xi>'
sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip \<Longrightarrow> R dip \<xi> \<xi>'

goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
unfolding quality_increases_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>dip\<in>kD (rt \<xi>). dip \<in> kD (rt \<xi>') \<and> rt \<xi> \<sqsubseteq>\<^bsub>dip\<^esub> rt \<xi>') \<and> (\<forall>dip. sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip)
sqn (rt \<xi>) dip \<le> sqn (rt \<xi>') dip \<Longrightarrow> R dip \<xi> \<xi>'

goal (1 subgoal):
 1. R dip \<xi> \<xi>'
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma quality_increases_refl [intro, simp]: "quality_increases \<xi> \<xi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quality_increases \<xi> \<xi>
[PROOF STEP]
by rule simp_all


[STATEMENT]
lemma strictly_fresher_quality_increases_right [elim]:
    fixes \<sigma> \<sigma>' dip
  assumes "rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma> nhip)"
      and qinc: "quality_increases (\<sigma> nhip) (\<sigma>' nhip)"
      and "dip\<in>kD(rt (\<sigma> nhip))"
    shows "rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
from qinc
[PROOF STATE]
proof (chain)
picking this:
quality_increases (\<sigma> nhip) (\<sigma>' nhip)
[PROOF STEP]
have "rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)"
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> nhip) (\<sigma>' nhip)

goal (1 subgoal):
 1. rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
using \<open>dip\<in>kD(rt (\<sigma> nhip))\<close>
[PROOF STATE]
proof (prove)
using this:
quality_increases (\<sigma> nhip) (\<sigma>' nhip)
dip \<in> kD (rt (\<sigma> nhip))

goal (1 subgoal):
 1. rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)

goal (1 subgoal):
 1. rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
with \<open>rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma> nhip)\<close>
[PROOF STATE]
proof (chain)
picking this:
rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma> nhip)
rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma> nhip)
rt (\<sigma> nhip) \<sqsubseteq>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)

goal (1 subgoal):
 1. rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rt (\<sigma> i) \<sqsubset>\<^bsub>dip\<^esub> rt (\<sigma>' nhip)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kD_quality_increases [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
    shows "i\<in>kD(rt \<xi>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> kD (rt \<xi>')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>')
[PROOF STEP]
by auto


[STATEMENT]
lemma kD_nsqn_quality_increases [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
    shows "i\<in>kD(rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
[PROOF STEP]
have "i\<in>kD(rt \<xi>')"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> kD (rt \<xi>')

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in> kD (rt \<xi>')

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
i \<in> kD (rt \<xi>')
[PROOF STEP]
have "rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
i \<in> kD (rt \<xi>')

goal (1 subgoal):
 1. rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>')
rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'
[PROOF STEP]
have "nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>')
rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'

goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
using \<open>i\<in>kD(rt \<xi>)\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>')
rt \<xi> \<sqsubseteq>\<^bsub>i\<^esub> rt \<xi>'
i \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
by - (erule(2) rt_fresher_imp_nsqn_le)
[PROOF STATE]
proof (state)
this:
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
with \<open>i\<in>kD(rt \<xi>')\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>')
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>')
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> kD (rt \<xi>') \<and> nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nsqn_quality_increases [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
    shows "nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
by (rule kD_nsqn_quality_increases [THEN conjunct2])


[STATEMENT]
lemma kD_nsqn_quality_increases_trans [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "s \<le> nsqn (rt \<xi>) i"
      and "quality_increases \<xi> \<xi>'"
    shows "i\<in>kD(rt \<xi>') \<and> s \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> kD (rt \<xi>') \<and> s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> kD (rt \<xi>')
 2. s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
from \<open>i\<in>kD(rt \<xi>)\<close> and \<open>quality_increases \<xi> \<xi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
[PROOF STEP]
show "i\<in>kD(rt \<xi>')"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. i \<in> kD (rt \<xi>')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> kD (rt \<xi>')

goal (1 subgoal):
 1. s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
from \<open>i\<in>kD(rt \<xi>)\<close> and \<open>quality_increases \<xi> \<xi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
[PROOF STEP]
have "nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'

goal (1 subgoal):
 1. nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
with \<open>s \<le> nsqn (rt \<xi>) i\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<le> nsqn (rt \<xi>) i
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i
[PROOF STEP]
show "s \<le> nsqn (rt \<xi>') i"
[PROOF STATE]
proof (prove)
using this:
s \<le> nsqn (rt \<xi>) i
nsqn (rt \<xi>) i \<le> nsqn (rt \<xi>') i

goal (1 subgoal):
 1. s \<le> nsqn (rt \<xi>') i
[PROOF STEP]
by (rule le_trans)
[PROOF STATE]
proof (state)
this:
s \<le> nsqn (rt \<xi>') i

goal:
No subgoals!
[PROOF STEP]
qed