[STATEMENT]
lemma Proc_CFG_Call_source_fst_cmd_Call:
  "\<lbrakk>labels prog l c; prog \<turnstile> Label l -CEdge (p,es,rets)\<rightarrow>\<^sub>p n'\<rbrakk>
  \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels prog l c; prog \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
proof(induct arbitrary:n' rule:labels.induct)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>c n'. c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>V e n'. V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 4. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 6. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 7. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 8. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 9. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_Base c n')
[PROOF STATE]
proof (state)
this:
c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (9 subgoals):
 1. \<And>c n'. c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>V e n'. V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 4. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 6. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 7. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 8. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 9. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
c \<turnstile> Label 0 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
by(induct c "Label 0" "CEdge (p, es, rets)" n' rule:Proc_CFG.induct) auto
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (8 subgoals):
 1. \<And>V e n'. V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 3. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 6. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 7. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 8. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>V e n'. V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 3. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 6. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 7. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 8. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_LAss V e n')
[PROOF STATE]
proof (state)
this:
V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (8 subgoals):
 1. \<And>V e n'. V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 3. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 6. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 7. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 8. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
V:=e \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
by(fastforce elim:Proc_CFG.cases)
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd Skip = Call p es rets

goal (7 subgoals):
 1. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 2. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 6. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 7. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 2. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 6. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 7. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_Seq1 c\<^sub>1 l c c\<^sub>2)
[PROOF STATE]
proof (state)
this:
labels c\<^sub>1 l c
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (7 subgoals):
 1. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 2. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 6. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 7. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
note IH = \<open>\<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
    \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets

goal (7 subgoals):
 1. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 2. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 6. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 7. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close> \<open>labels c\<^sub>1 l c\<close>
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>1 l c
[PROOF STEP]
have "c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>1 l c

goal (1 subgoal):
 1. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; labels c\<^sub>1 l c\<rbrakk> \<Longrightarrow> c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>labels c\<^sub>1 l c; Label l = n \<oplus> #:c\<^sub>1; n' = n' \<oplus> #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> c\<^sub>1 \<turnstile> n \<oplus> #:c\<^sub>1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<oplus> #:c\<^sub>1
[PROOF STEP]
by(case_tac n)(auto dest:label_less_num_inner_nodes)
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (7 subgoals):
 1. \<And>c\<^sub>1 l c c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
 2. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 5. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 6. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 7. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd (c;; c\<^sub>2) = Call p es rets

goal (6 subgoals):
 1. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 5. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 6. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 5. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 6. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_Seq2 c\<^sub>2 l c c\<^sub>1)
[PROOF STATE]
proof (state)
this:
labels c\<^sub>2 l c
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (6 subgoals):
 1. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 5. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 6. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
note IH = \<open>\<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
    \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets

goal (6 subgoals):
 1. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 5. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 6. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close> \<open>labels c\<^sub>2 l c\<close>
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>2 l c
[PROOF STEP]
obtain nx where "c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>2 l c

