[STATEMENT]
lemma abc_mopup_measure_induct [case_names Step]:
  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), f n) \<in> abc_mopup_measure) \<Longrightarrow> \<exists>n. P (f n)
[PROOF STEP]
using wf_abc_mopup_measure
[PROOF STATE]
proof (prove)
using this:
wf abc_mopup_measure

goal (1 subgoal):
 1. (\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), f n) \<in> abc_mopup_measure) \<Longrightarrow> \<exists>n. P (f n)
[PROOF STEP]
by (metis wf_iff_no_infinite_down_chain)


[STATEMENT]
lemma mopup_erase_nonempty[simp]:
  "mopup_bef_erase_a (a, aa, []) lm n ires = False"
  "mopup_bef_erase_b (a, aa, []) lm n ires = False"
  "mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_bef_erase_a (a, aa, []) lm n ires = False &&& mopup_bef_erase_b (a, aa, []) lm n ires = False &&& mopup_aft_erase_b (2 * n + 3, aa, []) lm n ires = False
[PROOF STEP]
by(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps mopup_aft_erase_b.simps)


[STATEMENT]
lemma fetch_mopup_a_shift[simp]:
  assumes "0 < q" "q \<le> n"
  shows "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*q) Bk = (R, 2*q - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
proof(cases q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q = 0 \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
 2. \<And>nat. q = Suc nat \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
case (Suc nat)
[PROOF STATE]
proof (state)
this:
q = Suc nat

goal (2 subgoals):
 1. q = 0 \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
 2. \<And>nat. q = Suc nat \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < q
q \<le> n
q = Suc nat
[PROOF STEP]
have "mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! ((4 * nat) + 2)"
[PROOF STATE]
proof (prove)
using this:
0 < q
q \<le> n
q = Suc nat

goal (1 subgoal):
 1. mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < q
q \<le> n
q = Suc nat
0 < q
q \<le> n

goal (1 subgoal):
 1. mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
by (metis Suc_le_lessD add_2_eq_Suc' less_Suc_eq mopup_a_nth numeral_Bit0)
[PROOF STATE]
proof (state)
this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (2 subgoals):
 1. q = 0 \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
 2. \<And>nat. q = Suc nat \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
0 < q
q \<le> n
q = Suc nat

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
by(auto simp: fetch.simps nth_of.simps nth_append)
[PROOF STATE]
proof (state)
this:
fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)

goal (1 subgoal):
 1. q = 0 \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * q) Bk = (R, 2 * q - 1)
[PROOF STEP]
qed (insert assms,auto)


[STATEMENT]
lemma mopup_halt:
  assumes
    less: "n < length lm"
    and inv: "mopup_inv (Suc 0, l, r) lm n ires"
    and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
    and P: "P = (\<lambda> (c, n). is_final c)"
  shows "\<exists> stp. P (f stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stp. P (f stp)
[PROOF STEP]
proof (induct rule: abc_mopup_measure_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>stp. \<not> P (f stp) \<Longrightarrow> (f (Suc stp), f stp) \<in> abc_mopup_measure
[PROOF STEP]
case (Step na)
[PROOF STATE]
proof (state)
this:
\<not> P (f na)

goal (1 subgoal):
 1. \<And>stp. \<not> P (f stp) \<Longrightarrow> (f (Suc stp), f stp) \<in> abc_mopup_measure
[PROOF STEP]
have h: "\<not> P (f na)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P (f na)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<not> P (f na)

goal (1 subgoal):
 1. \<And>stp. \<not> P (f stp) \<Longrightarrow> (f (Suc stp), f stp) \<in> abc_mopup_measure
[PROOF STEP]
show "(f (Suc na), f na) \<in> abc_mopup_measure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f (Suc na), f na) \<in> abc_mopup_measure
[PROOF STEP]
proof(simp add: f)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c. steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)
[PROOF STEP]
have "mopup_inv (a, b, c) lm n ires"
[PROOF STATE]
proof (prove)
using this:
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)

goal (1 subgoal):
 1. mopup_inv (a, b, c) lm n ires
[PROOF STEP]
using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
[PROOF STATE]
proof (prove)
using this:
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)
mopup_inv (Suc 0, l, r) lm n ires
n < length lm
\<lbrakk>n < length lm; mopup_inv (Suc 0, l, r) lm n ires\<rbrakk> \<Longrightarrow> mopup_inv (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) lm n ires

goal (1 subgoal):
 1. mopup_inv (a, b, c) lm n ires
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mopup_inv (a, b, c) lm n ires

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mopup_inv (a, b, c) lm n ires

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
have "a > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a
[PROOF STEP]
using h g
[PROOF STATE]
proof (prove)
using this:
\<not> P (f na)
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)

goal (1 subgoal):
 1. 0 < a
[PROOF STEP]
apply(simp add: f P)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < a

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mopup_inv (a, b, c) lm n ires
0 < a
[PROOF STEP]
have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure"
[PROOF STATE]
proof (prove)
using this:
mopup_inv (a, b, c) lm n ires
0 < a

