Theory WellFormed

section ‹Instantiate well-formedness locales with Proc CFG›

theory WellFormed imports Interpretation Labels "../StaticInter/CFGExit_wf" begin

subsection ‹Determining the first atomic command›

fun fst_cmd :: "cmd ⇒ cmd"
where "fst_cmd (c⇩1;;c⇩2) = fst_cmd c⇩1"
  | "fst_cmd c = c"

lemma Proc_CFG_Call_target_fst_cmd_Skip:
  "⟦labels prog l' c; prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'⟧ 
  ⟹ fst_cmd c = Skip"
proof(induct arbitrary:n rule:labels.induct) 
  case (Labels_Seq1 c⇩1 l c c⇩2)
  note IH = ‹⋀n. c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
  from ‹c⇩1;; c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l› ‹labels c⇩1 l c›
  have "c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n')(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_Seq2 c⇩2 l c c⇩1)
  note IH = ‹⋀n. c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
  from ‹c⇩1;; c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + #:c⇩1)› ‹labels c⇩2 l c›
  obtain nx where "c⇩2 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
    apply - apply(erule Proc_CFG.cases)
    apply(auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_CondTrue c⇩1 l c b c⇩2)
  note IH = ‹⋀n. c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
  from ‹if (b) c⇩1 else c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + 1)› ‹labels c⇩1 l c›
  obtain nx where "c⇩1 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n') apply auto
    by(case_tac n')(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_CondFalse c⇩2 l c b c⇩1)
  note IH = ‹⋀n. c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
  from ‹if (b) c⇩1 else c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + #:c⇩1 + 1)› 
    ‹labels c⇩2 l c›
  obtain nx where "c⇩2 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileBody c' l c b)
  note IH = ‹⋀n. c' ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
  from ‹while (b) c' ⊢ n -CEdge (p, es, rets)→⇩p Label (l + 2)› ‹labels c' l c›
  obtain nx where "c' ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_Call px esx retsx)
  from ‹Call px esx retsx ⊢ n -CEdge (p, es, rets)→⇩p Label 1›
  show ?case by(fastforce elim:Proc_CFG.cases)
qed(auto dest:Proc_CFG_Call_Labels)


lemma Proc_CFG_Call_source_fst_cmd_Call:
  "⟦labels prog l c; prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'⟧ 
  ⟹ ∃p es rets. fst_cmd c = Call p es rets"
proof(induct arbitrary:n' rule:labels.induct)
  case (Labels_Base c n')
  from ‹c ⊢ Label 0 -CEdge (p, es, rets)→⇩p n'› show ?case
    by(induct c "Label 0" "CEdge (p, es, rets)" n' rule:Proc_CFG.induct) auto
next
  case (Labels_LAss V e n')
  from ‹V:=e ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'› show ?case
    by(fastforce elim:Proc_CFG.cases)
next
  case (Labels_Seq1 c⇩1 l c c⇩2)
  note IH = ‹⋀n'. c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n' 
    ⟹ ∃p es rets. fst_cmd c = Call p es rets›
  from ‹c⇩1;; c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩1 l c›
  have "c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n'"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n)(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_Seq2 c⇩2 l c c⇩1)
  note IH = ‹⋀n'. c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n'
    ⟹ ∃p es rets. fst_cmd c = Call p es rets›
  from ‹c⇩1;; c⇩2 ⊢ Label (l + #:c⇩1) -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩2 l c›
  obtain nx where "c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes Proc_CFG_Call_Labels)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_CondTrue c⇩1 l c b c⇩2)
  note IH = ‹⋀n'. c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n' 
    ⟹ ∃p es rets. fst_cmd c = Call p es rets›
  from ‹if (b) c⇩1 else c⇩2 ⊢ Label (l + 1) -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩1 l c›
  obtain nx where "c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n) apply auto
    by(case_tac n)(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_CondFalse c⇩2 l c b c⇩1)
  note IH = ‹⋀n'. c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n' 
    ⟹ ∃p es rets. fst_cmd c = Call p es rets›
  from ‹if (b) c⇩1 else c⇩2 ⊢ Label  (l + #:c⇩1 + 1)-CEdge (p, es, rets)→⇩p n'› 
    ‹labels c⇩2 l c›
  obtain nx where "c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileBody c' l c b)
  note IH = ‹⋀n'. c' ⊢ Label l -CEdge (p, es, rets)→⇩p n' 
    ⟹ ∃p es rets. fst_cmd c = Call p es rets›
  from ‹while (b) c' ⊢ Label (l + 2) -CEdge (p, es, rets)→⇩p n'› ‹labels c' l c›
  obtain nx where "c' ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileExit b c' n')
  have "while (b) c' ⊢ Label 1 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_WhileFalseSkip)
  with ‹while (b) c' ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'›
  have False by(rule Proc_CFG_Call_Intra_edge_not_same_source)
  thus ?case by simp
next
  case (Labels_Call px esx retsx)
  from ‹Call px esx retsx ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'›
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


subsection ‹Definition of ‹Def› and ‹Use› sets›

subsubsection ‹‹ParamDefs››

lemma PCFG_CallEdge_THE_rets:
  "prog ⊢ n -CEdge (p,es,rets)→⇩p n'
⟹ (THE rets'. ∃p' es' n. prog ⊢ n -CEdge(p',es',rets')→⇩p n') = rets"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq')


definition ParamDefs_proc :: "cmd ⇒ label ⇒ vname list"
  where "ParamDefs_proc c n ≡ 
  if (∃n' p' es' rets'. c ⊢ n' -CEdge(p',es',rets')→⇩p n) then 
     (THE rets'. ∃p' es' n'. c ⊢ n' -CEdge(p',es',rets')→⇩p n)
  else []"


lemma in_procs_THE_in_procs_cmd:
  "⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
  ⟹ (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
  by(fastforce intro:the_equality)


definition ParamDefs :: "wf_prog ⇒ node ⇒ vname list"
  where "⋀wfp. ParamDefs wfp n ≡ let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (if (p = Main) then ParamDefs_proc prog l
   else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
         then ParamDefs_proc (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) l
         else []))"


lemma ParamDefs_Main_Return_target:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -CEdge(p',es,rets)→⇩p n'⟧
  ⟹ ParamDefs wfp (Main,n') = rets"
  by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_Return_target:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -CEdge(p',es,rets)→⇩p n'"
  shows "ParamDefs wfp (p,n') = rets"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
  moreover
  from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_IEdge_Nil:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -IEdge et→⇩p n'⟧
  ⟹ ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target 
            simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_IEdge_Nil:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -IEdge et→⇩p n'"
  shows "ParamDefs wfp (p,n') = []"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce  
  moreover
  from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target 
                simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_CEdge_Nil:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n' -CEdge(p',es,rets)→⇩p n''⟧
  ⟹ ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_CEdge_Nil:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n' -CEdge(p',es,rets)→⇩p n''"
  shows "ParamDefs wfp (p,n') = []"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce  
  moreover
  from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamDefs_def ParamDefs_proc_def)
qed


lemma
  fixes wfp
  assumes "valid_edge wfp a" and "kind a = Q'↩⇘p⇙f'"
  and "(p, ins, outs) ∈ set (lift_procs wfp)"
  shows ParamDefs_length:"length (ParamDefs wfp (targetnode a)) = length outs"
  (is ?length)
  and Return_update:"f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)"
  (is ?update)
proof -
  from Rep_wf_prog[of wfp]
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)" 
    by(fastforce simp:wf_prog_def)
  hence "wf prog procs" by(rule wf_wf_prog)
  hence wf:"well_formed procs" by fastforce
  from assms have "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
    by(simp add:valid_edge_def)
  from this ‹kind a = Q'↩⇘p⇙f'› wf have "?length ∧ ?update"
  proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
    case (MainReturn l p' es rets l' insx outsx cx)
    from ‹λcf. snd cf = (Main, Label l')↩⇘p'⇙λcf cf'. cf'(rets [:=] map cf outsx) =
      kind a› ‹kind a = Q'↩⇘p⇙f'› have "p' = p" 
      and f':"f' = (λcf cf'. cf'(rets [:=] map cf outsx))" by simp_all
    with ‹well_formed procs› ‹(p', insx, outsx, cx) ∈ set procs›
      ‹(p, ins, outs) ∈ set (lift_procs wfp)›
    have [simp]:"outsx = outs" by fastforce
    from ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "containsCall procs prog [] p'" by(rule Proc_CFG_Call_containsCall)
    with ‹wf prog procs› ‹(p', insx, outsx, cx) ∈ set procs› 
      ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "length rets = length outs" by fastforce
    from ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "ParamDefs wfp (Main,Label l') = rets"
      by(fastforce intro:ParamDefs_Main_Return_target)
    with ‹(Main, Label l') = targetnode a› f' ‹length rets = length outs›
    show ?thesis by simp
  next
    case (ProcReturn px insx outsx cx l p' es rets l' ins' outs' c' ps)
    from ‹λcf. snd cf = (px, Label l')↩⇘p'⇙λcf cf'. cf'(rets [:=] map cf outs') =
      kind a› ‹kind a = Q'↩⇘p⇙f'›
    have "p' = p" and f':"f' = (λcf cf'. cf'(rets [:=] map cf outs'))"
      by simp_all
    with ‹well_formed procs› ‹(p', ins', outs', c') ∈ set procs›
      ‹(p, ins, outs) ∈ set (lift_procs wfp)›
    have [simp]:"outs' = outs" by fastforce
    from ‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "containsCall procs cx [] p'" by(rule Proc_CFG_Call_containsCall)
    with ‹containsCall procs prog ps px› ‹(px, insx, outsx, cx) ∈ set procs›
    have "containsCall procs prog (ps@[px]) p'" by(rule containsCall_in_proc)
    with ‹wf prog procs› ‹(p', ins', outs', c') ∈ set procs›
      ‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "length rets = length outs" by fastforce
    from ‹(px, insx, outsx, cx) ∈ set procs›
      ‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
    have "ParamDefs wfp (px,Label l') = rets"
      by(fastforce intro:ParamDefs_Proc_Return_target simp:set_conv_nth)
    with ‹(px, Label l') = targetnode a› f' ‹length rets = length outs›
    show ?thesis by simp
  qed auto
  thus "?length" and "?update" by simp_all
qed


subsubsection ‹‹ParamUses››

fun fv :: "expr ⇒ vname set"
where
  "fv (Val v)       = {}"
  | "fv (Var V)       = {V}"
  | "fv (e1 «bop» e2) = (fv e1 ∪ fv e2)"


lemma rhs_interpret_eq: 
  "⟦state_check cf e v'; ∀V ∈ fv e. cf V = cf' V⟧ 
   ⟹ state_check cf' e v'"
proof(induct e arbitrary:v')
  case (Val v)
  from ‹state_check cf (Val v) v'› have "v' = Some v" 
    by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (Var V)
  hence "cf' (V) = v'" by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (BinOp b1 bop b2)
  note IH1 = ‹⋀v'. ⟦state_check cf b1 v'; ∀V∈fv b1. cf V = cf' V⟧
    ⟹ state_check cf' b1 v'›
  note IH2 = ‹⋀v'. ⟦state_check cf b2 v'; ∀V∈fv b2. cf V = cf' V⟧
    ⟹ state_check cf' b2 v'›
  from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b1. cf V = cf' V"
    and "∀V ∈ fv b2. cf V = cf' V" by simp_all
  from ‹state_check cf (b1 «bop» b2) v'›
  have "((state_check cf b1 None ∧ v' = None) ∨ 
          (state_check cf b2 None ∧ v' = None)) ∨
    (∃v⇩1 v⇩2. state_check cf b1 (Some v⇩1) ∧ state_check cf b2 (Some v⇩2) ∧
    binop bop v⇩1 v⇩2 = v')"
    apply(cases "interpret b1 cf",simp)
    apply(cases "interpret b2 cf",simp)
    by(case_tac "binop bop a aa",simp+)
  thus ?case apply - 
  proof(erule disjE)+
    assume "state_check cf b1 None ∧ v' = None"
    hence check:"state_check cf b1 None" and "v' = None" by simp_all
    from IH1[OF check ‹∀V ∈ fv b1. cf V = cf' V›] have "state_check cf' b1 None" .
    with ‹v' = None› show ?case by simp
  next
    assume "state_check cf b2 None ∧ v' = None"
    hence check:"state_check cf b2 None" and "v' = None" by simp_all
    from IH2[OF check ‹∀V ∈ fv b2. cf V = cf' V›] have "state_check cf' b2 None" .
    with ‹v' = None› show ?case by(cases "interpret b1 cf'") simp+
  next
    assume "∃v⇩1 v⇩2. state_check cf b1 (Some v⇩1) ∧
      state_check cf b2 (Some v⇩2) ∧ binop bop v⇩1 v⇩2 = v'"
    then obtain v⇩1 v⇩2 where "state_check cf b1 (Some v⇩1)"
      and "state_check cf b2 (Some v⇩2)" and "binop bop v⇩1 v⇩2 = v'" by blast
    from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b1. cf V = cf' V"
      by simp
    from IH1[OF ‹state_check cf b1 (Some v⇩1)› this]
    have "interpret b1 cf' = Some v⇩1" .
    from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b2. cf V = cf' V"
      by simp
    from IH2[OF ‹state_check cf b2 (Some v⇩2)› this] 
    have "interpret b2 cf' = Some v⇩2" .
    with ‹interpret b1 cf' = Some v⇩1› ‹binop bop v⇩1 v⇩2 = v'›
    show ?thesis by(cases v') simp+
  qed
qed



lemma PCFG_CallEdge_THE_es:
  "prog ⊢ n -CEdge(p,es,rets)→⇩p n'
⟹ (THE es'. ∃p' rets' n'. prog ⊢ n -CEdge(p',es',rets')→⇩p n') = es"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq)


definition ParamUses_proc :: "cmd ⇒ label ⇒ vname set list"
  where "ParamUses_proc c n ≡
  if (∃n' p' es' rets'. c ⊢ n -CEdge(p',es',rets')→⇩p n') then 
  (map fv (THE es'. ∃p' rets' n'. c ⊢ n -CEdge(p',es',rets')→⇩p n'))
  else []"


definition ParamUses :: "wf_prog ⇒ node ⇒ vname set list"
  where "⋀wfp. ParamUses wfp n ≡ let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (if (p = Main) then ParamUses_proc prog l
   else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
         then ParamUses_proc (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) l
         else []))"


lemma ParamUses_Main_Return_target:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -CEdge(p',es,rets)→⇩p n' ⟧
  ⟹ ParamUses wfp (Main,n) = map fv es"
  by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_Return_target:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -CEdge(p',es,rets)→⇩p n'"
  shows "ParamUses wfp (p,n) = map fv es"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce  
  moreover
  from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_IEdge_Nil:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -IEdge et→⇩p n'⟧
  ⟹ ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
            simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_IEdge_Nil:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -IEdge et→⇩p n'"
  shows "ParamUses wfp (p,n) = []"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce  
  moreover
  from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
                simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_CEdge_Nil:
  fixes wfp
  shows "⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n' -CEdge(p',es,rets)→⇩p n⟧
  ⟹ ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_CEdge_Nil:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n' -CEdge(p',es,rets)→⇩p n"
  shows "ParamUses wfp (p,n) = []"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce  
  moreover
  from ‹well_formed procs› 
    ‹(p,ins,outs,c) ∈ set procs›
  have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamUses_def ParamUses_proc_def)
qed


subsubsection ‹‹Def››

fun lhs :: "cmd ⇒ vname set"
where
  "lhs Skip                = {}"
  | "lhs (V:=e)              = {V}"
  | "lhs (c⇩1;;c⇩2)            = lhs c⇩1"
  | "lhs (if (b) c⇩1 else c⇩2) = {}"
  | "lhs (while (b) c)       = {}"
  | "lhs (Call p es rets)    = {}"

lemma lhs_fst_cmd:"lhs (fst_cmd c) = lhs c" by(induct c) auto

lemma Proc_CFG_Call_source_empty_lhs:
  assumes "prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'"
  shows "lhs (label prog l) = {}"
proof -
  from ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'› have "l < #:prog"
    by(rule Proc_CFG_sourcelabel_less_num_nodes)
  then obtain c' where "labels prog l c'"
    by(erule less_num_inner_nodes_label)
  hence "label prog l = c'" by(rule labels_label)
  from ‹labels prog l c'› ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'›
  have "∃p es rets. fst_cmd c' = Call p es rets" 
    by(rule Proc_CFG_Call_source_fst_cmd_Call)
  with lhs_fst_cmd[of c'] have "lhs c' = {}" by auto
  with ‹label prog l = c'› show ?thesis by simp
qed


lemma in_procs_THE_in_procs_ins:
  "⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
  ⟹ (THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs) = ins"
  by(fastforce intro:the_equality)


definition Def :: "wf_prog ⇒ node ⇒ vname set"
  where "⋀wfp. Def wfp n ≡ (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (case l of Label lx ⇒ 
    (if p = Main then lhs (label prog lx)
     else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
           then 
  lhs (label (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) lx)
           else {}))
  | Entry ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
            then (set 
      (THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs)) else {}
  | Exit ⇒ {}))
    ∪ set (ParamDefs wfp n)"

lemma Entry_Def_empty:
  fixes wfp
  shows "Def wfp (Main, Entry) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed


lemma Exit_Def_empty:
  fixes wfp
  shows "Def wfp (Main, Exit) = {}"
  proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis 
    by(auto dest:Proc_CFG_Call_Labels simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed



subsubsection ‹‹Use››

fun rhs :: "cmd ⇒ vname set"
where
  "rhs Skip                = {}"
  | "rhs (V:=e)              = fv e"
  | "rhs (c⇩1;;c⇩2)            = rhs c⇩1"
  | "rhs (if (b) c⇩1 else c⇩2) = fv b"
  | "rhs (while (b) c)       = fv b"
  | "rhs (Call p es rets)    = {}"

lemma rhs_fst_cmd:"rhs (fst_cmd c) = rhs c" by(induct c) auto

lemma Proc_CFG_Call_target_empty_rhs:
  assumes "prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'"
  shows "rhs (label prog l') = {}"
proof -
  from ‹prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'› have "l' < #:prog"
    by(rule Proc_CFG_targetlabel_less_num_nodes)
  then obtain c' where "labels prog l' c'"
    by(erule less_num_inner_nodes_label)
  hence "label prog l' = c'" by(rule labels_label)
  from ‹labels prog l' c'› ‹prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'›
  have "fst_cmd c' = Skip" by(rule Proc_CFG_Call_target_fst_cmd_Skip)
  with rhs_fst_cmd[of c'] have "rhs c' = {}" by simp
  with ‹label prog l' = c'› show ?thesis by simp
qed



lemma in_procs_THE_in_procs_outs:
  "⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
  ⟹ (THE outs'. ∃c' ins'. (p,ins',outs',c') ∈ set procs) = outs"
  by(fastforce intro:the_equality)


definition Use :: "wf_prog ⇒ node ⇒ vname set"
  where "⋀wfp. Use wfp n ≡ (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (case l of Label lx ⇒ 
    (if p = Main then rhs (label prog lx) 
     else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
           then 
  rhs (label (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) lx)
           else {}))
  | Exit ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
            then (set (THE outs'. ∃c' ins'. (p,ins',outs',c') ∈ set procs) )
            else {}
  | Entry ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
      then (set (THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs))
      else {}))
  ∪ Union (set (ParamUses wfp n)) ∪ set (ParamDefs wfp n)"


lemma Entry_Use_empty:
  fixes wfp
  shows "Use wfp (Main, Entry) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto dest:Proc_CFG_Call_Labels 
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed

lemma Exit_Use_empty:
  fixes wfp
  shows "Use wfp (Main, Exit) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto dest:Proc_CFG_Call_Labels 
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed


subsection ‹Lemmas about edges and call frames›

lemmas transfers_simps = ProcCFG.transfer.simps[simplified]
declare transfers_simps [simp]

abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val"
  where "state_val s V ≡ (fst (hd s)) V"

lemma Proc_CFG_edge_no_lhs_equal:
  fixes wfp
  assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "V ∉ lhs (label prog l)"
  shows "state_val (CFG.transfer (lift_procs wfp) et (cf#cfs)) V = fst cf V"
proof -
  from ‹prog ⊢ Label l -IEdge et→⇩p n'› 
  obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
  from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x› ‹V ∉ lhs (label prog l)›
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case (Proc_CFG_LAss V' e)
    have "labels (V':=e) 0 (V':=e)" by(rule Labels_Base)
    hence "label (V':=e) 0 = (V':=e)" by(rule labels_label)
    have "V' ∈ lhs (V':=e)" by simp
    with ‹V ∉ lhs (label (V':=e) 0)›
      ‹IEdge et = IEdge ⇑λcf. update cf V' e› ‹label (V':=e) 0 = (V':=e)›
    show ?case by fastforce
  next
    case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
    note IH = ‹⟦IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹c⇩1 ⊢ Label l -et'→⇩p n'› have "l < #:c⇩1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    hence "label (c⇩1;;c⇩2) l = c';;c⇩2" by(rule labels_label)
    with ‹V ∉ lhs (label (c⇩1;; c⇩2) l)› ‹labels c⇩1 l c'› 
    have "V ∉ lhs (label c⇩1 l)" by(fastforce dest:labels_label)
    with ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
    note IH = ‹⟦IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹c⇩1 ⊢ Label l -et'→⇩p Exit› have "l < #:c⇩1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    hence "label (c⇩1;;c⇩2) l = c';;c⇩2" by(rule labels_label)
    with ‹V ∉ lhs (label (c⇩1;; c⇩2) l)› ‹labels c⇩1 l c'› 
    have "V ∉ lhs (label c⇩1 l)" by(fastforce dest:labels_label)
    with ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1 l)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩2 l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹n ⊕ #:c⇩1 = Label l› obtain l' 
      where "n = Label l'" and "l = l' + #:c⇩1" by(cases n) auto
    from ‹n = Label l'› ‹c⇩2 ⊢ n -et'→⇩p n'› have "l' < #:c⇩2"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'" 
      by(fastforce intro:Labels_Seq2)
    hence "label (c⇩1;;c⇩2) l = c'" by(rule labels_label)
    with ‹V ∉ lhs (label (c⇩1;;c⇩2) l)› ‹labels c⇩2 l' c'› ‹l = l' + #:c⇩1›
    have "V ∉ lhs (label c⇩2 l')" by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2 l)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹n ⊕ 1 = Label l› obtain l' 
      where "n = Label l'" and "l = l' + 1" by(cases n) auto
    from ‹n = Label l'› ‹c⇩1 ⊢ n -et'→⇩p n'› have "l' < #:c⇩1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    hence "label (if (b) c⇩1 else c⇩2) l = c'" by(rule labels_label)
    with ‹V ∉ lhs (label (if (b) c⇩1 else c⇩2) l)› ‹labels c⇩1 l' c'› ‹l = l' + 1›
    have "V ∉ lhs (label c⇩1 l')" by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1 l)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩2 l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹n ⊕ #:c⇩1 + 1 = Label l› obtain l' 
      where "n = Label l'" and "l = l' + #:c⇩1 + 1" by(cases n) auto
    from ‹n = Label l'› ‹c⇩2 ⊢ n -et'→⇩p n'› have "l' < #:c⇩2"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    hence "label (if (b) c⇩1 else c⇩2) l = c'" by(rule labels_label)
    with ‹V ∉ lhs (label (if (b) c⇩1 else c⇩2) l)› ‹labels c⇩2 l' c'› ‹l = l' + #:c⇩1 + 1›
    have "V ∉ lhs (label c⇩2 l')" by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBody c' n et' n' b l)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c' l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹n ⊕ 2 = Label l› obtain l' 
      where "n = Label l'" and "l = l' + 2" by(cases n) auto
    from ‹n = Label l'› ‹c' ⊢ n -et'→⇩p n'› have "l' < #:c'"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
    with ‹V ∉ lhs (label (while (b) c') l)› ‹labels c' l' cx› ‹l = l' + 2›
    have "V ∉ lhs (label c' l')" by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b l)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c' l)⟧
      ⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
    from ‹n ⊕ 2 = Label l› obtain l' 
      where "n = Label l'" and "l = l' + 2" by(cases n) auto
    from ‹n = Label l'› ‹c' ⊢ n -et'→⇩p Exit› have "l' < #:c'"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
    with ‹V ∉ lhs (label (while (b) c') l)› ‹labels c' l' cx› ‹l = l' + 2›
    have "V ∉ lhs (label c' l')" by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  qed auto
qed



lemma Proc_CFG_edge_uses_only_rhs:
  fixes wfp
  assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "CFG.pred et s"
  and "CFG.pred et s'" and "∀V∈rhs (label prog l). state_val s V = state_val s' V"
  shows "∀V∈lhs (label prog l). 
    state_val (CFG.transfer (lift_procs wfp) et s) V =
    state_val (CFG.transfer (lift_procs wfp) et s') V"
proof -
  from ‹prog ⊢ Label l -IEdge et→⇩p n'› 
  obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
  from ‹CFG.pred et s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from ‹CFG.pred et s'› obtain cf' cfs' where [simp]:"s' = cf'#cfs'" 
    by(cases s') auto
  from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x›
    ‹∀V∈rhs (label prog l). state_val s V = state_val s' V›
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case Proc_CFG_Skip
    have "labels Skip 0 Skip" by(rule Labels_Base)
    hence "label Skip 0 = Skip" by(rule labels_label)
    hence "∀V. V ∉ lhs (label Skip 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_LAss V e)
    have "labels (V:=e) 0 (V:=e)" by(rule Labels_Base)
    hence "label (V:=e) 0 = V:=e" by(rule labels_label)
    then have "lhs (label (V:=e) 0) = {V}"
      and "rhs (label (V:=e) 0) = fv e" by auto
    with ‹IEdge et = IEdge ⇑λcf. update cf V e› 
      ‹∀V∈rhs (label (V:=e) 0). state_val s V = state_val s' V›
    show ?case by(fastforce intro:rhs_interpret_eq)
  next
    case (Proc_CFG_LAssSkip V e)
    have "labels (V:=e) 1 Skip" by(rule Labels_LAss)
    hence "label (V:=e) 1 = Skip" by(rule labels_label)
    hence "∀V'. V' ∉ lhs (label (V:=e) 1)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
    note IH = ‹⟦IEdge et = et'; 
      ∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹c⇩1 ⊢ Label l -et'→⇩p n'›
    have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹IEdge et = et'›
    have "∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c⇩1 l c'› ‹labels (c⇩1;;c⇩2) l (c';;c⇩2)›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
    note IH = ‹⟦IEdge et = et'; 
      ∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹c⇩1 ⊢ Label l -et'→⇩p Exit›
    have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹IEdge et = et'›
    have "∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c⇩1 l c'› ‹labels (c⇩1;;c⇩2) l (c';;c⇩2)›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; 
      ∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c⇩2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹n ⊕ #:c⇩1 = Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1"
      by(cases n) auto
    from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'" by(fastforce intro:Labels_Seq2)
    with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (c⇩1;;c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'›
    have "∀V∈lhs (label c⇩2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c⇩2 l' c'› ‹labels (c⇩1;;c⇩2) l c'›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CondTrue b c⇩1 c⇩2)
    have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
    hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (if (b) c⇩1 else c⇩2) 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_CondFalse b c⇩1 c⇩2)
    have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
    hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (if (b) c⇩1 else c⇩2) 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; 
      ∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹n ⊕ 1 = Label l› obtain l' where "n = Label l'" and "l = l' + 1"
      by(cases n) auto
    from ‹c⇩1 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    with ‹labels c⇩1 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'›
    have "∀V∈lhs (label c⇩1 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c⇩1 l' c'› ‹labels (if (b) c⇩1 else c⇩2) l c'›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c⇩2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹n ⊕ #:c⇩1 + 1= Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1+1"
      by(cases n) auto
    from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l). 
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'›
    have "∀V∈lhs (label c⇩2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c⇩2 l' c'› ‹labels (if (b) c⇩1 else c⇩2) l c'›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_WhileTrue b c')
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (while (b) c') 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileFalse b c')
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (while (b) c') 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileFalseSkip b c')
    have "labels (while (b) c') 1 Skip" by(rule Labels_WhileExit)
    hence "label (while (b) c') 1 = Skip" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (while (b) c') 1)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileBody c' n et' n' b)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from ‹c' ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l). 
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'›
    have "∀V∈lhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c' l' cx› ‹labels (while (b) c') l (cx;;while (b) c')›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
      ⟹ ∀V∈lhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V›
    from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from ‹c' ⊢ n -et'→⇩p Exit› ‹n = Label l'›
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l).
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'›
    have "∀V∈lhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with ‹labels c' l' cx› ‹labels (while (b) c') l (cx;;while (b) c')›
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CallSkip p es rets)
    have "labels (Call p es rets) 1 Skip" by(rule Labels_Call)
    hence "label (Call p es rets) 1 = Skip" by(rule labels_label)
    hence "∀V. V ∉ lhs (label (Call p es rets) 1)" by simp
    then show ?case by fastforce
  qed auto
qed


lemma Proc_CFG_edge_rhs_pred_eq:
  assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "CFG.pred et s"
  and "∀V∈rhs (label prog l). state_val s V = state_val s' V"
  and "length s = length s'"
  shows "CFG.pred et s'"
proof -
  from ‹prog ⊢ Label l -IEdge et→⇩p n'› 
  obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
  from ‹CFG.pred et s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from ‹length s = length s'› obtain cf' cfs' where [simp]:"s' = cf'#cfs'" 
    by(cases s') auto
  from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x› 
    ‹∀V∈rhs (label prog l). state_val s V = state_val s' V›
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
    note IH = ‹⟦IEdge et = et'; ∀V∈rhs (label c⇩1 l). 
      state_val s V = state_val s' V⟧ ⟹ CFG.pred et s'›
    from ‹c⇩1 ⊢ Label l -et'→⇩p n'›
    have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
    note IH = ‹⟦IEdge et = et'; 
      ∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
      ⟹ CFG.pred et s'›
    from ‹c⇩1 ⊢ Label l -et'→⇩p Exit›
    have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
    with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧ 
      ⟹ CFG.pred et s'›
    from ‹n ⊕ #:c⇩1 = Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1"
      by(cases n) auto
    from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'" by(fastforce intro:Labels_Seq2)
    with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (c⇩1;;c⇩2) l). state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_CondTrue b c⇩1 c⇩2)
    from ‹CFG.pred et s› ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
    have "state_check (fst cf) b (Some true)" by simp
    moreover
    have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
    hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
    with ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) 0). state_val s V = state_val s' V›
    have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some true)" 
      by simp(rule rhs_interpret_eq)
    with ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
    show ?case by simp
  next
    case (Proc_CFG_CondFalse b c⇩1 c⇩2)
    from ‹CFG.pred et s› 
      ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
    have "state_check (fst cf) b (Some false)" by simp
    moreover
    have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
    hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
    with ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) 0). state_val s V = state_val s' V›
    have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some false)" 
      by simp(rule rhs_interpret_eq)
    with ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√› 
    show ?case by simp
  next
    case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧ 
      ⟹ CFG.pred et s'›
    from ‹n ⊕ 1 = Label l› obtain l' where "n = Label l'" and "l = l' + 1"
      by(cases n) auto
    from ‹c⇩1 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    with ‹labels c⇩1 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l). 
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩1 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧ 
      ⟹ CFG.pred et s'›
    from ‹n ⊕ #:c⇩1 + 1= Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1+1"
      by(cases n) auto
    from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
    with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l). 
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_WhileTrue b c')
    from ‹CFG.pred et s› ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
    have "state_check (fst cf) b (Some true)" by simp
    moreover
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    with ‹∀V∈rhs (label (while (b) c') 0). state_val s V = state_val s' V› 
    have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some true)" 
      by simp(rule rhs_interpret_eq)
    with ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
    show ?case by simp
  next
    case (Proc_CFG_WhileFalse b c')
    from ‹CFG.pred et s›
      ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
    have "state_check (fst cf) b (Some false)" by simp
    moreover
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    with ‹∀V∈rhs (label (while (b) c') 0). state_val s V = state_val s' V› 
    have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some false)" 
      by simp(rule rhs_interpret_eq)
    with ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
    show ?case by simp
  next
    case (Proc_CFG_WhileBody c' n et' n' b)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c' l). state_val s V = state_val s' V⟧ 
      ⟹ CFG.pred et s'›
    from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from ‹c' ⊢ n -et'→⇩p n'› ‹n = Label l'›
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l). 
      state_val s V = state_val s' V›
    have "∀V∈rhs (label c' l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b)
    note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
      ∀V∈rhs (label c' l). state_val s V = state_val s' V⟧ 
      ⟹ CFG.pred et s'›
    from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from ‹c' ⊢ n -et'→⇩p Exit› ‹n = Label l'›
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l). 
      state_val s