[STATEMENT]
lemma CFG_call_edge_param_in:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "i < length ins"
  and "(p,ins,outs) \<in> set procs" and "pred (kind a) s" and "pred (kind a) s'"
  and "\<forall>V \<in> (ParamUses (sourcenode a))!i. state_val s V = state_val s' V"
  shows "state_val (transfer (kind a) s) (ins!i) =
         state_val (transfer (kind a) s') (ins!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
i < length ins
(p, ins, outs) \<in> set procs
pred (kind a) s
pred (kind a) s'
\<forall>V\<in>ParamUses (sourcenode a) ! i. state_val s V = state_val s' V
[PROOF STEP]
have params:"(params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
i < length ins
(p, ins, outs) \<in> set procs
pred (kind a) s
pred (kind a) s'
\<forall>V\<in>ParamUses (sourcenode a) ! i. state_val s V = state_val s' V

goal (1 subgoal):
 1. params fs (state_val s) ! i = params fs (state_val s') ! i
[PROOF STEP]
by(rule CFG_call_edge_params)
[PROOF STATE]
proof (state)
this:
params fs (state_val s) ! i = params fs (state_val s') ! i

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
[PROOF STEP]
have [simp]:"(THE ins. \<exists>outs. (p,ins,outs) \<in> set procs) = ins"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. (THE ins. \<exists>outs. (p, ins, outs) \<in> set procs) = ins
[PROOF STEP]
by(rule formal_in_THE)
[PROOF STATE]
proof (state)
this:
(THE ins. \<exists>outs. (p, ins, outs) \<in> set procs) = ins

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>pred (kind a) s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (kind a) s
[PROOF STEP]
obtain cf cfs where [simp]:"s = cf#cfs"
[PROOF STATE]
proof (prove)
using this:
pred (kind a) s

goal (1 subgoal):
 1. (\<And>cf cfs. s = cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s) auto
[PROOF STATE]
proof (state)
this:
s = cf # cfs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>pred (kind a) s'\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (kind a) s'
[PROOF STEP]
obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
[PROOF STATE]
proof (prove)
using this:
pred (kind a) s'

goal (1 subgoal):
 1. (\<And>cf' cfs'. s' = cf' # cfs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s') auto
[PROOF STATE]
proof (state)
this:
s' = cf' # cfs'

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have eqs:"fst (hd (transfer (kind a) s)) = (Map.empty(ins [:=] params fs (fst cf)))"
    "fst (hd (transfer (kind a) s')) = (Map.empty(ins [:=] params fs (fst cf')))"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) = Map.empty(ins [:=] params fs (fst cf)) &&& state_val (transfer (kind a) s') = Map.empty(ins [:=] params fs (fst cf'))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a) s) = Map.empty(ins [:=] params fs (fst cf))
state_val (transfer (kind a) s') = Map.empty(ins [:=] params fs (fst cf'))

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "length fs = length ins"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. length fs = length ins
[PROOF STEP]
by(rule CFG_call_edge_length)
[PROOF STATE]
proof (state)
this:
length fs = length ins

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
from \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "distinct ins"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. distinct ins
[PROOF STEP]
by(rule distinct_formal_ins)
[PROOF STATE]
proof (state)
this:
distinct ins

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
with \<open>i < length ins\<close> \<open>length fs = length ins\<close>
[PROOF STATE]
proof (chain)
picking this:
i < length ins
length fs = length ins
distinct ins
[PROOF STEP]
have "(Map.empty(ins [:=] params fs (fst cf))) (ins!i) = (params fs (fst cf))!i"
    "(Map.empty(ins [:=] params fs (fst cf'))) (ins!i) = (params fs (fst cf'))!i"
[PROOF STATE]
proof (prove)
using this:
i < length ins
length fs = length ins
distinct ins

