[STATEMENT]
lemma equiv_aux:
    assumes "g \<turnstile> ns\<Down>s" "g \<turnstile> ns\<Down>\<^sub>ss'" "g \<turnstile> last ns-ms\<rightarrow>m" "v \<in> allUses g m" "\<forall>n \<in> set (tl ms). var g v \<notin> var g ` allDefs g n"
    shows "s (var g v) = s' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (var g v) = s' v
[PROOF STEP]
using assms(2) assms(1,3-)
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> ns\<Down>\<^sub>s s'
g \<turnstile> ns\<Down>s
g \<turnstile> last ns-ms\<rightarrow>m
v \<in> allUses g m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. s (var g v) = s' v
[PROOF STEP]
proof (induction arbitrary: v s ms m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v s ms m. \<lbrakk>g \<turnstile> [Entry g]\<Down>s; g \<turnstile> last [Entry g]-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> s (var g v) = ssaStep g (Entry g) 0 Map.empty v
 2. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
g \<turnstile> [Entry g]\<Down>s
g \<turnstile> last [Entry g]-ms\<rightarrow>m
v \<in> allUses g m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n

goal (2 subgoals):
 1. \<And>v s ms m. \<lbrakk>g \<turnstile> [Entry g]\<Down>s; g \<turnstile> last [Entry g]-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> s (var g v) = ssaStep g (Entry g) 0 Map.empty v
 2. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
have "v \<in> defs g (Entry g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
from empty.prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
v \<in> allUses g m
[PROOF STEP]
have "defAss g m v"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
v \<in> allUses g m

goal (1 subgoal):
 1. defAss g m v
[PROOF STEP]
by - (rule allUses_def_ass, auto)
[PROOF STATE]
proof (state)
this:
defAss g m v

goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
with empty.prems(2)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
defAss g m v
[PROOF STEP]
obtain n where n: "n \<in> set ms" "v \<in> allDefs g n"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
defAss g m v

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> set ms; v \<in> allDefs g n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by - (drule defAssD, auto)
[PROOF STATE]
proof (state)
this:
n \<in> set ms
v \<in> allDefs g n

goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
with empty.prems(4)
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
n \<in> set ms
v \<in> allDefs g n
[PROOF STEP]
have "n \<notin> set (tl ms)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
n \<in> set ms
v \<in> allDefs g n

goal (1 subgoal):
 1. n \<notin> set (tl ms)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<notin> set (tl ms)

goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
with empty.prems(2) n
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
n \<in> set ms
v \<in> allDefs g n
n \<notin> set (tl ms)
[PROOF STEP]
have "n = Entry g"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last [Entry g]-ms\<rightarrow>m
n \<in> set ms
v \<in> allDefs g n
n \<notin> set (tl ms)

goal (1 subgoal):
 1. n = Entry g
[PROOF STEP]
by (cases ms, auto dest: old.path2_hd)
[PROOF STATE]
proof (state)
this:
n = Entry g

goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
with n(2)
[PROOF STATE]
proof (chain)
picking this:
v \<in> allDefs g n
n = Entry g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> allDefs g n
n = Entry g

goal (1 subgoal):
 1. v \<in> defs g (Entry g)
[PROOF STEP]
by (auto simp: allDefs_def)
[PROOF STATE]
proof (state)
this:
v \<in> defs g (Entry g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> defs g (Entry g)

goal (2 subgoals):
 1. \<And>v s ms m. \<lbrakk>g \<turnstile> [Entry g]\<Down>s; g \<turnstile> last [Entry g]-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> s (var g v) = ssaStep g (Entry g) 0 Map.empty v
 2. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
with empty.prems(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> [Entry g]\<Down>s
v \<in> defs g (Entry g)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> [Entry g]\<Down>s
v \<in> defs g (Entry g)

goal (1 subgoal):
 1. s (var g v) = ssaStep g (Entry g) 0 Map.empty v
[PROOF STEP]
by - (erule bs.cases, auto simp: step_def ssaStep_def oldDefs_def split: option.split)
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g (Entry g) 0 Map.empty v

goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
case (snoc ns s' n i)
[PROOF STATE]
proof (state)
this:
g \<turnstile> ns\<Down>\<^sub>s s'
last ns = old.predecessors g n ! i
n \<in> set (\<alpha>n g)
i < length (old.predecessors g n)
\<lbrakk>g \<turnstile> ns\<Down>?s1; g \<turnstile> last ns-?ms1\<rightarrow>?m1; ?v1 \<in> allUses g ?m1; \<forall>n\<in>set (tl ?ms1). var g ?v1 \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> ?s1 (var g ?v1) = s' ?v1
g \<turnstile> ns @ [n]\<Down>s
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
v \<in> allUses g m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
from snoc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
[PROOF STEP]
have[simp]: "n \<in> set (\<alpha>n g)" "m \<in> set (\<alpha>n g)"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m

goal (1 subgoal):
 1. n \<in> set (\<alpha>n g) &&& m \<in> set (\<alpha>n g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> set (\<alpha>n g)
m \<in> set (\<alpha>n g)

goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
from snoc.prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
v \<in> allUses g m
[PROOF STEP]
have[simp]: "v \<in> allVars g"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
v \<in> allUses g m

goal (1 subgoal):
 1. v \<in> allVars g
[PROOF STEP]
by - (rule allUses_in_allVars, auto)
[PROOF STATE]
proof (state)
this:
v \<in> allVars g

goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
from snoc.hyps(4)
[PROOF STATE]
proof (chain)
picking this:
i < length (old.predecessors g n)
[PROOF STEP]
have[simp]: "n \<noteq> Entry g"
[PROOF STATE]
proof (prove)
using this:
i < length (old.predecessors g n)

goal (1 subgoal):
 1. n \<noteq> Entry g
[PROOF STEP]
by (auto simp: Entry_no_predecessor)
[PROOF STATE]
proof (state)
this:
n \<noteq> Entry g

goal (1 subgoal):
 1. \<And>ns s m i v sa ms ma. \<lbrakk>g \<turnstile> ns\<Down>\<^sub>s s; \<And>v sa ms m. \<lbrakk>g \<turnstile> ns\<Down>sa; g \<turnstile> last ns-ms\<rightarrow>m; v \<in> allUses g m; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = s v; last ns = old.predecessors g m ! i; m \<in> set (\<alpha>n g); i < length (old.predecessors g m); g \<turnstile> ns @ [m]\<Down>sa; g \<turnstile> last (ns @ [m])-ms\<rightarrow>ma; v \<in> allUses g ma; \<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n\<rbrakk> \<Longrightarrow> sa (var g v) = ssaStep g m i s v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
proof (cases "var g v \<in> var g ` allDefs g n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. var g v \<in> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
 2. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
var g v \<in> var g ` allDefs g n

goal (2 subgoals):
 1. var g v \<in> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
 2. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
have[simp]: "defNode g v = n" (is "?n\<^sub>v = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
var g v \<in> var g ` allDefs g n
[PROOF STEP]
obtain v' where v': "v' \<in> allDefs g n" "var g v' = var g v"
[PROOF STATE]
proof (prove)
using this:
var g v \<in> var g ` allDefs g n

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>v' \<in> allDefs g n; var g v' = var g v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<in> allDefs g n
var g v' = var g v

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
from snoc.prems(3)
[PROOF STATE]
proof (chain)
picking this:
v \<in> allUses g m
[PROOF STEP]
have "defAss g m v"
[PROOF STATE]
proof (prove)
using this:
v \<in> allUses g m

goal (1 subgoal):
 1. defAss g m v
[PROOF STEP]
by - (rule allUses_def_ass, auto)
[PROOF STATE]
proof (state)
this:
defAss g m v

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
defAss g m v

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
from snoc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> ns @ [n]\<Down>s
[PROOF STEP]
obtain ns' where ns': "g \<turnstile> Entry g-ns'\<rightarrow>n" "set ns' \<subseteq> set (ns@[n])" "distinct ns'"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> ns @ [n]\<Down>s

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>g \<turnstile> Entry g-ns'\<rightarrow>n; set ns' \<subseteq> set (ns @ [n]); distinct ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: bs.cases intro: old.simple_path2)
[PROOF STATE]
proof (state)
this:
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
defAss g m v
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
[PROOF STEP]
have "?n\<^sub>v \<in> set (ns'@tl ms)"
[PROOF STATE]
proof (prove)
using this:
defAss g m v
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'

goal (1 subgoal):
 1. defNode g v \<in> set (ns' @ tl ms)
[PROOF STEP]
using snoc.prems(2)
[PROOF STATE]
proof (prove)
using this:
defAss g m v
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m

goal (1 subgoal):
 1. defNode g v \<in> set (ns' @ tl ms)
[PROOF STEP]
by - (drule defAss_defNode, auto elim!: bs.cases dest: old.path2_app)
[PROOF STATE]
proof (state)
this:
defNode g v \<in> set (ns' @ tl ms)

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
defNode g v \<in> set (ns' @ tl ms)

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
defNode g v \<in> set (ns' @ tl ms)

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
let ?n'' = "last (butlast ns')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
assume asm: "?n\<^sub>v \<in> set (butlast ns')"
[PROOF STATE]
proof (state)
this:
defNode g v \<in> set (butlast ns')

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
with ns'(1,3)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns'\<rightarrow>n
distinct ns'
defNode g v \<in> set (butlast ns')
[PROOF STEP]
have[simp]: "?n\<^sub>v \<noteq> n"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns'\<rightarrow>n
distinct ns'
defNode g v \<in> set (butlast ns')

goal (1 subgoal):
 1. defNode g v \<noteq> n
[PROOF STEP]
by (cases ns' rule: rev_cases, auto dest!: old.path2_last)
[PROOF STATE]
proof (state)
this:
defNode g v \<noteq> n

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
from ns'(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns'\<rightarrow>n
[PROOF STEP]
have "length ns' \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns'\<rightarrow>n

goal (1 subgoal):
 1. 2 \<le> length ns'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<le> length ns'

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
with ns'
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
2 \<le> length ns'
[PROOF STEP]
have bns': "g \<turnstile> Entry g-butlast ns'\<rightarrow>?n''" "?n'' \<in> set (old.predecessors g n)"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
2 \<le> length ns'

goal (1 subgoal):
 1. g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns') &&& last (butlast ns') \<in> set (old.predecessors g n)
[PROOF STEP]
by (auto elim: old.path2_unsnoc)
[PROOF STATE]
proof (state)
this:
g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns')
last (butlast ns') \<in> set (old.predecessors g n)

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
with asm
[PROOF STATE]
proof (chain)
picking this:
defNode g v \<in> set (butlast ns')
g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns')
last (butlast ns') \<in> set (old.predecessors g n)
[PROOF STEP]
obtain ns'' where ns'': "g \<turnstile> ?n\<^sub>v-ns''\<rightarrow>?n''" "suffix ns'' (butlast ns')" "?n\<^sub>v \<notin> set (tl ns'')"
[PROOF STATE]
proof (prove)
using this:
defNode g v \<in> set (butlast ns')
g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns')
last (butlast ns') \<in> set (old.predecessors g n)

goal (1 subgoal):
 1. (\<And>ns''. \<lbrakk>g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns'); suffix ns'' (butlast ns'); defNode g v \<notin> set (tl ns'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by - (rule old.path2_split_first_last, auto)
[PROOF STATE]
proof (state)
this:
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
suffix ns'' (butlast ns')
defNode g v \<notin> set (tl ns'')

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
with bns' snoc.prems(2)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns')
last (butlast ns') \<in> set (old.predecessors g n)
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
suffix ns'' (butlast ns')
defNode g v \<notin> set (tl ns'')
[PROOF STEP]
have "g \<turnstile> ?n\<^sub>v-(ns''@[n])@tl ms\<rightarrow>m"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-butlast ns'\<rightarrow>last (butlast ns')
last (butlast ns') \<in> set (old.predecessors g n)
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
suffix ns'' (butlast ns')
defNode g v \<notin> set (tl ns'')

goal (1 subgoal):
 1. g \<turnstile> defNode g v-(ns'' @ [n]) @ tl ms\<rightarrow>m
[PROOF STEP]
by - (rule old.path2_app, auto)
[PROOF STATE]
proof (state)
this:
g \<turnstile> defNode g v-(ns'' @ [n]) @ tl ms\<rightarrow>m

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
hence "defNode g v' \<notin> set (tl (ns''@[n]@tl ms))"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> defNode g v-(ns'' @ [n]) @ tl ms\<rightarrow>m

goal (1 subgoal):
 1. defNode g v' \<notin> set (tl (ns'' @ [n] @ tl ms))
[PROOF STEP]
using v' snoc.prems(3,4) bns'(2) ns''(1,3)
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> defNode g v-(ns'' @ [n]) @ tl ms\<rightarrow>m
v' \<in> allDefs g n
var g v' = var g v
v \<in> allUses g m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
last (butlast ns') \<in> set (old.predecessors g n)
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
defNode g v \<notin> set (tl ns'')

goal (1 subgoal):
 1. defNode g v' \<notin> set (tl (ns'' @ [n] @ tl ms))
[PROOF STEP]
by - (rule conventional''[of g v _ m], auto intro!: old.path2_app simp: old.path2_not_Nil)
[PROOF STATE]
proof (state)
this:
defNode g v' \<notin> set (tl (ns'' @ [n] @ tl ms))

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
with ns' ns''(1) v'(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
v' \<in> allDefs g n
defNode g v' \<notin> set (tl (ns'' @ [n] @ tl ms))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns'\<rightarrow>n
set ns' \<subseteq> set (ns @ [n])
distinct ns'
g \<turnstile> defNode g v-ns''\<rightarrow>last (butlast ns')
v' \<in> allDefs g n
defNode g v' \<notin> set (tl (ns'' @ [n] @ tl ms))

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

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
defNode g v \<in> set (butlast ns') \<Longrightarrow> False

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
defNode g v \<in> set (ns' @ tl ms)
defNode g v \<in> set (butlast ns') \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
defNode g v \<in> set (ns' @ tl ms)
defNode g v \<in> set (butlast ns') \<Longrightarrow> False

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
using snoc.prems(4) ns'(1)
[PROOF STATE]
proof (prove)
using this:
defNode g v \<in> set (ns' @ tl ms)
defNode g v \<in> set (butlast ns') \<Longrightarrow> False
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
g \<turnstile> Entry g-ns'\<rightarrow>n

goal (1 subgoal):
 1. defNode g v = n
[PROOF STEP]
by (cases ns' rule: rev_cases, auto dest: old.path2_last)
[PROOF STATE]
proof (state)
this:
defNode g v = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
defNode g v = n

goal (2 subgoals):
 1. var g v \<in> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
 2. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
from \<open>v \<in> allVars g\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> allVars g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> allVars g

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
proof (cases rule: defNode_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> defs g (defNode g v) \<Longrightarrow> s (var g v) = ssaStep g n i s' v
 2. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
case simpleDef
[PROOF STATE]
proof (state)
this:
v \<in> defs g (defNode g v)

goal (2 subgoals):
 1. v \<in> defs g (defNode g v) \<Longrightarrow> s (var g v) = ssaStep g n i s' v
 2. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> defs g (defNode g v)

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
v \<in> defs g (defNode g v)
g \<turnstile> ns @ [n]\<Down>s

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
by - (erule bs.cases, auto simp: step_def ssaStep_def oldDefs_def)
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g n i s' v

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
case phi
[PROOF STATE]
proof (state)
this:
phi g v \<noteq> None

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
phi g v \<noteq> None

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
fix v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
assume asm: "v' \<in> defs g n" "var g v = var g v'"
[PROOF STATE]
proof (state)
this:
v' \<in> defs g n
var g v = var g v'

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
with phi
[PROOF STATE]
proof (chain)
picking this:
phi g v \<noteq> None
v' \<in> defs g n
var g v = var g v'
[PROOF STEP]
have "v' = v"
[PROOF STATE]
proof (prove)
using this:
phi g v \<noteq> None
v' \<in> defs g n
var g v = var g v'

goal (1 subgoal):
 1. v' = v
[PROOF STEP]
using allDefs_var_disjoint[of n g v' v]
[PROOF STATE]
proof (prove)
using this:
phi g v \<noteq> None
v' \<in> defs g n
var g v = var g v'
\<lbrakk>n \<in> set (\<alpha>n g); v' \<in> allDefs g n; v \<in> allDefs g n; v' \<noteq> v\<rbrakk> \<Longrightarrow> var g v \<noteq> var g v'

goal (1 subgoal):
 1. v' = v
[PROOF STEP]
by (cases, auto dest!: phi_phiDefs)
[PROOF STATE]
proof (state)
this:
v' = v

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
with asm(1) phi
[PROOF STATE]
proof (chain)
picking this:
v' \<in> defs g n
phi g v \<noteq> None
v' = v
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
v' \<in> defs g n
phi g v \<noteq> None
v' = v

goal (1 subgoal):
 1. False
[PROOF STEP]
using simpleDefs_phiDefs_disjoint[of n g]
[PROOF STATE]
proof (prove)
using this:
v' \<in> defs g n
phi g v \<noteq> None
v' = v
n \<in> set (\<alpha>n g) \<Longrightarrow> defs g n \<inter> phiDefs g n = {}

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

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v'3 \<in> defs g n; var g v = var g ?v'3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
note 1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v'3 \<in> defs g n; var g v = var g ?v'3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v'3 \<in> defs g n; var g v = var g ?v'3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
fix vs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
assume asm: "g \<turnstile> Entry g-ns @ [n]\<rightarrow>n" "phis g (n, v) = Some vs" "var g v \<notin> var g ` defs g n"
[PROOF STATE]
proof (state)
this:
g \<turnstile> Entry g-ns @ [n]\<rightarrow>n
phis g (n, v) = Some vs
var g v \<notin> var g ` defs g n

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
let ?n' = "last ns"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
from asm(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns @ [n]\<rightarrow>n
[PROOF STEP]
have "length ns \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns @ [n]\<rightarrow>n

goal (1 subgoal):
 1. 1 \<le> length ns
[PROOF STEP]
by (cases ns, auto simp: old.path2_def)
[PROOF STATE]
proof (state)
this:
1 \<le> length ns

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
hence "g \<turnstile> Entry g-ns\<rightarrow>?n'"
[PROOF STATE]
proof (prove)
using this:
1 \<le> length ns

goal (1 subgoal):
 1. g \<turnstile> Entry g-ns\<rightarrow>last ns
[PROOF STEP]
by - (rule old.path2_unsnoc[OF asm(1)], auto)
[PROOF STATE]
proof (state)
this:
g \<turnstile> Entry g-ns\<rightarrow>last ns

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<turnstile> Entry g-ns\<rightarrow>last ns

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
have "vs ! i \<in> phiUses g ?n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs ! i \<in> phiUses g (last ns)
[PROOF STEP]
using snoc.hyps(2,4) phis_wf[OF asm(2)]
[PROOF STATE]
proof (prove)
using this:
last ns = old.predecessors g n ! i
i < length (old.predecessors g n)
length (old.predecessors g n) = length vs

goal (1 subgoal):
 1. vs ! i \<in> phiUses g (last ns)
[PROOF STEP]
by - (rule phiUsesI[OF _ asm(2)], auto simp: set_zip)
[PROOF STATE]
proof (state)
this:
vs ! i \<in> phiUses g (last ns)

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> Entry g-ns\<rightarrow>last ns
vs ! i \<in> phiUses g (last ns)
[PROOF STEP]
have "fold (step g) ns Map.empty (var g (vs ! i)) = s' (vs ! i)"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> Entry g-ns\<rightarrow>last ns
vs ! i \<in> phiUses g (last ns)

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g (vs ! i)) = s' (vs ! i)
[PROOF STEP]
by - (rule snoc.IH[where ms1="[?n']" and m1="?n'"], auto intro!: bs.intros)
[PROOF STATE]
proof (state)
this:
fold (step g) ns Map.empty (var g (vs ! i)) = s' (vs ! i)

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
hence "fold (step g) ns Map.empty (var g v) = s' (vs ! i)"
[PROOF STATE]
proof (prove)
using this:
fold (step g) ns Map.empty (var g (vs ! i)) = s' (vs ! i)

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' (vs ! i)
[PROOF STEP]
using phis_same_var[OF asm(2), of "vs ! i"] snoc.hyps(4) phis_wf[OF asm(2)]
[PROOF STATE]
proof (prove)
using this:
fold (step g) ns Map.empty (var g (vs ! i)) = s' (vs ! i)
vs ! i \<in> set vs \<Longrightarrow> var g (vs ! i) = var g v
i < length (old.predecessors g n)
length (old.predecessors g n) = length vs

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' (vs ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fold (step g) ns Map.empty (var g v) = s' (vs ! i)

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>g \<turnstile> Entry g-ns @ [n]\<rightarrow>n; phis g (n, v) = Some ?vs3; var g v \<notin> var g ` defs g n\<rbrakk> \<Longrightarrow> fold (step g) ns Map.empty (var g v) = s' (?vs3 ! i)

goal (1 subgoal):
 1. phi g v \<noteq> None \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g \<turnstile> Entry g-ns @ [n]\<rightarrow>n; phis g (n, v) = Some ?vs3; var g v \<notin> var g ` defs g n\<rbrakk> \<Longrightarrow> fold (step g) ns Map.empty (var g v) = s' (?vs3 ! i)

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
using phi snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g \<turnstile> Entry g-ns @ [n]\<rightarrow>n; phis g (n, v) = Some ?vs3; var g v \<notin> var g ` defs g n\<rbrakk> \<Longrightarrow> fold (step g) ns Map.empty (var g v) = s' (?vs3 ! i)
phi g v \<noteq> None
g \<turnstile> ns @ [n]\<Down>s

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
by - (erule bs.cases, auto dest!: 1 simp: step_def ssaStep_def oldDefs_def phi_def)
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g n i s' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g n i s' v

goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
hence "phis g (n, v) = None"
[PROOF STATE]
proof (prove)
using this:
var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. phis g (n, v) = None
[PROOF STEP]
by (auto simp: allDefs_def phiDefs_def)
[PROOF STATE]
proof (state)
this:
phis g (n, v) = None

goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
phis g (n, v) = None

goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
have "fold (step g) ns Map.empty (var g v) = s' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
from snoc.hyps(1)
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> ns\<Down>\<^sub>s s'
[PROOF STEP]
have "length ns \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> ns\<Down>\<^sub>s s'

goal (1 subgoal):
 1. 1 \<le> length ns
[PROOF STEP]
by (cases ns, auto)
[PROOF STATE]
proof (state)
this:
1 \<le> length ns

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> length ns

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
from snoc.prems(2,4) False
[PROOF STATE]
proof (chain)
picking this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
var g v \<notin> var g ` allDefs g n
[PROOF STEP]
have "\<forall>n \<in> set ms. var g v \<notin> var g ` allDefs g n"
[PROOF STATE]
proof (prove)
using this:
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
\<forall>n\<in>set (tl ms). var g v \<notin> var g ` allDefs g n
var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. \<forall>n\<in>set ms. var g v \<notin> var g ` allDefs g n
[PROOF STEP]
by (cases ms, auto simp: phiDefs_def dest: old.path2_hd)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set ms. var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> length ns
\<forall>n\<in>set ms. var g v \<notin> var g ` allDefs g n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> length ns
\<forall>n\<in>set ms. var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
using snoc.prems(1,2,3)
[PROOF STATE]
proof (prove)
using this:
1 \<le> length ns
\<forall>n\<in>set ms. var g v \<notin> var g ` allDefs g n
g \<turnstile> ns @ [n]\<Down>s
g \<turnstile> last (ns @ [n])-ms\<rightarrow>m
v \<in> allUses g m

goal (1 subgoal):
 1. fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
by - (rule snoc.IH[where ms1="last ns#ms"], auto elim!: bs.cases intro!: bs.intros elim: old.path2_unsnoc intro!: old.Cons_path2)
[PROOF STATE]
proof (state)
this:
fold (step g) ns Map.empty (var g v) = s' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fold (step g) ns Map.empty (var g v) = s' v

goal (1 subgoal):
 1. var g v \<notin> var g ` allDefs g n \<Longrightarrow> s (var g v) = ssaStep g n i s' v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
phis g (n, v) = None
fold (step g) ns Map.empty (var g v) = s' v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
phis g (n, v) = None
fold (step g) ns Map.empty (var g v) = s' v

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
using snoc.prems(1) False
[PROOF STATE]
proof (prove)
using this:
phis g (n, v) = None
fold (step g) ns Map.empty (var g v) = s' v
g \<turnstile> ns @ [n]\<Down>s
var g v \<notin> var g ` allDefs g n

goal (1 subgoal):
 1. s (var g v) = ssaStep g n i s' v
[PROOF STEP]
by - (erule bs.cases, auto simp: step_def ssaStep_def oldDefs_def)
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g n i s' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s (var g v) = ssaStep g n i s' v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma meval_ext: "\<forall>x. M\<langle>x\<rangle> = N\<langle>x\<rangle> \<Longrightarrow> M = N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. M\<langle>x\<rangle> = N\<langle>x\<rangle> \<Longrightarrow> M = N
[PROOF STEP]
apply (cases M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. M\<langle>x\<rangle> = N\<langle>x\<rangle>; M = Map x\<rbrakk> \<Longrightarrow> M = N
[PROOF STEP]
apply (cases N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x. M\<langle>x\<rangle> = N\<langle>x\<rangle>; M = Map x; N = Map xa\<rbrakk> \<Longrightarrow> M = N
[PROOF STEP]
by auto