[STATEMENT]
lemma assumes "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
  and "(p, ins, outs) \<in> set (lift_procs wfp)"
  shows ParamDefs_length:"length (ParamDefs wfp (targetnode a)) = length outs"
  (is ?length)
  and Return_update:"f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)"
  (is ?update)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (ParamDefs wfp (targetnode a)) = length outs &&& f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from Rep_wf_prog[of wfp]
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp \<in> wf_prog
[PROOF STEP]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp \<in> wf_prog

goal (1 subgoal):
 1. (\<And>prog procs. Rep_wf_prog wfp = (prog, procs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp:wf_prog_def)
[PROOF STATE]
proof (state)
this:
Rep_wf_prog wfp = (prog, procs)

goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
hence "wf prog procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. WellFormProgs.wf prog procs
[PROOF STEP]
by(rule wf_wf_prog)
[PROOF STATE]
proof (state)
this:
WellFormProgs.wf prog procs

goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
hence wf:"well_formed procs"
[PROOF STATE]
proof (prove)
using this:
WellFormProgs.wf prog procs

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
valid_edge wfp a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
(p, ins, outs) \<in> set (lift_procs wfp)
[PROOF STEP]
have "prog,procs \<turnstile> sourcenode a -kind a\<rightarrow> targetnode a"
[PROOF STATE]
proof (prove)
using this:
valid_edge wfp a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
(p, ins, outs) \<in> set (lift_procs wfp)

goal (1 subgoal):
 1. prog,procs \<turnstile> sourcenode a -kind a\<rightarrow> targetnode a
[PROOF STEP]
by(simp add:valid_edge_def)
[PROOF STATE]
proof (state)
this:
prog,procs \<turnstile> sourcenode a -kind a\<rightarrow> targetnode a

goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from this \<open>kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> wf
[PROOF STATE]
proof (chain)
picking this:
prog,procs \<turnstile> sourcenode a -kind a\<rightarrow> targetnode a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
well_formed procs
[PROOF STEP]
have "?length \<and> ?update"
[PROOF STATE]
proof (prove)
using this:
prog,procs \<turnstile> sourcenode a -kind a\<rightarrow> targetnode a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
well_formed procs

goal (1 subgoal):
 1. length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
case (MainReturn l p' es rets l' insx outsx cx)
[PROOF STATE]
proof (state)
this:
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
(p', insx, outsx, cx) \<in> set procs
(p', Exit) = sourcenode a
\<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsx) = kind a
(Main, Label l') = targetnode a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
well_formed procs

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>\<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsx) =
      kind a\<close> \<open>kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsx) = kind a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "p' = p"
      and f':"f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))"
[PROOF STATE]
proof (prove)
using this:
\<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsx) = kind a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. p' = p &&& f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>well_formed procs\<close> \<open>(p', insx, outsx, cx) \<in> set procs\<close>
      \<open>(p, ins, outs) \<in> set (lift_procs wfp)\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p', insx, outsx, cx) \<in> set procs
(p, ins, outs) \<in> set (lift_procs wfp)
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))
[PROOF STEP]
have [simp]:"outsx = outs"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p', insx, outsx, cx) \<in> set procs
(p, ins, outs) \<in> set (lift_procs wfp)
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))

goal (1 subgoal):
 1. outsx = outs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