goal (1 subgoal):
 1. Map.empty(ins [:=] params fs (fst cf)) (ins ! i) = params fs (fst cf) ! i &&& Map.empty(ins [:=] params fs (fst cf')) (ins ! i) = params fs (fst cf') ! i
[PROOF STEP]
by(fastforce intro:fun_upds_nth)+
[PROOF STATE]
proof (state)
this:
Map.empty(ins [:=] params fs (fst cf)) (ins ! i) = params fs (fst cf) ! i
Map.empty(ins [:=] params fs (fst cf')) (ins ! i) = params fs (fst cf') ! i

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ins ! i) = state_val (transfer (kind a) s') (ins ! i)
[PROOF STEP]
with eqs \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> params
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer (kind a) s) = Map.empty(ins [:=] params fs (fst cf))
state_val (transfer (kind a) s') = Map.empty(ins [:=] params fs (fst cf'))
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
params fs (state_val s) ! i = params fs (state_val s') ! i
Map.empty(ins [:=] params fs (fst cf)) (ins ! i) = params fs (fst cf) ! i
Map.empty(ins [:=] params fs (fst cf')) (ins ! i) = params fs (fst cf') ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a) s) = Map.empty(ins [:=] params fs (fst cf))
state_val (transfer (kind a) s') = Map.empty(ins [:=] params fs (fst cf'))
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
params fs (state_val s) ! i = params fs (state_val s') ! i
Map.empty(ins [:=] params fs (fst cf)) (ins ! i) = params fs (fst cf) ! i
Map.empty(ins [:=] params fs (fst cf')) (ins ! i) = params fs (fst cf') ! i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CFG_call_edge_no_param:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "V \<notin> set ins"
  and "(p,ins,outs) \<in> set procs" and "pred (kind a) s"
  shows "state_val (transfer (kind a) s) V = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) V = None
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) V = None
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
[PROOF STEP]
have [simp]:"(THE ins. \<exists>outs. (p,ins,outs) \<in> set procs) = ins"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. (THE ins. \<exists>outs. (p, ins, outs) \<in> set procs) = ins
[PROOF STEP]
by(rule formal_in_THE)
[PROOF STATE]
proof (state)
this:
(THE ins. \<exists>outs. (p, ins, outs) \<in> set procs) = ins

goal (1 subgoal):
 1. state_val (transfer (kind a) s) V = None
[PROOF STEP]
from \<open>pred (kind a) s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (kind a) s
[PROOF STEP]
obtain cf cfs where [simp]:"s = cf#cfs"
[PROOF STATE]
proof (prove)
using this:
pred (kind a) s

goal (1 subgoal):
 1. (\<And>cf cfs. s = cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s) auto
[PROOF STATE]
proof (state)
this:
s = cf # cfs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) V = None
[PROOF STEP]
from \<open>V \<notin> set ins\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<notin> set ins
[PROOF STEP]
have "(Map.empty(ins [:=] params fs (fst cf))) V = None"
[PROOF STATE]
proof (prove)
using this:
V \<notin> set ins

goal (1 subgoal):
 1. Map.empty(ins [:=] params fs (fst cf)) V = None
[PROOF STEP]
by(auto dest:fun_upds_notin)
[PROOF STATE]
proof (state)
this:
Map.empty(ins [:=] params fs (fst cf)) V = None

goal (1 subgoal):
 1. state_val (transfer (kind a) s) V = None
[PROOF STEP]
with \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
Map.empty(ins [:=] params fs (fst cf)) V = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
Map.empty(ins [:=] params fs (fst cf)) V = None

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CFG_return_edge_param_out:
  assumes "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f" and "i < length outs"
  and "(p,ins,outs) \<in> set procs" and "state_val s (outs!i) = state_val s' (outs!i)"
  and "s = cf#cfx#cfs" and "s' = cf'#cfx'#cfs'"
  shows "state_val (transfer (kind a) s) ((ParamDefs (targetnode a))!i) =
         state_val (transfer (kind a) s') ((ParamDefs (targetnode a))!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
[PROOF STEP]
have [simp]:"(THE outs. \<exists>ins. (p,ins,outs) \<in> set procs) = outs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. (THE outs. \<exists>ins. (p, ins, outs) \<in> set procs) = outs
[PROOF STEP]
by(rule formal_out_THE)
[PROOF STATE]
proof (state)
this:
(THE outs. \<exists>ins. (p, ins, outs) \<in> set procs) = outs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close> \<open>s = cf#cfx#cfs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
s = cf # cfx # cfs
[PROOF STEP]
have transfer:"fst (hd (transfer (kind a) s)) =
    (fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
s = cf # cfx # cfs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) = fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs)
[PROOF STEP]
by(fastforce intro:CFG_return_edge_fun)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a) s) = fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs)

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close> \<open>s' = cf'#cfx'#cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
s' = cf' # cfx' # cfs'
[PROOF STEP]
have transfer':"fst (hd (transfer (kind a) s')) =
    (fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
s' = cf' # cfx' # cfs'

goal (1 subgoal):
 1. state_val (transfer (kind a) s') = fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs)
[PROOF STEP]
by(fastforce intro:CFG_return_edge_fun)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a) s') = fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs)

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>state_val s (outs!i) = state_val s' (outs!i)\<close> \<open>i < length outs\<close>
    \<open>s = cf#cfx#cfs\<close> \<open>s' = cf'#cfx'#cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val s (outs ! i) = state_val s' (outs ! i)
i < length outs
s = cf # cfx # cfs
s' = cf' # cfx' # cfs'
[PROOF STEP]
have "(fst cf) (outs!i) = (fst cf') (outs!i)"
[PROOF STATE]
proof (prove)
using this:
state_val s (outs ! i) = state_val s' (outs ! i)
i < length outs
s = cf # cfx # cfs
s' = cf' # cfx' # cfs'

goal (1 subgoal):
 1. fst cf (outs ! i) = fst cf' (outs ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst cf (outs ! i) = fst cf' (outs ! i)

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
have "distinct (ParamDefs (targetnode a))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

goal (1 subgoal):
 1. distinct (ParamDefs (targetnode a))
[PROOF STEP]
by(fastforce intro:distinct_ParamDefs)
[PROOF STATE]
proof (state)
this:
distinct (ParamDefs (targetnode a))

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "length(ParamDefs (targetnode a)) = length outs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. length (ParamDefs (targetnode a)) = length outs
[PROOF STEP]
by(fastforce intro:ParamDefs_return_target_length)
[PROOF STATE]
proof (state)
this:
length (ParamDefs (targetnode a)) = length outs

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
with \<open>i < length outs\<close> \<open>distinct (ParamDefs (targetnode a))\<close>
[PROOF STATE]
proof (chain)
picking this:
i < length outs
distinct (ParamDefs (targetnode a))
length (ParamDefs (targetnode a)) = length outs
[PROOF STEP]
have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)
    ((ParamDefs (targetnode a))!i) = (map (fst cf) outs)!i"
    and "(fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)
             ((ParamDefs (targetnode a))!i) = (map (fst cf') outs)!i"
[PROOF STATE]
proof (prove)
using this:
i < length outs
distinct (ParamDefs (targetnode a))
length (ParamDefs (targetnode a)) = length outs

goal (1 subgoal):
 1. fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs) (ParamDefs (targetnode a) ! i) = map (fst cf) outs ! i &&& fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs) (ParamDefs (targetnode a) ! i) = map (fst cf') outs ! i
[PROOF STEP]
by(fastforce intro:fun_upds_nth)+
[PROOF STATE]
proof (state)
this:
fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs) (ParamDefs (targetnode a) ! i) = map (fst cf) outs ! i
fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs) (ParamDefs (targetnode a) ! i) = map (fst cf') outs ! i

goal (1 subgoal):
 1. state_val (transfer (kind a) s) (ParamDefs (targetnode a) ! i) = state_val (transfer (kind a) s') (ParamDefs (targetnode a) ! i)
[PROOF STEP]
with transfer transfer' \<open>(fst cf) (outs!i) = (fst cf') (outs!i)\<close> \<open>i < length outs\<close>
[PROOF STATE]
proof (chain)
picking this:
state_val (transfer (kind a) s) = fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs)
state_val (transfer (kind a) s') = fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs)
fst cf (outs ! i) = fst cf' (outs ! i)
i < length outs
fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs) (ParamDefs (targetnode a) ! i) = map (fst cf) outs ! i
fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs) (ParamDefs (targetnode a) ! i) = map (fst cf') outs ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfer (kind a) s) = fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs)
state_val (transfer (kind a) s') = fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs)
fst cf (outs ! i) = fst cf' (outs ! i)
i < length outs
fst cfx(ParamDefs (targetnode a) [:=] map (fst cf) outs) (ParamDefs (targetnode a) ! i) = map (fst cf) outs ! i
fst cfx'(ParamDefs (targetnode a) [:=] map (fst cf') outs) (ParamDefs (targetnode a) ! i) = map (fst cf') outs ! i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CFG_slp_no_Def_equal:
  assumes "n -as\<rightarrow>\<^bsub>sl\<^esub>* n'" and "valid_edge a" and "a' \<in> get_return_edges a"
  and "V \<notin> set (ParamDefs (targetnode a'))" and "preds (kinds (a#as@[a'])) s"
  shows "state_val (transfers (kinds (a#as@[a'])) s) V = state_val s V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q r p fs where "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:only_call_get_return_edges)