goal (1 subgoal):
 1. (\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; labels c\<^sub>2 l c\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule Proc_CFG.cases)
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>prog. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = prog; Label (l + #:c\<^sub>1) = Entry; CEdge (p, es, rets) = IEdge (\<lambda>s. False)\<^sub>\<surd>; n' = Exit\<rbrakk> \<Longrightarrow> thesis
 2. \<And>prog. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = prog; Label (l + #:c\<^sub>1) = Entry; CEdge (p, es, rets) = IEdge (\<lambda>s. True)\<^sub>\<surd>; n' = Label 0\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = Skip; Label (l + #:c\<^sub>1) = Label 0; CEdge (p, es, rets) = IEdge \<Up>id; n' = Exit\<rbrakk> \<Longrightarrow> thesis
 4. \<And>V e. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = V:=e; Label (l + #:c\<^sub>1) = Label 0; CEdge (p, es, rets) = IEdge \<Up>\<lambda>cf. update cf V e; n' = Label 1\<rbrakk> \<Longrightarrow> thesis
 5. \<And>V e. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = V:=e; Label (l + #:c\<^sub>1) = Label 1; CEdge (p, es, rets) = IEdge \<Up>id; n' = Exit\<rbrakk> \<Longrightarrow> thesis
 6. \<And>c\<^sub>1' n et n' c\<^sub>2'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = c\<^sub>1';; c\<^sub>2'; Label (l + #:c\<^sub>1) = n; CEdge (p, es, rets) = et; n' = n'; c\<^sub>1' \<turnstile> n -et\<rightarrow>\<^sub>p n'; n' \<noteq> Exit\<rbrakk> \<Longrightarrow> thesis
 7. \<And>c\<^sub>1' n et c\<^sub>2'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = c\<^sub>1';; c\<^sub>2'; Label (l + #:c\<^sub>1) = n; CEdge (p, es, rets) = et; n' = Label #:c\<^sub>1'; c\<^sub>1' \<turnstile> n -et\<rightarrow>\<^sub>p Exit; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
 8. \<And>c\<^sub>2' n et n' c\<^sub>1'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = c\<^sub>1';; c\<^sub>2'; Label (l + #:c\<^sub>1) = n \<oplus> #:c\<^sub>1'; CEdge (p, es, rets) = et; n' = n' \<oplus> #:c\<^sub>1'; c\<^sub>2' \<turnstile> n -et\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
 9. \<And>b c\<^sub>1' c\<^sub>2'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = if (b) c\<^sub>1' else c\<^sub>2'; Label (l + #:c\<^sub>1) = Label 0; CEdge (p, es, rets) = IEdge (\<lambda>cf. state_check cf b (Some true))\<^sub>\<surd>; n' = Label 1\<rbrakk> \<Longrightarrow> thesis
 10. \<And>b c\<^sub>1' c\<^sub>2'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; c\<^sub>1;; c\<^sub>2 = if (b) c\<^sub>1' else c\<^sub>2'; Label (l + #:c\<^sub>1) = Label 0; CEdge (p, es, rets) = IEdge (\<lambda>cf. state_check cf b (Some false))\<^sub>\<surd>; n' = Label (#:c\<^sub>1' + 1)\<rbrakk> \<Longrightarrow> thesis
A total of 19 subgoals...
[PROOF STEP]
apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes Proc_CFG_Call_Labels)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (l + #:c\<^sub>1) = n \<oplus> #:c\<^sub>1; n' = n' \<oplus> #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac n) auto
[PROOF STATE]
proof (state)
this:
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx

goal (6 subgoals):
 1. \<And>c\<^sub>2 l c c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; c\<^sub>1;; c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 4. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 5. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 6. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (5 subgoals):
 1. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 4. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 5. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 4. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 5. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_CondTrue c\<^sub>1 l c b c\<^sub>2)
[PROOF STATE]
proof (state)
this:
labels c\<^sub>1 l c
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (5 subgoals):
 1. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 4. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 5. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
note IH = \<open>\<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
    \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets

goal (5 subgoals):
 1. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 4. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 5. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close> \<open>labels c\<^sub>1 l c\<close>
[PROOF STATE]
proof (chain)
picking this:
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>1 l c
[PROOF STEP]
obtain nx where "c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx"
[PROOF STATE]
proof (prove)
using this:
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>1 l c

goal (1 subgoal):
 1. (\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; labels c\<^sub>1 l c\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule Proc_CFG.cases,auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
 2. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n n' x1. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Label x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Entry\<rbrakk> \<Longrightarrow> thesis
 3. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Exit\<rbrakk> \<Longrightarrow> thesis
 4. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>1 l c; Label (Suc l) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac n)(auto dest:label_less_num_inner_nodes)
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx

goal (5 subgoals):
 1. \<And>c\<^sub>1 l c b c\<^sub>2 n'. \<lbrakk>labels c\<^sub>1 l c; \<And>n'. c\<^sub>1 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 3. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 4. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 5. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (4 subgoals):
 1. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 3. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 4. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 3. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 4. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_CondFalse c\<^sub>2 l c b c\<^sub>1)
[PROOF STATE]
proof (state)
this:
labels c\<^sub>2 l c
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (4 subgoals):
 1. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 3. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 4. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
note IH = \<open>\<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
    \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets

goal (4 subgoals):
 1. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 3. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 4. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label  (l + #:c\<^sub>1 + 1)-CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close>
    \<open>labels c\<^sub>2 l c\<close>
[PROOF STATE]
proof (chain)
picking this:
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>2 l c
[PROOF STEP]
obtain nx where "c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx"
[PROOF STATE]
proof (prove)
using this:
if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c\<^sub>2 l c

goal (1 subgoal):
 1. (\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; labels c\<^sub>2 l c\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule Proc_CFG.cases,auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
 2. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(case_tac n)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n n' x1. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Label x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Entry\<rbrakk> \<Longrightarrow> thesis
 3. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc 0; n' = n' \<oplus> Suc 0; c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n = Exit\<rbrakk> \<Longrightarrow> thesis
 4. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c\<^sub>2 l c; Label (Suc (l + #:c\<^sub>1)) = n \<oplus> Suc #:c\<^sub>1; n' = n' \<oplus> Suc #:c\<^sub>1; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac n) auto
[PROOF STATE]
proof (state)
this:
c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx

goal (4 subgoals):
 1. \<And>c\<^sub>2 l c b c\<^sub>1 n'. \<lbrakk>labels c\<^sub>2 l c; \<And>n'. c\<^sub>2 \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> Label (l + #:c\<^sub>1 + 1) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
 2. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 3. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 4. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (3 subgoals):
 1. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 2. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 2. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_WhileBody c' l c b)
[PROOF STATE]
proof (state)
this:
labels c' l c
c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets
while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (3 subgoals):
 1. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 2. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
note IH = \<open>\<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
    \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets\<close>
[PROOF STATE]
proof (state)
this:
c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p ?n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets

goal (3 subgoals):
 1. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 2. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close> \<open>labels c' l c\<close>
[PROOF STATE]
proof (chain)
picking this:
while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c' l c
[PROOF STEP]
obtain nx where "c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx"
[PROOF STATE]
proof (prove)
using this:
while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
labels c' l c

goal (1 subgoal):
 1. (\<And>nx. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; labels c' l c\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx \<Longrightarrow> thesis; labels c' l c; Label (Suc (Suc l)) = n \<oplus> 2; n' = n' \<oplus> 2; c' \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'; n \<noteq> Entry; n' \<noteq> Exit\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac n) auto
[PROOF STATE]
proof (state)
this:
c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p nx

goal (3 subgoals):
 1. \<And>c' l c b n'. \<lbrakk>labels c' l c; \<And>n'. c' \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd c = Call p es rets; while (b) c' \<turnstile> Label (l + 2) -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
 2. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 3. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p es rets. fst_cmd c = Call p es rets
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>p es rets. fst_cmd c = Call p es rets

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd (c;; while (b) c') = Call p es rets

goal (2 subgoals):
 1. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_WhileExit b c' n')
[PROOF STATE]
proof (state)
this:
while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (2 subgoals):
 1. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
have "while (b) c' \<turnstile> Label 1 -IEdge \<Up>id\<rightarrow>\<^sub>p Exit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while (b) c' \<turnstile> Label 1 -IEdge \<Up>id\<rightarrow>\<^sub>p Exit
[PROOF STEP]
by(rule Proc_CFG_WhileFalseSkip)
[PROOF STATE]
proof (state)
this:
while (b) c' \<turnstile> Label 1 -IEdge \<Up>id\<rightarrow>\<^sub>p Exit

goal (2 subgoals):
 1. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
with \<open>while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
while (b) c' \<turnstile> Label 1 -IEdge \<Up>id\<rightarrow>\<^sub>p Exit
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
while (b) c' \<turnstile> Label 1 -IEdge \<Up>id\<rightarrow>\<^sub>p Exit

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

goal (2 subgoals):
 1. \<And>b c' n'. while (b) c' \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
 2. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd Skip = Call p es rets

goal (1 subgoal):
 1. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
case (Labels_Call px esx retsx)
[PROOF STATE]
proof (state)
this:
Call px esx retsx \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. \<And>pa esa retsa n'. Call pa esa retsa \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
from \<open>Call px esx retsx \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
Call px esx retsx \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Call px esx retsx \<turnstile> Label 1 -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd Skip = Call p es rets
[PROOF STEP]
by(fastforce elim:Proc_CFG.cases)
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd Skip = Call p es rets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PCFG_CallEdge_THE_rets:
  "prog \<turnstile> n -CEdge (p,es,rets)\<rightarrow>\<^sub>p n'
\<Longrightarrow> (THE rets'. \<exists>p' es' n. prog \<turnstile> n -CEdge(p',es',rets')\<rightarrow>\<^sub>p n') = rets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> (THE rets'. \<exists>p' es' n. prog \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n') = rets
[PROOF STEP]
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq')


[STATEMENT]
lemma in_procs_THE_in_procs_cmd:
  "\<lbrakk>well_formed procs; (p,ins,outs,c) \<in> set procs\<rbrakk>
  \<Longrightarrow> (THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed procs; (p, ins, outs, c) \<in> set procs\<rbrakk> \<Longrightarrow> (THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
by(fastforce intro:the_equality)


[STATEMENT]
lemma ParamDefs_Main_Return_target:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n -CEdge(p',es,rets)\<rightarrow>\<^sub>p n'\<rbrakk>
  \<Longrightarrow> ParamDefs wfp (Main,n') = rets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n -CEdge (p', es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> ParamDefs wfp (Main, n') = rets
[PROOF STEP]
by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)


[STATEMENT]
lemma ParamDefs_Proc_Return_target:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n -CEdge(p',es,rets)\<rightarrow>\<^sub>p n'"
  shows "ParamDefs wfp (p,n') = rets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
from \<open>well_formed procs\<close> \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n -CEdge (p', es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = rets
[PROOF STEP]
by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
ParamDefs wfp (p, n') = rets

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ParamDefs_Main_IEdge_Nil:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'\<rbrakk>
  \<Longrightarrow> ParamDefs wfp (Main,n') = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> ParamDefs wfp (Main, n') = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target
            simp:ParamDefs_def ParamDefs_proc_def)


[STATEMENT]
lemma ParamDefs_Proc_IEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'"
  shows "ParamDefs wfp (p,n') = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
from \<open>well_formed procs\<close> \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target
                simp:ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
ParamDefs wfp (p, n') = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ParamDefs_Main_CEdge_Nil:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n' -CEdge(p',es,rets)\<rightarrow>\<^sub>p n''\<rbrakk>
  \<Longrightarrow> ParamDefs wfp (Main,n') = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n' -CEdge (p', es, rets)\<rightarrow>\<^sub>p n''\<rbrakk> \<Longrightarrow> ParamDefs wfp (Main, n') = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamDefs_def ParamDefs_proc_def)


[STATEMENT]
lemma ParamDefs_Proc_CEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n' -CEdge(p',es,rets)\<rightarrow>\<^sub>p n''"
  shows "ParamDefs wfp (p,n') = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
from \<open>well_formed procs\<close> \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

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

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n' -CEdge (p', es, rets)\<rightarrow>\<^sub>p n''

goal (1 subgoal):
 1. ParamDefs wfp (p, n') = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
ParamDefs wfp (p, n') = []

goal:
No subgoals!
[PROOF STEP]
qed