[STATEMENT]
lemma slice_path_leqs_information_same_Uses:
  "\<lbrakk>n -as\<rightarrow>* n'; bs \<preceq>\<^sub>b bs'; slice_path as = bs;
    select_edge_kinds as bs = es; select_edge_kinds as bs' = es';
    \<forall>V xs. (V,xs,as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V;
    preds es' s'\<rbrakk>
  \<Longrightarrow> (\<forall>V \<in> Use n'. state_val (transfers es s) V =
      state_val (transfers es' s') V) \<and> preds es s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>* n'; bs \<preceq>\<^sub>b bs'; slice_path as = bs; select_edge_kinds as bs = es; select_edge_kinds as bs' = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(induct bs bs' arbitrary:as es es' n s s' rule:bv_leqs.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
[] \<preceq>\<^sub>b []
slice_path as = []
select_edge_kinds as [] = es
select_edge_kinds as [] = es'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
preds es' s'

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>slice_path as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_path as = []
[PROOF STEP]
have "as = []"
[PROOF STATE]
proof (prove)
using this:
slice_path as = []

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

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>select_edge_kinds as [] = es\<close> \<open>select_edge_kinds as [] = es'\<close>
[PROOF STATE]
proof (chain)
picking this:
select_edge_kinds as [] = es
select_edge_kinds as [] = es'
as = []
[PROOF STEP]
have "es = []" and "es' = []"
[PROOF STATE]
proof (prove)
using this:
select_edge_kinds as [] = es
select_edge_kinds as [] = es'
as = []

goal (1 subgoal):
 1. es = [] &&& es' = []
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
es = []
es' = []

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
es = []
es' = []

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V \<in> Use n'"
[PROOF STATE]
proof (state)
this:
V \<in> Use n'

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "(V,[],[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use n'

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
by(rule dep_vars_Use)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n'

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>\<forall>V xs. (V,xs,as) \<in> dependent_live_vars n' \<longrightarrow>
                  state_val s V = state_val s' V\<close> \<open>V \<in> Use n'\<close> \<open>as = []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
V \<in> Use n'
as = []
(V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
V \<in> Use n'
as = []
(V, [], []) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (4 subgoals):
 1. \<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b []; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 4. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>es = []\<close> \<open>es' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
es = []
es' = []
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
es = []
es' = []
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case (2 x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -?as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path ?as = xs; select_edge_kinds ?as xs = ?es; select_edge_kinds ?as ys = ?es'; \<forall>V xs. (V, xs, ?as) \<in> dependent_live_vars n' \<longrightarrow> state_val ?s V = state_val ?s' V; preds ?es' ?s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers ?es ?s) V = state_val (transfers ?es' ?s') V) \<and> preds ?es ?s
n -as\<rightarrow>* n'
x # xs \<preceq>\<^sub>b y # ys
slice_path as = x # xs
select_edge_kinds as (x # xs) = es
select_edge_kinds as (y # ys) = es'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
preds es' s'

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
note all = \<open>\<forall>V xs. (V,xs,as) \<in> dependent_live_vars n' \<longrightarrow>
                     state_val s V = state_val s' V\<close>
[PROOF STATE]
proof (state)
this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
note IH = \<open>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs;
                        select_edge_kinds as xs = es; select_edge_kinds as ys = es';
                        \<forall>V xs. (V,xs,as) \<in> dependent_live_vars n' \<longrightarrow>
                                   state_val s V = state_val s' V;
                           preds es' s'\<rbrakk>
            \<Longrightarrow> (\<forall>V \<in> Use n'. state_val (transfers es s) V =
                state_val (transfers es' s') V) \<and> preds es s\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n -?as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path ?as = xs; select_edge_kinds ?as xs = ?es; select_edge_kinds ?as ys = ?es'; \<forall>V xs. (V, xs, ?as) \<in> dependent_live_vars n' \<longrightarrow> state_val ?s V = state_val ?s' V; preds ?es' ?s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers ?es ?s) V = state_val (transfers ?es' ?s') V) \<and> preds ?es ?s

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>x#xs \<preceq>\<^sub>b y#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
x # xs \<preceq>\<^sub>b y # ys
[PROOF STEP]
have "x \<longrightarrow> y" and "xs \<preceq>\<^sub>b ys"
[PROOF STATE]
proof (prove)
using this:
x # xs \<preceq>\<^sub>b y # ys

goal (1 subgoal):
 1. x \<longrightarrow> y &&& xs \<preceq>\<^sub>b ys
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x \<longrightarrow> y
xs \<preceq>\<^sub>b ys

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>slice_path as = x#xs\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
[PROOF STEP]
obtain a' as' where "as = a'#as'"
    and "slice_path as' = xs"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs

goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; slice_path as' = xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule slice_path_right_Cons)
[PROOF STATE]
proof (state)
this:
as = a' # as'
slice_path as' = xs

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>as = a'#as'\<close> \<open>select_edge_kinds as (x#xs) = es\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
select_edge_kinds as (x # xs) = es
[PROOF STEP]
obtain ex esx where "es = ex#esx"
    and ex:"ex = (if x then kind a'
                    else (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>))"
    and "select_edge_kinds as' xs = esx"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
select_edge_kinds as (x # xs) = es

goal (1 subgoal):
 1. (\<And>ex esx. \<lbrakk>es = ex # esx; ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>); select_edge_kinds as' xs = esx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
es = ex # esx
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
select_edge_kinds as' xs = esx

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>as = a'#as'\<close> \<open>select_edge_kinds as (y#ys) = es'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
select_edge_kinds as (y # ys) = es'
[PROOF STEP]
obtain ex' esx'
    where "es' = ex'#esx'"
    and ex':"ex' = (if y then kind a'
                    else (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>))"
    and "select_edge_kinds as' ys = esx'"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
select_edge_kinds as (y # ys) = es'

goal (1 subgoal):
 1. (\<And>ex' esx'. \<lbrakk>es' = ex' # esx'; ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>); select_edge_kinds as' ys = esx'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
es' = ex' # esx'
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
select_edge_kinds as' ys = esx'

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>n -as\<rightarrow>* n'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = a' # as'
[PROOF STEP]
have [simp]:"n = sourcenode a'"
    and "valid_edge a'" and "targetnode a' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = a' # as'

goal (1 subgoal):
 1. n = sourcenode a' &&& valid_edge a' &&& targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
by(auto elim:path_split_Cons)
[PROOF STATE]
proof (state)
this:
n = sourcenode a'
valid_edge a'
targetnode a' -as'\<rightarrow>* n'

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>n -as\<rightarrow>* n'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
as = a' # as'
[PROOF STEP]
have "last(targetnodes as) = n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
as = a' # as'

goal (1 subgoal):
 1. last (targetnodes as) = n'
[PROOF STEP]
by(fastforce intro:path_targetnode)
[PROOF STATE]
proof (state)
this:
last (targetnodes as) = n'

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>preds es' s'\<close> \<open>es' = ex'#esx'\<close>
[PROOF STATE]
proof (chain)
picking this:
preds es' s'
es' = ex' # esx'
[PROOF STEP]
have "pred ex' s'"
    and "preds esx' (transfer ex' s')"
[PROOF STATE]
proof (prove)
using this:
preds es' s'
es' = ex' # esx'

goal (1 subgoal):
 1. pred ex' s' &&& preds esx' (transfer ex' s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
pred ex' s'
preds esx' (transfer ex' s')

goal (3 subgoals):
 1. \<And>x xs y ys as es es' n s s'. \<lbrakk>\<And>as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; xs \<preceq>\<^sub>b ys; slice_path as = xs; select_edge_kinds as xs = es; select_edge_kinds as ys = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s; n -as\<rightarrow>* n'; x # xs \<preceq>\<^sub>b y # ys; slice_path as = x # xs; select_edge_kinds as (x # xs) = es; select_edge_kinds as (y # ys) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 3. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence [simp]:"as' = []"
[PROOF STATE]
proof (prove)
using this:
as' = []

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

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>slice_path as' = xs\<close> \<open>xs \<preceq>\<^sub>b ys\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_path as' = xs
xs \<preceq>\<^sub>b ys
as' = []
[PROOF STEP]
have [simp]:"xs = [] \<and> ys = []"
[PROOF STATE]
proof (prove)
using this:
slice_path as' = xs
xs \<preceq>\<^sub>b ys
as' = []

goal (1 subgoal):
 1. xs = [] \<and> ys = []
[PROOF STEP]
by auto(cases ys,auto)+
[PROOF STATE]
proof (state)
this:
xs = [] \<and> ys = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>select_edge_kinds as' xs = esx\<close> \<open>select_edge_kinds as' ys = esx'\<close>
[PROOF STATE]
proof (chain)
picking this:
select_edge_kinds as' xs = esx
select_edge_kinds as' ys = esx'
xs = [] \<and> ys = []
[PROOF STEP]
have [simp]:"esx = []" and [simp]:"esx' = []"
[PROOF STATE]
proof (prove)
using this:
select_edge_kinds as' xs = esx
select_edge_kinds as' ys = esx'
xs = [] \<and> ys = []

goal (1 subgoal):
 1. esx = [] &&& esx' = []
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
esx = []
esx' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from True \<open>targetnode a' -as'\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = []
targetnode a' -as'\<rightarrow>* n'
[PROOF STEP]
have [simp]:"n' = targetnode a'"
[PROOF STATE]
proof (prove)
using this:
as' = []
targetnode a' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. n' = targetnode a'
[PROOF STEP]
by(auto elim:path.cases)
[PROOF STATE]
proof (state)
this:
n' = targetnode a'

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>x \<longrightarrow> y\<close> ex ex'
[PROOF STATE]
proof (chain)
picking this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
[PROOF STEP]
have [simp]:"ex = kind a' \<and> ex' = kind a'"
[PROOF STATE]
proof (prove)
using this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x

goal (1 subgoal):
 1. ex = kind a' \<and> ex' = kind a'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ex = kind a' \<and> ex' = kind a'

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
have "pred ex s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof(cases ex)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
case (Predicate Q)
[PROOF STATE]
proof (state)
this:
ex = (Q)\<^sub>\<surd>

goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
with ex ex' True \<open>x \<longrightarrow> y\<close>
[PROOF STATE]
proof (chain)
picking this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
x \<longrightarrow> y
ex = (Q)\<^sub>\<surd>
[PROOF STEP]
have [simp]:"transfer ex s = s"
          and [simp]:"transfer ex' s' = s'"
[PROOF STATE]
proof (prove)
using this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
x \<longrightarrow> y
ex = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. transfer ex s = s &&& transfer ex' s' = s'
[PROOF STEP]
by(cases "kind a'",auto)+
[PROOF STATE]
proof (state)
this:
transfer ex s = s
transfer ex' s' = s'

goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof(cases "n -[a']\<rightarrow>\<^sub>c\<^sub>d n'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n -[a']\<rightarrow>\<^sub>c\<^sub>d n'

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n -[a']\<rightarrow>\<^sub>c\<^sub>d n'

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
fix V'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
assume "V' \<in> Use n"
[PROOF STATE]
proof (state)
this:
V' \<in> Use n

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
with True \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -[a']\<rightarrow>\<^sub>c\<^sub>d n'
valid_edge a'
V' \<in> Use n
[PROOF STEP]
have "(V',[],a'#[]@[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
n -[a']\<rightarrow>\<^sub>c\<^sub>d n'
valid_edge a'
V' \<in> Use n

goal (1 subgoal):
 1. (V', [], a' # [] @ []) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil
                          simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
(V', [], a' # [] @ []) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], a' # [] @ []) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], a' # [] @ []) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (2 subgoals):
 1. n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
 2. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>pred ex' s'\<close> \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
pred ex' s'
valid_edge a'
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred ex' s'
valid_edge a'
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(fastforce elim:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred ex s

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n'

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
from ex True Predicate
[PROOF STATE]
proof (chain)
picking this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
ex = (Q)\<^sub>\<surd>
[PROOF STEP]
have "kind a' = (Q)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
ex = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. kind a' = (Q)\<^sub>\<surd>
[PROOF STEP]
by(auto split:if_split_asm)
[PROOF STATE]
proof (state)
this:
kind a' = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
from True \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
x
slice_path as = x # xs
as = a' # as'
[PROOF STEP]
have "n -[a']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
x
slice_path as = x # xs
as = a' # as'

goal (1 subgoal):
 1. n -[a']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
n -[a']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n -[a']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof(induct rule:DynPDG_path.cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>n = n; [a'] = []; n' = n; valid_node n\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case (DynPDG_path_Nil nx)
[PROOF STATE]
proof (state)
this:
n = nx
[a'] = []
n' = nx
valid_node nx

goal (3 subgoals):
 1. \<And>n. \<lbrakk>n = n; [a'] = []; n' = n; valid_node n\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
n = nx
[a'] = []
n' = nx
valid_node nx

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

goal (3 subgoals):
 1. \<And>n. \<lbrakk>n = n; [a'] = []; n' = n; valid_node n\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (2 subgoals):
 1. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case (DynPDG_path_Append_cdep nx asx n'' asx' nx')
[PROOF STATE]
proof (state)
this:
n = nx
[a'] = asx @ asx'
n' = nx'
nx -asx\<rightarrow>\<^sub>d* n''
n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'

goal (2 subgoals):
 1. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>[a'] = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
[a'] = asx @ asx'
[PROOF STEP]
have "(asx = [a'] \<and> asx' = []) \<or> (asx = [] \<and> asx' = [a'])"
[PROOF STATE]
proof (prove)
using this:
[a'] = asx @ asx'

goal (1 subgoal):
 1. asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']
[PROOF STEP]
by (cases asx) auto
[PROOF STATE]
proof (state)
this:
asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']

goal (2 subgoals):
 1. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. asx = [a'] \<and> asx' = [] \<Longrightarrow> False
 2. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
assume "asx = [a'] \<and> asx' = []"
[PROOF STATE]
proof (state)
this:
asx = [a'] \<and> asx' = []

goal (2 subgoals):
 1. asx = [a'] \<and> asx' = [] \<Longrightarrow> False
 2. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
with \<open>n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'
asx = [a'] \<and> asx' = []
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'
asx = [a'] \<and> asx' = []

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
assume "asx = [] \<and> asx' = [a']"
[PROOF STATE]
proof (state)
this:
asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
with \<open>nx -asx\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx\<rightarrow>\<^sub>d* n''
asx = [] \<and> asx' = [a']
[PROOF STEP]
have "nx = n''" and "asx' = [a']"
[PROOF STATE]
proof (prove)
using this:
nx -asx\<rightarrow>\<^sub>d* n''
asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. nx = n'' &&& asx' = [a']
[PROOF STEP]
by(auto intro:DynPDG_empty_path_eq_nodes)
[PROOF STATE]
proof (state)
this:
nx = n''
asx' = [a']

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> False
[PROOF STEP]
with \<open>n = nx\<close> \<open>n' = nx'\<close> \<open>n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'\<close> False
[PROOF STATE]
proof (chain)
picking this:
n = nx
n' = nx'
n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'
\<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n'
nx = n''
asx' = [a']
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n = nx
n' = nx'
n'' -asx'\<rightarrow>\<^sub>c\<^sub>d nx'
\<not> n -[a']\<rightarrow>\<^sub>c\<^sub>d n'
nx = n''
asx' = [a']

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>n as n'' as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case (DynPDG_path_Append_ddep nx asx n'' V asx' nx')
[PROOF STATE]
proof (state)
this:
n = nx
[a'] = asx @ asx'
n' = nx'
nx -asx\<rightarrow>\<^sub>d* n''
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>[a'] = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
[a'] = asx @ asx'
[PROOF STEP]
have "(asx = [a'] \<and> asx' = []) \<or> (asx = [] \<and> asx' = [a'])"
[PROOF STATE]
proof (prove)
using this:
[a'] = asx @ asx'

goal (1 subgoal):
 1. asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']
[PROOF STEP]
by (cases asx) auto
[PROOF STATE]
proof (state)
this:
asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. \<And>n as n'' V as' n'a. \<lbrakk>n = n; [a'] = as @ as'; n' = n'a; n -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
asx = [a'] \<and> asx' = [] \<or> asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. asx = [a'] \<and> asx' = [] \<Longrightarrow> pred ex s
 2. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
assume "asx = [a'] \<and> asx' = []"
[PROOF STATE]
proof (state)
this:
asx = [a'] \<and> asx' = []

goal (2 subgoals):
 1. asx = [a'] \<and> asx' = [] \<Longrightarrow> pred ex s
 2. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [a'] \<and> asx' = []
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [a'] \<and> asx' = []

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. asx = [a'] \<and> asx' = [] \<Longrightarrow> pred ex s
 2. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
assume "asx = [] \<and> asx' = [a']"
[PROOF STATE]
proof (state)
this:
asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>nx -asx\<rightarrow>\<^sub>d* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -asx\<rightarrow>\<^sub>d* n''
asx = [] \<and> asx' = [a']
[PROOF STEP]
have "nx = n''"
[PROOF STATE]
proof (prove)
using this:
nx -asx\<rightarrow>\<^sub>d* n''
asx = [] \<and> asx' = [a']

goal (1 subgoal):
 1. nx = n''
[PROOF STEP]
by(simp add:DynPDG_empty_path_eq_nodes)
[PROOF STATE]
proof (state)
this:
nx = n''

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
nx = n''

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
fix V'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
assume "V' \<in> Use n"
[PROOF STATE]
proof (state)
this:
V' \<in> Use n

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'\<close> \<open>asx = [] \<and> asx' = [a']\<close> \<open>n' = nx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [] \<and> asx' = [a']
n' = nx'
[PROOF STEP]
have "(V,[],[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [] \<and> asx' = [a']
n' = nx'

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Use elim:DynPDG_edge.cases
                    simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>V' \<in> Use n\<close> \<open>n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'\<close> \<open>asx = [] \<and> asx' = [a']\<close>
                  \<open>n = nx\<close> \<open>nx = n''\<close> \<open>n' = nx'\<close>
[PROOF STATE]
proof (chain)
picking this:
V' \<in> Use n
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [] \<and> asx' = [a']
n = nx
nx = n''
n' = nx'
(V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
have "(V',[],[a']) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
V' \<in> Use n
n'' -{V}asx'\<rightarrow>\<^sub>d\<^sub>d nx'
asx = [] \<and> asx' = [a']
n = nx
nx = n''
n' = nx'
(V, [], []) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. (V', [], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
by(auto elim:dep_vars_Cons_ddep simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
(V', [], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (1 subgoal):
 1. asx = [] \<and> asx' = [a'] \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>pred ex' s'\<close> \<open>valid_edge a'\<close> ex ex' True \<open>x \<longrightarrow> y\<close>
[PROOF STATE]
proof (chain)
picking this:
pred ex' s'
valid_edge a'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
x \<longrightarrow> y
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred ex' s'
valid_edge a'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
x
x \<longrightarrow> y
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(fastforce elim:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred ex s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pred ex s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pred ex s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pred ex s

goal (1 subgoal):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
pred ex s

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
pred ex s

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V \<in> Use n'"
[PROOF STATE]
proof (state)
this:
V \<in> Use n'

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>V \<in> Use n'\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<in> Use n'
[PROOF STEP]
have "(V,[],[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use n'

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
by(rule dep_vars_Use)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
have "state_val (transfer ex s) V = state_val (transfer ex' s') V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
proof(cases "n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
hence "V \<in> Def n"
[PROOF STATE]
proof (prove)
using this:
n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. V \<in> Def n
[PROOF STEP]
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
V \<in> Def n

goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
have "\<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V
[PROOF STEP]
fix V'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V
[PROOF STEP]
assume "V' \<in> Use n"
[PROOF STATE]
proof (state)
this:
V' \<in> Use n

goal (1 subgoal):
 1. \<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V
[PROOF STEP]
with \<open>(V,[],[]) \<in> dependent_live_vars n'\<close> True
[PROOF STATE]
proof (chain)
picking this:
(V, [], []) \<in> dependent_live_vars n'
n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
V' \<in> Use n
[PROOF STEP]
have "(V',[],[a']) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
(V, [], []) \<in> dependent_live_vars n'
n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
V' \<in> Use n

goal (1 subgoal):
 1. (V', [], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
(V', [], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<And>V. V \<in> Use n \<Longrightarrow> state_val s V = state_val s' V
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
show "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V', [], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?V \<in> Use n \<Longrightarrow> state_val s ?V = state_val s' ?V

goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>pred ex' s'\<close> \<open>pred ex s\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
pred ex' s'
pred ex s
?V \<in> Use n \<Longrightarrow> state_val s ?V = state_val s' ?V
[PROOF STEP]
have "\<forall>V \<in> Def n. state_val (transfer (kind a') s) V =
                              state_val (transfer (kind a') s') V"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
pred ex' s'
pred ex s
?V \<in> Use n \<Longrightarrow> state_val s ?V = state_val s' ?V

goal (1 subgoal):
 1. \<forall>V\<in>Def n. state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V
[PROOF STEP]
by simp(rule CFG_edge_transfer_uses_only_Use,auto)
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Def n. state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V

goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
with \<open>V \<in> Def n\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<in> Def n
\<forall>V\<in>Def n. state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V
[PROOF STEP]
have "state_val (transfer (kind a') s) V =
                         state_val (transfer (kind a') s') V"
[PROOF STATE]
proof (prove)
using this:
V \<in> Def n
\<forall>V\<in>Def n. state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V

goal (1 subgoal):
 1. state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V

goal (2 subgoals):
 1. n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
 2. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V

goal (1 subgoal):
 1. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
with \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
            \<open>(V,[],[]) \<in> dependent_live_vars n'\<close>
[PROOF STATE]
proof (chain)
picking this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "(V,[a'],[a']) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. (V, [a'], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_keep)
[PROOF STATE]
proof (state)
this:
(V, [a'], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
from \<open>(V,[a'],[a']) \<in> dependent_live_vars n'\<close> all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
(V, [a'], [a']) \<in> dependent_live_vars n'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
[PROOF STEP]
have states_eq:"state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
(V, [a'], [a']) \<in> dependent_live_vars n'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>V \<in> Use n'\<close> False \<open>pred ex s\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
V \<in> Use n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
pred ex s
[PROOF STEP]
have "state_val (transfers (kinds [a']) s) V = state_val s V"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
V \<in> Use n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
pred ex s

goal (1 subgoal):
 1. state_val (transfers (kinds [a']) s) V = state_val s V
[PROOF STEP]
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}[a']\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s\<rbrakk> \<Longrightarrow> preds (kinds [a']) s
 2. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:kinds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(case_tac as',auto)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds [a']) s) V = state_val s V

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds [a']) s) V = state_val s V

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>V \<in> Use n'\<close> False \<open>pred ex' s'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
V \<in> Use n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
pred ex' s'
[PROOF STEP]
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
V \<in> Use n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
pred ex' s'

goal (1 subgoal):
 1. state_val (transfers (kinds [a']) s') V = state_val s' V
[PROOF STEP]
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}[a']\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s'\<rbrakk> \<Longrightarrow> preds (kinds [a']) s'
 2. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s'; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:kinds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; pred (kind a') s'; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(case_tac as',auto)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds [a']) s') V = state_val s' V

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
state_val (transfers (kinds [a']) s) V = state_val s V
state_val (transfers (kinds [a']) s') V = state_val s' V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds [a']) s) V = state_val s V
state_val (transfers (kinds [a']) s') V = state_val s' V

goal (1 subgoal):
 1. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
using states_eq
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds [a']) s) V = state_val s V
state_val (transfers (kinds [a']) s') V = state_val s' V
state_val s V = state_val s' V

goal (1 subgoal):
 1. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
by(auto simp:kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfer ex s) V = state_val (transfer ex' s') V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use n' \<Longrightarrow> state_val (transfer ex s) ?V2 = state_val (transfer ex' s') ?V2

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "\<forall>V \<in> Use n'. state_val (transfer ex s) V =
                                state_val (transfer ex' s') V"
[PROOF STATE]
proof (prove)
using this:
?V2 \<in> Use n' \<Longrightarrow> state_val (transfer ex s) ?V2 = state_val (transfer ex' s') ?V2

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>pred ex s\<close> \<open>es = ex#esx\<close> \<open>es' = ex'#esx'\<close>
[PROOF STATE]
proof (chain)
picking this:
pred ex s
es = ex # esx
es' = ex' # esx'
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred ex s
es = ex # esx
es' = ex' # esx'
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x

goal (1 subgoal):
 1. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with ex
[PROOF STATE]
proof (chain)
picking this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> x
[PROOF STEP]
have cases_x:"ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)"
[PROOF STATE]
proof (prove)
using this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> x

goal (1 subgoal):
 1. ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from cases_x
[PROOF STATE]
proof (chain)
picking this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
have "pred ex s"
[PROOF STATE]
proof (prove)
using this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(cases "kind a'",auto)
[PROOF STATE]
proof (state)
this:
pred ex s

goal (1 subgoal):
 1. \<not> x \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with ex'
[PROOF STATE]
proof (chain)
picking this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
y
[PROOF STEP]
have [simp]:"ex' = kind a'"
[PROOF STATE]
proof (prove)
using this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
y

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

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ex' = kind a'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V \<in> Use n'"
[PROOF STATE]
proof (state)
this:
V \<in> Use n'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>V \<in> Use n'\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<in> Use n'
[PROOF STEP]
have "(V,[],[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use n'

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
by(rule dep_vars_Use)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close> \<open>\<not> x\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
as = a' # as'
\<not> x
[PROOF STEP]
have "\<not> n -[a']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs
as = a' # as'
\<not> x

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
\<not> n -[a']\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'"
[PROOF STATE]
proof (prove)
using this:
\<not> n -[a']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
by(fastforce dest:DynPDG_path_ddep)
[PROOF STATE]
proof (state)
this:
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
            \<open>(V,[],[]) \<in> dependent_live_vars n'\<close>
[PROOF STATE]
proof (chain)
picking this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "(V,[a'],[a']) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. (V, [a'], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_keep)
[PROOF STATE]
proof (state)
this:
(V, [a'], [a']) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [a'], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [a'], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>V \<in> Use n'\<close> \<open>pred ex' s'\<close>
            \<open>\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
V \<in> Use n'
pred ex' s'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
last (targetnodes as) = n'
as = a' # as'
[PROOF STEP]
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
V \<in> Use n'
pred ex' s'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
last (targetnodes as) = n'
as = a' # as'

goal (1 subgoal):
 1. state_val (transfers (kinds [a']) s') V = state_val s' V
[PROOF STEP]
apply(auto intro!:no_ddep_same_state path_edge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); pred (kind a') s'; \<not> sourcenode a' -{V}[a']\<rightarrow>\<^sub>d\<^sub>d targetnode a'; last (targetnodes [a']) = targetnode a'; as = [a']\<rbrakk> \<Longrightarrow> preds (kinds [a']) s'
 2. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); pred (kind a') s'; \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; last (targetnodes (as' @ a # as'')) = targetnode a'; as = as' @ a # as''; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(simp add:kinds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as' a as''. \<lbrakk>valid_edge a'; V \<in> Use (targetnode a'); pred (kind a') s'; \<not> sourcenode a' -{V}as' @ a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'; last (targetnodes (as' @ a # as'')) = targetnode a'; as = as' @ a # as''; [a'] = as' @ a # as''; sourcenode a -{V}a # as''\<rightarrow>\<^sub>d\<^sub>d targetnode a'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(case_tac as',auto)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds [a']) s') V = state_val s' V

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>state_val s V = state_val s' V\<close> cases_x
[PROOF STATE]
proof (chain)
picking this:
state_val s V = state_val s' V
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
state_val (transfers (kinds [a']) s') V = state_val s' V
[PROOF STEP]
have "state_val (transfer ex s) V =
                state_val (transfer ex' s') V"
[PROOF STATE]
proof (prove)
using this:
state_val s V = state_val s' V
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
state_val (transfers (kinds [a']) s') V = state_val s' V

goal (1 subgoal):
 1. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
by(cases "kind a'",simp_all add:kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use n' \<Longrightarrow> state_val (transfer ex s) ?V2 = state_val (transfer ex' s') ?V2

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "\<forall>V \<in> Use n'. state_val (transfer ex s) V =
                           state_val (transfer ex' s') V"
[PROOF STATE]
proof (prove)
using this:
?V2 \<in> Use n' \<Longrightarrow> state_val (transfer ex s) ?V2 = state_val (transfer ex' s') ?V2

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>as = a'#as'\<close> \<open>es = ex#esx\<close> \<open>es' = ex'#esx'\<close> \<open>pred ex s\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
es = ex # esx
es' = ex' # esx'
pred ex s
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
es = ex # esx
es' = ex' # esx'
pred ex s
\<forall>V\<in>Use n'. state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with ex'
[PROOF STATE]
proof (chain)
picking this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> y
[PROOF STEP]
have cases_y:"ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)"
[PROOF STATE]
proof (prove)
using this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> y

goal (1 subgoal):
 1. ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with cases_x
[PROOF STATE]
proof (chain)
picking this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
have [simp]:"ex = ex'"
[PROOF STATE]
proof (prove)
using this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. ex = ex'
[PROOF STEP]
by(cases "kind a'") auto
[PROOF STATE]
proof (state)
this:
ex = ex'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ex = ex'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V \<in> Use n'"
[PROOF STATE]
proof (state)
this:
V \<in> Use n'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>V \<in> Use n'\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<in> Use n'
[PROOF STEP]
have "(V,[],[]) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use n'

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n'
[PROOF STEP]
by(rule dep_vars_Use)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close> \<open>\<not> x\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
as = a' # as'
\<not> x
[PROOF STEP]
have "\<not> n -[a']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs
as = a' # as'
\<not> x

goal (1 subgoal):
 1. \<not> n -[a']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
\<not> n -[a']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence no_dep:"\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'"
[PROOF STATE]
proof (prove)
using this:
\<not> n -[a']\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
by(fastforce dest:DynPDG_path_ddep)
[PROOF STATE]
proof (state)
this:
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
            \<open>(V,[],[]) \<in> dependent_live_vars n'\<close>
[PROOF STATE]
proof (chain)
picking this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "(V,[a'],[a']) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
last (targetnodes as) = n'
as = a' # as'
(V, [], []) \<in> dependent_live_vars n'
\<not> n -{V}[a']\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. (V, [a'], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_keep)
[PROOF STATE]
proof (state)
this:
(V, [a'], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [a'], [a']) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [a'], [a']) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>as = a'#as'\<close> cases_x \<open>es = ex#esx\<close> \<open>es' = ex'#esx'\<close> \<open>pred ex s\<close>
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
es = ex # esx
es' = ex' # esx'
pred ex s
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
es = ex # esx
es' = ex' # esx'
pred ex s
?V2 \<in> Use n' \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by(cases "kind a'",auto)
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases "\<forall>V xs. (V,xs,as') \<in> dependent_live_vars n' \<longrightarrow>
                        state_val (transfer ex s) V = state_val (transfer ex' s') V")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence imp':"\<forall>V xs. (V,xs,as') \<in> dependent_live_vars n' \<longrightarrow>
                       state_val (transfer ex s) V = state_val (transfer ex' s') V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (1 subgoal):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V

goal (2 subgoals):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from IH[OF \<open>targetnode a' -as'\<rightarrow>* n'\<close> \<open>xs \<preceq>\<^sub>b ys\<close> \<open>slice_path as' = xs\<close>
        \<open>select_edge_kinds as' xs = esx\<close> \<open>select_edge_kinds as' ys = esx'\<close>
        this \<open>preds esx' (transfer ex' s')\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V) \<and> preds esx (transfer ex s)
[PROOF STEP]
have all':"\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V =
                             state_val (transfers esx' (transfer ex' s')) V"
        and "preds esx (transfer ex s)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V) \<and> preds esx (transfer ex s)

goal (1 subgoal):
 1. \<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V &&& preds esx (transfer ex s)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V
preds esx (transfer ex s)

goal (2 subgoals):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
have "pred ex s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof(cases ex)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
case (Predicate Q)
[PROOF STATE]
proof (state)
this:
ex = (Q)\<^sub>\<surd>

goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close> \<open>last(targetnodes as) = n'\<close> ex
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = (Q)\<^sub>\<surd>
[PROOF STEP]
have "ex = (\<lambda>s. True)\<^sub>\<surd> \<or> n -a'#as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. ex = (\<lambda>s. True)\<^sub>\<surd> \<or> n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(cases "kind a'",auto split:if_split_asm)
[PROOF STATE]
proof (state)
this:
ex = (\<lambda>s. True)\<^sub>\<surd> \<or> n -a' # as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
 2. \<And>x2. ex = (x2)\<^sub>\<surd> \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ex = (\<lambda>s. True)\<^sub>\<surd> \<or> n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ex = (\<lambda>s. True)\<^sub>\<surd> \<Longrightarrow> pred ex s
 2. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
assume "ex = (\<lambda>s. True)\<^sub>\<surd>"
[PROOF STATE]
proof (state)
this:
ex = (\<lambda>s. True)\<^sub>\<surd>

goal (2 subgoals):
 1. ex = (\<lambda>s. True)\<^sub>\<surd> \<Longrightarrow> pred ex s
 2. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ex = (\<lambda>s. True)\<^sub>\<surd>

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

goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
assume "n -a'#as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (state)
this:
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close> \<open>last(targetnodes as) = n'\<close> ex
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have [simp]:"ex = kind a'"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. ex = kind a'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
ex = kind a'

goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>x \<longrightarrow> y\<close> ex ex'
[PROOF STATE]
proof (chain)
picking this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = kind a'
[PROOF STEP]
have [simp]:"ex' = ex"
[PROOF STATE]
proof (prove)
using this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = kind a'

goal (1 subgoal):
 1. ex' = ex
[PROOF STEP]
by(cases x) auto
[PROOF STATE]
proof (state)
this:
ex' = ex

goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n -a'#as'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
proof(induct rule:DynPDG_path_rev_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>a' # as' = []; n = n'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case DynPDG_path_Nil
[PROOF STATE]
proof (state)
this:
a' # as' = []
n = n'

goal (3 subgoals):
 1. \<lbrakk>a' # as' = []; n = n'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
a' # as' = []
n = n'

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

goal (3 subgoals):
 1. \<lbrakk>a' # as' = []; n = n'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 3. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case (DynPDG_path_cdep_Append n'' asx asx')
[PROOF STATE]
proof (state)
this:
n -asx\<rightarrow>\<^sub>c\<^sub>d n''
n'' -asx'\<rightarrow>\<^sub>d* n'
a' # as' = asx @ asx'

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n -asx\<rightarrow>\<^sub>c\<^sub>d n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -asx\<rightarrow>\<^sub>c\<^sub>d n''
[PROOF STEP]
have "asx \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n -asx\<rightarrow>\<^sub>c\<^sub>d n''

goal (1 subgoal):
 1. asx \<noteq> []
[PROOF STEP]
by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
[PROOF STATE]
proof (state)
this:
asx \<noteq> []

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>n -asx\<rightarrow>\<^sub>c\<^sub>d n''\<close> \<open>n'' -asx'\<rightarrow>\<^sub>d* n'\<close> \<open>a'#as' = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -asx\<rightarrow>\<^sub>c\<^sub>d n''
n'' -asx'\<rightarrow>\<^sub>d* n'
a' # as' = asx @ asx'
asx \<noteq> []
[PROOF STEP]
have cdep:"\<exists>as1 as2 n''. n -a'#as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and>
                                     n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1@as2"
[PROOF STATE]
proof (prove)
using this:
n -asx\<rightarrow>\<^sub>c\<^sub>d n''
n'' -asx'\<rightarrow>\<^sub>d* n'
a' # as' = asx @ asx'
asx \<noteq> []

goal (1 subgoal):
 1. \<exists>as1 as2 n''. n -a' # as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1 @ as2
[PROOF STEP]
by(cases asx) auto
[PROOF STATE]
proof (state)
this:
\<exists>as1 as2 n''. n -a' # as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1 @ as2

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>as1 as2 n''. n -a' # as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1 @ as2

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
assume "V \<in> Use n"
[PROOF STATE]
proof (state)
this:
V \<in> Use n

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with cdep \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as1 as2 n''. n -a' # as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1 @ as2
last (targetnodes as) = n'
as = a' # as'
V \<in> Use n
[PROOF STEP]
have "(V,[],as) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
\<exists>as1 as2 n''. n -a' # as1\<rightarrow>\<^sub>c\<^sub>d n'' \<and> n'' -as2\<rightarrow>\<^sub>d* n' \<and> as' = as1 @ as2
last (targetnodes as) = n'
as = a' # as'
V \<in> Use n

goal (1 subgoal):
 1. (V, [], as) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_cdep)
[PROOF STATE]
proof (state)
this:
(V, [], as) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with all
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V, [], as) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V, [], as) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use n \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (2 subgoals):
 1. \<And>n'' asx asx'. \<lbrakk>n -asx\<rightarrow>\<^sub>c\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
 2. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>pred ex' s'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
pred ex' s'
?V2 \<in> Use n \<Longrightarrow> state_val s ?V2 = state_val s' ?V2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
pred ex' s'
?V2 \<in> Use n \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(fastforce elim:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred ex s

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
case (DynPDG_path_ddep_Append V n'' asx asx')
[PROOF STATE]
proof (state)
this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
n'' -asx'\<rightarrow>\<^sub>d* n'
a' # as' = asx @ asx'

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
[PROOF STEP]
obtain ai ais where "asx = ai#ais"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''

goal (1 subgoal):
 1. (\<And>ai ais. asx = ai # ais \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases asx)(auto dest:DynPDG_ddep_edge_CFG_path)
[PROOF STATE]
proof (state)
this:
asx = ai # ais

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
[PROOF STEP]
have "sourcenode ai = n"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais

goal (1 subgoal):
 1. sourcenode ai = n
[PROOF STEP]
by(fastforce dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
[PROOF STATE]
proof (state)
this:
sourcenode ai = n

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>asx = ai#ais\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
[PROOF STEP]
have "last(targetnodes asx) = n''"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais

goal (1 subgoal):
 1. last (targetnodes asx) = n''
[PROOF STEP]
by(fastforce intro:path_targetnode dest:DynPDG_ddep_edge_CFG_path)
[PROOF STATE]
proof (state)
this:
last (targetnodes asx) = n''

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
last (targetnodes asx) = n''

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
fix V'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
assume "V' \<in> Use n"
[PROOF STATE]
proof (state)
this:
V' \<in> Use n

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
from \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
[PROOF STEP]
have "(V,[],[]) \<in> dependent_live_vars n''"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars n''
[PROOF STEP]
by(fastforce elim:DynPDG_edge.cases dep_vars_Use
                            simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars n''

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>n'' -asx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -asx'\<rightarrow>\<^sub>d* n'
(V, [], []) \<in> dependent_live_vars n''
[PROOF STEP]
have "(V,[],[]@asx') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
n'' -asx'\<rightarrow>\<^sub>d* n'
(V, [], []) \<in> dependent_live_vars n''

goal (1 subgoal):
 1. (V, [], [] @ asx') \<in> dependent_live_vars n'
[PROOF STEP]
by(rule dependent_live_vars_dep_dependent_live_vars)
[PROOF STATE]
proof (state)
this:
(V, [], [] @ asx') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
have "(V',[],as) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
proof(cases "asx' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
 2. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
asx' = []

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
 2. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
with \<open>n'' -asx'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -asx'\<rightarrow>\<^sub>d* n'
asx' = []
[PROOF STEP]
have "n'' = n'"
[PROOF STATE]
proof (prove)
using this:
n'' -asx'\<rightarrow>\<^sub>d* n'
asx' = []

goal (1 subgoal):
 1. n'' = n'
[PROOF STEP]
by(fastforce intro:DynPDG_empty_path_eq_nodes)
[PROOF STATE]
proof (state)
this:
n'' = n'

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
 2. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
with \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>V' \<in> Use n\<close> True \<open>as = a'#as'\<close>
                  \<open>a'#as' = asx@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
V' \<in> Use n
asx' = []
as = a' # as'
a' # as' = asx @ asx'
n'' = n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
V' \<in> Use n
asx' = []
as = a' # as'
a' # as' = asx @ asx'
n'' = n'

goal (1 subgoal):
 1. (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dependent_live_vars_ddep_empty_fst)
[PROOF STATE]
proof (state)
this:
(V', [], as) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
asx' \<noteq> []

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
with \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>asx = ai#ais\<close>
                  \<open>(V,[],[]@asx') \<in> dependent_live_vars n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
(V, [], [] @ asx') \<in> dependent_live_vars n'
asx' \<noteq> []
[PROOF STEP]
have "(V,ais@[],ais@asx') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
(V, [], [] @ asx') \<in> dependent_live_vars n'
asx' \<noteq> []

goal (1 subgoal):
 1. (V, ais @ [], ais @ asx') \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:ddep_dependent_live_vars_keep_notempty)
[PROOF STATE]
proof (state)
this:
(V, ais @ [], ais @ asx') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
from \<open>n'' -asx'\<rightarrow>\<^sub>d* n'\<close> False
[PROOF STATE]
proof (chain)
picking this:
n'' -asx'\<rightarrow>\<^sub>d* n'
asx' \<noteq> []
[PROOF STEP]
have "last(targetnodes asx') = n'"
[PROOF STATE]
proof (prove)
using this:
n'' -asx'\<rightarrow>\<^sub>d* n'
asx' \<noteq> []

goal (1 subgoal):
 1. last (targetnodes asx') = n'
[PROOF STEP]
by -(rule path_targetnode,rule DynPDG_path_CFG_path)
[PROOF STATE]
proof (state)
this:
last (targetnodes asx') = n'

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
with \<open>(V,ais@[],ais@asx') \<in> dependent_live_vars n'\<close>
                  \<open>V' \<in> Use n\<close> \<open>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''\<close> \<open>asx = ai#ais\<close>
                  \<open>sourcenode ai = n\<close> \<open>last(targetnodes asx) = n''\<close> False
[PROOF STATE]
proof (chain)
picking this:
(V, ais @ [], ais @ asx') \<in> dependent_live_vars n'
V' \<in> Use n
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
sourcenode ai = n
last (targetnodes asx) = n''
asx' \<noteq> []
last (targetnodes asx') = n'
[PROOF STEP]
have "(V',[],ai#ais@asx') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
(V, ais @ [], ais @ asx') \<in> dependent_live_vars n'
V' \<in> Use n
n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''
asx = ai # ais
sourcenode ai = n
last (targetnodes asx) = n''
asx' \<noteq> []
last (targetnodes asx') = n'

goal (1 subgoal):
 1. (V', [], ai # ais @ asx') \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
(V', [], ai # ais @ asx') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
with \<open>asx = ai#ais\<close> \<open>a'#as' = asx@asx'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = ai # ais
a' # as' = asx @ asx'
as = a' # as'
(V', [], ai # ais @ asx') \<in> dependent_live_vars n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
asx = ai # ais
a' # as' = asx @ asx'
as = a' # as'
(V', [], ai # ais @ asx') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. (V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(V', [], as) \<in> dependent_live_vars n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(V', [], as) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with all
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', [], as) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (1 subgoal):
 1. \<And>V n'' asx asx'. \<lbrakk>n -{V}asx\<rightarrow>\<^sub>d\<^sub>d n''; n'' -asx'\<rightarrow>\<^sub>d* n'; a' # as' = asx @ asx'\<rbrakk> \<Longrightarrow> pred ex s
[PROOF STEP]
with \<open>pred ex' s'\<close> \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
pred ex' s'
valid_edge a'
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred ex' s'
valid_edge a'
?V'2 \<in> Use n \<Longrightarrow> state_val s ?V'2 = state_val s' ?V'2

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(fastforce elim:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred ex s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pred ex s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pred ex s

goal (1 subgoal):
 1. \<And>x1. ex = \<Up>x1 \<Longrightarrow> pred ex s
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
pred ex s

goal (2 subgoals):
 1. \<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with all' \<open>preds esx (transfer ex s)\<close> \<open>es = ex#esx\<close> \<open>es' = ex'#esx'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V
preds esx (transfer ex s)
es = ex # esx
es' = ex' # esx'
pred ex s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>Use n'. state_val (transfers esx (transfer ex s)) V = state_val (transfers esx' (transfer ex' s')) V
preds esx (transfer ex s)
es = ex # esx
es' = ex' # esx'
pred ex s

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V)

goal (1 subgoal):
 1. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V)
[PROOF STEP]
obtain V' xs' where "(V',xs',as') \<in> dependent_live_vars n'"
        and "state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V)

goal (1 subgoal):
 1. (\<And>V' xs'. \<lbrakk>(V', xs', as') \<in> dependent_live_vars n'; state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(V', xs', as') \<in> dependent_live_vars n'
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'

goal (1 subgoal):
 1. \<not> (\<forall>V xs. (V, xs, as') \<in> dependent_live_vars n' \<longrightarrow> state_val (transfer ex s) V = state_val (transfer ex' s') V) \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases "n -a'#as'\<rightarrow>\<^sub>d* n'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close> \<open>last(targetnodes as) = n'\<close> ex
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have [simp]:"ex = kind a'"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. ex = kind a'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
ex = kind a'

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>x \<longrightarrow> y\<close> ex ex'
[PROOF STATE]
proof (chain)
picking this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = kind a'
[PROOF STEP]
have [simp]:"ex' = ex"
[PROOF STATE]
proof (prove)
using this:
x \<longrightarrow> y
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex = kind a'

goal (1 subgoal):
 1. ex' = ex
[PROOF STEP]
by(cases x) auto
[PROOF STATE]
proof (state)
this:
ex' = ex

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ex' = ex

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V \<in> Use (sourcenode a')"
[PROOF STATE]
proof (state)
this:
V \<in> Use (sourcenode a')

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "(V,[],[]) \<in> dependent_live_vars (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use (sourcenode a')

goal (1 subgoal):
 1. (V, [], []) \<in> dependent_live_vars (sourcenode a')
[PROOF STEP]
by(rule dep_vars_Use)
[PROOF STATE]
proof (state)
this:
(V, [], []) \<in> dependent_live_vars (sourcenode a')

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>n -a'#as'\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a' # as'\<rightarrow>\<^sub>d* n'
(V, [], []) \<in> dependent_live_vars (sourcenode a')
[PROOF STEP]
have "(V,[],[]@a'#as') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
n -a' # as'\<rightarrow>\<^sub>d* n'
(V, [], []) \<in> dependent_live_vars (sourcenode a')

goal (1 subgoal):
 1. (V, [], [] @ a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dependent_live_vars_dep_dependent_live_vars)
[PROOF STATE]
proof (state)
this:
(V, [], [] @ a' # as') \<in> dependent_live_vars n'

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with all \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [], [] @ a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V = state_val s' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
as = a' # as'
(V, [], [] @ a' # as') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V = state_val s' V
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
state_val s V = state_val s' V

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use (sourcenode a') \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>pred ex' s'\<close> \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
pred ex' s'
valid_edge a'
?V2 \<in> Use (sourcenode a') \<Longrightarrow> state_val s ?V2 = state_val s' ?V2
[PROOF STEP]
have "pred ex s"
[PROOF STATE]
proof (prove)
using this:
pred ex' s'
valid_edge a'
?V2 \<in> Use (sourcenode a') \<Longrightarrow> state_val s ?V2 = state_val s' ?V2

goal (1 subgoal):
 1. pred ex s
[PROOF STEP]
by(fastforce intro:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred ex s

goal (2 subgoals):
 1. n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
proof(cases "V' \<in> Def n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
V' \<in> Def n

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'\<close>
            \<open>valid_edge a'\<close> \<open>pred ex' s'\<close> \<open>pred ex s\<close>
            CFG_edge_transfer_uses_only_Use[of a' s s']
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
valid_edge a'
pred ex' s'
pred ex s
\<lbrakk>valid_edge a'; \<forall>V\<in>Use (sourcenode a'). state_val s V = state_val s' V; pred (kind a') s; pred (kind a') s'\<rbrakk> \<Longrightarrow> \<forall>V\<in>Def (sourcenode a'). state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V
V' \<in> Def n
[PROOF STEP]
obtain V'' where "V'' \<in> Use n"
            and "state_val s V'' \<noteq> state_val s' V''"
[PROOF STATE]
proof (prove)
using this:
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
valid_edge a'
pred ex' s'
pred ex s
\<lbrakk>valid_edge a'; \<forall>V\<in>Use (sourcenode a'). state_val s V = state_val s' V; pred (kind a') s; pred (kind a') s'\<rbrakk> \<Longrightarrow> \<forall>V\<in>Def (sourcenode a'). state_val (transfer (kind a') s) V = state_val (transfer (kind a') s') V
V' \<in> Def n

goal (1 subgoal):
 1. (\<And>V''. \<lbrakk>V'' \<in> Use n; state_val s V'' \<noteq> state_val s' V''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V'' \<in> Use n
state_val s V'' \<noteq> state_val s' V''

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from True \<open>(V',xs',as') \<in> dependent_live_vars n'\<close>
            \<open>targetnode a' -as'\<rightarrow>* n'\<close> \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
            \<open>valid_edge a'\<close> \<open>n = sourcenode a'\<close>[THEN sym]
[PROOF STATE]
proof (chain)
picking this:
V' \<in> Def n
(V', xs', as') \<in> dependent_live_vars n'
targetnode a' -as'\<rightarrow>* n'
last (targetnodes as) = n'
as = a' # as'
valid_edge a'
sourcenode a' = n
[PROOF STEP]
have "n -{V'}a'#xs'\<rightarrow>\<^sub>d\<^sub>d last(targetnodes (a'#xs'))"
[PROOF STATE]
proof (prove)
using this:
V' \<in> Def n
(V', xs', as') \<in> dependent_live_vars n'
targetnode a' -as'\<rightarrow>* n'
last (targetnodes as) = n'
as = a' # as'
valid_edge a'
sourcenode a' = n

goal (1 subgoal):
 1. n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
by -(drule dependent_live_vars_dependent_edge,
              auto dest!: dependent_live_vars_dependent_edge
                   dest:DynPDG_ddep_edge_CFG_path path_targetnode
                   simp del:\<open>n = sourcenode a'\<close>)
[PROOF STATE]
proof (state)
this:
n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>(V',xs',as') \<in> dependent_live_vars n'\<close> \<open>V'' \<in> Use n\<close>
            \<open>last(targetnodes as) = n'\<close> \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
(V', xs', as') \<in> dependent_live_vars n'
V'' \<in> Use n
last (targetnodes as) = n'
as = a' # as'
n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
have "(V'',[],as) \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
(V', xs', as') \<in> dependent_live_vars n'
V'' \<in> Use n
last (targetnodes as) = n'
as = a' # as'
n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (1 subgoal):
 1. (V'', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_ddep)
[PROOF STATE]
proof (state)
this:
(V'', [], as) \<in> dependent_live_vars n'

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with all
[PROOF STATE]
proof (chain)
picking this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V'', [], as) \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V'' = state_val s' V''"
[PROOF STATE]
proof (prove)
using this:
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V'', [], as) \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V'' = state_val s' V''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_val s V'' = state_val s' V''

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>state_val s V'' \<noteq> state_val s' V''\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val s V'' \<noteq> state_val s' V''
state_val s V'' = state_val s' V''
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
state_val s V'' \<noteq> state_val s' V''
state_val s V'' = state_val s' V''

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

goal (2 subgoals):
 1. V' \<in> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
V' \<notin> Def n

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>pred ex s\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
pred ex s
V' \<notin> Def n
[PROOF STEP]
have "state_val (transfer (kind a') s) V' = state_val s V'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
pred ex s
V' \<notin> Def n

goal (1 subgoal):
 1. state_val (transfer (kind a') s) V' = state_val s V'
[PROOF STEP]
by(fastforce intro:CFG_edge_no_Def_equal)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') s) V' = state_val s V'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') s) V' = state_val s V'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from False \<open>valid_edge a'\<close> \<open>pred ex' s'\<close>
[PROOF STATE]
proof (chain)
picking this:
V' \<notin> Def n
valid_edge a'
pred ex' s'
[PROOF STEP]
have "state_val (transfer (kind a') s') V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
V' \<notin> Def n
valid_edge a'
pred ex' s'

goal (1 subgoal):
 1. state_val (transfer (kind a') s') V' = state_val s' V'
[PROOF STEP]
by(fastforce intro:CFG_edge_no_Def_equal)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') s') V' = state_val s' V'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer (kind a') s) V' = state_val s V'
state_val (transfer (kind a') s') V' = state_val s' V'
[PROOF STEP]
have "state_val s V' \<noteq> state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a') s) V' = state_val s V'
state_val (transfer (kind a') s') V' = state_val s' V'

goal (1 subgoal):
 1. state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
using \<open>state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'\<close>
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a') s) V' = state_val s V'
state_val (transfer (kind a') s') V' = state_val s' V'
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'

goal (1 subgoal):
 1. state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_val s V' \<noteq> state_val s' V'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
V' \<notin> Def n
[PROOF STEP]
have "\<not> n -{V'}a'#xs'\<rightarrow>\<^sub>d\<^sub>d
                           last(targetnodes (a'#xs'))"
[PROOF STATE]
proof (prove)
using this:
V' \<notin> Def n

goal (1 subgoal):
 1. \<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>(V',xs',as') \<in> dependent_live_vars n'\<close> \<open>last(targetnodes as) = n'\<close>
            \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
(V', xs', as') \<in> dependent_live_vars n'
last (targetnodes as) = n'
as = a' # as'
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
have "(V',a'#xs',a'#as') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
(V', xs', as') \<in> dependent_live_vars n'
last (targetnodes as) = n'
as = a' # as'
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (1 subgoal):
 1. (V', a' # xs', a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_keep)
[PROOF STATE]
proof (state)
this:
(V', a' # xs', a' # as') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>as = a'#as'\<close> all
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', a' # xs', a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', a' # xs', a' # as') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>state_val s V' \<noteq> state_val s' V'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val s V' \<noteq> state_val s' V'
state_val s V' = state_val s' V'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
state_val s V' \<noteq> state_val s' V'
state_val s V' = state_val s' V'

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

goal (1 subgoal):
 1. V' \<notin> Def n \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
assume "V' \<in> Def n"
[PROOF STATE]
proof (state)
this:
V' \<in> Def n

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>(V',xs',as') \<in> dependent_live_vars n'\<close> \<open>targetnode a' -as'\<rightarrow>* n'\<close>
            \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
(V', xs', as') \<in> dependent_live_vars n'
targetnode a' -as'\<rightarrow>* n'
valid_edge a'
V' \<in> Def n
[PROOF STEP]
have "n -a'#as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
(V', xs', as') \<in> dependent_live_vars n'
targetnode a' -as'\<rightarrow>* n'
valid_edge a'
V' \<in> Def n

goal (1 subgoal):
 1. n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by -(drule dependent_live_vars_dependent_edge,
              auto dest:DynPDG_path_ddep DynPDG_path_Append)
[PROOF STATE]
proof (state)
this:
n -a' # as'\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'
n -a' # as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'
n -a' # as'\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
V' \<in> Def n \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
hence "V' \<notin> Def (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
V' \<in> Def n \<Longrightarrow> False

goal (1 subgoal):
 1. V' \<notin> Def (sourcenode a')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
V' \<notin> Def (sourcenode a')

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from False \<open>slice_path as = x#xs\<close> \<open>as = a'#as'\<close>
          \<open>last(targetnodes as) = n'\<close> \<open>as' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
as' \<noteq> []
[PROOF STEP]
have "\<not> x"
[PROOF STATE]
proof (prove)
using this:
\<not> n -a' # as'\<rightarrow>\<^sub>d* n'
slice_path as = x # xs
as = a' # as'
last (targetnodes as) = n'
as' \<noteq> []

goal (1 subgoal):
 1. \<not> x
[PROOF STEP]
by(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
\<not> x

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with ex
[PROOF STATE]
proof (chain)
picking this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> x
[PROOF STEP]
have cases:"ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)"
[PROOF STATE]
proof (prove)
using this:
ex = (if x then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> x

goal (1 subgoal):
 1. ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
have "state_val s V' \<noteq> state_val s' V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
proof(cases y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
 2. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y

goal (2 subgoals):
 1. y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
 2. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
with ex'
[PROOF STATE]
proof (chain)
picking this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
y
[PROOF STEP]
have [simp]:"ex' = kind a'"
[PROOF STATE]
proof (prove)
using this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
y

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

goal (2 subgoals):
 1. y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
 2. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
from \<open>V' \<notin> Def (sourcenode a')\<close> \<open>valid_edge a'\<close> \<open>pred ex' s'\<close>
[PROOF STATE]
proof (chain)
picking this:
V' \<notin> Def (sourcenode a')
valid_edge a'
pred ex' s'
[PROOF STEP]
have states_eq:"state_val (transfer (kind a') s') V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
V' \<notin> Def (sourcenode a')
valid_edge a'
pred ex' s'

goal (1 subgoal):
 1. state_val (transfer (kind a') s') V' = state_val s' V'
[PROOF STEP]
by(fastforce intro:CFG_edge_no_Def_equal)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') s') V' = state_val s' V'

goal (2 subgoals):
 1. y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
 2. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
from cases
[PROOF STATE]
proof (chain)
picking this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
have "state_val s V' = state_val (transfer ex s) V'"
[PROOF STATE]
proof (prove)
using this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. state_val s V' = state_val (transfer ex s) V'
[PROOF STEP]
by(cases "kind a'") auto
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val (transfer ex s) V'

goal (2 subgoals):
 1. y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
 2. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
with states_eq
            \<open>state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer (kind a') s') V' = state_val s' V'
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
state_val s V' = state_val (transfer ex s) V'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a') s') V' = state_val s' V'
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
state_val s V' = state_val (transfer ex s) V'

goal (1 subgoal):
 1. state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_val s V' \<noteq> state_val s' V'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
with ex'
[PROOF STATE]
proof (chain)
picking this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> y
[PROOF STEP]
have "ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)"
[PROOF STATE]
proof (prove)
using this:
ex' = (if y then kind a' else case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
\<not> y

goal (1 subgoal):
 1. ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
with cases
[PROOF STATE]
proof (chain)
picking this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
[PROOF STEP]
have "state_val s V' = state_val (transfer ex s) V'"
            and "state_val s' V' = state_val (transfer ex' s') V'"
[PROOF STATE]
proof (prove)
using this:
ex = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)
ex' = (case kind a' of \<Up>f \<Rightarrow> \<Up>id | (Q)\<^sub>\<surd> \<Rightarrow> (\<lambda>s. True)\<^sub>\<surd>)

goal (1 subgoal):
 1. state_val s V' = state_val (transfer ex s) V' &&& state_val s' V' = state_val (transfer ex' s') V'
[PROOF STEP]
by(cases "kind a'",auto)+
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val (transfer ex s) V'
state_val s' V' = state_val (transfer ex' s') V'

goal (1 subgoal):
 1. \<not> y \<Longrightarrow> state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
with \<open>state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
state_val s V' = state_val (transfer ex s) V'
state_val s' V' = state_val (transfer ex' s') V'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfer ex s) V' \<noteq> state_val (transfer ex' s') V'
state_val s V' = state_val (transfer ex s) V'
state_val s' V' = state_val (transfer ex' s') V'

goal (1 subgoal):
 1. state_val s V' \<noteq> state_val s' V'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_val s V' \<noteq> state_val s' V'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
state_val s V' \<noteq> state_val s' V'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
from \<open>V' \<notin> Def (sourcenode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
V' \<notin> Def (sourcenode a')
[PROOF STEP]
have "\<not> n -{V'}a'#xs'\<rightarrow>\<^sub>d\<^sub>d last(targetnodes (a'#xs'))"
[PROOF STATE]
proof (prove)
using this:
V' \<notin> Def (sourcenode a')

goal (1 subgoal):
 1. \<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>(V',xs',as') \<in> dependent_live_vars n'\<close> \<open>last(targetnodes as) = n'\<close>
          \<open>as = a'#as'\<close>
[PROOF STATE]
proof (chain)
picking this:
(V', xs', as') \<in> dependent_live_vars n'
last (targetnodes as) = n'
as = a' # as'
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))
[PROOF STEP]
have "(V',a'#xs',a'#as') \<in> dependent_live_vars n'"
[PROOF STATE]
proof (prove)
using this:
(V', xs', as') \<in> dependent_live_vars n'
last (targetnodes as) = n'
as = a' # as'
\<not> n -{V'}a' # xs'\<rightarrow>\<^sub>d\<^sub>d last (targetnodes (a' # xs'))

goal (1 subgoal):
 1. (V', a' # xs', a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
by(fastforce intro:dep_vars_Cons_keep)
[PROOF STATE]
proof (state)
this:
(V', a' # xs', a' # as') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>as = a'#as'\<close> all
[PROOF STATE]
proof (chain)
picking this:
as = a' # as'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', a' # xs', a' # as') \<in> dependent_live_vars n'
[PROOF STEP]
have "state_val s V' = state_val s' V'"
[PROOF STATE]
proof (prove)
using this:
as = a' # as'
\<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V
(V', a' # xs', a' # as') \<in> dependent_live_vars n'

goal (1 subgoal):
 1. state_val s V' = state_val s' V'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_val s V' = state_val s' V'

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
with \<open>state_val s V' \<noteq> state_val s' V'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val s V' \<noteq> state_val s' V'
state_val s V' = state_val s' V'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
state_val s V' \<noteq> state_val s' V'
state_val s V' = state_val s' V'

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

goal (1 subgoal):
 1. \<not> n -a' # as'\<rightarrow>\<^sub>d* n' \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s

goal (2 subgoals):
 1. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; v # va \<preceq>\<^sub>b []; slice_path as = v # va; select_edge_kinds as (v # va) = es; select_edge_kinds as [] = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
 2. \<And>v va as es es' n s s'. \<lbrakk>n -as\<rightarrow>* n'; [] \<preceq>\<^sub>b v # va; slice_path as = []; select_edge_kinds as [] = es; select_edge_kinds as (v # va) = es'; \<forall>V xs. (V, xs, as) \<in> dependent_live_vars n' \<longrightarrow> state_val s V = state_val s' V; preds es' s'\<rbrakk> \<Longrightarrow> (\<forall>V\<in>Use n'. state_val (transfers es s) V = state_val (transfers es' s') V) \<and> preds es s
[PROOF STEP]
qed simp_all