Theory EgHighBranchRevC

theory EgHighBranchRevC
imports Dependent_SIFUM_Type_Systems.Compositionality
        Dependent_SIFUM_Type_Systems.Language
        "HOL-Eisbach.Eisbach_Tools"
        "../CompositionalRefinement"
begin

text ‹
  Theory for exploring refinement of a program that branches on a high variable.

  The purpose of this particular example is to demonstrate that in order to prove any branching
  on a High-classified variable remains safe when refined to a concrete implementation, it is
  necessary to ensure that the two concrete branches of execution take the same number of steps,
  possibly by skip-padding the one with less steps in it, and provide an appropriate coupling
  invariant to link the corresponding concrete steps of the two branches of the if-statement.
›

type_synonym 'var addr = 'var
type_synonym val = nat
type_synonym 'var mem = "'var addr  val"

(* Arithmetic expression evaluation *)
datatype 'var aexp = Const "val" |
                     Load "'var addr" |
                     Add "'var aexp" "'var aexp" |
                     Sub "'var aexp" "'var aexp"

fun
  evA :: "'var mem  'var aexp  val"
where
  "evA mem (Const v) = v" |
  "evA mem (Load x) = mem x" |
  "evA mem (Add x y) = evA mem x + evA mem y" |
  "evA mem (Sub x y) = evA mem x - evA mem y"

(* Boolean expression evaluation *)
datatype 'var bexp = Eq "'var aexp" "'var aexp" |
                     Neq "'var aexp" "'var aexp" |
                     Lte "'var aexp" "'var aexp" |
                     Gt "'var aexp" "'var aexp"

fun
  evB :: "'var mem  'var bexp  bool"
where
  "evB mem (Eq x y) = (evA mem x = evA mem y)" |
  "evB mem (Neq x y) = (evA mem x  evA mem y)" |
  "evB mem (Lte x y) = (evA mem x  evA mem y)" |
  "evB mem (Gt x y) = (evA mem x > evA mem y)"

(* Function that gives the control variables of a given variable.
 * None for this example. *)
definition
  𝒞_vars :: "'var addr  'var addr set"
where
  "𝒞_vars x  {}"

(* NB: mds ~ "mode state"
 * mdss is the initial mode state *)
definition
  mdss :: "Mode  'var set"
where
  "mdss  λm. case m of AsmNoReadOrWrite  {} | _  {}"

primrec
  aexp_vars :: "'var aexp  'var set"
where
  "aexp_vars (Const _) = {}" |
  "aexp_vars (Load v) = {v}" |
  "aexp_vars (Add x y) = aexp_vars x  aexp_vars y" |
  "aexp_vars (Sub x y) = aexp_vars x  aexp_vars y"

fun
  bexp_vars :: "'var bexp  'var addr set"
where
  "bexp_vars (Neq x y) = aexp_vars x  aexp_vars y" |
  "bexp_vars (Eq x y) = aexp_vars x  aexp_vars y" |
  "bexp_vars (Lte x y) = aexp_vars x  aexp_vars y" |
  "bexp_vars (Gt x y) = aexp_vars x  aexp_vars y"

fun
  bexp_neg :: "'var bexp  'var bexp"
where
  "bexp_neg (Neq x y) = (Eq x y)" |
  "bexp_neg (Eq x y) = (Neq x y)" |
  "bexp_neg (Lte x y) = (Gt x y)" |
  "bexp_neg (Gt x y) = (Lte x y)"

fun
  bexp_assign :: "'var addr  'var aexp  'var bexp"
where
  "bexp_assign x a = (Eq (Load x) a)"

datatype var = h_var | x_var | y_var | z_var

definition
  dma :: "var mem  var addr  Sec"
where
  "dma m x  if x = h_var then High else Low"

type_synonym t_evA = "var mem  var aexp  val"
type_synonym t_evB = "var mem  var bexp  bool"
type_synonym t_aexp_vars = "var aexp  var set"
type_synonym t_bexp_vars = "var bexp  var addr set"

locale sifum_example =
  sifum_lang_no_dma "evA::t_evA" "evB::t_evB" "aexp_vars::t_aexp_vars" "bexp_vars::t_bexp_vars" +
  assumes eval_det: "(lc, lc')  evalw  (lc, lc'')  evalw  lc' = lc''"

definition
  𝒞 :: "var addr set"
where
  "𝒞  x. 𝒞_vars x"

sublocale sifum_example   sifum_security dma 𝒞_vars 𝒞 evalw undefined
  apply(unfold_locales)
       apply(blast intro: eval_det)
      apply(rule Var_finite)
     apply(auto simp: 𝒞_vars_def dma_def 𝒞_def split: if_splits)[3]
  apply(auto simp: 𝒞_def)
  done

context sifum_example begin
(*
  y := 0; z := 0;
  x := y;
  if h then x := y
       else x := y + z

  Must have NoWrite z to prevent an agent getting something observable by spiking the value of z.
  Also take NoWrite y & h to simplify reasoning about reg values staying consistent with the mem.
 *)
definition
  prog_high_branch :: "(var addr, var aexp, var bexp) Stmt"
where
  "prog_high_branch 
     ModeDecl Skip (Acq h_var AsmNoWrite) ;;
     ModeDecl Skip (Acq y_var AsmNoWrite) ;;
     ModeDecl Skip (Acq z_var AsmNoWrite) ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     )"
end

datatype varC = h_mem | x_mem | y_mem | z_mem | reg0 | reg1 | reg2 | reg3

definition
  dmaC :: "varC mem  varC addr  Sec"
where
  "dmaC m x  if x = h_mem then High else Low"

type_synonym t_evAC = "varC mem  varC aexp  val"
type_synonym t_evBC = "varC mem  varC bexp  bool"
type_synonym t_aexp_varsC = "varC aexp  varC set"
type_synonym t_bexp_varsC = "varC bexp  varC addr set"

locale sifum_exampleC =
  sifum_lang_no_dma "evA::t_evAC" "evB::t_evBC" "aexp_vars::t_aexp_varsC" "bexp_vars::t_bexp_varsC" +
  assumes eval_det: "(lc, lc')  evalw  (lc, lc'')  evalw  lc' = lc''"

definition
  𝒞C :: "varC addr set"
where
  "𝒞C  x. 𝒞_vars x"

sublocale sifum_exampleC   sifum_security dmaC 𝒞_vars 𝒞C evalw undefined
  apply(unfold_locales)
       apply(blast intro: eval_det)
      apply(rule Var_finite)
     apply(auto simp: 𝒞_vars_def dmaC_def 𝒞_def split: if_splits)[3]
  apply(auto simp: 𝒞C_def)
  done

context sifum_exampleC begin
(*
  y := 0; z := 0;
  x := y;
  if h
    then
      // "then"-branch: x := y
      NOP ;
      NOP ;
      LOAD r0 y ;
      STORE x r0 ;
    else
      // "else"-branch: x := y + z
      LOAD r1 y ;
      LOAD r2 z ;
      ADD r0 r1 r2 ;
      STORE x r0 ;
 *)
definition
  prog_high_branchC :: "(varC addr, varC aexp, varC bexp) Stmt"
where
  "prog_high_branchC 
     ModeDecl Skip (Acq h_mem AsmNoWrite) ;;
     ModeDecl Skip (Acq y_mem AsmNoWrite) ;;
     ModeDecl Skip (Acq z_mem AsmNoWrite) ;;
     ― ‹Just set up the memory to match our assumptions›
     Assign y_mem (Const 0) ;;
     Assign z_mem (Const 0) ;;
     Assign x_mem (Load y_mem) ;;
     ― ‹From this point onwards we model the if-statement using registers.›
     ― ‹Note that we can just as well (re-)use reg0 instead of reg3 - verify with a search-replace.›
     ― ‹Leaving it this way to make the reg usages easier to distinguish for the reader, though.›
     Assign reg3 (Load h_mem) ;;
     If (Neq (Load reg3) (Const 0)) (
       Skip ;;
       Skip ;;
       Assign reg0 (Load y_mem) ;;
       Assign x_mem (Load reg0)
     ) (
       Assign reg1 (Load y_mem) ;;
       Assign reg2 (Load z_mem) ;;
       Assign reg0 (Add (Load reg1) (Load reg2)) ;;
       Assign x_mem (Load reg0)
     )"
end

context sifum_example begin
lemma 𝒞_simp[simp]:
  "𝒞 = {}"
  by(auto simp: 𝒞_def 𝒞_vars_def split: if_splits)

declare 𝒞_vars_def [simp]

(* Manual proof of bisimulation because we can't use the type system *)
inductive inv :: "(((var addr, var aexp, var bexp) Stmt, var addr, val) LocalConf)  bool"
where
  inv1h: "c = prog_high_branch; mds AsmNoReadOrWrite = {}; mds AsmNoWrite = {}  inv c, mds, mem" |
  inv1h': "c =
     Stop ;;
     ModeDecl Skip (Acq y_var AsmNoWrite) ;;
     ModeDecl Skip (Acq z_var AsmNoWrite) ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv1y: "c =
     ModeDecl Skip (Acq y_var AsmNoWrite) ;;
     ModeDecl Skip (Acq z_var AsmNoWrite) ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv1y': "c =
     Stop ;;
     ModeDecl Skip (Acq z_var AsmNoWrite) ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv1z: "c =
     ModeDecl Skip (Acq z_var AsmNoWrite) ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv1z': "c =
     Stop ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv2: "c =
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv2': "c =
     Stop ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv3: "c =
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {} 
   inv c, mds, mem" |
  inv3': "c =
     Stop ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv4: "c =
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv4': "c =
     Stop ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv5: "c =
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ); mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv5_then: "c = Assign x_var (Load y_var);
     mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv5_else: "c = Assign x_var (Add (Load y_var) (Load z_var));
     mds AsmNoWrite = {z_var, y_var, h_var}; mds AsmNoReadOrWrite = {}; mem z_var = 0 
   inv c, mds, mem" |
  inv6: "c = Stop 
   inv c, mds, mem"

definition z_locked_steps
where "z_locked_steps  {
     Stop ;;
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ),
     Assign y_var (Const 0) ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ),
     Stop ;;
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     ),
     Assign z_var (Const 0) ;;
     Assign x_var (Load y_var) ;;
     If (Neq (Load h_var) (Const 0)) (
       Assign x_var (Load y_var)
     ) (
       Assign x_var (Add (Load y_var) (Load z_var))
     )}"