outsx = outs

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "containsCall procs prog [] p'"
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. containsCall procs prog [] p'
[PROOF STEP]
by(rule Proc_CFG_Call_containsCall)
[PROOF STATE]
proof (state)
this:
containsCall procs prog [] p'

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>wf prog procs\<close> \<open>(p', insx, outsx, cx) \<in> set procs\<close>
      \<open>prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
WellFormProgs.wf prog procs
(p', insx, outsx, cx) \<in> set procs
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
containsCall procs prog [] p'
[PROOF STEP]
have "length rets = length outs"
[PROOF STATE]
proof (prove)
using this:
WellFormProgs.wf prog procs
(p', insx, outsx, cx) \<in> set procs
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
containsCall procs prog [] p'

goal (1 subgoal):
 1. length rets = length outs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length rets = length outs

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "ParamDefs wfp (Main,Label l') = rets"
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. ParamDefs wfp (Main, Label l') = rets
[PROOF STEP]
by(fastforce intro:ParamDefs_Main_Return_target)
[PROOF STATE]
proof (state)
this:
ParamDefs wfp (Main, Label l') = rets

goal (8 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>l pa es rets l' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p Label l'; (pa, ins, outsa, c) \<in> set procs; (pa, Exit) = sourcenode a; \<lambda>cf. snd cf = (Main, Label l')\<hookleftarrow>\<^bsub>pa\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outsa) = kind a; (Main, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 8. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>(Main, Label l') = targetnode a\<close> f' \<open>length rets = length outs\<close>
[PROOF STATE]
proof (chain)
picking this:
(Main, Label l') = targetnode a
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))
length rets = length outs
ParamDefs wfp (Main, Label l') = rets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Main, Label l') = targetnode a
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outsx))
length rets = length outs
ParamDefs wfp (Main, Label l') = rets

goal (1 subgoal):
 1. length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
case (ProcReturn px insx outsx cx l p' es rets l' ins' outs' c' ps)
[PROOF STATE]
proof (state)
this:
(px, insx, outsx, cx) \<in> set procs
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
(p', ins', outs', c') \<in> set procs
containsCall procs prog ps px
(p', Exit) = sourcenode a
\<lambda>cf. snd cf = (px, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outs') = kind a
(px, Label l') = targetnode a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
well_formed procs

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>\<lambda>cf. snd cf = (px, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outs') =
      kind a\<close> \<open>kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lambda>cf. snd cf = (px, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outs') = kind a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "p' = p" and f':"f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))"
[PROOF STATE]
proof (prove)
using this:
\<lambda>cf. snd cf = (px, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets [:=] map cf outs') = kind a
kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. p' = p &&& f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>well_formed procs\<close> \<open>(p', ins', outs', c') \<in> set procs\<close>
      \<open>(p, ins, outs) \<in> set (lift_procs wfp)\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p', ins', outs', c') \<in> set procs
(p, ins, outs) \<in> set (lift_procs wfp)
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))
[PROOF STEP]
have [simp]:"outs' = outs"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p', ins', outs', c') \<in> set procs
(p, ins, outs) \<in> set (lift_procs wfp)
p' = p
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))

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

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "containsCall procs cx [] p'"
[PROOF STATE]
proof (prove)
using this:
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. containsCall procs cx [] p'
[PROOF STEP]
by(rule Proc_CFG_Call_containsCall)
[PROOF STATE]
proof (state)
this:
containsCall procs cx [] p'

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>containsCall procs prog ps px\<close> \<open>(px, insx, outsx, cx) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
containsCall procs prog ps px
(px, insx, outsx, cx) \<in> set procs
containsCall procs cx [] p'
[PROOF STEP]
have "containsCall procs prog (ps@[px]) p'"
[PROOF STATE]
proof (prove)
using this:
containsCall procs prog ps px
(px, insx, outsx, cx) \<in> set procs
containsCall procs cx [] p'

goal (1 subgoal):
 1. containsCall procs prog (ps @ [px]) p'
[PROOF STEP]
by(rule containsCall_in_proc)
[PROOF STATE]
proof (state)
this:
containsCall procs prog (ps @ [px]) p'

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>wf prog procs\<close> \<open>(p', ins', outs', c') \<in> set procs\<close>
      \<open>cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
WellFormProgs.wf prog procs
(p', ins', outs', c') \<in> set procs
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
containsCall procs prog (ps @ [px]) p'
[PROOF STEP]
have "length rets = length outs"
[PROOF STATE]
proof (prove)
using this:
WellFormProgs.wf prog procs
(p', ins', outs', c') \<in> set procs
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
containsCall procs prog (ps @ [px]) p'

goal (1 subgoal):
 1. length rets = length outs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length rets = length outs

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
from \<open>(px, insx, outsx, cx) \<in> set procs\<close>
      \<open>cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
(px, insx, outsx, cx) \<in> set procs
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "ParamDefs wfp (px,Label l') = rets"
[PROOF STATE]
proof (prove)
using this:
(px, insx, outsx, cx) \<in> set procs
cx \<turnstile> Label l -CEdge (p', es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. ParamDefs wfp (px, Label l') = rets
[PROOF STEP]
by(fastforce intro:ParamDefs_Proc_Return_target simp:set_conv_nth)
[PROOF STATE]
proof (state)
this:
ParamDefs wfp (px, Label l') = rets

goal (7 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (p', Exit) = sourcenode a; \<lambda>cf. snd cf = (pa, Label l')\<hookleftarrow>\<^bsub>p'\<^esub>\<lambda>cf cf'. cf'(rets' [:=] map cf outs') = kind a; (pa, Label l') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 7. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
with \<open>(px, Label l') = targetnode a\<close> f' \<open>length rets = length outs\<close>
[PROOF STATE]
proof (chain)
picking this:
(px, Label l') = targetnode a
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))
length rets = length outs
ParamDefs wfp (px, Label l') = rets
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(px, Label l') = targetnode a
f' = (\<lambda>cf cf'. cf'(rets [:=] map cf outs'))
length rets = length outs
ParamDefs wfp (px, Label l') = rets

goal (1 subgoal):
 1. length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)

goal (6 subgoals):
 1. \<And>n n'. \<lbrakk>prog \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 2. \<And>pa ins outsa c n n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -IEdge (kind a)\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 3. \<And>l pa es rets n' ins outsa c. \<lbrakk>prog \<turnstile> Label l -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (pa, ins, outsa, c) \<in> set procs; (Main, Label l) = sourcenode a; \<lambda>s. True:(Main, n')\<hookrightarrow>\<^bsub>pa\<^esub>map interpret es = kind a; (pa, Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 4. \<And>pa ins outsa c l p' es' rets' l' ins' outs' c' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> Label l -CEdge (p', es', rets')\<rightarrow>\<^sub>p Label l'; (p', ins', outs', c') \<in> set procs; containsCall procs prog ps pa; (pa, Label l) = sourcenode a; \<lambda>s. True:(pa, Label l')\<hookrightarrow>\<^bsub>p'\<^esub>map interpret es' = kind a; (p', Entry) = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 5. \<And>n pa es rets n'. \<lbrakk>prog \<turnstile> n -CEdge (pa, es, rets)\<rightarrow>\<^sub>p n'; (Main, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (Main, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
 6. \<And>pa ins outsa c n p' es' rets' n' ps. \<lbrakk>(pa, ins, outsa, c) \<in> set procs; c \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n'; containsCall procs prog ps pa; (pa, n) = sourcenode a; (\<lambda>s. False)\<^sub>\<surd> = kind a; (pa, n') = targetnode a; kind a = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; well_formed procs\<rbrakk> \<Longrightarrow> length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)

goal (2 subgoals):
 1. length (ParamDefs wfp (targetnode a)) = length outs
 2. f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
thus "?length" and "?update"
[PROOF STATE]
proof (prove)
using this:
length (ParamDefs wfp (targetnode a)) = length outs \<and> f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)

goal (1 subgoal):
 1. length (ParamDefs wfp (targetnode a)) = length outs &&& f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length (ParamDefs wfp (targetnode a)) = length outs
f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)

goal:
No subgoals!
[PROOF STEP]
qed