goal (1 subgoal):
 1. ((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
[PROOF STEP]
apply(case_tac c;cases "hd c")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>mopup_inv (a, b, c) lm n ires; 0 < a; c = []; mopup_inv (a, b, c) lm n ires; 0 < a; hd c = Bk\<rbrakk> \<Longrightarrow> ((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
 2. \<lbrakk>mopup_inv (a, b, c) lm n ires; 0 < a; c = []; mopup_inv (a, b, c) lm n ires; 0 < a; hd c = Oc\<rbrakk> \<Longrightarrow> ((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
 3. \<And>aa list. \<lbrakk>mopup_inv (a, b, c) lm n ires; 0 < a; c = aa # list; mopup_inv (a, b, c) lm n ires; 0 < a; hd c = Bk\<rbrakk> \<Longrightarrow> ((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
 4. \<And>aa list. \<lbrakk>mopup_inv (a, b, c) lm n ires; 0 < a; c = aa # list; mopup_inv (a, b, c) lm n ires; 0 < a; hd c = Oc\<rbrakk> \<Longrightarrow> ((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
[PROOF STEP]
apply(auto split:if_splits simp add:step.simps mopup_inv.simps mopup_bef_erase_b.simps)
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<lbrakk>hd [] = Bk; mopup_jump_over1 (Suc (2 * n), b, []) lm n ires; c = []; a = Suc (2 * n)\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (Suc (2 * n), b, []), n) \<in> abc_mopup_measure
 2. \<lbrakk>c = []; mopup_aft_erase_a (Suc (Suc (2 * n)), b, []) lm n ires; hd [] = Bk; a = Suc (Suc (2 * n))\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (Suc (Suc (2 * n)), b, []), n) \<in> abc_mopup_measure
 3. \<lbrakk>c = []; mopup_aft_erase_c (2 * n + 4, b, []) lm n ires; hd [] = Bk; a = 2 * n + 4\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (2 * n + 4, b, []), n) \<in> abc_mopup_measure
 4. \<lbrakk>hd [] = Bk; mopup_left_moving (2 * n + 5, b, []) lm n ires; c = []; a = 2 * n + 5\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (2 * n + 5, b, []), n) \<in> abc_mopup_measure
 5. \<lbrakk>hd [] = Oc; mopup_jump_over1 (Suc (2 * n), b, []) lm n ires; c = []; a = Suc (2 * n)\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (Suc (2 * n), b, []), n) \<in> abc_mopup_measure
 6. \<lbrakk>c = []; mopup_aft_erase_a (Suc (Suc (2 * n)), b, []) lm n ires; hd [] = Oc; a = Suc (Suc (2 * n))\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (Suc (Suc (2 * n)), b, []), n) \<in> abc_mopup_measure
 7. \<lbrakk>c = []; mopup_aft_erase_c (2 * n + 4, b, []) lm n ires; hd [] = Oc; a = 2 * n + 4\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (2 * n + 4, b, []), n) \<in> abc_mopup_measure
 8. \<lbrakk>hd [] = Oc; mopup_left_moving (2 * n + 5, b, []) lm n ires; c = []; a = 2 * n + 5\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk of (a, s') \<Rightarrow> (s', update a (b, [])), n), (2 * n + 5, b, []), n) \<in> abc_mopup_measure
 9. \<And>list. \<lbrakk>0 < a; a \<le> 2 * n; mopup_bef_erase_a (a, b, Bk # list) lm n ires; c = Bk # list; a mod 2 = Suc 0\<rbrakk> \<Longrightarrow> (((Suc (Suc a), Bk # b, list), n), (a, b, Bk # list), n) \<in> abc_mopup_measure
 10. \<And>ln m rn. \<lbrakk>0 < a; a \<le> 2 * n; c = Bk # Oc \<up> m @ Bk # <drop (a div 2) lm> @ Bk \<up> rn; even a; b = Bk \<up> ln @ Bk # Bk # ires\<rbrakk> \<Longrightarrow> ((case fetch (mopup_a n @ shift mopup_b (2 * n)) a Bk of (aa, s') \<Rightarrow> (s', update aa (Bk \<up> ln @ Bk # Bk # ires, Bk # Oc \<up> m @ Bk # <drop (a div 2) lm> @ Bk \<up> rn)), n), (a, Bk \<up> ln @ Bk # Bk # ires, Bk # Oc \<up> m @ Bk # <drop (a div 2) lm> @ Bk \<up> rn), n) \<in> abc_mopup_measure
A total of 22 subgoals...
[PROOF STEP]
by (auto split:if_splits simp: mopupfetchs abc_mopup_measure_def )
[PROOF STATE]
proof (state)
this:
((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na)
      (mopup_a n @ shift mopup_b (2 * n), 0), n),
      steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
      \<in> abc_mopup_measure"
[PROOF STATE]
proof (prove)
using this:
((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
((step0 (a, b, c) (mopup_a n @ shift mopup_b (2 * n)), n), (a, b, c), n) \<in> abc_mopup_measure
steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na = (a, b, c)

goal (1 subgoal):
 1. ((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((step0 (steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na) (mopup_a n @ shift mopup_b (2 * n)), n), steps0 (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n)) na, n) \<in> abc_mopup_measure

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f (Suc na), f na) \<in> abc_mopup_measure

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mopup_inv_start:
  "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
[PROOF STEP]
apply(cases am;auto simp: mopup_inv.simps mopup_bef_erase_a.simps mopup_jump_over1.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>n < Suc (length list); am = a # list; Suc 0 \<le> n\<rbrakk> \<Longrightarrow> \<exists>m rn. <a # list> @ Bk \<up> k = Oc \<up> m @ Bk # <list> @ Bk \<up> rn
 2. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. <a # list> @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> <a # list> @ Bk \<up> k = Oc # Oc \<up> (a # list) ! n
 3. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. <a # list> @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> length list \<le> n
[PROOF STEP]
apply(auto simp: tape_of_nl_cons)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a list. \<lbrakk>n < Suc (length list); am = a # list; Suc 0 \<le> n; list \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>m rn. Oc # Oc \<up> a @ Bk # <list> @ Bk \<up> k = Oc \<up> m @ Bk # <list> @ Bk \<up> rn
 2. \<And>a. \<lbrakk>am = [a]; \<not> Suc 0 \<le> n; \<forall>rn. Oc \<up> a @ Bk \<up> k \<noteq> Oc \<up> [a] ! n @ Bk # Bk \<up> rn\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk \<up> k = Oc \<up> [a] ! n
 3. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. Oc \<up> a @ Bk # <list> @ Bk \<up> k \<noteq> Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn; list \<noteq> []\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk # <list> @ Bk \<up> k = Oc \<up> (a # list) ! n
 4. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. (if list = [] then Oc \<up> Suc a else Oc \<up> Suc a @ Bk # <list>) @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> length list \<le> n
[PROOF STEP]
apply(rule_tac x = "Suc (hd am)" in exI, rule_tac x = k in exI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>am = [a]; \<not> Suc 0 \<le> n; \<forall>rn. Oc \<up> a @ Bk \<up> k \<noteq> Oc \<up> [a] ! n @ Bk # Bk \<up> rn\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk \<up> k = Oc \<up> [a] ! n
 2. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. Oc \<up> a @ Bk # <list> @ Bk \<up> k \<noteq> Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn; list \<noteq> []\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk # <list> @ Bk \<up> k = Oc \<up> (a # list) ! n
 3. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. (if list = [] then Oc \<up> Suc a else Oc \<up> Suc a @ Bk # <list>) @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> length list \<le> n
[PROOF STEP]
apply(cases k;cases n;force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. Oc \<up> a @ Bk # <list> @ Bk \<up> k \<noteq> Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn; list \<noteq> []\<rbrakk> \<Longrightarrow> Oc \<up> a @ Bk # <list> @ Bk \<up> k = Oc \<up> (a # list) ! n
 2. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. (if list = [] then Oc \<up> Suc a else Oc \<up> Suc a @ Bk # <list>) @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> length list \<le> n
[PROOF STEP]
apply(cases n; force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>am = a # list; \<not> Suc 0 \<le> n; \<forall>rn. (if list = [] then Oc \<up> Suc a else Oc \<up> Suc a @ Bk # <list>) @ Bk \<up> k \<noteq> Oc # Oc \<up> (a # list) ! n @ Bk # <drop n list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> length list \<le> n
[PROOF STEP]
by(cases n; force split:if_splits)


[STATEMENT]
lemma mopup_correct:
  assumes less: "n < length (am::nat list)"
    and rs: "am ! n = rs"
  shows "\<exists> stp i j. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
    = (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
n < length am

goal (1 subgoal):
 1. \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < length am \<Longrightarrow> \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
have a: "mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
n < length am

goal (1 subgoal):
 1. mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
[PROOF STEP]
apply(simp add: mopup_inv_start)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires

goal (1 subgoal):
 1. n < length am \<Longrightarrow> \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
[PROOF STEP]
have "\<exists> stp. is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)"
[PROOF STATE]
proof (prove)
using this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires

goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
[PROOF STEP]
using less mopup_halt[of n am  "Bk # Bk # ires" "<am> @ Bk \<up> k" ires
        "(\<lambda>stp. (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
        "(\<lambda>(c, n). is_final c)"]
[PROOF STATE]
proof (prove)
using this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
n < length am
\<lbrakk>n < length am; mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires; (\<lambda>stp. (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp, n)) = (\<lambda>stp. (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp, n)); (\<lambda>(c, n). is_final c) = (\<lambda>(c, n). is_final c)\<rbrakk> \<Longrightarrow> \<exists>stp. case (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp, n) of (c, n) \<Rightarrow> is_final c

goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)

goal (1 subgoal):
 1. n < length am \<Longrightarrow> \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
[PROOF STEP]
obtain stp where b:
    "is_final (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)

goal (1 subgoal):
 1. (\<And>stp. is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)

goal (1 subgoal):
 1. n < length am \<Longrightarrow> \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
[PROOF STEP]
have
    "mopup_inv (steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n), 0) stp)
    am n ires"
[PROOF STATE]
proof (prove)
using this:
mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires
is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)

goal (1 subgoal):
 1. mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires
[PROOF STEP]
apply(rule_tac mopup_inv_steps, simp_all add: less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires

goal (1 subgoal):
 1. n < length am \<Longrightarrow> \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
from b and this
[PROOF STATE]
proof (chain)
picking this:
is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp)
mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires

goal (1 subgoal):
 1. \<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
apply(rule_tac x = stp in exI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp); mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires\<rbrakk> \<Longrightarrow> \<exists>i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
apply(case_tac "steps (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k)
      (mopup_a n @ shift mopup_b (2 * n), 0) stp")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>is_final (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp); mopup_inv (steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp) am n ires; steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (a, b, c)\<rbrakk> \<Longrightarrow> \<exists>i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)
[PROOF STEP]
apply(simp add: mopup_inv.simps mopup_stop.simps rs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a = 0; (\<exists>ln. b = Bk \<up> ln @ Bk # Bk # ires) \<and> (\<exists>rn. c = <rs> @ Bk \<up> rn); steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, b, c)\<rbrakk> \<Longrightarrow> \<exists>j. c = Oc # Oc \<up> rs @ Bk \<up> j
[PROOF STEP]
using rs
[PROOF STATE]
proof (prove)
using this:
am ! n = rs

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>a = 0; (\<exists>ln. b = Bk \<up> ln @ Bk # Bk # ires) \<and> (\<exists>rn. c = <rs> @ Bk \<up> rn); steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, b, c)\<rbrakk> \<Longrightarrow> \<exists>j. c = Oc # Oc \<up> rs @ Bk \<up> j
[PROOF STEP]
apply(simp add: tape_of_nat_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>stp i j. steps0 (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) (mopup_a n @ shift mopup_b (2 * n)) stp = (0, Bk \<up> i @ Bk # Bk # ires, Oc # Oc \<up> rs @ Bk \<up> j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma composable_mopup_n_tm[intro]: "composable_tm (mopup_n_tm n, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composable_tm0 (mopup_n_tm n)
[PROOF STEP]
by(induct n, auto simp add: shift.simps mopup_b_def composable_tm.simps)


[STATEMENT]
lemma true_lit_simps[simp]:
  "I \<Turnstile>l Pos A \<longleftrightarrow> A \<in> I"
  "I \<Turnstile>l Neg A \<longleftrightarrow> A \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>l Pos A) = (A \<in> I) &&& (I \<Turnstile>l Neg A) = (A \<notin> I)
[PROOF STEP]
unfolding true_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if is_pos (Pos A) then \<lambda>P. P else Not) (atm_of (Pos A) \<in> I) = (A \<in> I) &&& (if is_pos (Neg A) then \<lambda>P. P else Not) (atm_of (Neg A) \<in> I) = (A \<notin> I)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_lit_iff[iff]: "I \<Turnstile>l L \<longleftrightarrow> (\<exists>A. L = Pos A \<and> A \<in> I \<or> L = Neg A \<and> A \<notin> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>l L) = (\<exists>A. L = Pos A \<and> A \<in> I \<or> L = Neg A \<and> A \<notin> I)
[PROOF STEP]
by (cases L) simp+


[STATEMENT]
lemma true_cls_empty[iff]: "\<not> I \<Turnstile> {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> I \<Turnstile> {#}
[PROOF STEP]
unfolding true_cls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Multiset.Bex {#} ((\<Turnstile>l) I)
[PROOF STEP]
by simp


[STATEMENT]
lemma true_cls_singleton[iff]: "I \<Turnstile> {#L#} \<longleftrightarrow> I \<Turnstile>l L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile> {#L#}) = (I \<Turnstile>l L)
[PROOF STEP]
unfolding true_cls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Bex {#L#} ((\<Turnstile>l) I) = (I \<Turnstile>l L)
[PROOF STEP]
by simp


[STATEMENT]
lemma true_cls_add_mset[iff]: "I \<Turnstile> add_mset C D \<longleftrightarrow> I \<Turnstile>l C \<or> I \<Turnstile> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile> add_mset C D) = (I \<Turnstile>l C \<or> I \<Turnstile> D)
[PROOF STEP]
unfolding true_cls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Bex (add_mset C D) ((\<Turnstile>l) I) = (I \<Turnstile>l C \<or> Multiset.Bex D ((\<Turnstile>l) I))
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_union[iff]: "I \<Turnstile> C + D \<longleftrightarrow> I \<Turnstile> C \<or> I \<Turnstile> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile> C + D) = (I \<Turnstile> C \<or> I \<Turnstile> D)
[PROOF STEP]
unfolding true_cls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Bex (C + D) ((\<Turnstile>l) I) = (Multiset.Bex C ((\<Turnstile>l) I) \<or> Multiset.Bex D ((\<Turnstile>l) I))
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mono: "set_mset C \<subseteq> set_mset D \<Longrightarrow> I \<Turnstile> C \<Longrightarrow> I \<Turnstile> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_mset C \<subseteq> set_mset D; I \<Turnstile> C\<rbrakk> \<Longrightarrow> I \<Turnstile> D
[PROOF STEP]
unfolding true_cls_def subset_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>#C. x \<in># D; Multiset.Bex C ((\<Turnstile>l) I)\<rbrakk> \<Longrightarrow> Multiset.Bex D ((\<Turnstile>l) I)
[PROOF STEP]
by metis


[STATEMENT]
lemma true_cls_replicate_mset[iff]: "I \<Turnstile> replicate_mset n L \<longleftrightarrow> n \<noteq> 0 \<and> I \<Turnstile>l L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile> replicate_mset n L) = (n \<noteq> 0 \<and> I \<Turnstile>l L)
[PROOF STEP]
by (simp add: true_cls_def)


[STATEMENT]
lemma neg_literal_notin_imp_true_cls[intro]: "Neg A \<in># C \<Longrightarrow> A \<notin> I \<Longrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Neg A \<in># C; A \<notin> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
using true_cls_def
[PROOF STATE]
proof (prove)
using this:
(?I \<Turnstile> ?C) = (\<exists>L\<in>#?C. ?I \<Turnstile>l L)

goal (1 subgoal):
 1. \<lbrakk>Neg A \<in># C; A \<notin> I\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
by blast


[STATEMENT]
lemma pos_neg_in_imp_true: "Pos A \<in># C \<Longrightarrow> Neg A \<in># C \<Longrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; Neg A \<in># C\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
using true_cls_def
[PROOF STATE]
proof (prove)
using this:
(?I \<Turnstile> ?C) = (\<exists>L\<in>#?C. ?I \<Turnstile>l L)

goal (1 subgoal):
 1. \<lbrakk>Pos A \<in># C; Neg A \<in># C\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
by blast


[STATEMENT]
lemma true_clss_empty[iff]: "I \<Turnstile>s {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile>s {}
[PROOF STEP]
by (simp add: true_clss_def)


[STATEMENT]
lemma true_clss_singleton[iff]: "I \<Turnstile>s {C} \<longleftrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>s {C}) = (I \<Turnstile> C)
[PROOF STEP]
unfolding true_clss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball {C} ((\<Turnstile>) I) = (I \<Turnstile> C)
[PROOF STEP]
by blast


[STATEMENT]
lemma true_clss_insert[iff]: "I \<Turnstile>s insert C DD \<longleftrightarrow> I \<Turnstile> C \<and> I \<Turnstile>s DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>s insert C DD) = (I \<Turnstile> C \<and> I \<Turnstile>s DD)
[PROOF STEP]
unfolding true_clss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (insert C DD) ((\<Turnstile>) I) = (I \<Turnstile> C \<and> Ball DD ((\<Turnstile>) I))
[PROOF STEP]
by blast


[STATEMENT]
lemma true_clss_union[iff]: "I \<Turnstile>s CC \<union> DD \<longleftrightarrow> I \<Turnstile>s CC \<and> I \<Turnstile>s DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>s CC \<union> DD) = (I \<Turnstile>s CC \<and> I \<Turnstile>s DD)
[PROOF STEP]
unfolding true_clss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (CC \<union> DD) ((\<Turnstile>) I) = (Ball CC ((\<Turnstile>) I) \<and> Ball DD ((\<Turnstile>) I))
[PROOF STEP]
by blast


[STATEMENT]
lemma true_clss_Union[iff]: "I \<Turnstile>s \<Union> CCC \<longleftrightarrow> (\<forall>CC \<in> CCC. I \<Turnstile>s CC)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>s \<Union> CCC) = (\<forall>CC\<in>CCC. I \<Turnstile>s CC)
[PROOF STEP]
unfolding true_clss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (\<Union> CCC) ((\<Turnstile>) I) = (\<forall>CC\<in>CCC. Ball CC ((\<Turnstile>) I))
[PROOF STEP]
by simp


[STATEMENT]
lemma true_clss_mono: "DD \<subseteq> CC \<Longrightarrow> I \<Turnstile>s CC \<Longrightarrow> I \<Turnstile>s DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>DD \<subseteq> CC; I \<Turnstile>s CC\<rbrakk> \<Longrightarrow> I \<Turnstile>s DD
[PROOF STEP]
by (simp add: subsetD true_clss_def)


[STATEMENT]
lemma true_clss_mono_strong: "(\<forall>D \<in> DD. \<exists>C \<in> CC. C \<subseteq># D) \<Longrightarrow> I \<Turnstile>s CC \<Longrightarrow> I \<Turnstile>s DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>D\<in>DD. \<exists>C\<in>CC. C \<subseteq># D; I \<Turnstile>s CC\<rbrakk> \<Longrightarrow> I \<Turnstile>s DD
[PROOF STEP]
unfolding true_clss_def true_cls_def true_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>D\<in>DD. \<exists>C\<in>CC. C \<subseteq># D; \<forall>C\<in>CC. \<exists>L\<in>#C. (if is_pos L then \<lambda>P. P else Not) (atm_of L \<in> I)\<rbrakk> \<Longrightarrow> \<forall>C\<in>DD. \<exists>L\<in>#C. (if is_pos L then \<lambda>P. P else Not) (atm_of L \<in> I)
[PROOF STEP]
by (meson mset_subset_eqD)


[STATEMENT]
lemma true_clss_subclause: "C \<subseteq># D \<Longrightarrow> I \<Turnstile>s {C} \<Longrightarrow> I \<Turnstile>s {D}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<subseteq># D; I \<Turnstile>s {C}\<rbrakk> \<Longrightarrow> I \<Turnstile>s {D}
[PROOF STEP]
by (rule true_clss_mono_strong[of _ "{C}"]) auto


[STATEMENT]
lemma satisfiable_antimono: "CC \<subseteq> DD \<Longrightarrow> satisfiable DD \<Longrightarrow> satisfiable CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>CC \<subseteq> DD; satisfiable DD\<rbrakk> \<Longrightarrow> satisfiable CC
[PROOF STEP]
using true_clss_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?DD \<subseteq> ?CC; ?I \<Turnstile>s ?CC\<rbrakk> \<Longrightarrow> ?I \<Turnstile>s ?DD

goal (1 subgoal):
 1. \<lbrakk>CC \<subseteq> DD; satisfiable DD\<rbrakk> \<Longrightarrow> satisfiable CC
[PROOF STEP]
by blast


[STATEMENT]
lemma unsatisfiable_mono: "CC \<subseteq> DD \<Longrightarrow> \<not> satisfiable CC \<Longrightarrow> \<not> satisfiable DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>CC \<subseteq> DD; \<not> satisfiable CC\<rbrakk> \<Longrightarrow> \<not> satisfiable DD
[PROOF STEP]
using satisfiable_antimono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?CC \<subseteq> ?DD; satisfiable ?DD\<rbrakk> \<Longrightarrow> satisfiable ?CC

goal (1 subgoal):
 1. \<lbrakk>CC \<subseteq> DD; \<not> satisfiable CC\<rbrakk> \<Longrightarrow> \<not> satisfiable DD
[PROOF STEP]
by blast


[STATEMENT]
lemma true_cls_mset_empty[iff]: "I \<Turnstile>m {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<Turnstile>m {#}
[PROOF STEP]
unfolding true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball {#} ((\<Turnstile>) I)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_singleton[iff]: "I \<Turnstile>m {#C#} \<longleftrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>m {#C#}) = (I \<Turnstile> C)
[PROOF STEP]
by (simp add: true_cls_mset_def)


[STATEMENT]
lemma true_cls_mset_union[iff]: "I \<Turnstile>m CC + DD \<longleftrightarrow> I \<Turnstile>m CC \<and> I \<Turnstile>m DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>m CC + DD) = (I \<Turnstile>m CC \<and> I \<Turnstile>m DD)
[PROOF STEP]
unfolding true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball (CC + DD) ((\<Turnstile>) I) = (Multiset.Ball CC ((\<Turnstile>) I) \<and> Multiset.Ball DD ((\<Turnstile>) I))
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_Union[iff]: "I \<Turnstile>m \<Sum>\<^sub># CCC \<longleftrightarrow> (\<forall>CC \<in># CCC. I \<Turnstile>m CC)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>m \<Sum>\<^sub># CCC) = (\<forall>CC\<in>#CCC. I \<Turnstile>m CC)
[PROOF STEP]
unfolding true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball (\<Sum>\<^sub># CCC) ((\<Turnstile>) I) = (\<forall>CC\<in>#CCC. Multiset.Ball CC ((\<Turnstile>) I))
[PROOF STEP]
by simp


[STATEMENT]
lemma true_cls_mset_add_mset[iff]: "I \<Turnstile>m add_mset C CC \<longleftrightarrow> I \<Turnstile> C \<and> I \<Turnstile>m CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>m add_mset C CC) = (I \<Turnstile> C \<and> I \<Turnstile>m CC)
[PROOF STEP]
unfolding true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball (add_mset C CC) ((\<Turnstile>) I) = (I \<Turnstile> C \<and> Multiset.Ball CC ((\<Turnstile>) I))
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_image_mset[iff]: "I \<Turnstile>m image_mset f A \<longleftrightarrow> (\<forall>x \<in># A. I \<Turnstile> f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>m image_mset f A) = (\<forall>x\<in>#A. I \<Turnstile> f x)
[PROOF STEP]
unfolding true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball (image_mset f A) ((\<Turnstile>) I) = (\<forall>x\<in>#A. I \<Turnstile> f x)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_mono: "set_mset DD \<subseteq> set_mset CC \<Longrightarrow> I \<Turnstile>m CC \<Longrightarrow> I \<Turnstile>m DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_mset DD \<subseteq> set_mset CC; I \<Turnstile>m CC\<rbrakk> \<Longrightarrow> I \<Turnstile>m DD
[PROOF STEP]
unfolding true_cls_mset_def subset_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. t \<in># DD \<longrightarrow> t \<in># CC; Multiset.Ball CC ((\<Turnstile>) I)\<rbrakk> \<Longrightarrow> Multiset.Ball DD ((\<Turnstile>) I)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_mono_strong: "(\<forall>D \<in># DD. \<exists>C \<in># CC. C \<subseteq># D) \<Longrightarrow> I \<Turnstile>m CC \<Longrightarrow> I \<Turnstile>m DD"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>D\<in>#DD. \<exists>C\<in>#CC. C \<subseteq># D; I \<Turnstile>m CC\<rbrakk> \<Longrightarrow> I \<Turnstile>m DD
[PROOF STEP]
unfolding true_cls_mset_def true_cls_def true_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>D\<in>#DD. \<exists>C\<in>#CC. C \<subseteq># D; \<forall>C\<in>#CC. \<exists>L\<in>#C. (if is_pos L then \<lambda>P. P else Not) (atm_of L \<in> I)\<rbrakk> \<Longrightarrow> \<forall>C\<in>#DD. \<exists>L\<in>#C. (if is_pos L then \<lambda>P. P else Not) (atm_of L \<in> I)
[PROOF STEP]
by (meson mset_subset_eqD)


[STATEMENT]
lemma true_clss_set_mset[iff]: "I \<Turnstile>s set_mset CC \<longleftrightarrow> I \<Turnstile>m CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<Turnstile>s set_mset CC) = (I \<Turnstile>m CC)
[PROOF STEP]
unfolding true_clss_def true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multiset.Ball CC ((\<Turnstile>) I) = Multiset.Ball CC ((\<Turnstile>) I)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_clss_mset_set[simp]: "finite CC \<Longrightarrow> I \<Turnstile>m mset_set CC \<longleftrightarrow> I \<Turnstile>s CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite CC \<Longrightarrow> (I \<Turnstile>m mset_set CC) = (I \<Turnstile>s CC)
[PROOF STEP]
unfolding true_clss_def true_cls_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite CC \<Longrightarrow> Multiset.Ball (mset_set CC) ((\<Turnstile>) I) = Ball CC ((\<Turnstile>) I)
[PROOF STEP]
by auto


[STATEMENT]
lemma true_cls_mset_true_cls: "I \<Turnstile>m CC \<Longrightarrow> C \<in># CC \<Longrightarrow> I \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<Turnstile>m CC; C \<in># CC\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
using true_cls_mset_def
[PROOF STATE]
proof (prove)
using this:
(?I \<Turnstile>m ?CC) = (\<forall>C\<in>#?CC. ?I \<Turnstile> C)

goal (1 subgoal):
 1. \<lbrakk>I \<Turnstile>m CC; C \<in># CC\<rbrakk> \<Longrightarrow> I \<Turnstile> C
[PROOF STEP]
by auto


[STATEMENT]
lemma Afix_eq: "Afix \<Gamma>\<cdot>ae = (\<mu> ae'. (ABinds \<Gamma>\<cdot>ae') \<squnion> ae)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>ae = (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)
[PROOF STEP]
unfolding Afix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> ae. \<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ae = (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)
[PROOF STEP]
by simp


[STATEMENT]
lemma Afix_strict[simp]: "Afix \<Gamma>\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> \<bottom>) = \<bottom>
[PROOF STEP]
by (rule fix_eqI) auto


[STATEMENT]
lemma Afix_least_below: "ABinds \<Gamma> \<cdot> ae' \<sqsubseteq> ae' \<Longrightarrow> ae \<sqsubseteq> ae' \<Longrightarrow> Afix \<Gamma> \<cdot> ae \<sqsubseteq> ae'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ABinds \<Gamma>\<cdot>ae' \<sqsubseteq> ae'; ae \<sqsubseteq> ae'\<rbrakk> \<Longrightarrow> Afix \<Gamma>\<cdot>ae \<sqsubseteq> ae'
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ABinds \<Gamma>\<cdot>ae' \<sqsubseteq> ae'; ae \<sqsubseteq> ae'\<rbrakk> \<Longrightarrow> (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) \<sqsubseteq> ae'
[PROOF STEP]
by (auto intro: fix_least_below)


[STATEMENT]
lemma Afix_unroll: "Afix \<Gamma>\<cdot>ae = ABinds \<Gamma> \<cdot> (Afix \<Gamma>\<cdot>ae) \<squnion> ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>ae = ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<squnion> ae
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) = ABinds \<Gamma>\<cdot>(\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) \<squnion> ae
[PROOF STEP]
apply (subst fix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>(\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) = ABinds \<Gamma>\<cdot>(\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) \<squnion> ae
[PROOF STEP]
by simp


[STATEMENT]
lemma Abinds_below_Afix: "ABinds \<Delta> \<sqsubseteq> Afix \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Delta> \<sqsubseteq> Afix \<Delta>
[PROOF STEP]
apply (rule cfun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ABinds \<Delta>\<cdot>x \<sqsubseteq> Afix \<Delta>\<cdot>x
[PROOF STEP]
apply (simp add: Afix_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ABinds \<Delta>\<cdot>x \<sqsubseteq> (\<mu> xa. x \<squnion> ABinds \<Delta>\<cdot>xa)
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ABinds \<Delta>\<cdot>x \<sqsubseteq> x \<squnion> ABinds \<Delta>\<cdot>(\<mu> xa. x \<squnion> ABinds \<Delta>\<cdot>xa)
[PROOF STEP]
apply (rule below_trans[OF _ join_above2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ABinds \<Delta>\<cdot>x \<sqsubseteq> ABinds \<Delta>\<cdot>(\<mu> xa. x \<squnion> ABinds \<Delta>\<cdot>xa)
[PROOF STEP]
apply (rule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<sqsubseteq> (\<mu> xa. x \<squnion> ABinds \<Delta>\<cdot>xa)
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_above_arg: "ae \<sqsubseteq> Afix \<Gamma> \<cdot> ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae \<sqsubseteq> Afix \<Gamma>\<cdot>ae
[PROOF STEP]
by (subst Afix_unroll) simp


[STATEMENT]
lemma Abinds_Afix_below[simp]: "ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<sqsubseteq> Afix \<Gamma>\<cdot>ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<sqsubseteq> Afix \<Gamma>\<cdot>ae
[PROOF STEP]
apply (subst Afix_unroll)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<squnion> ae) \<sqsubseteq> Afix \<Gamma>\<cdot>ae
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<sqsubseteq> ABinds \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>ae) \<squnion> ae
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_reorder: "map_of \<Gamma> = map_of \<Delta> \<Longrightarrow> Afix \<Gamma> = Afix \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of \<Gamma> = map_of \<Delta> \<Longrightarrow> Afix \<Gamma> = Afix \<Delta>
[PROOF STEP]
by (intro cfun_eqI)(simp add: Afix_eq cong: Abinds_reorder)


[STATEMENT]
lemma Afix_repeat_singleton: "(\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) = Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) = Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)
[PROOF STEP]
apply (rule below_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)
 2. Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae) \<sqsubseteq> (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae) \<sqsubseteq> (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae))
 2. (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)
[PROOF STEP]
apply (subst fix_eq, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>n) \<sqsubseteq> Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>(n \<squnion> (\<mu> xa. Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>(n \<squnion> xa x))) x))
 2. (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)
[PROOF STEP]
apply (intro monofun_cfun_arg join_mono below_refl join_above1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> xa. Afix \<Gamma>\<cdot>(esing x\<cdot>(n \<squnion> xa x) \<squnion> ae)) \<sqsubseteq> Afix \<Gamma>\<cdot>(esing x\<cdot>n \<squnion> ae)
[PROOF STEP]
apply (rule fix_least_below, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>(n \<squnion> (Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>n)) x)) \<sqsubseteq> Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>n)
[PROOF STEP]
apply (rule Afix_least_below, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae \<squnion> esing x\<cdot>(n \<squnion> (Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>n)) x) \<sqsubseteq> Afix \<Gamma>\<cdot>(ae \<squnion> esing x\<cdot>n)
[PROOF STEP]
apply (intro join_below below_refl iffD2[OF esing_below_iff] below_trans[OF _ fun_belowD[OF Afix_above_arg]]  below_trans[OF _ Afix_above_arg] join_above1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<sqsubseteq> (ae \<squnion> esing x\<cdot>n) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_join_fresh: "ae' ` (domA \<Delta>) \<subseteq> {\<bottom>}  \<Longrightarrow>  Afix \<Delta>\<cdot>(ae \<squnion> ae') = (Afix \<Delta>\<cdot>ae) \<squnion> ae'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>(ae \<squnion> ae') = Afix \<Delta>\<cdot>ae \<squnion> ae'
[PROOF STEP]
apply (rule below_antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>(ae \<squnion> ae') \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule Afix_least_below)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Delta>\<cdot>ae \<squnion> ae') \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 3. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (subst Abinds_join_fresh, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 3. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule below_trans[OF Abinds_Afix_below join_above1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule join_below)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae' \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 3. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule below_trans[OF Afix_above_arg join_above1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae' \<sqsubseteq> Afix \<Delta>\<cdot>ae \<squnion> ae'
 2. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule join_above2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> Afix \<Delta>\<cdot>ae \<squnion> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule join_below[OF monofun_cfun_arg [OF join_above1]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ae' ` domA \<Delta> \<subseteq> {\<bottom>} \<Longrightarrow> ae' \<sqsubseteq> Afix \<Delta>\<cdot>(ae \<squnion> ae')
[PROOF STEP]
apply (rule below_trans[OF join_above2 Afix_above_arg])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_restr_fresh:
  assumes "atom ` S \<sharp>* \<Gamma>"
  shows "Afix \<Gamma>\<cdot>ae f|` (- S) = Afix \<Gamma>\<cdot>(ae  f|` (- S)) f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>ae f|` (- S) = Afix \<Gamma>\<cdot>(ae f|` (- S)) f|` (- S)
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) f|` (- S) = (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S)) f|` (- S)
[PROOF STEP]
proof (rule parallel_fix_ind[where P = "\<lambda> x y . x f|` (- S) = y  f|` (- S)"], goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. adm (\<lambda>x. fst x f|` (- S) = snd x f|` (- S))
 2. \<bottom> f|` (- S) = \<bottom> f|` (- S)
 3. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. adm (\<lambda>x. fst x f|` (- S) = snd x f|` (- S))
 2. \<bottom> f|` (- S) = \<bottom> f|` (- S)
 3. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. fst x f|` (- S) = snd x f|` (- S))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adm (\<lambda>x. fst x f|` (- S) = snd x f|` (- S))

goal (2 subgoals):
 1. \<bottom> f|` (- S) = \<bottom> f|` (- S)
 2. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bottom> f|` (- S) = \<bottom> f|` (- S)
 2. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<bottom> f|` (- S) = \<bottom> f|` (- S)
 2. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> f|` (- S) = \<bottom> f|` (- S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<bottom> f|` (- S) = \<bottom> f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
case prems: (3 aeL aeR)
[PROOF STATE]
proof (state)
this:
aeL f|` (- S) = aeR f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
have "(ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = ABinds \<Gamma>\<cdot>aeL  f|` (- S) \<squnion> ae  f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S)
[PROOF STEP]
by (simp add: env_restr_join)
[PROOF STATE]
proof (state)
this:
(ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
have "\<dots> = ABinds \<Gamma>\<cdot>(aeL  f|` (- S)) f|` (- S) \<squnion> ae  f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)
[PROOF STEP]
by (rule arg_cong[OF ABinds_restr_fresh[OF assms]])
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>aeL f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
have "\<dots> = ABinds \<Gamma>\<cdot>(aeR  f|` (- S)) f|` (- S) \<squnion> ae  f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)
[PROOF STEP]
unfolding prems
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>(aeL f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
have "\<dots> = ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae  f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae f|` (- S)
[PROOF STEP]
by (rule arg_cong[OF ABinds_restr_fresh[OF assms, symmetric]])
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>(aeR f|` (- S)) f|` (- S) \<squnion> ae f|` (- S) = ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
have "\<dots> = (ABinds \<Gamma>\<cdot>aeR \<squnion> ae f|` (- S)) f|` (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae f|` (- S) = (ABinds \<Gamma>\<cdot>aeR \<squnion> ae f|` (- S)) f|` (- S)
[PROOF STEP]
by (simp add: env_restr_join)
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>\<cdot>aeR f|` (- S) \<squnion> ae f|` (- S) = (ABinds \<Gamma>\<cdot>aeR \<squnion> ae f|` (- S)) f|` (- S)

goal (1 subgoal):
 1. \<And>x y. x f|` (- S) = y f|` (- S) \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>y f|` (- S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = (ABinds \<Gamma>\<cdot>aeR \<squnion> ae f|` (- S)) f|` (- S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(ABinds \<Gamma>\<cdot>aeL \<squnion> ae) f|` (- S) = (ABinds \<Gamma>\<cdot>aeR \<squnion> ae f|` (- S)) f|` (- S)

goal (1 subgoal):
 1. (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>aeL f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>aeR f|` (- S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>aeL f|` (- S) = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` (- S))\<cdot>aeR f|` (- S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Afix_restr:
  assumes "domA \<Gamma> \<subseteq> S"
  shows "Afix \<Gamma>\<cdot>ae f|` S = Afix \<Gamma>\<cdot>(ae  f|` S) f|` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>\<cdot>ae f|` S = Afix \<Gamma>\<cdot>(ae f|` S) f|` S
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) f|` S = (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S) f|` S
[PROOF STEP]
apply (rule parallel_fix_ind[where P = "\<lambda> x y . x f|`S = y  f|` S"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>x. fst x f|` S = snd x f|` S)
 2. \<bottom> f|` S = \<bottom> f|` S
 3. \<And>x y. x f|` S = y f|` S \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>y f|` S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bottom> f|` S = \<bottom> f|` S
 2. \<And>x y. x f|` S = y f|` S \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>y f|` S
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x f|` S = y f|` S \<Longrightarrow> (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>x f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>y f|` S
[PROOF STEP]
apply (auto   simp add: env_restr_join)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x f|` S = y f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>\<cdot>x f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>y f|` S
[PROOF STEP]
apply (metis  ABinds_restr[OF assms, symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_restr_subst':
  assumes "\<And> x' e a. (x',e) \<in> set \<Gamma> \<Longrightarrow> Aexp e[x::=y]\<cdot>a f|` S = Aexp e\<cdot>a f|` S"
  assumes "x \<notin> S"
  assumes "y \<notin> S"
  assumes "domA \<Gamma> \<subseteq> S"
  shows "Afix \<Gamma>[x::h=y]\<cdot>ae f|` S = Afix \<Gamma>\<cdot>(ae f|` S) f|` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>[x::h=y]\<cdot>ae f|` S = Afix \<Gamma>\<cdot>(ae f|` S) f|` S
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> xa. ABinds \<Gamma>[x::h=y]\<cdot>xa \<squnion> ae) f|` S = (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S) f|` S
[PROOF STEP]
apply (rule parallel_fix_ind[where P = "\<lambda> x y . x f|`S = y  f|` S"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>x. fst x f|` S = snd x f|` S)
 2. \<bottom> f|` S = \<bottom> f|` S
 3. \<And>xa ya. xa f|` S = ya f|` S \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[x::h=y]\<cdot>xa \<squnion> ae)\<cdot>xa f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>ya f|` S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<bottom> f|` S = \<bottom> f|` S
 2. \<And>xa ya. xa f|` S = ya f|` S \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[x::h=y]\<cdot>xa \<squnion> ae)\<cdot>xa f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>ya f|` S
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. xa f|` S = ya f|` S \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[x::h=y]\<cdot>xa \<squnion> ae)\<cdot>xa f|` S = (\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae f|` S)\<cdot>ya f|` S
[PROOF STEP]
apply (auto   simp add: env_restr_join)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya. xa f|` S = ya f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>[x::h=y]\<cdot>xa f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>ya f|` S
[PROOF STEP]
apply (subst ABinds_restr_subst[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y x' e a. \<lbrakk>x f|` S = y f|` S; (x', e) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> (?x'6 x y x' e a, e) \<in> set \<Gamma>
 2. \<And>x y. x f|` S = y f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>\<cdot>(x f|` S) f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>y f|` S
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x f|` S = y f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>\<cdot>(x f|` S) f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>y f|` S
[PROOF STEP]
apply (subst ABinds_restr[OF assms(4)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x f|` S = y f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>\<cdot>(x f|` S f|` S) f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>y f|` S
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x f|` S = y f|` S \<Longrightarrow> ae f|` S \<squnion> ABinds \<Gamma>\<cdot>(x f|` S) f|` S = ae f|` S \<squnion> ABinds \<Gamma>\<cdot>(y f|` S) f|` S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Afix_subst_approx:
  assumes "\<And> v n. v \<in> domA \<Gamma> \<Longrightarrow> Aexp (the (map_of \<Gamma> v))[y::=x]\<cdot>n \<sqsubseteq> (Aexp (the (map_of \<Gamma> v))\<cdot>n)(y := \<bottom>, x := up\<cdot>0)"
  assumes "x \<notin> domA \<Gamma>"
  assumes "y \<notin> domA \<Gamma>"
  shows "Afix \<Gamma>[y::h= x]\<cdot>(ae(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (Afix \<Gamma>\<cdot>ae)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Afix \<Gamma>[y::h=x]\<cdot>(ae(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (Afix \<Gamma>\<cdot>ae)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
proof (rule parallel_fix_ind[where P = "\<lambda> aeL aeR . aeL \<sqsubseteq> aeR(y := \<bottom>, x := up\<cdot>0)"], goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. adm (\<lambda>xa. fst xa \<sqsubseteq> (snd xa)(y := \<bottom>, x := up\<cdot>0))
 2. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
 3. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. adm (\<lambda>xa. fst xa \<sqsubseteq> (snd xa)(y := \<bottom>, x := up\<cdot>0))
 2. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
 3. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>xa. fst xa \<sqsubseteq> (snd xa)(y := \<bottom>, x := up\<cdot>0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adm (\<lambda>xa. fst xa \<sqsubseteq> (snd xa)(y := \<bottom>, x := up\<cdot>0))

goal (2 subgoals):
 1. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
 2. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
 2. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
 2. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<bottom> \<sqsubseteq> \<bottom>(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
case (3 aeL aeR)
[PROOF STATE]
proof (state)
this:
aeL \<sqsubseteq> aeR(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
hence "ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> ABinds \<Gamma>[y::h=x]\<cdot>(aeR (y := \<bottom>, x := up\<cdot>0))"
[PROOF STATE]
proof (prove)
using this:
aeL \<sqsubseteq> aeR(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0))
[PROOF STEP]
by (rule monofun_cfun_arg)
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0))

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0))

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
have "\<dots>  \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?v \<in> domA \<Gamma> \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of \<Gamma> ?v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of \<Gamma> ?v)))(y := \<bottom>, x := up\<cdot>0)
x \<notin> domA \<Gamma>
y \<notin> domA \<Gamma>

goal (1 subgoal):
 1. ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
proof (induction rule: ABinds.induct, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>v n. v \<in> domA [] \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of [] v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of [] v)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA []; y \<notin> domA []\<rbrakk> \<Longrightarrow> ABinds [][y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds []\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
 2. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
?v \<in> domA [] \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of [] ?v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of [] ?v)))(y := \<bottom>, x := up\<cdot>0)
x \<notin> domA []
y \<notin> domA []

goal (2 subgoals):
 1. \<lbrakk>\<And>v n. v \<in> domA [] \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of [] v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of [] v)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA []; y \<notin> domA []\<rbrakk> \<Longrightarrow> ABinds [][y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds []\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
 2. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?v \<in> domA [] \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of [] ?v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of [] ?v)))(y := \<bottom>, x := up\<cdot>0)
x \<notin> domA []
y \<notin> domA []

goal (1 subgoal):
 1. ABinds [][y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds []\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ABinds [][y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds []\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
case prems: (2 v e \<Gamma>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>va n. va \<in> domA (delete v \<Gamma>) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v \<Gamma>); y \<notin> domA (delete v \<Gamma>)\<rbrakk> \<Longrightarrow> ABinds (delete v \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
?v \<in> domA ((v, e) # \<Gamma>) \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) ?v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) ?v)))(y := \<bottom>, x := up\<cdot>0)
x \<notin> domA ((v, e) # \<Gamma>)
y \<notin> domA ((v, e) # \<Gamma>)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
have "\<And>n. Aexp e[y::=x]\<cdot>n \<sqsubseteq> (Aexp e\<cdot>n)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<A>\<^bsub>n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
using prems(2)[where v = v]
[PROOF STATE]
proof (prove)
using this:
v \<in> domA ((v, e) # \<Gamma>) \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) v)))(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>n. \<A>\<^bsub>n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<A>\<^bsub>?n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
hence IH1: "\<And> n. fup\<cdot>(Aexp e[y::=x])\<cdot>n \<sqsubseteq> (fup\<cdot>(Aexp e)\<cdot>n)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
using this:
\<A>\<^bsub>?n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>n. \<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^sup>\<bottom>\<^bsub>n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by (case_tac n) auto
[PROOF STATE]
proof (state)
this:
\<A>\<^sup>\<bottom>\<^bsub>?n\<^esub> e[y::=x] \<sqsubseteq> (\<A>\<^sup>\<bottom>\<^bsub>?n\<^esub> e)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
have "ABinds (delete v \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds (delete v \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
apply (rule prems)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>va n. va \<in> domA (delete v \<Gamma>) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va)))(y := \<bottom>, x := up\<cdot>0)
 2. x \<notin> domA (delete v \<Gamma>)
 3. y \<notin> domA (delete v \<Gamma>)
[PROOF STEP]
using prems(2,3,4)
[PROOF STATE]
proof (prove)
using this:
?v \<in> domA ((v, e) # \<Gamma>) \<Longrightarrow> \<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) ?v))[y::=x] \<sqsubseteq> (\<A>\<^bsub>?n\<^esub> (the (map_of ((v, e) # \<Gamma>) ?v)))(y := \<bottom>, x := up\<cdot>0)
x \<notin> domA ((v, e) # \<Gamma>)
y \<notin> domA ((v, e) # \<Gamma>)

goal (3 subgoals):
 1. \<And>va n. va \<in> domA (delete v \<Gamma>) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v \<Gamma>) va)))(y := \<bottom>, x := up\<cdot>0)
 2. x \<notin> domA (delete v \<Gamma>)
 3. y \<notin> domA (delete v \<Gamma>)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
ABinds (delete v \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
hence IH2: "ABinds (delete v \<Gamma>[y::h=x])\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
using this:
ABinds (delete v \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. ABinds (delete v \<Gamma>[y::h=x])\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
unfolding subst_heap_delete
[PROOF STATE]
proof (prove)
using this:
ABinds (delete v \<Gamma>[y::h=x])\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. ABinds (delete v \<Gamma>[y::h=x])\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ABinds (delete v \<Gamma>[y::h=x])\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
have [simp]: "(aeR(y := \<bottom>, x := up\<cdot>0)) v = aeR v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (aeR(y := \<bottom>, x := up\<cdot>0)) v = aeR v
[PROOF STEP]
using prems(3,4)
[PROOF STATE]
proof (prove)
using this:
x \<notin> domA ((v, e) # \<Gamma>)
y \<notin> domA ((v, e) # \<Gamma>)

goal (1 subgoal):
 1. (aeR(y := \<bottom>, x := up\<cdot>0)) v = aeR v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(aeR(y := \<bottom>, x := up\<cdot>0)) v = aeR v

goal (1 subgoal):
 1. \<And>v e binds. \<lbrakk>\<lbrakk>\<And>va n. va \<in> domA (delete v binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of (delete v binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA (delete v binds); y \<notin> domA (delete v binds)\<rbrakk> \<Longrightarrow> ABinds (delete v binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds (delete v binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0); \<And>va n. va \<in> domA ((v, e) # binds) \<Longrightarrow> \<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va))[y::=x] \<sqsubseteq> (\<A>\<^bsub>n\<^esub> (the (map_of ((v, e) # binds) va)))(y := \<bottom>, x := up\<cdot>0); x \<notin> domA ((v, e) # binds); y \<notin> domA ((v, e) # binds)\<rbrakk> \<Longrightarrow> ABinds ((v, e) # binds)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # binds)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ABinds ((v, e) # \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by (simp del: fun_upd_apply join_comm) (rule join_mono[OF IH1 IH2])
[PROOF STATE]
proof (state)
this:
ABinds ((v, e) # \<Gamma>)[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds ((v, e) # \<Gamma>)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>[y::h=x]\<cdot>(aeR(y := \<bottom>, x := up\<cdot>0)) \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cont (\<lambda>a. a) \<Longrightarrow> ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
have "ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)"
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>a. a) \<Longrightarrow> ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by this simp
[PROOF STATE]
proof (state)
this:
ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. \<And>xa ya. xa \<sqsubseteq> ya(y := \<bottom>, x := up\<cdot>0) \<Longrightarrow> (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>xa \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>ya)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ABinds \<Gamma>[y::h=x]\<cdot>aeL \<sqsubseteq> (ABinds \<Gamma>\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal (1 subgoal):
 1. (\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>aeL \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)
[PROOF STEP]
by (auto simp add: join_below_iff elim: below_trans)
[PROOF STATE]
proof (state)
this:
(\<Lambda> xa. ABinds \<Gamma>[y::h=x]\<cdot>xa \<squnion> ae(y := \<bottom>, x := up\<cdot>0))\<cdot>aeL \<sqsubseteq> ((\<Lambda> x. ABinds \<Gamma>\<cdot>x \<squnion> ae)\<cdot>aeR)(y := \<bottom>, x := up\<cdot>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Afix_eqvt[eqvt]: "\<pi> \<bullet> (ArityAnalysis.Afix Aexp \<Gamma>) = ArityAnalysis.Afix  (\<pi> \<bullet> Aexp) (\<pi> \<bullet> \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> ArityAnalysis.Afix Aexp \<Gamma> = ArityAnalysis.Afix (\<pi> \<bullet> Aexp) (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
unfolding ArityAnalysis.Afix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> (\<Lambda> ae. \<mu> x. ArityAnalysis.ABinds Aexp \<Gamma>\<cdot>x \<squnion> ae) = (\<Lambda> ae. \<mu> x. ArityAnalysis.ABinds (\<pi> \<bullet> Aexp) (\<pi> \<bullet> \<Gamma>)\<cdot>x \<squnion> ae)
[PROOF STEP]
by perm_simp (simp add: Abs_cfun_eqvt)


[STATEMENT]
lemma Afix_cong[fundef_cong]:
  "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> aexp1 e = aexp2 e); heap1 = heap2 \<rbrakk>
      \<Longrightarrow> ArityAnalysis.Afix aexp1 heap1 = ArityAnalysis.Afix aexp2 heap2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>e. e \<in> snd ` set heap2 \<Longrightarrow> aexp1 e = aexp2 e; heap1 = heap2\<rbrakk> \<Longrightarrow> ArityAnalysis.Afix aexp1 heap1 = ArityAnalysis.Afix aexp2 heap2
[PROOF STEP]
unfolding ArityAnalysis.Afix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>e. e \<in> snd ` set heap2 \<Longrightarrow> aexp1 e = aexp2 e; heap1 = heap2\<rbrakk> \<Longrightarrow> (\<Lambda> ae. \<mu> x. ArityAnalysis.ABinds aexp1 heap1\<cdot>x \<squnion> ae) = (\<Lambda> ae. \<mu> x. ArityAnalysis.ABinds aexp2 heap2\<cdot>x \<squnion> ae)
[PROOF STEP]
by (metis Abinds_cong)


[STATEMENT]
lemma Afix_edom: "edom (Afix \<Gamma> \<cdot> ae) \<subseteq> fv \<Gamma> \<union> edom ae"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edom (Afix \<Gamma>\<cdot>ae) \<subseteq> fv \<Gamma> \<union> edom ae
[PROOF STEP]
unfolding Afix_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edom (\<mu> x. ABinds \<Gamma>\<cdot>x \<squnion> ae) \<subseteq> fv \<Gamma> \<union> edom ae
[PROOF STEP]
by (rule fix_ind[where P = "\<lambda> ae' . edom ae' \<subseteq> fv \<Gamma> \<union> edom ae"] )
     (auto dest: subsetD[OF edom_AnalBinds])