inductive_set rel_inv :: "(((var addr, var aexp, var bexp) Stmt, var addr, val) LocalConf) rel"
where
  rel_inv_if:
  "c = Assign x_var (Load y_var);
    c' = Assign x_var (Add (Load y_var) (Load z_var));
    z_var  mds AsmNoWrite; mds AsmNoReadOrWrite = {}; mem z_var = mem' z_var 
      (c, mds, mem, c', mds', mem')  rel_inv" |
  rel_inv_if':
  "c' = Assign x_var (Load y_var);
    c = Assign x_var (Add (Load y_var) (Load z_var));
    z_var  mds AsmNoWrite; mds AsmNoReadOrWrite = {}; mem z_var = mem' z_var 
      (c, mds, mem, c', mds', mem')  rel_inv" |
  rel_inv_start:
  "c = c'; z_var  mds AsmNoWrite; mds AsmNoReadOrWrite = {} 
      (c, mds, mem, c', mds', mem')  rel_inv" |
  rel_inv_z_locked:
  "c  z_locked_steps;
    c = c'; z_var  mds AsmNoWrite; mds AsmNoReadOrWrite = {} 
      (c, mds, mem, c', mds', mem')  rel_inv" |
  rel_inv_z_initted:
  "c  z_locked_steps;
    c = c'; mem z_var = mem' z_var; z_var  mds AsmNoWrite; mds AsmNoReadOrWrite = {} 
      (c, mds, mem, c', mds', mem')  rel_inv"

declare z_locked_steps_def[simp add]

(* the bisimulation is phrased as a conjunction of a global invariant and a
   relational invariant, defined above, plus the background requirement
   of low-equivalence modulo modes *)
inductive_set  R :: "(((var addr, var aexp, var bexp) Stmt, var addr, val) LocalConf) rel"
where
(* Having a c = c' requirement here is actually too restrictive *)
  "mds = mds'; low_mds_eq mds mem mem'; inv c,mds,mem; inv c',mds',mem';
    (c, mds, mem, c', mds', mem')  rel_inv 
 (c, mds, mem, c', mds', mem')  R"

lemma rel_inv_sym:
  "low_mds_eq mds mem mem'  (c, mds, mem, c, mds, mem')  rel_inv 
    (c, mds, mem', c, mds, mem)  rel_inv"
  apply(auto elim!: rel_inv.cases intro: rel_inv.intros)
  done

lemma R_sym':
  "(c, mds, mem, c', mds', mem')  R 
   (c', mds', mem', c, mds, mem)  R"
  apply(rule R.intros)
      apply(blast elim: R.cases dest: low_mds_eq_sym dest: rel_inv_sym)+
  apply(erule R.cases)
  apply(erule rel_inv.cases)
      apply clarsimp
      apply(rule rel_inv_if', simp+)
     apply(rule rel_inv_if, simp+)
    apply(rule rel_inv_start, simp+)
   apply(rule rel_inv_z_locked, simp+)
  apply(rule rel_inv_z_initted, simp+)
  done

lemma R_sym:
  "sym R"
  by(rule symI, clarify, erule R_sym')

lemma inv_closed_glob_consistent:
  "inv c', mds', mem 
       x. case A x of None  True | Some (v, v')  mem x  v  ¬ var_asm_not_written mds' x 
       x. dma mem [∥1 A] x  dma mem x  ¬ var_asm_not_written mds' x  
       inv c', mds', mem [∥1 A]"
  apply(erule inv.cases)
             using inv.intros apply (force, force, force, force, force, force, force, force, force)
        apply(rule inv3', clarsimp+)
        apply(erule_tac x=z_var in allE)
        apply(erule_tac x=z_var in allE)
        apply(cases "A z_var")
         apply(simp add:apply_adaptation_def)
        apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
       apply(rule inv4, clarsimp+)
       apply(erule_tac x=z_var in allE)
       apply(erule_tac x=z_var in allE)
       apply(cases "A z_var")
        apply(simp add:apply_adaptation_def)
       apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
      apply(rule inv4', clarsimp+)
      apply(erule_tac x=z_var in allE)
      apply(erule_tac x=z_var in allE)
      apply(cases "A z_var")
       apply(simp add:apply_adaptation_def)
      apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
     apply(rule inv5, clarsimp+)
     apply(erule_tac x=z_var in allE)
     apply(erule_tac x=z_var in allE)
     apply(cases "A z_var")
      apply(simp add:apply_adaptation_def)
     apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
    apply(rule inv5_then, clarsimp+)
    apply(erule_tac x=z_var in allE)
    apply(erule_tac x=z_var in allE)
    apply(cases "A z_var")
     apply(simp add:apply_adaptation_def)
    apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
   apply(rule inv5_else, clarsimp+)
   apply(erule_tac x=z_var in allE)
   apply(erule_tac x=z_var in allE)
   apply(cases "A z_var")
    apply(simp add:apply_adaptation_def)
   apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
  apply(rule inv6, clarsimp+)
  done

(* The "right-hand" side of inv_closed_glob_consistent *)
lemma inv_closed_glob_consistent_r:
  "inv c', mds', mem 
       x. case A x of None  True | Some (v, v')  mem x  v'  ¬ var_asm_not_written mds' x 
       x. dma mem [∥2 A] x  dma mem x  ¬ var_asm_not_written mds' x  
       inv c', mds', mem [∥2 A]"
  apply(erule inv.cases)
               using inv.intros apply (force, force, force, force, force, force, force, force, force)
        apply(rule inv3', clarsimp+)
        apply(erule_tac x=z_var in allE)
        apply(erule_tac x=z_var in allE)
        apply(cases "A z_var")
         apply(simp add:apply_adaptation_def)
        apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
       apply(rule inv4, clarsimp+)
       apply(erule_tac x=z_var in allE)
       apply(erule_tac x=z_var in allE)
       apply(cases "A z_var")
        apply(simp add:apply_adaptation_def)
       apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
      apply(rule inv4', clarsimp+)
      apply(erule_tac x=z_var in allE)
      apply(erule_tac x=z_var in allE)
      apply(cases "A z_var")
       apply(simp add:apply_adaptation_def)
      apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
     apply(rule inv5, clarsimp+)
     apply(erule_tac x=z_var in allE)
     apply(erule_tac x=z_var in allE)
     apply(cases "A z_var")
      apply(simp add:apply_adaptation_def)
     apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
    apply(rule inv5_then, clarsimp+)
    apply(erule_tac x=z_var in allE)
    apply(erule_tac x=z_var in allE)
    apply(cases "A z_var")
     apply(simp add:apply_adaptation_def)
    apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
   apply(rule inv5_else, clarsimp+)
   apply(erule_tac x=z_var in allE)
   apply(erule_tac x=z_var in allE)
   apply(cases "A z_var")
    apply(simp add:apply_adaptation_def)
   apply(clarsimp simp add:var_asm_not_written_def dma_def apply_adaptation_def)
  apply(rule inv6, clarsimp+)
  done

lemma rel_inv_closed_glob_consistent:
  "(c, mds', mem, c', mds', mem')  rel_inv 
       x a b.
          A x = Some (a, b) 
          (mem x = a  mem' x  b)  ¬ var_asm_not_written mds' x 
       x. dma mem [∥1 A] x  dma mem x  ¬ var_asm_not_written mds' x 
       x. dma mem [∥1 A] x = Low  (x  mds' AsmNoReadOrWrite  x  𝒞) 
           mem [∥1 A] x = mem' [∥2 A] x 
       (c, mds', mem [∥1 A], c', mds', mem' [∥2 A])  rel_inv"
  apply(safe elim!: rel_inv.cases)
  using rel_inv.intros dma_def by simp+

lemma R_closed_glob_consistent:
  "closed_glob_consistent R"
  unfolding closed_glob_consistent_def
  apply clarsimp
  apply(erule R.cases)
  apply clarsimp
  apply(rule R.intros)
      apply simp
     apply(fastforce simp: low_mds_eq_def)
    apply(rule inv_closed_glob_consistent)
      apply simp
     apply(fastforce split: option.splits)
    apply assumption
   apply(rule inv_closed_glob_consistent_r)
     apply simp
    apply(fastforce split: option.splits)
   apply(subgoal_tac "dma mem = dma mem'  dma mem [∥1 A] = dma mem' [∥2 A]")
    apply simp
   apply(rule conjI)
    apply(rule low_mds_eq_dma)
    apply assumption
   apply(rule dma_𝒞)
   apply(simp add: 𝒞_Low)
  apply(rule rel_inv_closed_glob_consistent)
  apply(simp_all)
  apply(fastforce split: option.splits)
  done

lemma R_low_mds_eq:
  "(c1, mds, mem1, c2, mds, mem2)  R 
        low_mds_eq mds mem1 mem2"
  apply(blast elim: R.cases)
  done

inductive_cases rel_invE: "(c, mds, mem, c', mds', mem')  rel_inv"

method seq_decl_inv_method uses inv_rule rel_inv_rule =
 (erule rel_invE, simp+,
   drule seq_elim, simp,
   clarsimp,
   drule upd_elim, drule skip_elim, simp,
   clarsimp,
   rule conjI,
    rule evalw.seq,
    rule decl_evalw', simp+,
   rule R.intros, simp+,
      fastforce simp: low_mds_eq_def,
     rule inv_rule, simp+,
    rule inv_rule, simp+,
   rule rel_inv_rule, simp+)

method seq_stop_inv_method uses inv_rule rel_inv_rule =
 (erule rel_invE, simp+,
   drule seq_stop_elim, clarsimp,
   (rule exI)+,
   intro conjI,
    rule seq_stop_evalw,
   rule R.intros, (simp|clarsimp simp: low_mds_eq_def dma_def evA.simps)+,
     (rule inv_rule; simp|blast?),
    (rule inv_rule; simp|blast?),
   rule rel_inv_rule, simp+)

method assign_inv6_method =
 (rule_tac x=c1' in exI,
  rule_tac x="mem2(x_var := evA mem2 (Load y_var))" in exI,
  erule rel_invE, simp+,
  (drule assign_elim, simp,
   rule conjI,
    clarsimp simp: evA.simps,
    erule_tac x=z_var in allE,
    clarsimp,
    rule assign_evalw', simp+,
    clarsimp simp: evA.simps,
   rule R.intros, simp+,
      unfold low_mds_eq_def dma_def, clarsimp simp: evA.simps,
     (rule inv6, simp+)+,
   rule rel_inv_z_initted, simp+)+)

lemma R_inv:
  notes evA.simps[simp del]
  shows  "(c1, mds, mem1, c2, mds, mem2)  R 
       (c1, mds, mem1, c1', mds', mem1')  evalw 
       c2' mem2'.
          (c2, mds, mem2, c2', mds', mem2')  evalw 
          (c1', mds', mem1', c2', mds', mem2')  R"
  apply(erule R.cases)
  apply clarsimp
  apply(erule inv.cases)
                 apply(unfold prog_high_branch_def)
                 apply clarsimp
                 apply(rule_tac x=c1' in exI)
                 apply(rule_tac x=mem2 in exI)
                 apply(seq_decl_inv_method inv_rule:inv1h' rel_inv_rule:rel_inv_start)
                apply(seq_stop_inv_method inv_rule:inv1y rel_inv_rule:rel_inv_start)
               apply(rule_tac x=c1' in exI)
               apply(rule_tac x=mem2 in exI)
               apply(seq_decl_inv_method inv_rule:inv1y' rel_inv_rule:rel_inv_start)
              apply(seq_stop_inv_method inv_rule:inv1z rel_inv_rule:rel_inv_start)
             apply(rule_tac x=c1' in exI)
             apply(rule_tac x=mem2 in exI)
             apply(seq_decl_inv_method inv_rule:inv1z' rel_inv_rule:rel_inv_z_locked)
            apply(seq_stop_inv_method inv_rule:inv2 rel_inv_rule:rel_inv_z_locked)

           (* Assign ;; *)
           apply clarsimp
           apply(rule_tac x=c1' in exI)
           apply(rule_tac x="mem2(y_var := evA mem2 (Const 0))" in exI)
           apply(erule rel_invE, simp+)
            apply(drule seq_elim, simp)
            apply clarsimp
            apply(drule assign_elim, simp)
            apply(rule conjI)
             apply(rule evalw.seq)
             apply(rule assign_evalw)
            apply(rule R.intros, simp+)
               apply(unfold low_mds_eq_def dma_def, clarsimp simp: evA.simps)
              apply(rule inv2', fast+)+
            apply(rule rel_inv_z_locked, simp+)
          apply(seq_stop_inv_method inv_rule:inv3 rel_inv_rule:rel_inv_z_locked)

         (* Assign ;; *)
         apply clarsimp
         apply(rule_tac x=c1' in exI)
         apply(rule_tac x="mem2(z_var := evA mem2 (Const 0))" in exI)
         apply(erule rel_invE, simp+)
          apply(drule seq_elim, simp)
          apply clarsimp
          apply(drule assign_elim, simp)
          apply(rule conjI)
           apply(rule evalw.seq)
           apply(rule assign_evalw)
          apply(rule R.intros, simp+)
             apply(unfold low_mds_eq_def dma_def, clarsimp simp: evA.simps)
            apply(rule inv3', simp+)
            apply(simp add: evA.simps)
           apply(rule inv3', simp+)
           apply(simp add: evA.simps)
          apply(rule rel_inv_z_initted, simp+)
            apply(simp add: evA.simps) (* do it separately so it doesn't mess everything else up *)
           apply simp+
        apply(seq_stop_inv_method inv_rule:inv4 rel_inv_rule:rel_inv_z_initted)

       (* Assign ;; *)
       apply clarsimp
       apply(rule_tac x=c1' in exI)
       apply(rule_tac x="mem2(x_var := evA mem2 (Load y_var))" in exI)
       apply(erule rel_invE, simp+)
       apply(drule seq_elim, simp)
       apply clarsimp
       apply(drule assign_elim, simp)
       apply(rule conjI)
        apply(rule evalw.seq)
        apply(rule assign_evalw)
       apply(rule R.intros, simp+)
          apply(unfold low_mds_eq_def dma_def, clarsimp simp: evA.simps)
         apply(rule inv4', simp+)+
       apply(rule rel_inv_z_initted, simp+)
      apply(seq_stop_inv_method inv_rule:inv5 rel_inv_rule:rel_inv_z_initted)

     (* (If (cond) Then Else) *)
     apply clarsimp
     apply(erule rel_invE, simp+)
     apply(rule_tac x="(if evB mem2 (Neq (Load h_var) (Const 0))
                        then (x_var  Load y_var)
                        else (x_var  Add (Load y_var) (Load z_var)))" in exI)
     apply(rule_tac x="mem2" in exI)
     apply(rule conjI)
       apply(erule if_elim)
        apply clarify
        apply(rule if_evalw)
       apply clarify
       apply(rule if_evalw)
      apply(erule if_elim)
       apply(rule R.intros, simp+)
          apply(unfold low_mds_eq_def dma_def, clarsimp)
         apply(rule inv5_then, simp+)
        apply safe
         apply(rule inv5_then, simp+)
        apply(rule inv5_else, simp+)
       apply safe
        apply(rule rel_inv_z_initted, simp+)
       apply(rule rel_inv_if, simp, simp, simp, simp, simp)
 
     apply(rule R.intros, simp+)
        apply(unfold low_mds_eq_def dma_def, clarsimp)
       apply(rule inv5_else, simp+)
      apply safe
       apply(rule inv5_then, simp+)
      apply(rule inv5_else, simp+)
     apply safe
      apply(rule rel_inv_if', simp+)
     apply(rule rel_inv_z_initted, simp+)
 
    (* Assign - then | else *)
    apply assign_inv6_method
   apply assign_inv6_method
  using stop_no_eval by fastforce

lemma strong_low_bisim_mm_R:
  "strong_low_bisim_mm R"
  unfolding strong_low_bisim_mm_def
  proof(safe)
    show "sym R" by(rule R_sym)
  next
    show "closed_glob_consistent R" by(rule R_closed_glob_consistent)
  next
    fix c1 mds mem1 c2  mem2
    assume "(c1, mds, mem1, c2, mds, mem2)  R"
    thus "low_mds_eq mds mem1 mem2"
    by(rule R_low_mds_eq)
  next
    fix c1 mds mem1 c2  mem2 c1' mds' mem1'
    assume "(c1, mds, mem1, c2, mds, mem2)  R"
       and "(c1, mds, mem1, c1', mds', mem1')  evalw"
    thus "c2' mem2'.
          (c2, mds, mem2, c2', mds', mem2')  evalw 
          (c1', mds', mem1', c2', mds', mem2')  R"
       by(rule R_inv)
  qed

lemma prog_high_branch_secure':
  "low_mds_eq mdss mem1 mem2 
       (prog_high_branch, mdss, mem1, prog_high_branch, mdss, mem2)  R"
  apply(rule R.intros)
  apply simp_all
   apply(rule inv1h)
     apply (simp_all add: mdss_def)
   apply(rule inv1h)
     apply (simp_all add: mdss_def)
  unfolding prog_high_branch_def by(fastforce intro: rel_inv.intros)

lemma "com_sifum_secure (prog_high_branch, mdss)"
  unfolding com_sifum_secure_def low_indistinguishable_def
  apply clarify
  apply(rule mm_equiv_intro)
   apply(rule strong_low_bisim_mm_R)
  by (rule prog_high_branch_secure')

end

locale sifum_refinement_high_branch =
  A: sifum_example +
  C: sifum_exampleC

primrec varC_of :: "var  varC"
where
  "varC_of h_var = h_mem" |
  "varC_of x_var = x_mem" |
  "varC_of y_var = y_mem" |
  "varC_of z_var = z_mem"

sublocale sifum_refinement_high_branch 
  sifum_refinement dma dmaC 𝒞_vars 𝒞_vars 𝒞 𝒞C A.evalw C.evalw undefined varC_of
  apply(unfold_locales)
     apply(rule inj_onI, simp)
     apply(case_tac x)
         apply(case_tac y, simp+)
        apply(case_tac y, simp+)
       apply(case_tac y, simp+)
      apply(case_tac y, simp+)
    apply(case_tac xA)
       apply(clarsimp simp:dma_def dmaC_def)+
  done

context sifum_refinement_high_branch begin

(* Adapted these helpers from Eg1Eg2 *)
lemma conc_only_vars_not_visible_abs:
  "(vC. vC  range varC_of  memC vC = memC' vC)  memA_of memC = memA_of memC'"
  by (simp add: memA_of_def)

lemma conc_only_var_assign_not_visible_abs:
  "vC e. vC  range varC_of  memA_of memC = memA_of (memC(vC := e))"
  using conc_only_vars_not_visible_abs
  by simp

lemma reg_is_not_the_varC_of_anything:
  "reg  {reg0, reg1, reg2, reg3}  reg = varC_of x  False"
  by (induct x, clarsimp+)

lemma reg_not_visible_abs:
  "reg  {reg0, reg1, reg2, reg3}  reg  range varC_of"
  using reg_is_not_the_varC_of_anything
  by blast

(* Helpers carried over from Eg1Eg2 *)
lemma assign_evalw_loadA:
  shows "(x  Load y, mds, memA, Stop, mds, mem (x := mem y)A)  A.evalw"
  by (metis A.assign_evalw evA.simps(2))

lemma assign_evalw_loadC:
  shows "(x  Load y, mds, memC, Stop, mds, mem (x := mem y)C)  C.evalw"
  using C.unannotated[OF C.assign, where E="[]", simplified]
  apply(drule_tac x=x in meta_spec)
  apply(drule_tac x="Load y" in meta_spec)
  apply(drule_tac x=mds in meta_spec)
  apply(drule_tac x=mem in meta_spec)
  apply clarsimp
  done

lemma assign_evalw_constA:
  shows "(x  Const c, mds, mem, Stop, mds, mem (x := c))  A.evalw"
  by (metis A.assign_evalw evA.simps(1))

lemma assign_evalw_constC:
  shows "(x  Const c, mds, mem, Stop, mds, mem (x := c))  C.evalw"
  using C.unannotated[OF C.assign, where E="[]", simplified]
  apply(drule_tac x=x in meta_spec)
  apply(drule_tac x="Const c" in meta_spec)
  apply(drule_tac x=mds in meta_spec)
  apply(drule_tac x=mem in meta_spec)
  apply clarsimp
  done

lemma mem_assign_refinement_helper_var:
  "memA_of (memC (varC_of x := memC (varC_of y)))
       = (memA_of memC) (x := (memA_of memC) y)"
  apply(clarsimp simp: memA_of_def)
  apply(rule ext, clarsimp)
  apply(cases x)
   apply(case_tac xA, clarsimp+)+
  done

lemma mem_assign_refinement_helper_const:
  "memA_of (memC (varC_of x := c))
       = (memA_of memC) (x := c)"
  apply(clarsimp simp: memA_of_def)
  apply(rule ext, clarsimp)
  apply(cases x)
      apply(case_tac xA, clarsimp+)+
  done

lemma NoRWA_implies_NoRWC:
  "x  mdsA_of mdsC AsmNoReadOrWrite 
   varC_of x  mdsC AsmNoReadOrWrite"
  unfolding mdsA_of_def
  apply clarsimp
  apply (simp only: varC_of_def)
  apply clarsimp
  apply (simp add: f_inv_into_f)
  done

lemma NoWriteA_implies_NoWriteC:
  "x  mdsA_of mdsC AsmNoWrite 
   varC_of x  mdsC AsmNoWrite"
  unfolding mdsA_of_def
  apply clarsimp
  apply (simp only: varC_of_def)
  apply clarsimp
  apply (simp add: f_inv_into_f)
  done

lemma if_seq_evalw_helperA:
  "(If B T E, mds, mem,
    if evB mem B then T else E, mds, memA)  A.evalw
    
   (If B T E ;; TAIL, mds, mem,
    if evB mem B then T ;; TAIL else E ;; TAIL, mds, memA)  A.evalw"
  using A.evalw.seq
  by auto

lemma if_seq_evalw_helperC:
  "(If B T E, mds, mem,
    if evBC mem B then T else E, mds, memC)  C.evalw
    
   (If B T E ;; TAIL, mds, mem,
    if evBC mem B then T ;; TAIL else E ;; TAIL, mds, memC)  C.evalw"
  using C.evalw.seq
  by auto

fun aexpC_of
where
  "aexpC_of (Const c) = (Const c)" |
  "aexpC_of (Load v) = (Load (varC_of v))" |
  "aexpC_of (Add x y) = Add (aexpC_of x) (aexpC_of y)" |
  "aexpC_of (Sub x y) = Sub (aexpC_of x) (aexpC_of y)"

lemma mem_assign_refinement_helper_aexp:
  "memA_of (memC (varC_of x := evA memC (aexpC_of a)))
       = (memA_of memC) (x := evA (memA_of memC) a)"
  apply(clarsimp simp: memA_of_def)
  apply(rule ext, clarsimp)
  apply(rename_tac xA)
  apply(cases x)
     apply(case_tac xA, induct rule:aexpC_of.induct, clarsimp+)
    apply(case_tac xA, induct rule:aexpC_of.induct, clarsimp+)
      apply(induct rule:aexpC_of.induct, clarsimp+)
   apply(case_tac xA, induct rule:aexpC_of.induct, clarsimp+)
    apply(induct rule:aexpC_of.induct, clarsimp+)
  apply(case_tac xA, induct rule:aexpC_of.induct, clarsimp+)
  apply(induct rule:aexpC_of.induct, clarsimp+)
  done

inductive_set rel_invC :: "(((varC addr, varC aexp, varC bexp) Stmt, varC addr, val) LocalConf) rel"
where
  rel_invC_1:
  "c =
     Skip ;;
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c' =
     Assign reg1 (Load y_mem) ;;
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_1':
  "c' =
     Skip ;;
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c =
     Assign reg1 (Load y_mem) ;;
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_2:
  "c =
     Stop ;;
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c' =
     Stop ;;
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_2':
  "c' =
     Stop ;;
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c =
     Stop ;;
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_3:
  "c =
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c' =
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_3':
  "c' =
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c =
     Assign reg2 (Load z_mem) ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_4:
  "c =
     Stop ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c' =
     Stop ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_4':
  "c' =
     Stop ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c =
     Stop ;;
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_5:
  "c =
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c' =
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_5':
  "c' =
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    c =
     Assign reg0 (Add (Load reg1) (Load reg2)) ;;
     Assign x_mem (Load reg0) 
      (c, mds, mem, c', mds', mem')  rel_invC" |
  rel_invC_default:
  "c = c' 
      (c, mds, mem, c', mds', mem')  rel_invC"

inductive_cases rel_invCE: "(c, mds, memC, c', mds', mem'C)  rel_invC"

lemma rel_invC_sym:
  "sym rel_invC"
  unfolding sym_def
  apply(auto elim!: rel_invC.cases intro: rel_invC.intros)
  done

lemma rel_invC_closed_glob_consistent:
  "C.closed_glob_consistent rel_invC"
  unfolding C.closed_glob_consistent_def
  apply(safe elim!: rel_invC.cases)
  using rel_invC.intros by simp+

inductive_set RefRel_HighBranch :: "(
    (((var, var aexp, var bexp) Stmt × (Mode  var set)) × (var  val)) ×
     ((varC, varC aexp, varC bexp) Stmt × (Mode  varC set)) × (varC  val)
    ) set"
where
  acq_mode_rel: "cA = ModeDecl Skip (Acq x SomeMode) ;; cA_tail;
    cC = ModeDecl Skip (Acq (varC_of x) SomeMode) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cA, mdsA, memA''A, Stop ;; cA_tail, mdsA', memA'A)  A.evalw 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (Stop ;; cA_tail, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  assign_load_rel: "cA = (x  aexp.Load y) ;; cA_tail;
    cC = ((varC_of x)  aexp.Load (varC_of y)) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    x  mdsA GuarNoReadOrWrite;
    x  mdsA GuarNoWrite;
    y  mdsA GuarNoReadOrWrite;
    x  𝒞;
    y  𝒞;
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cA, mdsA, memA''A, Stop ;; cA_tail, mdsA', memA'A)  A.evalw 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (Stop ;; cA_tail, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  assign_const_rel: "cA = (x  Const z) ;; cA_tail;
    cC = ((varC_of x)  Const z) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    x  mdsA GuarNoReadOrWrite;
    x  mdsA GuarNoWrite;
    x  𝒞;
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cA, mdsA, memA''A, Stop ;; cA_tail, mdsA', memA'A)  A.evalw 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (Stop ;; cA_tail, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_reg_load_rel: "
    cA = (If (Neq (Load x) (Const 0)) cA_then cA_else);
    cC = (reg3  (Load (varC_of x))) ;; ((If (Neq (Load reg3) (Const 0)) cC_then cC_else));
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    x  mdsA AsmNoWrite  x  mdsA AsmNoReadOrWrite;
    reg3  mdsC GuarNoReadOrWrite  reg3  mdsC GuarNoWrite;
    x  mdsA GuarNoReadOrWrite;
    x'. x  𝒞_vars x'  x'  mdsA GuarNoReadOrWrite;
    (memA' memC' memA'' memC''.
        (
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹The change in memC does not affect memA
         memA'' = memA' 
         ― ‹The concrete and abstract versions of the bool condition must become consistent›
         evB memC' (Neq (Load reg3) (Const 0)) = evB memA' (Neq (Load x) (Const 0)) 
         (cC, mdsC, memC''C,
          Stop ;; (If (Neq (Load reg3) (Const 0)) cC_then cC_else), mdsC, memC'C)  C.evalw
        )
         
         (cA, mdsA, memA''A,
          Stop ;; (If (Neq (Load reg3) (Const 0)) cC_then cC_else), mdsC, memC'C)  RefRel_HighBranch)
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_reg_stop_rel: "
    cA = (If (Neq (Load x) (Const 0)) cA_then cA_else);
    cC = Stop ;; ((If (Neq (Load reg3) (Const 0)) cC_then cC_else));
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    x  mdsA AsmNoWrite  x  mdsA AsmNoReadOrWrite;
    ― ‹We will need to carry this through to the if_reg_rel› case.›
    evB memC (Neq (Load reg3) (Const 0)) = evB memA (Neq (Load x) (Const 0));
    (memA' memC' memA'' memC''.
        (
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹The change in memC does not affect memA
         memA'' = memA' 
         ― ‹The concrete and abstract versions of the bool condition must remain consistent›
         evB memC' (Neq (Load reg3) (Const 0)) = evB memA' (Neq (Load x) (Const 0)) 
         evB memC'' (Neq (Load reg3) (Const 0)) = evB memA'' (Neq (Load x) (Const 0)) 
         (cC, mdsC, memC''C,
          (If (Neq (Load reg3) (Const 0)) cC_then cC_else), mdsC, memC'C)  C.evalw
        )
         
         (cA, mdsA, memA''A,
          (If (Neq (Load reg3) (Const 0)) cC_then cC_else), mdsC, memC'C)  RefRel_HighBranch)
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_reg_rel: "
    ― ‹Is a more generic version possible for an arbitrary bA?›
    ⌦‹cA = (If bA cA_then cA_else);›
    ⌦‹bA = Eq (Load x) (Const 0);›  ― ‹evB memA bA
    cA = (If (Neq (Load x) (Const 0)) cA_then cA_else);
    cC = (If (Neq (Load reg3) (Const 0)) cC_then cC_else);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    x  mdsA AsmNoWrite  x  mdsA AsmNoReadOrWrite;
    ― ‹The concrete and abstract versions of the bool condition must have remained consistent›
    evB memC (Neq (Load reg3) (Const 0)) = evB memA (Neq (Load x) (Const 0));
    ― ‹As for ― ‹if_reg_load_rel››
    reg3  mdsC GuarNoReadOrWrite  reg3  mdsC GuarNoWrite;
    x  mdsA GuarNoReadOrWrite;
    x'. x  𝒞_vars x'  x'  mdsA GuarNoReadOrWrite;
    ― ‹As we would expect, the two branches must be related by the coupling invariant.›
    memC' memC''. (cC_then, mdsC, memC'C, cC_else, mdsC, memC''C)  rel_invC;
    (memA' memC' memA'' memC''.
       memA' = memA_of memC' 
       memA'' = memA_of memC'' 
       evB memC'' (Neq (Load reg3) (Const 0)) = evB memA'' (Neq (Load x) (Const 0)) 
       evB memC' (Neq (Load reg3) (Const 0)) = evB memA' (Neq (Load x) (Const 0)) 
       (cA, mdsA, memA''A,
        (if (evB memA'' (Neq (Load x) (Const 0))) then cA_then else cA_else), mdsA, memA'A)  A.evalw 
       (cC, mdsC, memC''C,
        (if (evB memC'' (Neq (Load reg3) (Const 0))) then cC_then else cC_else), mdsC, memC'C)  C.evalw
       
       ((if (evB memA'' (Neq (Load x) (Const 0))) then cA_then else cA_else), mdsA, memA'A,
        (if (evB memC'' (Neq (Load reg3) (Const 0))) then cC_then else cC_else), mdsC, memC'C)  RefRel_HighBranch)
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

(*
  Assign x_var (Load y_var)
    - to -
  Skip ;;
  Skip ;;
  Assign reg0 (Load y_mem) ;;
  Assign x_mem (Load reg0);
*)
  if_then_rel_1: "cA = (x_var  Load y_var);
    cC = Skip ;; cC_tail;
    cC_tail =
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_1': "cA = (x_var  Load y_var);
    cC = Stop ;; cC_tail;
    cC_tail =
     Skip ;;
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_2: "cA = (x_var  Load y_var);
    cC = Skip ;; cC_tail;
    cC_tail =
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_2': "cA = (x_var  Load y_var);
    cC = Stop ;; cC_tail;
    cC_tail =
     Assign reg0 (Load y_mem) ;;
     Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_3: "cA = (x_var  Load y_var);
    cC = Assign reg0 (Load y_mem) ;; cC_tail;
    cC_tail = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹The value of reg0› and y_var› must now become consistent›
         evA memC' (Load reg0) = evA memA' (Load y_var) 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_3': "cA = (x_var  Load y_var);
    cC = Stop ;; cC_tail;
    cC_tail = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    ― ‹The value of reg0› and y_var› at this point must be consistent›
    evA memC (Load reg0) = evA memA (Load y_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹and must remain consistent›
         evA memC' (Load reg0) = evA memA' (Load y_var) 
         evA memC'' (Load reg0) = evA memA'' (Load y_var) 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_then_rel_4: "cA = (x_var  Load y_var);
    cC = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    ― ‹The value of reg0› and y_var› at this point must be consistent›
    evA memC (Load reg0) = evA memA (Load y_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cA, mdsA, memA''A, Stop, mdsA', memA'A)  A.evalw 
         (cC, mdsC, memC''C, Stop, mdsC', memC'C)  C.evalw
        )
         
         (Stop, mdsA', memA'A, Stop, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

(*
  Assign x_var (Add (Load y_var) (Load z_var))
    - to -
  Assign reg1 (Load y_mem) ;;
  Assign reg2 (Load z_mem) ;;
  Assign reg0 (Add (Load reg1) (Load reg2)) ;;
  Assign x_mem (Load reg0)
*)
  if_else_rel_1: "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = (reg1  Load y_mem) ;; cC_tail;
    cC_tail =
      Assign reg2 (Load z_mem) ;;
      Assign reg0 (Add (Load reg1) (Load reg2)) ;;
      Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹Now reg1› takes on y_var›
         evA memC' (Load reg1) = evA memA' (Load y_var) 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_1': "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Stop ;; cC_tail;
    cC_tail =
      Assign reg2 (Load z_mem) ;;
      Assign reg0 (Add (Load reg1) (Load reg2)) ;;
      Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    ― ‹At this point reg1› contains y_var›
    evA memC (Load reg1) = evA memA (Load y_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹maintain it›
         evA memC' (Load reg1) = evA memA' (Load y_var) 
         evA memC'' (Load reg1) = evA memA'' (Load y_var) 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_2: "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Assign reg2 (Load z_mem) ;; cC_tail;
    cC_tail =
      Assign reg0 (Add (Load reg1) (Load reg2)) ;;
      Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    ― ‹At this point reg1› contains y_var›
    evA memC (Load reg1) = evA memA (Load y_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹maintain it›
         evA memC'' (Load reg1) = evA memA'' (Load y_var) 
         evA memC' (Load reg1) = evA memA' (Load y_var) 
         ― ‹Now reg2› takes on z_var›
         evA memC' (Load reg2) = evA memA' (Load z_var) 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_2': "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Stop ;; cC_tail;
    cC_tail =
      Assign reg0 (Add (Load reg1) (Load reg2)) ;;
      Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    z_var  mdsA AsmNoWrite  z_var  mdsA AsmNoReadOrWrite;
    ― ‹At this point reg1› contains y_var› and reg2› contains z_var›
    evA memC (Load reg1) = evA memA (Load y_var);
    evA memC (Load reg2) = evA memA (Load z_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹maintain it›
         evA memC'' (Load reg1) = evA memA'' (Load y_var) 
         evA memC'' (Load reg2) = evA memA'' (Load z_var) 
         evA memC' (Load reg1) = evA memA' (Load y_var) 
         evA memC' (Load reg2) = evA memA' (Load z_var) 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_3: "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Assign reg0 (Add (Load reg1) (Load reg2)) ;; cC_tail;
    cC_tail = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    z_var  mdsA AsmNoWrite  z_var  mdsA AsmNoReadOrWrite;
    ― ‹At this point reg1› contains y_var› and reg2› contains z_var›
    evA memC (Load reg1) = evA memA (Load y_var);
    evA memC (Load reg2) = evA memA (Load z_var);
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         evA memC'' (Load reg1) = evA memA'' (Load y_var) 
         evA memC'' (Load reg2) = evA memA'' (Load z_var) 
         ― ‹Thus the value of reg0› becomes consistent with y_var + z_var›
         evA memC' (Load reg0) = evA memA' (Add (Load y_var) (Load z_var)) 
         (cC, mdsC, memC''C, Stop ;; cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, Stop ;; cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_3': "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Stop ;; cC_tail;
    cC_tail = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    z_var  mdsA AsmNoWrite  z_var  mdsA AsmNoReadOrWrite;
    ― ‹The value of reg0› and y_var + z_var› at this point must be consistent›
    evA memC (Load reg0) = evA memA (Add (Load y_var) (Load z_var));
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         ― ‹and must remain consistent›
         evA memC' (Load reg0) = evA memA' (Add (Load y_var) (Load z_var)) 
         evA memC'' (Load reg0) = evA memA'' (Add (Load y_var) (Load z_var)) 
         (cC, mdsC, memC''C, cC_tail, mdsC', memC'C)  C.evalw
        )
         
         (cA, mdsA', memA'A, cC_tail, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  if_else_rel_4: "cA = (x_var  Add (Load y_var) (Load z_var));
    cC = Assign x_mem (Load reg0);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (vC. vC  range varC_of  vC  mdsC AsmNoReadOrWrite);
    y_var  mdsA AsmNoWrite  y_var  mdsA AsmNoReadOrWrite;
    z_var  mdsA AsmNoWrite  z_var  mdsA AsmNoReadOrWrite;
    ― ‹The value of reg0› and y_var + z_var› at this point must be consistent›
    evA memC (Load reg0) = evA memA (Add (Load y_var) (Load z_var));
    mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' 
         memA' = memA_of memC' 
         memA'' = memA_of memC'' 
         (cA, mdsA, memA''A, Stop, mdsA', memA'A)  A.evalw 
         (cC, mdsC, memC''C, Stop, mdsC', memC'C)  C.evalw
        )
         
         (Stop, mdsA', memA'A, Stop, mdsC', memC'C)  RefRel_HighBranch
    
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  stop_seq_rel: "cA = Stop ;; cA_tail;
    cC = Stop ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (cA_tail, mdsA, memAA, cC_tail, mdsC, memCC)  RefRel_HighBranch
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" |

  stop_rel:
    "(Stop, mdsA_of mdsC, memA_of memCA, Stop, mdsC, memCC)  RefRel_HighBranch"

inductive_cases RefRelE: "(c, mds, memA, c', mds', mem'C)  RefRel_HighBranch"

definition abs_steps' :: "(_,_,_) Stmt  (_,_,_) Stmt  nat" where
  "abs_steps' cA cC 
    (if (x m cA_tail. cA = ((Skip@[x +=m m]) ;; cA_tail)) 
        (x m cC_tail. cC = ((Skip@[varC_of x +=m m]) ;; cC_tail)) then (Suc 0)
     else if ( cA_tail cC_tail. cA = (Stop ;; cA_tail)  cC = (Stop ;; cC_tail)) then (Suc 0)
     else if ( x thenA elseA thenC elseC.
        cA = (Stmt.If (Neq (Load x) (Const 0)) thenA elseA) 
        (cC = ((reg3  Load (varC_of x)) ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC)) 
         cC = (Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC))
        then 0
     else if (cA = (x_var  Load y_var) 
        cC  {Skip ;; Skip ;; Assign reg0 (Load y_mem) ;; Assign x_mem (Load reg0),
              Stop ;; Skip ;; Assign reg0 (Load y_mem) ;; Assign x_mem (Load reg0),
              Skip ;; Assign reg0 (Load y_mem) ;; Assign x_mem (Load reg0),
              Stop ;; Assign reg0 (Load y_mem) ;; Assign x_mem (Load reg0),
              Assign reg0 (Load y_mem) ;; Assign x_mem (Load reg0),
              Stop ;; Assign x_mem (Load reg0)})
        then 0
     else if (cA = (x_var  Add (Load y_var) (Load z_var)) 
        cC  {(reg1  Load y_mem) ;; Assign reg2 (Load z_mem) ;;
                Assign reg0 (Add (Load reg1) (Load reg2)) ;; Assign x_mem (Load reg0),
              Stop ;; Assign reg2 (Load z_mem) ;;
                Assign reg0 (Add (Load reg1) (Load reg2)) ;; Assign x_mem (Load reg0),
              Assign reg2 (Load z_mem) ;;
                Assign reg0 (Add (Load reg1) (Load reg2)) ;; Assign x_mem (Load reg0),
              Stop ;;
                Assign reg0 (Add (Load reg1) (Load reg2)) ;; Assign x_mem (Load reg0),
              Assign reg0 (Add (Load reg1) (Load reg2)) ;; Assign x_mem (Load reg0),
              Stop ;; Assign x_mem (Load reg0)})
        then 0
     else (Suc 0))"

fun abs_steps
where
"abs_steps cA, _, _A cC, _, _C = abs_steps' cA cC"

lemma closed_others_RefRel_HighBranch:
  "closed_others RefRel_HighBranch"
unfolding closed_others_def
proof(clarify)
fix cA cC mdsC memC memC'
assume
  in_rel: "(cA, mdsA_of mdsC, memA_of memCA,
    cC, mdsC, memCC)  RefRel_HighBranch" and
  vars: " x. memC x  memC' x  ¬ var_asm_not_written mdsC x"
and  dmas: "x. dmaC memC x  dmaC memC' x  ¬ var_asm_not_written mdsC x"
from in_rel vars dmas
show "(cA, mdsA_of mdsC, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
  proof (induct rule: RefRel_HighBranch.induct)
  case (acq_mode_rel cA x SomeMode tailA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using acq_mode_rel
    by (simp add:RefRel_HighBranch.acq_mode_rel)
  next
  case (assign_load_rel cA x y tailA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using assign_load_rel
    by (simp add:RefRel_HighBranch.assign_load_rel)
  next
  case (assign_const_rel cA x z tailA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using assign_const_rel
    by (simp add:RefRel_HighBranch.assign_const_rel)
  next
  case (if_reg_load_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_reg_load_rel
    by (simp add:RefRel_HighBranch.if_reg_load_rel)
  next
  case (if_reg_stop_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_reg_stop_rel
    proof (clarsimp)
      from if_reg_stop_rel.hyps(3,5,6) if_reg_stop_rel.prems(1)
      have reg_untouched: "memC reg3 = memC' reg3" and
        xC_untouched: "memC (varC_of x) = memC' (varC_of x)" and
        xA_untouched: "memA_of memC x = memA_of memC' x"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC
        by (clarsimp simp:var_asm_not_written_def, blast)+
      with if_reg_stop_rel.hyps
      have conds_still_match: "(memC' reg3 = 0) = (memA_of memC' x = 0)"
        by fastforce
      with if_reg_stop_rel RefRel_HighBranch.if_reg_stop_rel
      show "(Stmt.If (Neq (Load x) (Const 0)) thenA elseA, mdsA_of mdsC, memA_of memC'A,
             Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC, mdsC, memC'C)
              RefRel_HighBranch"
        by auto
    qed
  next
  case (if_reg_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_reg_rel(1-11)
    proof (clarsimp)
      from if_reg_rel.hyps(3,5,6) if_reg_rel.prems(1)
      have reg_untouched: "memC reg3 = memC' reg3" and
        xC_untouched: "memC (varC_of x) = memC' (varC_of x)" and
        xA_untouched: "memA_of memC x = memA_of memC' x"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC
        by (clarsimp simp:var_asm_not_written_def, blast)+
      with if_reg_rel.hyps
      have conds_still_match: "(memC' reg3 = 0) = (memA_of memC' x = 0)"
        by auto
      show "(Stmt.If (Neq (Load x) (Const 0)) thenA elseA, mdsA_of mdsC, memA_of memC'A,
             Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC, mdsC, memC'C)
              RefRel_HighBranch"
        apply (rule RefRel_HighBranch.if_reg_rel, simp+)
            using if_reg_rel apply simp
           using if_reg_rel apply simp
          using conds_still_match apply simp
         using if_reg_rel apply blast+
        done
    qed
  next
  case (if_then_rel_1 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_1
    by (simp add:RefRel_HighBranch.if_then_rel_1)
  next
  case (if_then_rel_1' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_1'
    by (simp add:RefRel_HighBranch.if_then_rel_1')
  next
  case (if_then_rel_2 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_2
    by (simp add:RefRel_HighBranch.if_then_rel_2)
  next
  case (if_then_rel_2' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_2'
    by (simp add:RefRel_HighBranch.if_then_rel_2')
  next
  case (if_then_rel_3 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_3
    by (simp add:RefRel_HighBranch.if_then_rel_3)
  next
  case (if_then_rel_3' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_3'
    proof (clarsimp)
      from if_then_rel_3'.hyps(4,5,6,7) if_then_rel_3'.prems(1)
      have reg_untouched: "memC reg0 = memC' reg0" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by fastforce+
      with if_then_rel_3'.hyps
      have conds_still_match: "memC' reg0 = memA_of memC' y_var"
        by simp
      show "(x_var  Load y_var, mdsA_of mdsC, memA_of memC'A,
             Stop ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_then_rel_3' if_then_rel_3' conds_still_match by simp
    qed
  next
  case (if_then_rel_4 cA cC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_then_rel_4
    proof (clarsimp)
      from if_then_rel_4.hyps(3-7) if_then_rel_4.prems(1)
      have reg_untouched: "memC reg0 = memC' reg0" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (fast, metis+)
      with if_then_rel_4.hyps
      have conds_still_match: "memC' reg0 = memA_of memC' y_var"
        by simp
      show "(x_var  Load y_var, mdsA_of mdsC, memA_of memC'A,
             x_mem  Load reg0, mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_then_rel_4 if_then_rel_4 conds_still_match by simp
    qed
  next
  case (if_else_rel_1 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_1
    by (simp add:RefRel_HighBranch.if_else_rel_1)
  next
  case (if_else_rel_1' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_1'
    proof (clarsimp)
      from if_else_rel_1'.hyps(4-7) if_else_rel_1'.prems(1)
      have reg_untouched: "memC reg1 = memC' reg1" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_1'.hyps
      have conds_still_match: "memC' reg1 = memA_of memC' y_var"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             Stop ;; (reg2  Load z_mem) ;; (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_1' if_else_rel_1' conds_still_match by simp
    qed
  next
  case (if_else_rel_2 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_2
    proof (clarsimp)
      from if_else_rel_2.hyps(4-7) if_else_rel_2.prems(1)
      have reg_untouched: "memC reg1 = memC' reg1" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_2.hyps
      have conds_still_match: "memC' reg1 = memA_of memC' y_var"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             (reg2  Load z_mem) ;; (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_2 if_else_rel_2 conds_still_match by simp
    qed
  next
  case (if_else_rel_2' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_2'
    proof (clarsimp)
      from if_else_rel_2'.hyps(4-8) if_else_rel_2'.prems(1)
      have regs_untouched: "memC reg1 = memC' reg1  memC reg2 = memC' reg2" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var" and
        zC_untouched: "memC (varC_of z_var) = memC' (varC_of z_var)" and
        zA_untouched: "memA_of memC z_var = memA_of memC' z_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_2'.hyps(5,9,10)
      have conds_still_match: "memC' reg1 = memA_of memC' y_var  memC' reg2 = memA_of memC' z_var"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             Stop ;; (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_2' if_else_rel_2' conds_still_match by simp
    qed
  next
  case (if_else_rel_3 cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_3
    proof (clarsimp)
      from if_else_rel_3.hyps(4-8) if_else_rel_3.prems(1)
      have regs_untouched: "memC reg1 = memC' reg1  memC reg2 = memC' reg2" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var" and
        zC_untouched: "memC (varC_of z_var) = memC' (varC_of z_var)" and
        zA_untouched: "memA_of memC z_var = memA_of memC' z_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_3.hyps(5,9,10)
      have conds_still_match: "memC' reg1 = memA_of memC' y_var  memC' reg2 = memA_of memC' z_var"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_3 if_else_rel_3 conds_still_match by simp
    qed
  next
  case (if_else_rel_3' cA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_3'
    proof (clarsimp)
      from if_else_rel_3'.hyps(4-8) if_else_rel_3'.prems(1)
      have reg_untouched: "memC reg0 = memC' reg0" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var" and
        zC_untouched: "memC (varC_of z_var) = memC' (varC_of z_var)" and
        zA_untouched: "memA_of memC z_var = memA_of memC' z_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_3'.hyps(5,9)
      have conds_still_match:
        "evA memC' (Load reg0) = evA (memA_of memC') (Add (Load y_var) (Load z_var))"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             Stop ;; (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_3' if_else_rel_3' conds_still_match by simp
    qed
  next
  case (if_else_rel_4 cA cC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using if_else_rel_4
    proof (clarsimp)
      from if_else_rel_4.hyps(3-7) if_else_rel_4.prems(1)
      have reg_untouched: "memC reg0 = memC' reg0" and
        yC_untouched: "memC (varC_of y_var) = memC' (varC_of y_var)" and
        yA_untouched: "memA_of memC y_var = memA_of memC' y_var" and
        zC_untouched: "memC (varC_of z_var) = memC' (varC_of z_var)" and
        zA_untouched: "memA_of memC z_var = memA_of memC' z_var"
        using reg_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC var_asm_not_written_def
        by (metis (no_types) insertCI reg_not_visible_abs, metis+)
      with if_else_rel_4.hyps(4,8)
      have conds_still_match:
        "evA memC' (Load reg0) = evA (memA_of memC') (Add (Load y_var) (Load z_var))"
        by simp
      show "(x_var  Add (Load y_var) (Load z_var), mdsA_of mdsC, memA_of memC'A,
             (x_mem  Load reg0), mdsC, memC'C)
              RefRel_HighBranch"
        using RefRel_HighBranch.if_else_rel_4 if_else_rel_4 conds_still_match by simp
    qed
  next
  case (stop_seq_rel cA tailA cC tailC mdsA mdsC memA memC)
  show "(cA, mdsA, memA_of memC'A, cC, mdsC, memC'C)  RefRel_HighBranch"
    using stop_seq_rel
    by (simp add:RefRel_HighBranch.stop_seq_rel)
  next
  case (stop_rel mdsC memC)
  show ?case by (simp add:RefRel_HighBranch.stop_rel)
  qed
qed

lemma preserves_modes_mem_RefRel_HighBranch:
  "preserves_modes_mem RefRel_HighBranch"
unfolding preserves_modes_mem_def2
proof(clarsimp)
  fix cA mdsA memA cC mdsC memC
  assume in_rel: "(cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch"
  thus "memA = memA_of memC  mdsA = mdsA_of mdsC"
    by (cases rule:RefRel_HighBranch.cases, blast+)
qed

lemma new_vars_private_RefRel_HighBranch:
  "sifum_refinement.new_vars_private dmaC C.evalw varC_of RefRel_HighBranch"
unfolding new_vars_private_def
(* Slightly more intuitive goals without simp converting ∨ to ⟶ *)
proof(clarify)
  fix cA mdsA memA cC mdsC memC cC' mdsC' memC'
  assume in_rel: "(cA, mdsA, memAA, cC, mdsC, memCC)  RefRel_HighBranch" and
      does_eval: "(cC, mdsC, memCC, cC', mdsC', memC'C)  C.evalw"
  let "?diff_mem vC" = "memC' vC  memC vC"
  let "?diff_dma vC" = "dmaC memC' vC < dmaC memC vC"
  let "?conc_only vC" = "vC  range varC_of"
  show "(vC. (?diff_mem vC  ?diff_dma vC)  ?conc_only vC  vC  mdsC' AsmNoReadOrWrite) 
         mdsC AsmNoReadOrWrite - range varC_of  mdsC' AsmNoReadOrWrite - range varC_of"
  using in_rel does_eval
  proof(cases rule:RefRel_HighBranch.cases)
  case (acq_mode_rel x SomeMode tailA tailC)
    moreover with does_eval
    have "mdsC' = mdsC (SomeMode := insert (varC_of x) (mdsC SomeMode))"
      by (metis (mono_tags) C.seq_decl_elim C.update_modes.simps(1))
    ultimately show ?thesis
      by simp
  next
  case (assign_load_rel x y tailA tailC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(13) set_eq_subset)
  next
  case (assign_const_rel x z tailA tailC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(13) set_eq_subset)
  next
  case (if_reg_load_rel x thenA elseA thenC elseC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(13) set_eq_subset)
  next
  case (if_reg_stop_rel x thenA elseA thenC elseC)
    with does_eval
    show ?thesis
      by (metis C.seq_stop_elim subset_refl)
  next
  case (if_reg_rel x thenA elseA thenC elseC)
    with does_eval
    have mdsC_unchanged: "mdsC = mdsC'"
      by (metis C.if_elim C.seq_elim Stmt.distinct(39))
    moreover with if_reg_rel(5)
    have "vC. (?diff_mem vC  ?diff_dma vC)  ?conc_only vC  vC  mdsC' AsmNoReadOrWrite"
      by simp
    moreover from mdsC_unchanged
    have "mdsC AsmNoReadOrWrite - range varC_of  mdsC' AsmNoReadOrWrite - range varC_of"
      by clarify
    ultimately show ?thesis
      by simp
  next
  case (if_then_rel_1 tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.evalw.seq C.eval_det C.seq_stop_elim C.seq_stop_evalw C.skip_evalw subsetI)
  next
  case (if_then_rel_1' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_then_rel_2 tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.evalw.seq C.eval_det C.seq_stop_elim C.seq_stop_evalw C.skip_evalw subsetI)
  next
  case (if_then_rel_2' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_then_rel_3 tailC)
    with does_eval
    show ?thesis
      by (metis (full_types) C.seq_assign_elim subset_refl)
  next
  case (if_then_rel_3' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_then_rel_4)
    with does_eval
    show ?thesis
      by (metis C.assign_elim order_refl)
  next
  case (if_else_rel_1 tailC)
    with does_eval
    show ?thesis
      by (metis (full_types) C.seq_assign_elim subset_refl)
  next
  case (if_else_rel_1' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_else_rel_2 tailC)
    with does_eval
    show ?thesis
      by (metis (full_types) C.seq_assign_elim subset_refl)
  next
  case (if_else_rel_2' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_else_rel_3 tailC)
    with does_eval
    show ?thesis
      by (metis (full_types) C.seq_assign_elim subset_refl)
  next
  case (if_else_rel_3' tailC)
    with does_eval
    show ?thesis
      by (metis (no_types, opaque_lifting) C.seq_stop_elim subsetI)
  next
  case (if_else_rel_4)
    with does_eval
    show ?thesis
      by (metis C.assign_elim order_refl)
  next
  case (stop_seq_rel tailA tailC)
    with does_eval C.seq_stop_elim
    show ?thesis by blast
  next
  case (stop_rel)
    with does_eval C.stop_no_eval have False by simp
    thus ?thesis by simp
  qed
qed

inductive_cases inR_E:
"(c, mds, memA, c', mds', mem'A)  A.R"

lemma refrel_helper_Acq_Rel_ex1I:
"
  ((Skip@[x +=m SomeMode]) ;; cA_tail, mdsA_of mdsC, memA_of mem2CA,
      c2C, mdsC, mem2CC)
      RefRel_HighBranch
  
  ∃!cC_tail.
  c2C = (Skip@[varC_of x +=m SomeMode]) ;; cC_tail 
        (((Skip@[varC_of x +=m SomeMode]) ;; cC_tail, mdsC, mem2CC,
          Stop ;; cC_tail, mdsC(SomeMode := insert (varC_of x) (mdsC SomeMode)), mem2CC)
           C.evalw)"
  apply(cases rule:RefRel_HighBranch.cases)
       apply simp
      apply clarsimp
      apply(erule_tac x="memA_of mem2C" in allE)
      apply(erule_tac x="mdsC(SomeMode := insert (varC_of x) (mdsC SomeMode))" in allE)
      apply(erule_tac x="mem2C" in allE)
      apply(erule impE)
       apply(rule_tac x="mem2C" in exI)
       apply(rule conjI)
        apply(rule HOL.refl)
       apply(rule conjI)
        apply(rule A.evalw.seq)
        apply(rule A.decl_evalw', rule HOL.refl, clarsimp)
        apply(rule mode_acquire_refinement_helper)
       apply(rule C.evalw.seq)
       apply(rule C.decl_evalw', rule HOL.refl, clarsimp)
      apply(rule_tac a=cC_tail in ex1I)
       apply clarsimp
        apply(rule C.evalw.seq)
        apply(rule C.decl_evalw', rule HOL.refl, clarsimp)
       apply blast+
  done

lemma refrel_helper_Assign_Load_ex1I:
"
  ((x  Load y) ;; tailA, mdsA_of mdsC, memA_of mem2CA,
      c2C, mdsC, mem2CC)
      RefRel_HighBranch
  
  ∃!tailC.
  c2C = (varC_of x  Load (varC_of y)) ;; tailC 
        (((varC_of x  Load (varC_of y)) ;; tailC, mdsC, mem2CC,
          Stop ;; tailC, mdsC, mem2C((varC_of x) := mem2C (varC_of y))C)
           C.evalw)"
  apply(cases rule:RefRel_HighBranch.cases, simp+)
          apply clarsimp
          apply(erule_tac x="memA_of mem2C" in allE)
          apply(erule_tac x="mdsC" in allE)
          apply(erule_tac x="mem2C((varC_of x) := mem2C (varC_of y))" in allE)
          apply(erule impE)
           apply(rule_tac x="mem2C" in exI)
           apply(rule conjI)
            apply(rule HOL.refl)
           apply(rule conjI)
            apply(rule A.evalw.seq)
            apply(simp add: assign_evalw_loadA mem_assign_refinement_helper_var)
           apply(rule C.evalw.seq)
           apply(simp add: assign_evalw_loadC)
          apply(rule_tac a=cC_tail in ex1I)
           apply clarsimp
           apply(rule C.evalw.seq)
           apply(simp add:assign_evalw_loadC)
          apply blast
         apply clarsimp
        apply(simp add: assign_evalw_loadA mem_assign_refinement_helper_var)
       apply(simp add:assign_evalw_loadC)
      apply(rule_tac a=cC_tail in ex1I)
       apply clarsimp
      apply(simp add:assign_evalw_loadC)
     apply blast
    apply(rule ex1I, clarsimp+)
  done


lemma refrel_helper_Assign_Const_ex1I:
"
  ((x  Const z) ;; tailA, mdsA_of mdsC, memA_of mem2CA,
      c2C, mdsC, mem2CC)
      RefRel_HighBranch
  
  ∃!tailC.
  c2C = (varC_of x  Const z) ;; tailC 
        (((varC_of x  Const z) ;; tailC, mdsC, mem2CC,
          Stop ;; tailC, mdsC, mem2C((varC_of x) := z)C)
           C.evalw)"
  apply(cases rule:RefRel_HighBranch.cases, simp+)
          apply clarsimp
          apply(erule_tac x="memA_of mem2C" in allE)
          apply(erule_tac x="mdsC" in allE)
          apply(erule_tac x="mem2C((varC_of x) := z)" in allE)
          apply(erule impE)
           apply(rule_tac x="mem2C" in exI)
           apply(rule conjI)
            apply(rule HOL.refl)
           apply(rule conjI)
            apply(rule A.evalw.seq)
            apply(simp add: assign_evalw_constA mem_assign_refinement_helper_const)
           apply(rule C.evalw.seq)
           apply(simp add:assign_evalw_constC)
          apply(rule_tac a=cC_tail in ex1I)
           apply clarsimp
           apply(rule C.evalw.seq)
           apply(simp add:assign_evalw_constC)
          apply blast
         apply clarsimp
        apply(simp add: assign_evalw_loadA mem_assign_refinement_helper_var)
       apply(simp add:assign_evalw_constC)
      apply(rule_tac a=cC_tail in ex1I)
       apply clarsimp
      apply(simp add:assign_evalw_constC)
     apply blast
    apply(rule ex1I, clarsimp+)
  done

(* Could possibly be useful if we have one that just does seq *)
lemma refrel_helper_Assign_Const:
"
  ((x  Const z), mdsA_of mdsC, memA_of mem2CA,
      c2C, mdsC, mem2CC)
      RefRel_HighBranch
  
  c2C = (varC_of x  Const z) 
        (((varC_of x  Const z), mdsC, mem2CC,
          Stop, mdsC, mem2C((varC_of x) := z)C)
           C.evalw)"
  by (cases rule:RefRel_HighBranch.cases, (simp add:assign_evalw_constC)+)

type_synonym t_Neq_C = "(varC aexp  varC aexp  varC bexp)"

lemma refrel_helper_If_Reg_Load_exI:
  "
  cC = (reg3  Load (varC_of x)) ;; Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC elseC
  
  c2A = If (Neq (Load x) (Const 0)) thenA elseA
  
  (c2A, mdsA_of mdsC, memA_of mem2CA,
    c2C, mdsC, mem2CC)
    RefRel_HighBranch
  
  A.neval
     c2A, mdsA_of mdsC, memA_of mem2CA 0
     c2A, mdsA_of mdsC', mem2A'A
  
  ― ‹Distinguish between the different concrete cases›
  ― ‹for which the abstract program remains the same.›
  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC
  
  thenC' elseC'.
  ((c2C = (reg3  Load (varC_of x)) ;; Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC' elseC')
 
   (c2C, mdsC, mem2CC,
    Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, mem2C(reg3 := mem2C (varC_of x))C)
      C.evalw
)"
  apply(cases rule:RefRel_HighBranch.cases, simp+)
       apply clarsimp
       apply(erule_tac x="mem2C(reg3 := mem2C (varC_of x))" in allE)
       apply(erule impE)
        apply(rule_tac x="mem2C" in exI)
        apply(rule conjI)
         apply(simp add: conc_only_var_assign_not_visible_abs reg_not_visible_abs)
        apply(rule conjI)
         apply clarsimp
         apply(simp add: memA_of_def)
        apply(rule C.evalw.seq)
        apply(simp add:assign_evalw_loadC)
       apply(rule C.evalw.seq)
       apply(simp add:assign_evalw_loadC)
      apply(erule rel_invCE, simp+)+
  done

lemma refrel_helper_If_Reg_Stop_exI:
  "
  cC = Stop ;; Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC elseC
  
  c2A = If (Neq (Load x) (Const 0)) thenA elseA
  
  (c2A, mdsA_of mdsC, memA_of mem2CA,
    c2C, mdsC, mem2CC)
    RefRel_HighBranch
  
  A.neval
     c2A, mdsA_of mdsC, memA_of mem2CA 0
     c2A, mdsA_of mdsC', mem2A'A
  
  ― ‹Distinguish between concrete cases for which abstract program remains the same.›
  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC
  
  thenC' elseC'.
  ((c2C = Stop ;; Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC' elseC')
 
   (c2C, mdsC, mem2CC,
    Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC' elseC', mdsC, mem2CC)
      C.evalw
)"
  apply(cases rule:RefRel_HighBranch.cases, simp+)
      apply(erule rel_invCE, simp+)+
     apply(rule C.seq_stop_evalw)+
    apply(erule rel_invCE, simp+)+
  done

lemma refrel_helper_If_Reg_exI:
assumes
  conds_match: "evB (sifum_refinement.memA_of varC_of mem2C) (Neq (Load x) (Const 0)) =
    evB mem2C ((Neq::t_Neq_C) (Load reg3) (Const 0))" and
  rest_assms: "cC = Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC elseC 
  ― ‹Distinguish between concrete cases for which abstract program remains the same.›
  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC"
shows
"
  thenC' elseC'.
  ((c2C = Stmt.If ((Neq::t_Neq_C) (Load reg3) (Const 0)) thenC' elseC')
 
   (c2C, mdsC, mem2CC,
    if (evB mem2C ((Neq::t_Neq_C) (Load reg3) (Const 0))) then (thenC') else (elseC'),
                  mdsC, mem2CC)
      C.evalw
)"
  using rest_assms
  apply(clarsimp simp del:evB.simps split del:if_splits)
  apply(erule rel_invCE, (clarsimp simp del:evB.simps split del:if_splits)+)
  apply(rule C.if_evalw)
  done

inductive_cases Skip_tail_RefRel_HighBranchE: "(Skip ;; cA_tail, mdsA, memA, Skip ;; cC_tail, mdsC, memC)  RefRel_HighBranch"
thm Skip_tail_RefRel_HighBranchE

inductive_cases Stop_tail_RefRel_HighBranchE: "(Stop ;; cA_tail, mdsA, memA, Stop ;; cC_tail, mdsC, memC)  RefRel_HighBranch"
thm Stop_tail_RefRel_HighBranchE

inductive_cases Acq_Mode_RefRel_HighBranchE:
"((Skip@[x +=m SomeMode]) ;; cA_tail, mdsA_of mdsC, memA_of memCA,
  (Skip@[varC_of x +=m SomeMode]) ;; cC_tail, mdsC, memCC)  RefRel_HighBranch"
thm Acq_Mode_RefRel_HighBranchE

inductive_cases Assign_Load_RefRel_HighBranchE:
"((x  aexp.Load y) ;; cA_tail, mdsA_of mdsC, memA_of memCA,
  ((varC_of x)  Load (varC_of y)) ;; cC_tail, mdsC, memCC)  RefRel_HighBranch"
thm Assign_Load_RefRel_HighBranchE

inductive_cases Assign_Const_RefRel_HighBranchE:
"((x  Const z) ;; cA_tail, mdsA_of mdsC, memA_of memCA,
  ((varC_of x)  Const z) ;; cC_tail, mdsC, memCC)  RefRel_HighBranch"
thm Assign_Const_RefRel_HighBranchE

inductive_cases If_Reg_Load_RefRel_HighBranchE:
"((If (Neq (Load x) (Const 0)) cA_then cA_else), mdsA_of mdsC, memA_of memCA,
  (reg3  Load (varC_of y)) ;; ((If (Neq (Load reg3) (Const 0)) cC_then cC_else)), mdsC, memCC)  RefRel_HighBranch"
thm If_Reg_Load_RefRel_HighBranchE

inductive_cases If_Reg_Stop_RefRel_HighBranchE:
"((If (Neq (Load x) (Const 0)) cA_then cA_else), mdsA_of mdsC, memA_of memCA,
  Stop ;; ((If (Neq (Load reg3) (Const 0)) cC_then cC_else)), mdsC, memCC)  RefRel_HighBranch"
thm If_Reg_Stop_RefRel_HighBranchE

inductive_cases If_Reg_RefRel_HighBranchE:
"((If (Neq (Load x) (Const 0)) cA_then cA_else), mdsA_of mdsC, memA_of memCA,
  ((If (Neq (Load reg3) (Const 0)) cC_then cC_else)), mdsC, memCC)  RefRel_HighBranch"
thm If_Reg_RefRel_HighBranchE

inductive_cases If_Then_RefRel_HighBranchE:
"((x_var  Load y_var), mdsA_of mdsC, memA_of memCA, cC, mdsC, memCC)
   RefRel_HighBranch"

inductive_cases If_Else_RefRel_HighBranchE:
"((x_var  Add (Load y_var) (Load z_var)), mdsA_of mdsC, memA_of memCA, cC, mdsC, memCC)
   RefRel_HighBranch"

inductive_cases inv5E:
"A.inv Assign x_var (Load y_var), mds, mem"

inductive_cases inv6E:
"A.inv Assign x_var (Add (Load y_var) (Load z_var)), mds, mem"

lemma induction_full_RefRel_HighBranch:
  notes neq0_conv[simp del] neq0_conv[symmetric, simp add]
  shows
  "(c1A, sifum_refinement.mdsA_of varC_of mdsC, sifum_refinement.memA_of varC_of mem1CA,
         c1C, mdsC, mem1CC)
         RefRel_HighBranch;
        (c1C, mdsC, mem1CC, c1C', mdsC', mem1C'C)  sifum_lang_no_dma.evalw evA evB
        n c1A'.
              A.neval
               c1A, sifum_refinement.mdsA_of varC_of mdsC, sifum_refinement.memA_of varC_of mem1CA n
               c1A', sifum_refinement.mdsA_of varC_of
                         mdsC', sifum_refinement.memA_of varC_of mem1C'A 
              (c1A', sifum_refinement.mdsA_of varC_of mdsC', sifum_refinement.memA_of varC_of mem1C'A,
               c1C', mdsC', mem1C'C)
               RefRel_HighBranch 
              (c2A c2C mem2C c2A' mem2A'.
                  (c1A, sifum_refinement.mdsA_of varC_of
                            mdsC, sifum_refinement.memA_of varC_of mem1CA,
                   c2A, sifum_refinement.mdsA_of varC_of
                            mdsC, sifum_refinement.memA_of varC_of mem2CA)
                   A.R 
                  (c2A, sifum_refinement.mdsA_of varC_of
                            mdsC, sifum_refinement.memA_of varC_of mem2CA,
                   c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (c1C, mdsC, mem1CC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, sifum_refinement.mdsA_of varC_of mdsC, sifum_refinement.memA_of varC_of mem2CA
                   n c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)
                       sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A,
                       c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
proof(induct rule: RefRel_HighBranch.induct)
case (acq_mode_rel cA x m tailA cC tailC mdsA mdsC memA memC)
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  let ?c1A' = "Stop ;; tailA"
  from acq_mode_rel(1,2)
  have abs_steps_acq: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  moreover from acq_mode_rel.prems acq_mode_rel(2)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC(m := insert (varC_of x) (mdsC m))" and
    mem1C'_def: "mem1C' = memC"
    by (metis (mono_tags) C.seq_decl_elim C.update_modes.simps(1))+
  moreover from mdsC'_def
  have mdsA'_def: "?mdsA' = A.update_modes (x +=m m) (mdsA_of mdsC)"
    unfolding A.update_modes.simps
    by(blast intro: mode_acquire_refinement_helper)
  moreover with mem1C'_def acq_mode_rel A.evalw.seq A.decl_evalw
  have evalA: "(cA, mdsA, memAA, ?c1A', ?mdsA', ?mem1A'A)  A.evalw"
    by presburger
  hence nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    by clarsimp
  moreover from acq_mode_rel(5)
  have mdsC'_concrete_vars_unwritable:
    "(vC. vC  range varC_of  vC  mdsC' AsmNoReadOrWrite)"
    by(auto simp: mdsC'_def)
  moreover with acq_mode_rel(6)[simplified] acq_mode_rel.hyps(4) nevalA c1C'_def
  have in_Rel': "(?c1A', ?mdsA', ?mem1A'A, c1C', mdsC', mem1C'C)  RefRel_HighBranch"
    by (metis A.neval_Suc_simp One_nat_def acq_mode_rel.prems)
  moreover have "(c2A c2C mem2C c2A' mem2A'.
           (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
           (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
            RefRel_HighBranch 
           (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
           A.neval
            c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 1
            c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
           (c2C' mem2C'.
               (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
               (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                RefRel_HighBranch 
               (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
    proof(clarsimp)
      fix c2A c2C mem2C c2A' mem2A'
      assume in_R: "(cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R" and
        in_RefRel: "(c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
            RefRel_HighBranch" and
        in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
        eval2A: "(c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA,
         c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A)
         sifum_lang_no_dma.evalw evA evB"
      let ?c2C' = "Stop ;; tailC"
      from in_rel_invC acq_mode_rel(2) rel_invCE
      have "c2C = (Skip@[varC_of x +=m m]) ;; tailC" by blast
      hence eval_tailC: "(c2C, mdsC, mem2CC, Stop ;; tailC, mdsC', mem2CC)  sifum_lang_no_dma.evalw evA evB"
        by (simp del:fun_upd_apply add:C.evalw.seq C.decl_evalw' mdsC'_def)
      from in_R acq_mode_rel(1)
      have c2A_def: "c2A = (Skip@[x +=m m]) ;; tailA" by (blast elim:inR_E A.rel_invE)
      with acq_mode_rel(1,3,4)
      have "(c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA,
            Stop ;; tailA, sifum_refinement.mdsA_of varC_of mdsC', memA_of mem2CA)  A.evalw"
        by (simp del:fun_upd_apply add:A.evalw.seq A.decl_evalw' mdsC'_def mode_acquire_refinement_helper)
      with eval2A acq_mode_rel(1,3,4)
      have c2A'_def: "c2A' = Stop ;; tailA" and
        mem2A'_def: "mem2A' = memA_of mem2C"
        using A.eval_det by blast+
      from acq_mode_rel(3) in_RefRel c2A_def refrel_helper_Acq_Rel_ex1I
      obtain tailC' where
        c2C_def: "c2C = (Skip@[varC_of x +=m m]) ;; tailC'" and
        eval2C': "((Skip@[varC_of x +=m m]) ;; tailC', mdsC, mem2CC,
                   Stop ;; tailC', mdsC(m := insert (varC_of x) (mdsC m)), mem2CC)
                   C.evalw"
        by blast
      have eval_tailC': "(c2C, mdsC, mem2CC, Stop ;; tailC', mdsC', mem2CC)  C.evalw"
        by(simp add: mdsC'_def c2C_def eval2C')
      with eval_tailC C.eval_det have
        tails_eq: "tailC = tailC'" by blast
      moreover have "(c2A', mdsA_of mdsC', mem2A'A, Stop ;; tailC', mdsC', mem2CC)  RefRel_HighBranch"
      proof -
        from Acq_Mode_RefRel_HighBranchE[OF in_RefRel[simplified c2A_def c2C_def acq_mode_rel(3)]]
        have "(((Skip@[x +=m m]) ;; tailA, mdsA_of  mdsC,  memA_of mem2CA,
                Stop ;; tailA, mdsA_of mdsC', memA_of mem2CA)
                A.evalw) 
              (Stop ;; tailA, mdsA_of mdsC', memA_of mem2CA,
               Stop ;; tailC', mdsC', mem2CC)
               RefRel_HighBranch"
        using eval2C' mdsC'_concrete_vars_unwritable
          by (metis (mono_tags, lifting) mdsC'_def)
        hence "(Stop ;; tailA, mdsA_of mdsC', memA_of mem2CA,
                Stop ;; tailC', mdsC', mem2CC)
                RefRel_HighBranch"
        using A.evalw.seq A.decl_evalw' mdsC'_def A.update_modes.simps mode_acquire_refinement_helper
          by simp
        thus ?thesis
          by(simp add: c2C_def c2A'_def mem2A'_def)
      qed
      moreover have "(c1C', mdsC', mem1C'C, Stop ;; tailC', mdsC', mem2CC)  rel_invC"
        using c1C'_def tails_eq rel_invC_default
        by simp
      moreover note eval_tailC
      ultimately show "c2C' mem2C'.
              (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
              (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
               RefRel_HighBranch 
              (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC"
              by blast
    qed
  thus ?case using in_Rel' abs_steps_acq nevalA by blast
next
case (assign_load_rel cA x y tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "Stop ;; tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from assign_load_rel(1) assign_load_rel(2)
  have abs_steps_load: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from assign_load_rel.prems assign_load_rel(2)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC((varC_of x) := memC (varC_of y))"
    using C.seq_elim C.assign_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from assign_load_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(cA, mdsA, memAA,?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    using A.evalw.seq assign_evalw_loadA mem_assign_refinement_helper_var abs_steps_load by simp+
  with assign_load_rel(11)[simplified] assign_load_rel.prems c1C'_def
  have in_Rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    using assign_load_rel.hyps(4-5) mdsC'_def by blast
  have
    "c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R 
                  (c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, memA_of mem2CA 1
                   c2A', mdsA_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', mdsA_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)  RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
    proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    let ?mem2C' = "(mem2C((varC_of x) := mem2C (varC_of y)))"
    from in_rel_invC assign_load_rel(2) reg_is_not_the_varC_of_anything
    have "c2C = (varC_of x  Load (varC_of y)) ;; tailC"
      by (blast elim:rel_invCE)
    hence eval_tailC: "(c2C, mdsC, mem2CC, Stop ;; tailC, mdsC, ?mem2C'C)  sifum_lang_no_dma.evalw evA evB"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def)
    from assign_load_rel(1) in_R inR_E
    have c2A_def: "c2A = (x  aexp.Load y) ;; tailA"
      by (blast elim:inR_E A.rel_invE)
    hence c2A'_def: "c2A' = Stop ;; tailA"
      and mem2A'_def: "mem2A' = memA_of ?mem2C'"
      using eval2A abs_steps_load A.assign_elim A.seq_elim mem_assign_refinement_helper_var
      by fastforce+
    from assign_load_rel(3) in_Rel c2A_def refrel_helper_Assign_Load_ex1I
    obtain tailC' where
      c2C_def: "c2C = (varC_of x  Load (varC_of y)) ;; tailC'" and
      eval2C': "((varC_of x  Load (varC_of y)) ;; tailC', mdsC, mem2CC,
                 Stop ;; tailC', mdsC, mem2C((varC_of x) := mem2C (varC_of y))C)
                 C.evalw"
      by blast
    have eval_tailC': "(c2C, mdsC, mem2CC,
                  Stop ;; tailC', mdsC', mem2C((varC_of x) := mem2C (varC_of y))C)
                   C.evalw"
      by(simp add: mdsC'_def c2C_def eval2C')
    with eval_tailC C.eval_det have
        tails_eq: "tailC = tailC'" by blast
    moreover have "(c2A', mdsA_of mdsC', mem2A'A, Stop ;; tailC', mdsC', ?mem2C'C)
                     RefRel_HighBranch"
    proof -
      from Assign_Load_RefRel_HighBranchE[OF in_Rel[simplified c2A_def c2C_def assign_load_rel(3)]]
      have "(((x  aexp.Load y) ;; tailA, mdsA_of mdsC, memA_of mem2CA,
              Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A)
              A.evalw) 
            (Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A,
             Stop ;; tailC', mdsC', ?mem2C'C)
             RefRel_HighBranch"
      using eval2C'
        by (metis mdsC'_def)
      hence "(Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A,
              Stop ;; tailC', mdsC', ?mem2C'C)
              RefRel_HighBranch"
      using A.evalw.seq assign_evalw_loadA mdsC'_def A.update_modes.simps mem_assign_refinement_helper_var
        by simp
      thus ?thesis
        by(simp add: c2C_def c2A'_def mem2A'_def)
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; tailC', mdsC', ?mem2C'C)  rel_invC"
      using c1C'_def tails_eq rel_invC_default
      by simp
    moreover note eval_tailC eval_tailC'
    ultimately show "(c2C' mem2C'.
                  (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  C.evalw 
                  (c2A', mdsA_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)  RefRel_HighBranch 
                  (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      by blast
  qed
  thus ?case using in_Rel' abs_steps_load nevalA by blast
next
case (assign_const_rel cA x z tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "Stop ;; tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from assign_const_rel(1,2)
  have abs_steps_const: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from assign_const_rel.prems assign_const_rel(2)
  have c1C'_def: "c1C' = Stop ;; tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC((varC_of x) := z)"
    using C.seq_elim C.assign_elim assign_evalw_constC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from assign_const_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(cA, mdsA, memAA, ?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    using A.evalw.seq assign_evalw_constA mem_assign_refinement_helper_const abs_steps_const by simp+
  with assign_const_rel c1C'_def stop_rel mdsC'_def
  have in_Rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch" by blast
  have
    "c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R 
                  (c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, memA_of mem2CA 1
                   c2A', mdsA_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', mdsA_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)  RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
    proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    let ?mem2C' = "(mem2C((varC_of x) := z))"
    from in_rel_invC assign_const_rel(2) rel_invCE
    have "c2C = (varC_of x  Const z) ;; tailC" by blast
    moreover hence eval_tailC: "(c2C, mdsC, mem2CC, Stop ;; tailC, mdsC, ?mem2C'C)  sifum_lang_no_dma.evalw evA evB"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_constC mdsC'_def)
    moreover from assign_const_rel(1) in_R inR_E
    have c2A_def: "c2A = (x  Const z) ;; tailA"
      by (blast elim:inR_E A.rel_invE)
    moreover hence c2A'_def: "c2A' = Stop ;; tailA"
      and mem2A'_def: "mem2A' = memA_of ?mem2C'"
      using eval2A abs_steps_const A.assign_elim A.seq_elim mem_assign_refinement_helper_const
      by fastforce+
    moreover from assign_const_rel(3) in_Rel c2A_def refrel_helper_Assign_Const_ex1I
    obtain tailC' where c2C_def: "c2C = (varC_of x  Const z) ;; tailC'" and
      eval2C': "((varC_of x  Const z) ;; tailC', mdsC, mem2CC,
                 Stop ;; tailC', mdsC, mem2C((varC_of x) := z)C)
                 C.evalw"
      by blast
    have eval_tailC': "(c2C, mdsC, mem2CC,
                  Stop ;; tailC', mdsC', mem2C((varC_of x) := z)C)
                   C.evalw"
      by(simp add: mdsC'_def c2C_def eval2C')
    with eval_tailC C.eval_det have
        tails_eq: "tailC = tailC'" by blast
    moreover have "(c2A', mdsA_of mdsC', mem2A'A, Stop ;; tailC', mdsC', ?mem2C'C)
                     RefRel_HighBranch"
    proof -
      from Assign_Const_RefRel_HighBranchE[OF in_Rel[simplified c2A_def c2C_def assign_const_rel(3)]]
      have "(((x  Const z) ;; tailA, mdsA_of mdsC, memA_of mem2CA,
              Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A)
              A.evalw) 
            (Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A,
             Stop ;; tailC', mdsC', ?mem2C'C)
             RefRel_HighBranch"
      using eval2C'
        by (metis mdsC'_def)
      hence "(Stop ;; tailA, mdsA_of mdsC', memA_of ?mem2C'A,
              Stop ;; tailC', mdsC', ?mem2C'C)
              RefRel_HighBranch"
      using A.evalw.seq assign_evalw_constA mdsC'_def A.update_modes.simps mem_assign_refinement_helper_const
        by simp
      thus ?thesis
        by(simp add: c2C_def c2A'_def mem2A'_def)
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; tailC', mdsC', ?mem2C'C)  rel_invC"
      using c1C'_def tails_eq rel_invC_default
      by simp
    moreover note eval_tailC eval_tailC'
    ultimately show "(c2C' mem2C'.
                  (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  C.evalw 
                  (c2A', mdsA_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)  RefRel_HighBranch 
                  (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      by blast
  qed
  thus ?case using in_Rel' abs_steps_const nevalA by blast
next
case (if_reg_load_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_load_rel.hyps(1,2)
  have abs_steps_if_reg_load: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_reg_load_rel.prems if_reg_load_rel(2)
  have c1C'_def: "c1C' = (Stop ;; If (Neq (Load reg3) (Const 0)) thenC elseC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(reg3 := memC (varC_of x))"
    using C.seq_elim C.assign_elim C.skip_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from if_reg_load_rel(1-4) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using reg_not_visible_abs conc_only_var_assign_not_visible_abs A.neval.intros(1) by simp+
  with if_reg_load_rel c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    apply clarsimp
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_reg_load_rel.prems memA_of_def apply blast
    apply clarsimp
    done
  (* This might be usable for an Isar proof of rel', but not sure how best to approach that *)
  from reg_not_visible_abs conc_only_var_assign_not_visible_abs memA_of_def mem1C'_def
  have mem1C'_conds_match: "(mem1C' reg3 = 0) = (memA_of mem1C' x = 0)"
    by simp
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
    proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "(mem2C(reg3 := mem2C (varC_of x)))"
    from in_rel_invC if_reg_load_rel(2) rel_invCE
    have "c2C = (reg3  Load (varC_of x)) ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC" by blast
    hence eval_tailC: "(c2C, mdsC, mem2CC, Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC, mdsC, ?mem2C'C)  sifum_lang_no_dma.evalw evA evB"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def)
    from if_reg_load_rel(1) in_R
    have c2A_def: "c2A = If (Neq (Load x) (Const 0)) thenA elseA"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
    using neval2A abs_steps_if_reg_load A.neval_ZeroE
      by (clarsimp, blast)+
    from if_reg_load_rel.hyps(2,3) c2A_def c2A'_def in_Rel neval2A abs_steps_if_reg_load in_rel_invC
         refrel_helper_If_Reg_Load_exI
    obtain thenC' elseC' where
      c2C_def: "(c2C = (reg3  Load (varC_of x)) ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC')" and
      eval_tailC': "(c2C, mdsC, mem2CC,
                 Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC',
                      mdsC, mem2C(reg3 := mem2C (varC_of x))C)
                 C.evalw"
      by metis
    with eval_tailC C.eval_det have
      tails_eq: "elseC = elseC'  thenC = thenC'" by blast
    moreover from c2A'_def mem2A'_def c2A_def if_reg_load_rel(1-9)
    have "(c2A', mdsA, mem2A'A,
                    Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC',
                       mdsC, mem2C(reg3 := mem2C (varC_of x))C)
                    RefRel_HighBranch"
    proof -
      from If_Reg_Load_RefRel_HighBranchE[OF in_Rel[simplified c2A_def c2C_def if_reg_load_rel(1-9)]]
      have "(memC''.
           sifum_refinement.memA_of varC_of memC'' = sifum_refinement.memA_of varC_of ?mem2C' 
           (?mem2C' reg3 = 0) = (sifum_refinement.memA_of varC_of ?mem2C' x = 0) 
           ((reg3  Load (varC_of x)) ;;
             Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, memC''C,
            Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
            sifum_lang_no_dma.evalw evA evB) 
             (Stmt.If (Neq (Load x) (Const 0)) thenA elseA,
              sifum_refinement.mdsA_of varC_of mdsC, sifum_refinement.memA_of varC_of ?mem2C'A,
              Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
              RefRel_HighBranch"  
        by (metis neq0_conv)
      moreover have "(?mem2C' reg3 = 0) = (sifum_refinement.memA_of varC_of ?mem2C' x = 0)"
         using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def if_reg_load_rel(1-9)
         by simp
      moreover obtain memC'' where
        "sifum_refinement.memA_of varC_of memC'' = sifum_refinement.memA_of varC_of ?mem2C'"
        by simp
      ultimately have "(Stmt.If (Neq (Load x) (Const 0)) thenA elseA,
              sifum_refinement.mdsA_of varC_of mdsC, sifum_refinement.memA_of varC_of ?mem2C'A,
             Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
             RefRel_HighBranch"
        using c2C_def eval_tailC' if_reg_load_rel(1-9) conc_only_var_assign_not_visible_abs reg_not_visible_abs
        by auto
      thus ?thesis
      using if_reg_load_rel(1-9) c2A'_def c2A_def conc_only_var_assign_not_visible_abs mdsC'_def mem2A'_def reg_not_visible_abs
        by simp
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC', ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default tails_eq
      by simp
    moreover note eval_tailC' eval_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_reg_load_rel.hyps(3) by blast
  qed
  thus ?case using rel' abs_steps_if_reg_load nevalA by blast
next
case (if_reg_stop_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_stop_rel.hyps(1,2)
  have abs_steps_if_reg_stop: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_reg_stop_rel.prems if_reg_stop_rel(2)
  have c1C'_def: "c1C' = (If (Neq (Load reg3) (Const 0)) thenC elseC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by simp+
  from if_reg_stop_rel(1-4) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using reg_not_visible_abs conc_only_var_assign_not_visible_abs A.neval.intros(1) by simp+
  with if_reg_stop_rel c1C'_def mdsC'_def mem1C'_def
  have in_Rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch" by blast
  have
    "c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
    proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "mem2C"
    from in_rel_invC if_reg_stop_rel(2) rel_invCE
    have "c2C = Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC" by blast
    hence eval_tailC: "(c2C, mdsC, mem2CC, Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC, mdsC, ?mem2C'C)  sifum_lang_no_dma.evalw evA evB"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def)
    from if_reg_stop_rel in_R inR_E
    have c2A_def: "c2A = If (Neq (Load x) (Const 0)) thenA elseA"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
    using neval2A abs_steps_if_reg_stop A.neval_ZeroE
      by (clarsimp, blast)+
    from if_reg_stop_rel.hyps(2,3,7) c2A_def c2A'_def in_Rel neval2A abs_steps_if_reg_stop in_rel_invC
         refrel_helper_If_Reg_Stop_exI
    obtain thenC' elseC' where
      c2C_def: "(c2C = Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC')" and
      eval_tailC': "(c2C, mdsC, mem2CC,
                 Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, mem2CC)
                 C.evalw"
      by metis+
    with eval_tailC C.eval_det have
      tails_eq: "elseC = elseC'  thenC = thenC'" by blast
    moreover have "(c2A', mdsA_of mdsC', mem2A'A,
                    Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, mem2CC)
                    RefRel_HighBranch"
    proof -
      from If_Reg_Stop_RefRel_HighBranchE[OF in_Rel[simplified c2A_def c2C_def if_reg_stop_rel(3)]]
      have "(Stop ;; Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, mem2CC,
             Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
                 C.evalw 
            (Stmt.If (Neq (Load x) (Const 0)) thenA elseA, sifum_refinement.mdsA_of varC_of
                       mdsC, sifum_refinement.memA_of varC_of ?mem2C'A,
             Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
             RefRel_HighBranch"
      using eval_tailC' mdsC'_def
        by metis
      hence "(Stmt.If (Neq (Load x) (Const 0)) thenA elseA, mdsA_of mdsC, memA_of ?mem2C'A,
             Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC, ?mem2C'C)
             RefRel_HighBranch"
      using c2C_def eval_tailC'
        by auto
      thus ?thesis
      using c2A'_def c2A_def conc_only_var_assign_not_visible_abs mdsC'_def mem2A'_def reg_not_visible_abs
        by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC', mdsC', ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default tails_eq
      by simp
    moreover note eval_tailC' eval_tailC c2A'_def
    ultimately show "c2C' mem2C'.
              (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)
               sifum_lang_no_dma.evalw evA evB 
              (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
               RefRel_HighBranch 
              (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC"
      using mdsC'_def if_reg_stop_rel.hyps(3) by blast
  qed
  thus ?case using in_Rel' abs_steps_if_reg_stop nevalA by blast
next
case (if_reg_rel cA x thenA elseA cC thenC elseC mdsA mdsC memA memC)
  let ?c1A' = "if (evB memA (Neq (Load x) (Const 0))) then (thenA) else (elseA)"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_rel(1) if_reg_rel(2)
  have abs_steps_if_reg: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from if_reg_rel.prems if_reg_rel(2)
  have c1C'_def: "c1C' = (if (evB memC (Neq (Load reg3) (Const 0))) then (thenC) else (elseC))" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    apply simp_all
    by (erule C.if_elim, clarsimp+)+
  from if_reg_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(cA, mdsA, memAA, ?c1A', ?mdsA', ?mem1A'A)  A.evalw"
    using if_seq_evalw_helperA A.if_evalw by presburger
  hence nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    using abs_steps_if_reg by simp
  from if_reg_rel(3,4,7,12) if_reg_rel.prems c1C'_def mdsC'_def mem1C'_def evalA
  have in_Rel': "(?c1A',?mdsA',?mem1A'A, c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by clarsimp
  have
    "c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 1
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
    proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    let ?mem2C' = "mem2C"
    from in_rel_invC if_reg_rel(2) rel_invCE
    have "c2C = Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC" by blast
    hence eval_tailC: "(c2C, mdsC, mem2CC,
        if (evB mem2C (Neq (Load reg3) (Const 0)))
         then (thenC) else (elseC), mdsC, mem2CC)  sifum_lang_no_dma.evalw evA evB"
      by (blast intro:C.if_evalw if_seq_evalw_helperC)
    from if_reg_rel(1-10) in_R inR_E
    have c2A_def: "c2A = If (Neq (Load x) (Const 0)) thenA elseA"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = (if (evB (memA_of mem2C) (Neq (Load x) (Const 0)))
         then (thenA) else (elseA))" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using eval2A if_seq_evalw_helperA A.if_evalw if_reg_rel(1-4) A.eval_det
      by blast+
    from in_Rel c2A_def in_rel_invC if_reg_rel(2)
    have mem2C_reg_memA_x: "evB (memA_of mem2C) (Neq (Load x) (Const 0)) = evB mem2C (Neq (Load reg3) (Const 0))"
      apply -
      apply(erule RefRelE, simp_all)
      by (erule rel_invCE, simp+)
    with if_reg_rel.hyps(2,3,7) c2A_def c2A'_def in_Rel eval2A abs_steps_if_reg in_rel_invC
         refrel_helper_If_Reg_exI
    obtain thenC' elseC' where
      c2C_def: "(c2C = Stmt.If (Neq (Load reg3) (Const 0)) thenC' elseC')" and
      eval_tailC': "(c2C, mdsC, mem2CC,
                 if (evB mem2C (Neq (Load reg3) (Const 0)))
                  then (thenC') else (elseC'), mdsC, mem2CC)
                   C.evalw"
      by blast
    with eval_tailC C.eval_det have
      tails_eq: "elseC = elseC'  thenC = thenC'"
      by (simp add: c2C = Stmt.If (Neq (Load reg3) (Const 0)) thenC elseC)
    let ?c2C' = "if (evB mem2C (Neq (Load reg3) (Const 0))) then (thenC') else (elseC')"
    have "(c2A', mdsA_of mdsC', mem2A'A, ?c2C', mdsC', ?mem2C'C)  RefRel_HighBranch"
    proof -
      from in_Rel c2A_def c2C_def if_reg_rel(3,7,9) eval_tailC mdsC'_def c2A'_def mem2A'_def
           eval2A abs_steps_if_reg
      have "(c2C, mdsC, mem2CC, ?c2C', mdsC', ?mem2C'C)  C.evalw 
            (c2A', ?mdsA', memA_of ?mem2C'A, ?c2C', mdsC', ?mem2C'C)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Reg_RefRel_HighBranchE)
        apply(erule_tac x=mem2C in allE)
        apply(erule_tac x=mem2C in allE)
        apply(clarsimp split del: if_split)
        by presburger
      hence "(c2A', ?mdsA', memA_of ?mem2C'A, ?c2C', mdsC', ?mem2C'C)  RefRel_HighBranch"
      using c2C_def eval_tailC' mdsC'_def
        by auto
      thus ?thesis
      using c2A'_def c2A_def conc_only_var_assign_not_visible_abs mdsC'_def mem2A'_def reg_not_visible_abs
        by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?c2C', mdsC', ?mem2C'C)  rel_invC"
    proof -
      have "(if evB mem2C (Neq (Load reg3) (Const 0)) then thenC' else elseC', mdsC', mem2CC,
             c1C', mdsC', mem1C'C)
              rel_invC 
            (c1C', mdsC', mem1C'C,
             if evB mem2C (Neq (Load reg3) (Const 0)) then thenC' else elseC', mdsC', mem2CC)
              rel_invC"
        using c1C'_def if_reg_rel.hyps(11) mdsC'_def rel_invC.rel_invC_default tails_eq by auto
      thus ?thesis
        by (meson rel_invC_sym symE)
    qed
    moreover note eval_tailC' eval_tailC c2A'_def
    ultimately show "c2C' mem2C'.
              (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
              (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
               RefRel_HighBranch 
              (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC"
      using mdsC'_def by blast
  qed
  thus ?case using in_Rel' abs_steps_if_reg nevalA by blast
next
case (if_then_rel_1 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_1.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_1.prems if_then_rel_1(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_elim C.skip_elim by blast+
  from if_then_rel_1(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.intros(1) by auto
  with if_then_rel_1 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "mem2C(reg1 := mem2C y_mem)"
    let ?tail2C = "(reg2  Load z_mem) ;;
                (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0)"
    from in_rel_invC if_then_rel_1(2-3)
    have "c2C = cC 
          c2C = (reg1  Load y_mem) ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_1(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      using if_then_rel_1(2,3) c1C'_def C.evalw.seq C.skip_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_1(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_1(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
      by (clarsimp, meson C.evalw.seq C.skip_evalw)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "((reg1  Load y_mem) ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, ?mem2C'C)  C.evalw"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def)
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_1(1-6)
    have c2C_else_def: "c2A  cA  c2C = (reg1  Load y_mem) ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'C)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_1.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C' 
           ((reg1  Load y_mem) ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, ?mem2C'C)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'C)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C(reg1 := mem2C y_mem)" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'"
        by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def if_then_rel_1(3) rel_invC_2 by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_1.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_1 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_1.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_1.prems if_else_rel_1(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(reg1 := memC y_mem)"
    using C.seq_elim C.assign_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from if_else_rel_1(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 conc_only_var_assign_not_visible_abs reg_not_visible_abs by simp+
  with if_else_rel_1 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    apply clarsimp
    apply(erule_tac x=memA in allE)
    apply(erule_tac x=mdsC in allE)
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_else_rel_1.prems memA_of_def apply blast
    apply clarsimp
    done
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "mem2C(reg1 := mem2C y_mem)"
    let ?tail2C = "Skip ;;
                (reg0  Load y_mem) ;; (x_mem  Load reg0)"
    from in_rel_invC if_else_rel_1(2-3)
    have "c2C = cC 
          c2C = Skip ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_1(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "(Skip ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, mem2CC)  C.evalw"
      using if_else_rel_1(2,3) c1C'_def C.evalw.seq C.skip_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_1(1-6)
    have c2C_then_def: "c2A  cA  c2C = Skip ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_then: "c2A  cA"
      with in_then in_Rel c2A_def c2C_then_def if_else_rel_1.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Skip ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Then_RefRel_HighBranchE)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C" in allE)
        by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C"
        by simp
      ultimately show ?thesis
        using eval_then_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_else_rel_1(2,3) rel_invC_2' mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, ?mem2C'C)  C.evalw"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def c1C'_def if_else_rel_1(2,3))
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_1(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_1.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C' 
           (cC, mdsC, memC''C,
            c1C', mdsC, ?mem2C'C)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'"
        by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_1.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_1' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_1'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_1'.prems if_then_rel_1'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_then_rel_1'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.intros(1) by auto
  with if_then_rel_1' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "(reg2  Load z_mem) ;;
                (reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0)"
    from in_rel_invC if_then_rel_1'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_1'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      using if_then_rel_1'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_1'(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_1'(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
      by (clarsimp, meson C.seq_stop_evalw)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def)
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_1'(1-6)
    have c2C_else_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_1'(1-8) c1C'_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_1'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C" in allE)
        using eval_else_tailC by blast+
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_then_rel_1'(3) rel_invC_3 by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_1'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_1' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_1'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_1'.prems if_else_rel_1'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_else_rel_1'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 by simp+
  with if_else_rel_1' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "Skip ;; (reg0  Load y_mem) ;; (x_mem  Load reg0)"
    from in_rel_invC if_else_rel_1'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_1'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      using if_else_rel_1'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_1'(1-6)
    have c2C_then_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_1'(1-8) c1C'_def c2A_then_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      with in_else in_Rel c2A_def c2C_then_def if_else_rel_1'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        by (blast elim: If_Then_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C"
        by simp
      ultimately show ?thesis
        using eval_then_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_else_rel_1'(2,3) rel_invC_3' mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def c1C'_def if_else_rel_1'(2,3))
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_1'(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_1'(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      from in_else c2A_def if_else_rel_1'(1) have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_1'.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (cC, mdsC, memC''C,
            c1C', mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C" in allE)
        using eval_else_tailC by blast+
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_1'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_2 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_2.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_2.prems if_then_rel_2(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_elim C.skip_elim by blast+
  from if_then_rel_2(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.intros(1) by auto
  with if_then_rel_2 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "mem2C(reg2 := mem2C z_mem)"
    let ?tail2C = "(reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0)"
    from in_rel_invC if_then_rel_2(2-3)
    have "c2C = cC  c2C = (reg2  Load z_mem) ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_2(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      using if_then_rel_2(2,3) c1C'_def C.evalw.seq C.skip_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_2(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_2(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
      by (clarsimp, meson C.evalw.seq C.skip_evalw)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "((reg2  Load z_mem) ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, ?mem2C'C)  C.evalw"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def)
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_2(1-6)
    have c2C_else_def: "c2A  cA  c2C = (reg2  Load z_mem) ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'C)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_2.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C' 
           ((reg2  Load z_mem) ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, ?mem2C'C)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'C)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def eval_else_tailC by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'" by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def if_then_rel_2(3) rel_invC_4 by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_2.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_2 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_2.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_2.prems if_else_rel_2(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(reg2 := memC z_mem)"
    using C.seq_elim C.assign_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from if_else_rel_2(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 conc_only_var_assign_not_visible_abs reg_not_visible_abs by simp+
  with if_else_rel_2 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    apply clarsimp
    apply(erule_tac x=memA in allE)
    apply(erule_tac x=mdsC in allE)
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_else_rel_2.prems memA_of_def apply blast
    apply clarsimp
    done
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C' = "mem2C(reg2 := mem2C z_mem)"
    let ?tail2C = "(reg0  Load y_mem) ;; (x_mem  Load reg0)"
    from in_rel_invC if_else_rel_2(2-3)
    have "c2C = cC 
          c2C = Skip ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_2(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "(Skip ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, mem2CC)  C.evalw"
      using if_else_rel_2(2,3) c1C'_def C.evalw.seq C.skip_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_2(1-6)
    have c2C_then_def: "c2A  cA  c2C = Skip ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      with in_else in_Rel c2A_def c2C_then_def if_else_rel_2.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Skip ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Then_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C" in allE)
        by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C"
        by simp
      ultimately show ?thesis
        using eval_then_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_else_rel_2(2,3) rel_invC_4' mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, ?mem2C'C)  C.evalw"
      by (simp del:fun_upd_apply add:C.evalw.seq assign_evalw_loadC mdsC'_def c1C'_def if_else_rel_2(2,3))
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_2(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_2.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C' 
           (cC, mdsC, memC''C,
            c1C', mdsC, ?mem2C'C)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def eval_else_tailC by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'"
        by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_2.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_2' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_2'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_2'.prems if_then_rel_2'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_then_rel_2'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.intros(1) by auto
  with if_then_rel_2' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "(reg0  Add (Load reg1) (Load reg2)) ;; (x_mem  Load reg0)"
    from in_rel_invC if_then_rel_2'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_2'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      using if_then_rel_2'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_2'(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_2'(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
      by (clarsimp, meson C.seq_stop_evalw)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def)
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_2'(1-6)
    have c2C_else_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_2'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        using eval_else_tailC by (blast elim: If_Else_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_then_rel_2'(3) rel_invC_5 by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_2'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_2' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_2'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_2'.prems if_else_rel_2'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_else_rel_2'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 by simp+
  with if_else_rel_2' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "(reg0  Load y_mem) ;; (x_mem  Load reg0)"
    from in_rel_invC if_else_rel_2'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_2'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      using if_else_rel_2'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_2'(1-6)
    have c2C_then_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      with in_else in_Rel c2A_def c2C_then_def if_else_rel_2'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        by (blast elim: If_Then_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C"
        by simp
      ultimately show ?thesis
        using eval_then_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_else_rel_2'(2,3) rel_invC_5' mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def c1C'_def if_else_rel_2'(2,3))
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_2'(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      from in_else c2A_def if_else_rel_2'(1) have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_2'.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (cC, mdsC, memC''C,
            c1C', mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
        using eval_else_tailC by (blast elim: If_Else_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_2'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_3 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_3.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_3.prems if_then_rel_3(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(reg0 := memC y_mem)"
    using C.seq_elim C.assign_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from if_then_rel_3(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 conc_only_var_assign_not_visible_abs reg_not_visible_abs by simp+
  with if_then_rel_3 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    apply clarsimp
    apply(erule_tac x=memA in allE)
    apply(erule_tac x=mdsC in allE)
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_then_rel_3.prems memA_of_def apply blast
    apply clarsimp
    done
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C'_t = "mem2C(reg0 := mem2C y_mem)"
    let ?mem2C'_e = "mem2C(reg0 := evA mem2C (Add (Load reg1) (Load reg2)))"
    let ?tail2C = "x_mem  Load reg0"
    from in_rel_invC if_then_rel_3(2-3)
    have "c2C = cC  c2C = (reg0  Add (Load reg1) (Load reg2)) ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_3(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, ?mem2C'_tC)  C.evalw"
      using if_then_rel_3(2,3) c1C'_def C.evalw.seq assign_evalw_loadC by simp
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_3(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'_tC)  RefRel_HighBranch"
    proof -
      assume in_then: "c2A = cA"
      from in_then c2A_def if_then_rel_3(1) have
        c2A_then_def: "c2A = x_var  Load y_var"
        by clarsimp
      with in_then in_Rel c2A_def c2C_then_def if_then_rel_3.hyps(2-4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C'_t 
           ((reg0  Load y_mem) ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Then_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="mem2C(reg0 := mem2C y_mem)" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'_t" by simp
      moreover note c2A'_def mem2A'_def if_then_rel_3(1-3) c1C'_def
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_then_tailC reg_not_visible_abs by fast
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'_tC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "((reg0  Add (Load reg1) (Load reg2)) ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, ?mem2C'_eC)  C.evalw"
      using C.evalw.seq C.assign_evalw' evA.simps mdsC'_def by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_3(1-6)
    have c2C_else_def: "c2A  cA  c2C = (reg0  Add (Load reg1) (Load reg2)) ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_3(1-8) c1C'_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'_eC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_3.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C'_e 
           ((reg0  Add (Load reg1) (Load reg2)) ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, ?mem2C'_eC)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'_eC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'_e" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs eval_else_tailC memA_of_def by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'_e" by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, ?mem2C'_eC)  rel_invC"
      using c1C'_def if_then_rel_3(3) rel_invC_default by clarsimp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_3.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_3 cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_3.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_3.prems if_else_rel_3(2,3)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(reg0 := evA memC (Add (Load reg1) (Load reg2)))"
    using C.seq_elim C.assign_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(13))+
  from if_else_rel_3(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 conc_only_var_assign_not_visible_abs reg_not_visible_abs by simp+
  with if_else_rel_3 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    apply clarsimp
    apply(erule_tac x=memA in allE)
    apply(erule_tac x=mdsC in allE)
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_else_rel_3.prems memA_of_def apply blast
    apply clarsimp
    done
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?mem2C'_t = "mem2C(reg0 := mem2C y_mem)"
    let ?mem2C'_e = "mem2C(reg0 := evA mem2C (Add (Load reg1) (Load reg2)))"
    let ?tail2C = "x_mem  Load reg0"
    from in_rel_invC if_else_rel_3(2-3)
    have "c2C = cC 
          c2C = (reg0  Load y_mem) ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_3(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "((reg0  Load y_mem) ;; ?tail2C, mdsC, mem2CC, Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  C.evalw"
      using if_else_rel_3(2,3) C.evalw.seq assign_evalw_loadC by simp
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_3(1-6)
    have c2C_then_def: "c2A  cA  c2C = (reg0  Load y_mem) ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_3(1-8) c1C'_def c2A_then_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  RefRel_HighBranch"
    proof -
      assume in_then: "c2A  cA"
      with c2A_then_def in_Rel c2A_def c2C_then_def if_else_rel_3.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C'_t 
           ((reg0  Load y_mem) ;; ?tail2C, mdsC, memC''C,
            Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  C.evalw) 
             (c2A', mdsA, mem2A'A, Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Then_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'_t" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'_t" by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_then_tailC reg_not_visible_abs by fast
    qed
    moreover have "(c1C', mdsC', mem1C'C, Stop ;; ?tail2C, mdsC, ?mem2C'_tC)  rel_invC"
      using c1C'_def if_else_rel_3(2,3) rel_invC_default mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, ?mem2C'_eC)  C.evalw"
      using C.evalw.seq C.assign_evalw' evA.simps mdsC'_def c1C'_def if_else_rel_3(2,3) by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_3(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_3(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'_eC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_3.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of ?mem2C'_e 
           (cC, mdsC, memC''C,
            c1C', mdsC, ?mem2C'_eC)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'_eC)  RefRel_HighBranch"
        apply clarsimp
        apply(erule If_Else_RefRel_HighBranchE, simp+)
        apply(erule_tac x="memA_of memC''" in allE)
        apply(erule_tac x="mdsC" in allE)
        apply(erule_tac x="?mem2C'_e" in allE)
        using conc_only_var_assign_not_visible_abs reg_not_visible_abs memA_of_def eval_else_tailC by auto
      moreover obtain memC'' where "memA_of memC'' = memA_of ?mem2C'_e"
        by simp
      ultimately show ?thesis
        using conc_only_var_assign_not_visible_abs eval_else_tailC reg_not_visible_abs by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'_eC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_3.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_3' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_3'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_then_rel_3'.prems if_then_rel_3'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_then_rel_3'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.intros(1) by auto
  with if_then_rel_3' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "x_mem  Load reg0"
    from in_rel_invC if_then_rel_3'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_then_rel_3'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is also in the 'then' branch *)
    moreover have eval_then_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      using if_then_rel_3'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_3'(1-6)
    have c2C_then_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_3'(1-8) c1C'_def
    have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_then: "c2A = cA"
      from in_then c2A_def if_then_rel_3'(1) have
        c2A_then_def: "c2A = x_var  Load y_var"
        by clarsimp
      with in_then in_Rel c2A_def c2C_then_def if_then_rel_3'.hyps(2-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (cC, mdsC, memC''C,
            c1C', mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
        using eval_then_tailC by (blast elim: If_Then_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      moreover note c2A'_def mem2A'_def if_then_rel_3'(1-3) c1C'_def
      ultimately show ?thesis using eval_then_tailC by fast
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    (* c2C is in the other, 'else' branch *)
    moreover have eval_else_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def)
    moreover from c2A_def in_Rel in_rel_invC if_then_rel_3'(1-6)
    have c2C_else_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_3'(1-8) c1C'_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      from in_else c2A_def have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_then_rel_3'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        using eval_else_tailC by (blast elim: If_Else_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_then_rel_3'(3) rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_3'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_3' cA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_3'.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_else_rel_3'.prems if_else_rel_3'(2,3)
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by blast+
  from if_else_rel_3'(1-5) mdsC'_def mem1C'_def
  have nevalA: "A.neval cA, mdsA, memAA 0 ?c1A', ?mdsA', ?mem1A'A" and
    memA_unchanged: "?mem1A' = memA"
    using A.neval.neval_0 by simp+
  with if_else_rel_3' c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 0
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           neval2A: "A.neval c2A, mdsA, memA_of mem2CA 0 c2A', mdsA_of mdsC', mem2A'A"
    let ?tail2C = "x_mem  Load reg0"
    from in_rel_invC if_else_rel_3'(2-3)
    have "c2C = cC 
          c2C = Stop ;; ?tail2C"
      by (blast elim: rel_invCE)
    moreover from in_R if_else_rel_3'(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)
    moreover hence
      c2A'_def: "c2A' = c2A" and
      mem2A'_def: "mem2A' = memA_of mem2C"
      using neval2A abs_steps_this A.neval_ZeroE
      by (clarsimp, blast)+

    (* c2C is in the other, 'then' branch *)
    moreover have eval_then_tailC: "(Stop ;; ?tail2C, mdsC, mem2CC, ?tail2C, mdsC, mem2CC)  C.evalw"
      using if_else_rel_3'(2,3) c1C'_def C.seq_stop_evalw by blast
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_3'(1-6)
    have c2C_then_def: "c2A  cA  c2C = Stop ;; ?tail2C"
      by (blast elim: If_Then_RefRel_HighBranchE rel_invCE)
    moreover with c2A_def
    have c2A_then_def: "c2A  cA  c2A = x_var  Load y_var"
      by clarsimp
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_3'(1-8) c1C'_def c2A_then_def
    have "c2A  cA  (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A  cA"
      with in_else in_Rel c2A_def c2C_then_def if_else_rel_3'.hyps(4) c2A'_def mem2A'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (Stop ;; ?tail2C, mdsC, memC''C,
            ?tail2C, mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, ?tail2C, mdsC, mem2CC)  RefRel_HighBranch"
        using eval_then_tailC by (blast elim: If_Then_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C"
        by simp
      ultimately show ?thesis
        using eval_then_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, ?tail2C, mdsC, mem2CC)  rel_invC"
      using c1C'_def if_else_rel_3'(2,3) rel_invC_default mem1C'_def mdsC'_def by simp

    (* c2C is also in the 'else' branch *)
    moreover have eval_else_tailC: "(cC, mdsC, mem2CC, c1C', mdsC, mem2CC)  C.evalw"
      by (simp del:fun_upd_apply add:C.seq_stop_evalw mdsC'_def c1C'_def if_else_rel_3'(2,3))
    moreover from c2A_def in_Rel in_rel_invC if_else_rel_3'(1-6)
    have c2C_else_def: "c2A = cA  c2C = cC"
      by (blast elim: If_Else_RefRel_HighBranchE rel_invCE)
    moreover have "c2A = cA  (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
    proof -
      assume in_else: "c2A = cA"
      from in_else c2A_def if_else_rel_3'(1) have
        c2A_else_def: "c2A = x_var  Add (Load y_var) (Load z_var)"
        by clarsimp
      with in_else in_Rel c2A_def c2C_else_def if_else_rel_3'.hyps(1-4) c2A'_def mem2A'_def c1C'_def
      have "(memC''.
           memA_of memC'' = memA_of mem2C 
           (cC, mdsC, memC''C,
            c1C', mdsC, mem2CC)  C.evalw) 
             (c2A', mdsA, mem2A'A, c1C', mdsC, mem2CC)  RefRel_HighBranch"
        using eval_else_tailC by (blast elim: If_Else_RefRel_HighBranchE)
      moreover obtain memC'' where "memA_of memC'' = memA_of mem2C" by simp
      ultimately show ?thesis using eval_else_tailC by auto
    qed
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, mem2CC)  rel_invC"
      using c1C'_def rel_invC_default by simp

    moreover note eval_then_tailC eval_else_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_3'.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_then_rel_4 cA cC mdsA mdsC memA memC)
  let ?c1A' = "Stop"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_then_rel_4.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from if_then_rel_4.prems if_then_rel_4(2,3)
  have c1C'_def: "c1C' = Stop" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(x_mem := memC reg0)"
    using C.assign_elim assign_evalw_loadC
    by metis+
  from if_then_rel_4(1-7) mdsC'_def mem1C'_def
  have evalA: "(cA, mdsA, memAA,?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    using A.assign_evalw' evA.simps(2) mem_assign_refinement_helper_const varC_of.simps(2) abs_steps_this
    by (metis, simp, metis)
  with if_then_rel_4 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 1
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    let ?mem2C' = "mem2C(x_mem := mem2C reg0)"
    from in_rel_invC if_then_rel_4(2-3)
    have c2C_def: "c2C = cC"
      by (blast elim: rel_invCE)
    from in_rel_invC if_then_rel_4(1-4,6) in_R
    have zA: "memA z_var = 0"
      using A.prog_high_branch_def inR_E inv5E
      by (metis if_then_rel_4.hyps(6))
    from in_rel_invC if_then_rel_4(1-4) in_R
    have "memA z_var = memA_of mem2C z_var"
      using inR_E A.low_mds_eq_def dma_def emptyE inv5E var.distinct(5)
      by (metis (mono_tags, opaque_lifting))
    with zA have z2A: "memA_of mem2C z_var = 0"
      by simp

    moreover from in_R if_then_rel_4(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Add (Load y_var) (Load z_var)"
      by (blast elim: inR_E A.rel_invE)

    from in_Rel c2C_def if_then_rel_4(1,2,3) in_rel_invC c2A_def z2A
    have r0y: "mem2C reg0 = mem2C y_mem"
      apply clarsimp
      apply(case_tac "cA = c2A")
       apply clarsimp
       apply(erule If_Then_RefRel_HighBranchE, simp+)
       using memA_of_def apply force
      apply clarsimp
      apply(erule If_Else_RefRel_HighBranchE, simp+)
      using memA_of_def by force

    moreover from c2A_def have
      c2A'_def: "c2A' = Stop"
      using eval2A A.assign_elim if_then_rel_4(1)
      by (case_tac "cA = c2A", clarsimp+)

    moreover with c2A_def if_then_rel_4(1-7) have
      mem2A'_def: "mem2A' = memA_of ?mem2C'"
      using eval2A c2A_def mdsC'_def
      apply clarsimp
      apply(case_tac "cA = c2A")
       apply clarsimp
       apply(drule A.assign_elim)
       apply clarsimp
       using r0y apply clarsimp
       using memA_of_def
       apply (metis mem_assign_refinement_helper_const varC_of.simps(2) varC_of.simps(3))
      apply clarsimp
      apply(drule A.assign_elim)
      apply clarsimp
      using r0y z2A apply clarsimp
      using memA_of_def 
      apply (metis mem_assign_refinement_helper_const varC_of.simps(2) varC_of.simps(3))
      done

    moreover have eval_tailC: "(c2C, mdsC, mem2CC, c1C', mdsC, ?mem2C'C)  C.evalw"
      using if_then_rel_4(2,3) c2C_def c1C'_def C.evalw.seq assign_evalw_loadC by simp
    moreover from c2A'_def mem2A'_def c2A_def if_then_rel_4(1-8) c1C'_def
    have "(c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
      by (meson RefRel_HighBranch.stop_rel)
    (* c2C is also in the 'then' branch *)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default by simp
    (* c2C is in the other, 'else' branch *)
    moreover have "(c1C', mdsC', mem1C'C, Stop, mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def if_then_rel_4(3) rel_invC_default by clarsimp
    moreover note eval_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_then_rel_4.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (if_else_rel_4 cA cC mdsA mdsC memA memC)
  let ?c1A' = "Stop"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_else_rel_4.hyps(1-3)
  have abs_steps_this: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from if_else_rel_4.prems if_else_rel_4(2,3)
  have c1C'_def: "c1C' = Stop" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(x_mem := memC reg0)"
    using C.assign_elim assign_evalw_loadC
    by metis+
  from if_else_rel_4(1-8) mdsC'_def mem1C'_def
  have evalA: "(cA, mdsA, memAA,?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A"
    using A.assign_evalw' evA.simps(2) mem_assign_refinement_helper_const varC_of.simps(2) abs_steps_this
    by (metis, simp, metis)
  with if_else_rel_4 c1C'_def mdsC'_def mem1C'_def
  have rel': "(?c1A',?mdsA',?mem1A'A,c1C',mdsC',mem1C'C)  RefRel_HighBranch"
    by blast
  have
    "(c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 1
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC))"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    let ?mem2C' = "mem2C(x_mem := mem2C reg0)"
    from in_rel_invC if_else_rel_4(2-3)
    have c2C_def: "c2C = cC"
      by (blast elim: rel_invCE)
    from in_rel_invC if_else_rel_4(1-4,6) in_R
    have zA: "memA z_var = 0"
      using A.prog_high_branch_def inR_E inv6E
      by (metis if_else_rel_4.hyps(6))
    from in_rel_invC if_else_rel_4(1-4) in_R
    have "memA z_var = memA_of mem2C z_var"
      using inR_E A.low_mds_eq_def dma_def emptyE inv6E var.distinct(5)
      by (metis (mono_tags, opaque_lifting))
    with zA have z2A: "memA_of mem2C z_var = 0"
      by simp

    moreover from in_R if_else_rel_4(1) inR_E A.rel_invE have
      c2A_def: "c2A = cA  c2A = x_var  Load y_var"
      by (blast elim: inR_E A.rel_invE)

    from in_Rel c2C_def if_else_rel_4(1,2,3) in_rel_invC c2A_def z2A
    have r0y: "mem2C reg0 = mem2C y_mem"
      apply clarsimp
      apply(case_tac "cA = c2A")
       apply clarsimp
       apply(erule If_Else_RefRel_HighBranchE, simp+)
       using memA_of_def apply force
      apply clarsimp
      apply(erule If_Then_RefRel_HighBranchE, simp+)
      using memA_of_def by force

    moreover from c2A_def have
      c2A'_def: "c2A' = Stop"
      using eval2A A.assign_elim if_else_rel_4(1)
      by (case_tac "cA = c2A", clarsimp+)

    moreover with c2A_def if_else_rel_4(1-7) have
      mem2A'_def: "mem2A' = memA_of ?mem2C'"
      using eval2A c2A_def mdsC'_def
      apply clarsimp
      apply(case_tac "cA  c2A")
       apply clarsimp
       apply(drule A.assign_elim)
       apply clarsimp
       using r0y apply clarsimp
       using memA_of_def
       apply (metis mem_assign_refinement_helper_const varC_of.simps(2) varC_of.simps(3))
      apply clarsimp
      apply(drule A.assign_elim)
      apply clarsimp
      using r0y z2A apply clarsimp
      using memA_of_def 
      apply (metis mem_assign_refinement_helper_const varC_of.simps(2) varC_of.simps(3))
      done

    moreover have eval_tailC: "(c2C, mdsC, mem2CC, c1C', mdsC, ?mem2C'C)  C.evalw"
      using if_else_rel_4(2,3) c2C_def c1C'_def C.evalw.seq assign_evalw_loadC by simp
    moreover from c2A'_def mem2A'_def c2A_def if_else_rel_4(1-8) c1C'_def
    have "(c2A', mdsA, mem2A'A, c1C', mdsC, ?mem2C'C)  RefRel_HighBranch"
      by (meson RefRel_HighBranch.stop_rel)
    (* c2C is also in the 'then' branch *)
    moreover have "(c1C', mdsC', mem1C'C, c1C', mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def rel_invC_default by simp
    (* c2C is in the other, 'else' branch *)
    moreover have "(c1C', mdsC', mem1C'C, Stop, mdsC, ?mem2C'C)  rel_invC"
      using c1C'_def if_else_rel_4(3) rel_invC_default by clarsimp
    moreover note eval_tailC c2A'_def
    ultimately show "(c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
      using mdsC'_def if_else_rel_4.hyps(1-6) by blast
  qed
  thus ?case using rel' abs_steps_this nevalA by blast
next
case (stop_seq_rel cA tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from stop_seq_rel(1,2)
  have abs_steps_stop: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from stop_seq_rel
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by auto
  hence nevalA: "A.neval cA, mdsA, memAA 1 ?c1A', ?mdsA', ?mem1A'A" and
    rel': "(?c1A', ?mdsA', ?mem1A'A, c1C', mdsC', mem1C'C)  RefRel_HighBranch"
    using stop_seq_rel A.seq_stop_evalw by auto
  have "c2A c2C mem2C c2A' mem2A'.
                  (cA, mdsA, memAA, c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA)  A.R 
                  (c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA, c2C, mdsC, mem2CC)
                   RefRel_HighBranch 
                  (cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC 
                  A.neval
                   c2A, mdsA, sifum_refinement.memA_of varC_of mem2CA 1
                   c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A 
                  (c2C' mem2C'.
                      (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
                      (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
                       RefRel_HighBranch 
                      (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC)"
  proof(clarsimp)
    fix c2A c2C mem2C c2A' mem2A'
    assume in_R: "(cA, mdsA, memAA, c2A, mdsA, memA_of mem2CA)  A.R" and
           in_Rel: "(c2A, mdsA, memA_of mem2CA, c2C, mdsC, mem2CC)  RefRel_HighBranch" and
           in_rel_invC: "(cC, mdsC, memCC, c2C, mdsC, mem2CC)  rel_invC" and
           eval2A: "(c2A, mdsA, memA_of mem2CA, c2A', mdsA_of mdsC', mem2A'A)  A.evalw"
    from in_rel_invC stop_seq_rel(2) obtain tailC' where c2C_def:
      "c2C = Stop ;; tailC'"
      by (blast elim:rel_invCE)
    hence eval_tailC': "(c2C, mdsC, mem2CC, tailC', mdsC, mem2CC)  C.evalw"
      by (blast intro:C.seq_stop_evalw)
    moreover from stop_seq_rel(1) in_R inR_E
    have c2A_def: "c2A = Stop ;; tailA"
      by (blast elim: inR_E A.rel_invE)
    moreover from c2A_def
    have c2A'_def: "c2A' = tailA" and
      mem2A'_def: "mem2A' = memA_of mem2C"
    using eval2A abs_steps_stop A.seq_stop_elim
      by simp+
    moreover with c2C_def have
      "(c2A', mdsA_of mdsC', mem2A'A, tailC', mdsC', mem2CC)  RefRel_HighBranch"
      using in_Rel c2A_def c2C_def mdsC'_def Stop_tail_RefRel_HighBranchE C.seq_stop_evalw
      by blast
    moreover have "(c1C', mdsC', mem1C'C, tailC', mdsC', mem2CC)  rel_invC"
      using c1C'_def in_rel_invC stop_seq_rel(2) c2C_def
      by (blast elim:rel_invCE intro:rel_invC.intros)
    ultimately show "c2C' mem2C'.
              (c2C, mdsC, mem2CC, c2C', mdsC', mem2C'C)  sifum_lang_no_dma.evalw evA evB 
              (c2A', sifum_refinement.mdsA_of varC_of mdsC', mem2A'A, c2C', mdsC', mem2C'C)
               RefRel_HighBranch 
              (c1C', mdsC', mem1C'C, c2C', mdsC', mem2C'C)  rel_invC"
      using mdsC'_def by blast
  qed
  thus ?case using rel' abs_steps_stop nevalA by blast
next
case stop_rel
  with C.stop_no_eval have False by simp
  thus ?case by simp
qed

lemma RefRel_HighBranch_secure_refinement:
  "secure_refinement A.R RefRel_HighBranch rel_invC"
  apply(unfold secure_refinement_def2)
  apply(rule conjI)
   apply(rule closed_others_RefRel_HighBranch)
  apply(rule conjI)
   apply(rule preserves_modes_mem_RefRel_HighBranch)
  apply(rule conjI)
   apply(rule new_vars_private_RefRel_HighBranch)
  apply(rule conjI)
   apply(rule rel_invC_closed_glob_consistent)
  apply clarsimp
  apply(rule induction_full_RefRel_HighBranch, simp+)
  done

lemma strong_low_bisim_mm_RC_of_R:
  "C.strong_low_bisim_mm (RC_of A.R RefRel_HighBranch rel_invC)"
  apply(rule RC_of_strong_low_bisim_mm)
    apply(rule A.strong_low_bisim_mm_R)
   apply(rule RefRel_HighBranch_secure_refinement)
  apply(rule rel_invC_sym)
  done

definition
  mds0 :: "Mode  varC set"
where
  "mds0  λm. case m of AsmNoReadOrWrite  {reg0, reg1, reg2, reg3} |
                        AsmNoWrite  {} |
                        _  {}"

lemma regs_the_only_concrete_only_vars:
  "vC  range varC_of  vC  {reg0, reg1, reg2, reg3}"
  by (case_tac vC, (clarsimp|metis rangeI varC_of.simps)+)

lemma prog_high_branch_RefRel:
  "(A.prog_high_branch, mdsA_of mds0, memA_of memCA, C.prog_high_branchC, mds0, memCC)  RefRel_HighBranch"
  unfolding A.prog_high_branch_def C.prog_high_branchC_def mds0_def
  using regs_the_only_concrete_only_vars doesnt_have_mode has_modeA NoRWA_implies_NoRWC
  apply clarsimp

  apply(rule acq_mode_rel, (simp|clarsimp)+)
  apply(drule C.seq_decl_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)

  apply(rule acq_mode_rel, (simp|clarsimp)+)
  apply(drule C.seq_decl_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)

  apply(rule acq_mode_rel, (simp|clarsimp)+)
  apply(drule C.seq_decl_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)

  apply(rule assign_const_rel, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)
  
  apply(rule assign_const_rel, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)

  apply(rule assign_load_rel, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)

  apply(rule if_reg_load_rel, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule if_reg_stop_rel, (simp|clarsimp)+)

  apply(drule C.seq_stop_elim, clarsimp)

  apply(rule if_reg_rel, (simp|clarsimp)+)
   apply(rule rel_invC_1, clarsimp+)
  apply(rule conjI)

   (* Then *)
   apply clarsimp
   apply(rule if_then_rel_1, (simp|clarsimp)+)
   apply(drule C.if_elim, simp+)
   apply(drule C.seq_elim, simp+)
   apply(drule C.skip_elim, simp+)
   apply(rule if_then_rel_1', (simp|clarsimp)+)
   apply(drule C.seq_stop_elim, simp+)
   apply(rule if_then_rel_2, (simp|clarsimp)+)
   apply(drule C.seq_elim, simp+)
   apply(drule C.skip_elim, simp+)
   apply(rule if_then_rel_2', (simp|clarsimp)+)
   apply(drule C.seq_stop_elim, simp+)
   apply(rule if_then_rel_3, (simp|clarsimp)+)
   apply(drule C.seq_assign_elim, simp+)
   apply(rule if_then_rel_3', (simp|clarsimp)+)
   apply(drule C.seq_stop_elim, simp+)
   apply(rule if_then_rel_4, (simp|clarsimp)+)
   apply(drule C.assign_elim, simp+)
   apply(rule stop_rel)

  (* Else *)
  apply clarsimp
  apply(rule if_else_rel_1, (simp|clarsimp)+)
  apply(drule C.if_elim, simp+)
  apply(drule C.seq_assign_elim, simp+)
  apply(rule if_else_rel_1', (simp|clarsimp)+)
  apply(drule C.seq_stop_elim, simp+)
  apply(rule if_else_rel_2, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, simp+)
  apply(rule if_else_rel_2', (simp|clarsimp)+)
  apply(drule C.seq_stop_elim, simp+)
  apply(rule if_else_rel_3, (simp|clarsimp)+)
  apply(drule C.seq_assign_elim, simp+)
  apply(rule if_else_rel_3', (simp|clarsimp)+)
  apply(drule C.seq_stop_elim, simp+)
  apply(rule if_else_rel_4, (simp|clarsimp)+)
  apply(drule C.assign_elim, simp+)
  apply(rule stop_rel)
  done

lemma mdss_A_of_mds0:
  "mdss = mdsA_of mds0"
  apply(rule preserves_modes_mem_mdsA_simp)
  apply clarsimp
  apply(case_tac m)
     unfolding mdss_def mds0_def mdsA_of_def
     apply(clarsimp simp: reg_not_visible_abs)+
  done

lemma A_of_mds0_is_mdss:
  "mdsA_of mds0 = mdss"
  by (simp add: mdss_A_of_mds0)

lemma prog_high_branchC_in_RC_of_R:
  "C.low_mds_eq mds0 mem1 mem2 
       (C.prog_high_branchC, mds0, mem1C, C.prog_high_branchC, mds0, mem2C)
         (RC_of A.R RefRel_HighBranch rel_invC)"
  apply(clarsimp simp: RC_of_def)
  apply(rule_tac x=A.prog_high_branch in exI)
  apply(rule_tac x="mdsA_of mds0" in exI)
  apply(rule_tac x="memA_of mem1" in exI)
  apply(rule conjI)
   apply(rule prog_high_branch_RefRel)
  apply(rule_tac x=A.prog_high_branch in exI)
  apply(rule_tac x="mdsA_of mds0" in exI)
  apply(rule_tac x="memA_of mem2" in exI)
  apply(rule conjI)
   apply(rule prog_high_branch_RefRel)
  apply(simp add: A_of_mds0_is_mdss)
  apply(rule conjI)
   apply(rule A.prog_high_branch_secure')
   apply(clarsimp simp: A.low_mds_eq_def)
   apply(case_tac x)
   unfolding C.low_mds_eq_def memA_of_def dma_def dmaC_def 𝒞C_def mds0_def
   apply clarsimp+
  apply(rule rel_invC_default, simp)
  done

lemma "C.com_sifum_secure (C.prog_high_branchC, mds0)"
  unfolding C.com_sifum_secure_def C.low_indistinguishable_def
  apply clarify
  apply(rule C.mm_equiv_intro)
   apply(rule strong_low_bisim_mm_RC_of_R)
  by (rule prog_high_branchC_in_RC_of_R)

end

end