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

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

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

goal (1 subgoal):
 1. c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c\<^sub>1;; c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l; labels c\<^sub>1 l c\<rbrakk> \<Longrightarrow> c\<^sub>1 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l
[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; n = n \<oplus> #:c\<^sub>1; Label l = 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> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l

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

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

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

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

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

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

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

goal (1 subgoal):
 1. fst_cmd c = Skip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst_cmd c = Skip

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

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

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

goal (1 subgoal):
 1. (\<And>nx. c\<^sub>1 \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c\<^sub>1 \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label (l + 1); 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc 0; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc 0; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc 0; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc 0; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>1 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc l) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l

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

goal (1 subgoal):
 1. fst_cmd c = Skip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst_cmd c = Skip

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

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

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

goal (1 subgoal):
 1. (\<And>nx. c\<^sub>2 \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; if (b) c\<^sub>1 else c\<^sub>2 \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label (l + #:c\<^sub>1 + 1); 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc 0; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc 0; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc 0; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc 0; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc (l + #:c\<^sub>1)) = 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_targetlabel_less_num_nodes)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c\<^sub>2 \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c\<^sub>2 l c; n = n \<oplus> Suc #:c\<^sub>1; Label (Suc (l + #:c\<^sub>1)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l

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

goal (1 subgoal):
 1. fst_cmd c = Skip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst_cmd c = Skip

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

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

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

goal (1 subgoal):
 1. (\<And>nx. c' \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>nx. c' \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; while (b) c' \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label (l + 2); labels c' l c\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule Proc_CFG.cases,auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n n'. \<lbrakk>\<And>nx. c' \<turnstile> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l \<Longrightarrow> thesis; labels c' l c; n = n \<oplus> 2; Label (Suc (Suc l)) = 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> nx -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l

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

goal (1 subgoal):
 1. fst_cmd (c;; while (b) c') = Skip
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst_cmd (c;; while (b) c') = Skip

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

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

goal (1 subgoal):
 1. fst_cmd Skip = Skip
[PROOF STEP]
by(fastforce elim:Proc_CFG.cases)
[PROOF STATE]
proof (state)
this:
fst_cmd Skip = Skip

goal (3 subgoals):
 1. \<And>c n. c \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label 0 \<Longrightarrow> fst_cmd c = Skip
 2. \<And>V e n. V:=e \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label 1 \<Longrightarrow> fst_cmd Skip = Skip
 3. \<And>b c' n. while (b) c' \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label 1 \<Longrightarrow> fst_cmd Skip = Skip
[PROOF STEP]
qed(auto dest:Proc_CFG_Call_Labels)