[PROOF STATE]
proof (state)
this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>Q' f'. kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge a'

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>preds (kinds (a#as@[a'])) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds (a # as @ [a'])) s
[PROOF STEP]
obtain cf cfs where [simp]:"s = cf#cfs"
[PROOF STATE]
proof (prove)
using this:
preds (kinds (a # as @ [a'])) s

goal (1 subgoal):
 1. (\<And>cf cfs. s = cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s,auto simp:kinds_def)
[PROOF STATE]
proof (state)
this:
s = cf # cfs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain ins outs
    where "(p,ins,outs) \<in> set procs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>ins outs. (p, ins, outs) \<in> set procs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:callee_in_procs)
[PROOF STATE]
proof (state)
this:
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain cfx where "transfer (kind a) s = cfx#cf#cfs"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>cfx. transfer (kind a) s = cfx # cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = cfx # cf # cfs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = cfx # cf # cfs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^bsub>sl\<^esub>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'
[PROOF STEP]
obtain cfx'
    where "transfers (kinds as) (cfx#cf#cfs) = cfx'#cf#cfs"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'

goal (1 subgoal):
 1. (\<And>cfx'. transfers (kinds as) (cfx # cf # cfs) = cfx' # cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:slp_callstack_length_equal)
[PROOF STATE]
proof (state)
this:
transfers (kinds as) (cfx # cf # cfs) = cfx' # cf # cfs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
transfers (kinds as) (cfx # cf # cfs) = cfx' # cf # cfs

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
from \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>valid_edge a'\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
valid_edge a'
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "fst (hd (transfer (kind a') (cfx'#cf#cfs))) =
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
[PROOF STATE]
proof (prove)
using this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
valid_edge a'
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. state_val (transfer (kind a') (cfx' # cf # cfs)) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)
[PROOF STEP]
by(simp,simp only:formal_out_THE,fastforce intro:CFG_return_edge_fun)
[PROOF STATE]
proof (state)
this:
state_val (transfer (kind a') (cfx' # cf # cfs)) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
transfer (kind a) s = cfx # cf # cfs
transfers (kinds as) (cfx # cf # cfs) = cfx' # cf # cfs
state_val (transfer (kind a') (cfx' # cf # cfs)) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)
[PROOF STEP]
have "fst (hd (transfers (kinds (a#as@[a'])) s)) =
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
[PROOF STATE]
proof (prove)
using this:
transfer (kind a) s = cfx # cf # cfs
transfers (kinds as) (cfx # cf # cfs) = cfx' # cf # cfs
state_val (transfer (kind a') (cfx' # cf # cfs)) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)
[PROOF STEP]
by(simp add:kinds_def transfers_split)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds (a # as @ [a'])) s) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
with \<open>V \<notin> set (ParamDefs (targetnode a'))\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<notin> set (ParamDefs (targetnode a'))
state_val (transfers (kinds (a # as @ [a'])) s) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V \<notin> set (ParamDefs (targetnode a'))
state_val (transfers (kinds (a # as @ [a'])) s) = fst cf(ParamDefs (targetnode a') [:=] map (fst cfx') outs)

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V
[PROOF STEP]
by(simp add:fun_upds_notin)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds (a # as @ [a'])) s) V = state_val s V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [dest!]: "V \<in> Use (_Entry_) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Use (_Entry_) \<Longrightarrow> False
[PROOF STEP]
by(simp add:Entry_empty)


[STATEMENT]
lemma [dest!]: "V \<in> Def (_Entry_) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Def (_Entry_) \<Longrightarrow> False
[PROOF STEP]
by(simp add:Entry_empty)


[STATEMENT]
lemma CFG_intra_path_no_Def_equal:
  assumes "n -as\<rightarrow>\<^sub>\<iota>* n'" and "\<forall>n \<in> set (sourcenodes as). V \<notin> Def n"
  and "preds (kinds as) s"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -as\<rightarrow>* n'" and "\<forall>a \<in> set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by(simp_all add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
from this \<open>\<forall>n \<in> set (sourcenodes as). V \<notin> Def n\<close> \<open>preds (kinds as) s\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n
preds (kinds as) s
[PROOF STEP]
have "state_val (transfers (kinds as) s) V = state_val s V"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
\<forall>a\<in>set as. intra_kind (kind a)
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n
preds (kinds as) s

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
proof(induct arbitrary:s rule:path.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n s. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n\<in>set (sourcenodes []). V \<notin> Def n; preds (kinds []) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds []) s) V = state_val s V
 2. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
case (empty_path n)
[PROOF STATE]
proof (state)
this:
valid_node n
\<forall>a\<in>set []. intra_kind (kind a)
\<forall>n\<in>set (sourcenodes []). V \<notin> Def n
preds (kinds []) s

goal (2 subgoals):
 1. \<And>n s. \<lbrakk>valid_node n; \<forall>a\<in>set []. intra_kind (kind a); \<forall>n\<in>set (sourcenodes []). V \<notin> Def n; preds (kinds []) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds []) s) V = state_val s V
 2. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node n
\<forall>a\<in>set []. intra_kind (kind a)
\<forall>n\<in>set (sourcenodes []). V \<notin> Def n
preds (kinds []) s

goal (1 subgoal):
 1. state_val (transfers (kinds []) s) V = state_val s V
[PROOF STEP]
by(simp add:sourcenodes_def kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds []) s) V = state_val s V

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
case (Cons_path n'' as n' a n)
[PROOF STATE]
proof (state)
this:
n'' -as\<rightarrow>* n'
\<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) ?s) V = state_val ?s V
valid_edge a
sourcenode a = n
targetnode a = n''
\<forall>a\<in>set (a # as). intra_kind (kind a)
\<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n
preds (kinds (a # as)) s

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
note IH = \<open>\<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a);
                    \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk>
      \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) ?s) V = state_val ?s V

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
from \<open>preds (kinds (a#as)) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds (a # as)) s
[PROOF STEP]
have "pred (kind a) s"
      and "preds (kinds as) (transfer (kind a) s)"
[PROOF STATE]
proof (prove)
using this:
preds (kinds (a # as)) s

goal (1 subgoal):
 1. pred (kind a) s &&& preds (kinds as) (transfer (kind a) s)
[PROOF STEP]
by(simp_all add:kinds_def)
[PROOF STATE]
proof (state)
this:
pred (kind a) s
preds (kinds as) (transfer (kind a) s)

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
from \<open>\<forall>n\<in>set (sourcenodes (a#as)). V \<notin> Def n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n
[PROOF STEP]
have noDef:"V \<notin> Def (sourcenode a)"
      and all:"\<forall>n\<in>set (sourcenodes as). V \<notin> Def n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n

goal (1 subgoal):
 1. V \<notin> Def (sourcenode a) &&& \<forall>n\<in>set (sourcenodes as). V \<notin> Def n
[PROOF STEP]
by(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
V \<notin> Def (sourcenode a)
\<forall>n\<in>set (sourcenodes as). V \<notin> Def n

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
from \<open>\<forall>a\<in>set (a#as). intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). intra_kind (kind a)
[PROOF STEP]
have "intra_kind (kind a)" and all':"\<forall>a\<in>set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). intra_kind (kind a)

goal (1 subgoal):
 1. intra_kind (kind a) &&& \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
intra_kind (kind a)
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
from \<open>valid_edge a\<close> noDef \<open>intra_kind (kind a)\<close> \<open>pred (kind a) s\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
V \<notin> Def (sourcenode a)
intra_kind (kind a)
pred (kind a) s
[PROOF STEP]
have "state_val (transfer (kind a) s) V = state_val s V"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
V \<notin> Def (sourcenode a)
intra_kind (kind a)
pred (kind a) s

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

goal (1 subgoal):
 1. \<And>n'' as n' a n s. \<lbrakk>n'' -as\<rightarrow>* n'; \<And>s. \<lbrakk>\<forall>a\<in>set as. intra_kind (kind a); \<forall>n\<in>set (sourcenodes as). V \<notin> Def n; preds (kinds as) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) s) V = state_val s V; valid_edge a; sourcenode a = n; targetnode a = n''; \<forall>a\<in>set (a # as). intra_kind (kind a); \<forall>n\<in>set (sourcenodes (a # as)). V \<notin> Def n; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
with IH[OF all' all \<open>preds (kinds as) (transfer (kind a) s)\<close>]
[PROOF STATE]
proof (chain)
picking this:
state_val (transfers (kinds as) (transfer (kind a) s)) V = state_val (transfer (kind a) s) V
state_val (transfer (kind a) s) V = state_val s V
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds as) (transfer (kind a) s)) V = state_val (transfer (kind a) s) V
state_val (transfer (kind a) s) V = state_val s V

goal (1 subgoal):
 1. state_val (transfers (kinds (a # as)) s) V = state_val s V
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds (a # as)) s) V = state_val s V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
state_val (transfers (kinds as) s) V = state_val s V

goal (1 subgoal):
 1. state_val (transfers (kinds as) s) V = state_val s V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
state_val (transfers (kinds as) s) V = state_val s V

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma slpa_preds:
  "\<lbrakk>same_level_path_aux cs as; s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; \<forall>a \<in> set as. valid_edge a; length cs = length cfsx;
    preds (kinds as) s\<rbrakk>
  \<Longrightarrow> preds (kinds as) s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_level_path_aux cs as; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'
[PROOF STEP]
proof(induct arbitrary:s s' cf cfsx rule:slpa_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>cs s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set []) valid_edge; length cs = length cfsx; preds (kinds []) s\<rbrakk> \<Longrightarrow> preds (kinds []) s'
 2. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 4. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (slpa_empty cs)
[PROOF STATE]
proof (state)
this:
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
\<forall>a\<in>set []. valid_edge a
length cs = length cfsx
preds (kinds []) s

goal (4 subgoals):
 1. \<And>cs s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set []) valid_edge; length cs = length cfsx; preds (kinds []) s\<rbrakk> \<Longrightarrow> preds (kinds []) s'
 2. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 4. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
\<forall>a\<in>set []. valid_edge a
length cs = length cfsx
preds (kinds []) s

goal (1 subgoal):
 1. preds (kinds []) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds []) s'

goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (slpa_intra cs a as)
[PROOF STATE]
proof (state)
this:
intra_kind (kind a)
same_level_path_aux cs as
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length cs = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
\<forall>a\<in>set (a # as). valid_edge a
length cs = length cfsx
preds (kinds (a # as)) s

goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
note IH = \<open>\<And>s s' cf cfsx. \<lbrakk>s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; \<forall>a \<in> set as. valid_edge a; length cs = length cfsx;
    preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length cs = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'

goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>\<forall>a\<in>set (a#as). valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). valid_edge a
[PROOF STEP]
have "valid_edge a"
    and "\<forall>a \<in> set as. valid_edge a"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). valid_edge a

goal (1 subgoal):
 1. valid_edge a &&& \<forall>a\<in>set as. valid_edge a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
valid_edge a
\<forall>a\<in>set as. valid_edge a

goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>preds (kinds (a#as)) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds (a # as)) s
[PROOF STEP]
have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)"
[PROOF STATE]
proof (prove)
using this:
preds (kinds (a # as)) s

goal (1 subgoal):
 1. pred (kind a) s &&& preds (kinds as) (transfer (kind a) s)
[PROOF STEP]
by(simp_all add:kinds_def)
[PROOF STATE]
proof (state)
this:
pred (kind a) s
preds (kinds as) (transfer (kind a) s)

goal (3 subgoals):
 1. \<And>cs a as s s' cf cfsx. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 3. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
proof(cases cfsx)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cfsx = []

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>length cs = length cfsx\<close>
[PROOF STATE]
proof (chain)
picking this:
length cs = length cfsx
cfsx = []
[PROOF STEP]
have "length cs = length []"
[PROOF STATE]
proof (prove)
using this:
length cs = length cfsx
cfsx = []

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

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from Nil \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
cfsx = []
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
intra_kind (kind a)
[PROOF STEP]
obtain cfx where "transfer (kind a) s = []@cfx#cfs"
      and "transfer (kind a) s' = []@cfx#cfs'"
[PROOF STATE]
proof (prove)
using this:
cfsx = []
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
intra_kind (kind a)

goal (1 subgoal):
 1. (\<And>cfx. \<lbrakk>transfer (kind a) s = [] @ cfx # cfs; transfer (kind a) s' = [] @ cfx # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "kind a",auto simp:kinds_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = [] @ cfx # cfs
transfer (kind a) s' = [] @ cfx # cfs'

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from IH[OF this \<open>length cfs = length cfs'\<close> \<open>\<forall>a \<in> set as. valid_edge a\<close>
      \<open>length cs = length []\<close> \<open>preds (kinds as) (transfer (kind a) s)\<close>]
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
have "preds (kinds as) (transfer (kind a) s')"
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')

goal (1 subgoal):
 1. preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from Nil \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
      \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
cfsx = []
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
cfsx = []
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'

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

goal (2 subgoals):
 1. cfsx = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'

goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
cfsx = x # xs

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
intra_kind (kind a)
cfsx = x # xs
[PROOF STEP]
obtain cfx where "transfer (kind a) s = (cfx#xs)@cf#cfs"
      and "transfer (kind a) s' = (cfx#xs)@cf#cfs'"
[PROOF STATE]
proof (prove)
using this:
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
intra_kind (kind a)
cfsx = x # xs

goal (1 subgoal):
 1. (\<And>cfx. \<lbrakk>transfer (kind a) s = (cfx # xs) @ cf # cfs; transfer (kind a) s' = (cfx # xs) @ cf # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "kind a",auto simp:kinds_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = (cfx # xs) @ cf # cfs
transfer (kind a) s' = (cfx # xs) @ cf # cfs'

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from IH[OF this \<open>length cfs = length cfs'\<close> \<open>\<forall>a \<in> set as. valid_edge a\<close> _
      \<open>preds (kinds as) (transfer (kind a) s)\<close>] \<open>length cs = length cfsx\<close> Cons
[PROOF STATE]
proof (chain)
picking this:
length cs = length (cfx # xs) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
length cs = length cfsx
cfsx = x # xs
[PROOF STEP]
have "preds (kinds as) (transfer (kind a) s')"
[PROOF STATE]
proof (prove)
using this:
length cs = length (cfx # xs) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
length cs = length cfsx
cfsx = x # xs

goal (1 subgoal):
 1. preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from Cons \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
      \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
cfsx = x # xs
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
cfsx = x # xs
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'

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

goal (1 subgoal):
 1. \<And>aa list. cfsx = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'

goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (slpa_Call cs a as Q r p fs)
[PROOF STATE]
proof (state)
this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
same_level_path_aux (a # cs) as
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length (a # cs) = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
\<forall>a\<in>set (a # as). valid_edge a
length cs = length cfsx
preds (kinds (a # as)) s

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
note IH = \<open>\<And>s s' cf cfsx. \<lbrakk>s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; \<forall>a \<in> set as. valid_edge a; length (a#cs) = length cfsx;
    preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length (a # cs) = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>\<forall>a\<in>set (a#as). valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). valid_edge a
[PROOF STEP]
have "valid_edge a"
    and "\<forall>a \<in> set as. valid_edge a"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). valid_edge a

goal (1 subgoal):
 1. valid_edge a &&& \<forall>a\<in>set as. valid_edge a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
valid_edge a
\<forall>a\<in>set as. valid_edge a

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>preds (kinds (a#as)) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds (a # as)) s
[PROOF STEP]
have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)"
[PROOF STATE]
proof (prove)
using this:
preds (kinds (a # as)) s

goal (1 subgoal):
 1. pred (kind a) s &&& preds (kinds as) (transfer (kind a) s)
[PROOF STEP]
by(simp_all add:kinds_def)
[PROOF STATE]
proof (state)
this:
pred (kind a) s
preds (kinds as) (transfer (kind a) s)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
[PROOF STEP]
obtain cfx
    where "transfer (kind a) s = (cfx#cfsx)@cf#cfs"
    and "transfer (kind a) s' = (cfx#cfsx)@cf#cfs'"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'

goal (1 subgoal):
 1. (\<And>cfx. \<lbrakk>transfer (kind a) s = (cfx # cfsx) @ cf # cfs; transfer (kind a) s' = (cfx # cfsx) @ cf # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases cfsx) auto
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = (cfx # cfsx) @ cf # cfs
transfer (kind a) s' = (cfx # cfsx) @ cf # cfs'

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from IH[OF this \<open>length cfs = length cfs'\<close> \<open>\<forall>a \<in> set as. valid_edge a\<close> _
    \<open>preds (kinds as) (transfer (kind a) s)\<close>] \<open>length cs = length cfsx\<close>
[PROOF STATE]
proof (chain)
picking this:
length (a # cs) = length (cfx # cfsx) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
length cs = length cfsx
[PROOF STEP]
have "preds (kinds as) (transfer (kind a) s')"
[PROOF STATE]
proof (prove)
using this:
length (a # cs) = length (cfx # cfsx) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
length cs = length cfsx

goal (1 subgoal):
 1. preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
    \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'

goal (1 subgoal):
 1. pred (kind a) s'
[PROOF STEP]
by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred (kind a) s'

goal (2 subgoals):
 1. \<And>cs a as Q r p fs s s' cf cfsx. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length (a # cs) = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'

goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (slpa_Return cs a as Q p f c' cs')
[PROOF STATE]
proof (state)
this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
cs = c' # cs'
same_level_path_aux cs' as
a \<in> get_return_edges c'
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length cs' = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
\<forall>a\<in>set (a # as). valid_edge a
length cs = length cfsx
preds (kinds (a # as)) s

goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
note IH = \<open>\<And>s s' cf cfsx. \<lbrakk>s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; \<forall>a \<in> set as. valid_edge a; length cs' = length cfsx;
    preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s = ?cfsx @ ?cf # cfs; ?s' = ?cfsx @ ?cf # cfs'; length cfs = length cfs'; \<forall>a\<in>set as. valid_edge a; length cs' = length ?cfsx; preds (kinds as) ?s\<rbrakk> \<Longrightarrow> preds (kinds as) ?s'

goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>\<forall>a\<in>set (a#as). valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). valid_edge a
[PROOF STEP]
have "valid_edge a"
    and "\<forall>a \<in> set as. valid_edge a"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). valid_edge a

goal (1 subgoal):
 1. valid_edge a &&& \<forall>a\<in>set as. valid_edge a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
valid_edge a
\<forall>a\<in>set as. valid_edge a

goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>preds (kinds (a#as)) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (kinds (a # as)) s
[PROOF STEP]
have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)"
[PROOF STATE]
proof (prove)
using this:
preds (kinds (a # as)) s

goal (1 subgoal):
 1. pred (kind a) s &&& preds (kinds as) (transfer (kind a) s)
[PROOF STEP]
by(simp_all add:kinds_def)
[PROOF STATE]
proof (state)
this:
pred (kind a) s
preds (kinds as) (transfer (kind a) s)

goal (1 subgoal):
 1. \<And>cs a as Q p f c' cs' s s' cf cfsx. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>s s' cf cfsx. \<lbrakk>s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set as) valid_edge; length cs' = length cfsx; preds (kinds as) s\<rbrakk> \<Longrightarrow> preds (kinds as) s'; s = cfsx @ cf # cfs; s' = cfsx @ cf # cfs'; length cfs = length cfs'; Ball (set (a # as)) valid_edge; length cs = length cfsx; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
proof(cases cs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs' = []

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>cs = c'#cs'\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
      \<open>length cs = length cfsx\<close>
[PROOF STATE]
proof (chain)
picking this:
cs = c' # cs'
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cs = length cfsx
cs' = []
[PROOF STEP]
obtain cf' where "s = cf'#cf#cfs" and "s' = cf'#cf#cfs'"
[PROOF STATE]
proof (prove)
using this:
cs = c' # cs'
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cs = length cfsx
cs' = []

goal (1 subgoal):
 1. (\<And>cf'. \<lbrakk>s = cf' # cf # cfs; s' = cf' # cf # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases cfsx) auto
[PROOF STATE]
proof (state)
this:
s = cf' # cf # cfs
s' = cf' # cf # cfs'

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
s = cf' # cf # cfs
s' = cf' # cf # cfs'
[PROOF STEP]
obtain cf'' where "transfer (kind a) s = []@cf''#cfs"
      and "transfer (kind a) s' = []@cf''#cfs'"
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
s = cf' # cf # cfs
s' = cf' # cf # cfs'

goal (1 subgoal):
 1. (\<And>cf''. \<lbrakk>transfer (kind a) s = [] @ cf'' # cfs; transfer (kind a) s' = [] @ cf'' # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = [] @ cf'' # cfs
transfer (kind a) s' = [] @ cf'' # cfs'

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from IH[OF this \<open>length cfs = length cfs'\<close> \<open>\<forall>a \<in> set as. valid_edge a\<close> _
      \<open>preds (kinds as) (transfer (kind a) s)\<close>] Nil
[PROOF STATE]
proof (chain)
picking this:
length cs' = length [] \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
cs' = []
[PROOF STEP]
have "preds (kinds as) (transfer (kind a) s')"
[PROOF STATE]
proof (prove)
using this:
length cs' = length [] \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
cs' = []

goal (1 subgoal):
 1. preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
      \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'

goal (1 subgoal):
 1. pred (kind a) s'
[PROOF STEP]
by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred (kind a) s'

goal (2 subgoals):
 1. cs' = [] \<Longrightarrow> preds (kinds (a # as)) s'
 2. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'

goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
case (Cons cx csx)
[PROOF STATE]
proof (state)
this:
cs' = cx # csx

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>cs = c'#cs'\<close> \<open>length cs = length cfsx\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
cs = c' # cs'
length cs = length cfsx
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
cs' = cx # csx
[PROOF STEP]
obtain x x' xs where "s = (x#x'#xs)@cf#cfs" and "s' = (x#x'#xs)@cf#cfs'"
      and "length xs = length csx"
[PROOF STATE]
proof (prove)
using this:
cs = c' # cs'
length cs = length cfsx
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
cs' = cx # csx

goal (1 subgoal):
 1. (\<And>x x' xs. \<lbrakk>s = (x # x' # xs) @ cf # cfs; s' = (x # x' # xs) @ cf # cfs'; length xs = length csx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases cfsx,auto,case_tac list,fastforce+)
[PROOF STATE]
proof (state)
this:
s = (x # x' # xs) @ cf # cfs
s' = (x # x' # xs) @ cf # cfs'
length xs = length csx

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
with \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
s = (x # x' # xs) @ cf # cfs
s' = (x # x' # xs) @ cf # cfs'
length xs = length csx
[PROOF STEP]
obtain cf' where "transfer (kind a) s = (cf'#xs)@cf#cfs"
      and "transfer (kind a) s' = (cf'#xs)@cf#cfs'"
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
s = (x # x' # xs) @ cf # cfs
s' = (x # x' # xs) @ cf # cfs'
length xs = length csx

goal (1 subgoal):
 1. (\<And>cf'. \<lbrakk>transfer (kind a) s = (cf' # xs) @ cf # cfs; transfer (kind a) s' = (cf' # xs) @ cf # cfs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
transfer (kind a) s = (cf' # xs) @ cf # cfs
transfer (kind a) s' = (cf' # xs) @ cf # cfs'

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from IH[OF this \<open>length cfs = length cfs'\<close> \<open>\<forall>a \<in> set as. valid_edge a\<close> _
      \<open>preds (kinds as) (transfer (kind a) s)\<close>] Cons \<open>length xs = length csx\<close>
[PROOF STATE]
proof (chain)
picking this:
length cs' = length (cf' # xs) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
cs' = cx # csx
length xs = length csx
[PROOF STEP]
have "preds (kinds as) (transfer (kind a) s')"
[PROOF STATE]
proof (prove)
using this:
length cs' = length (cf' # xs) \<Longrightarrow> preds (kinds as) (transfer (kind a) s')
cs' = cx # csx
length xs = length csx

goal (1 subgoal):
 1. preds (kinds as) (transfer (kind a) s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (kinds as) (transfer (kind a) s')

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>pred (kind a) s\<close> \<open>s = cfsx@cf#cfs\<close> \<open>s' = cfsx@cf#cfs'\<close>
      \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'
[PROOF STEP]
have "pred (kind a) s'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
pred (kind a) s
s = cfsx @ cf # cfs
s' = cfsx @ cf # cfs'
length cfs = length cfs'

goal (1 subgoal):
 1. pred (kind a) s'
[PROOF STEP]
by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
[PROOF STATE]
proof (state)
this:
pred (kind a) s'

goal (1 subgoal):
 1. \<And>aa list. cs' = aa # list \<Longrightarrow> preds (kinds (a # as)) s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preds (kinds as) (transfer (kind a) s')
pred (kind a) s'

goal (1 subgoal):
 1. preds (kinds (a # as)) s'
[PROOF STEP]
by(simp add:kinds_def)
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
preds (kinds (a # as)) s'

goal:
No subgoals!
[PROOF STEP]
qed