Theory Fun6

section "Proof of Relative Security for fun6"
theory Fun6
imports "../Instance_IMP/Instance_Secret_IMem_Inp"
  "Relative_Security.Unwinding"
begin 

subsection "Function definition and Boilerplate"
no_notation bot ("⊥")
consts NN :: nat
lemma NN: "NN ≥ 0" by auto

definition aa1 :: "avname" where "aa1 = ''a1''" 
definition aa2 :: "avname" where "aa2 = ''a2''" 
definition vv :: "vname" where "vv = ''v''" 
definition tt :: "vname" where "tt = ''y''" 


lemmas vvars_defs = aa1_def aa2_def vv_def xx_def tt_def yy_def ffile_def

lemma vvars_dff[simp]: 
"aa1 ≠ aa2" "aa1 ≠ vv" "aa1 ≠ xx" "aa1 ≠ yy" "aa1 ≠ tt" "aa1 ≠ ffile"
"aa2 ≠ aa1" "aa2 ≠ vv" "aa2 ≠ xx" "aa2 ≠ yy" "aa2 ≠ tt" "aa2 ≠ ffile"
"vv ≠ aa1" "vv ≠ aa2"  "vv ≠ xx" "vv ≠ yy" "vv ≠ tt" "vv ≠ ffile"
"xx ≠ aa1" "xx ≠ aa2" "xx ≠ vv" "xx ≠ yy" "xx ≠ tt" "xx ≠ ffile"
"tt ≠ aa1" "tt ≠ aa2" "tt ≠ vv" "tt ≠ yy" "tt ≠ xx" "tt ≠ ffile"
"yy ≠ aa1" "yy ≠ aa2" "yy ≠ vv" "yy ≠ xx" "yy ≠ tt" "yy ≠ ffile"
"ffile ≠ aa1" "ffile ≠ aa2" "ffile ≠ vv" "ffile ≠ xx" "ffile ≠ tt" "ffile ≠ yy"
unfolding vvars_defs by auto

consts size_aa1 :: nat
consts size_aa2 :: nat

(* The initial avstore contains two arrays named aa1 and aa2 located one after the other *)
fun initAvstore :: "avstore ⇒ bool" where
"initAvstore (Avstore as)  = (as aa1 = (0, size_aa1) ∧ as aa2 = (size_aa1, size_aa2))"

fun istate ::"state ⇒ bool" where
"istate s = (initAvstore (getAvstore s))"

definition "prog ≡ 
[
 ⌦‹0 › Start , 
 ⌦‹1 › tt ::= (N 0),
 ⌦‹2 › xx ::= (N 1),
 ⌦‹3 › IfJump (Not (Eq (V xx) (N 0))) 4 13 ,
 ⌦‹4 › Input U xx ,
 ⌦‹5 › Input T yy ,
 ⌦‹6 › IfJump (Less (V xx) (N NN)) 7 12 ,
 ⌦‹7 ›   vv ::= VA aa1 (V xx) ,
 ⌦‹8 ›   writeSecretOnFile,
 ⌦‹9 ›   Fence ,
 ⌦‹10›   tt ::= (VA aa2 (Times (V vv) (N 512))) ,
 ⌦‹11›   Output U (V tt) ,
 ⌦‹12› Jump 3,
 ⌦‹13› Output U (N 0)
]"


definition "PC ≡ {0..13}"
(* we read "before" as "before or at" *)
definition "beforeWhile = {0,1,2}"
definition "afterWhile = {3..13}"
definition "startOfWhileThen = 4"
definition "startOfIfThen = 7"
definition "inThenIfBeforeOutput = {7,8}"
definition "startOfElseBranch = 12"
definition "inElseIf = {12,3,4,13}" (*for specualtive cases*)
definition "whileElse = 13"

fun leftWhileSpec where 
  "leftWhileSpec cfg cfg' = 
      (pcOf cfg = whileElse ∧ 
       pcOf cfg' = startOfWhileThen)"

fun rightWhileSpec where 
  "rightWhileSpec cfg cfg' = 
      (pcOf cfg = startOfWhileThen ∧ 
       pcOf cfg' = whileElse)"

fun whileSpeculation where  
 "whileSpeculation cfg cfg' = 
  (leftWhileSpec cfg cfg' ∨
   rightWhileSpec cfg cfg')"
lemmas whileSpec_def = whileSpeculation.simps 
                       startOfWhileThen_def
                       whileElse_def

lemmas whileSpec_defs = whileSpec_def
                        leftWhileSpec.simps 
                        rightWhileSpec.simps
(* *)

lemma cases_14: "(i::pcounter) = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ 
 i = 6 ∨ i = 7 ∨ i = 8 ∨ i = 9 ∨ i = 10 ∨ i = 11 ∨ i = 12 ∨ i = 13 ∨ i = 14 ∨ i > 14"
apply(cases i, simp_all) 
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
. . . . . . . . . . . . . . .


lemma xx_0_cases: "vs xx = 0 ∨ vs xx ≠ 0" by auto

lemma xx_NN_cases: "vs xx < int NN ∨ vs xx ≥ int NN" by auto

lemma is_If_pcOf[simp]: 
"pcOf cfg < 14 ⟹ is_IfJump (prog ! (pcOf cfg)) ⟷ pcOf cfg = 3 ∨ pcOf cfg = 6"
apply(cases cfg) using cases_14[of "pcOf cfg"] by (auto simp: prog_def)

lemma is_If_pc[simp]: 
"pc < 14 ⟹ is_IfJump (prog ! pc) ⟷ pc = 3 ∨ pc = 6"
using cases_14[of pc] by (auto simp: prog_def) 

lemma eq_Fence_pc[simp]: 
"pc < 14 ⟹ prog ! pc = Fence ⟷ pc = 9"
using cases_14[of pc] by (auto simp: prog_def) 

lemma output1[simp]:"prog ! 11 = Output U (V tt)" by(simp add: prog_def)
lemma output2[simp]:"prog ! 13 = Output U (N 0)" by(simp add: prog_def)
lemma is_if[simp]:"is_IfJump (prog ! 3)" by(simp add: prog_def)

lemma is_nif1[simp]:"¬is_IfJump (prog ! 7)" by(simp add: prog_def)
lemma is_nif2[simp]:"¬is_IfJump (prog ! 8)" by(simp add: prog_def)

lemma getInput_not6[simp]:"¬ is_getInput (prog ! 6)" by(simp add: prog_def)
lemma Output_not6[simp]:"¬ is_Output (prog ! 6)" by(simp add: prog_def)

lemma getInput_not7[simp]:"¬ is_getInput (prog ! 7)" by(simp add: prog_def)
lemma Output_not7[simp]:"¬ is_Output (prog ! 7)" by(simp add: prog_def)

lemma getInput_not8[simp]:"¬ is_getInput (prog ! 8)" by(simp add: prog_def)
lemma Output_not8[simp]:"is_Output (prog ! 8)" by(simp add: prog_def)

lemma is_nif[simp]:"¬ is_IfJump (prog ! 9)" by(simp add: prog_def)
lemma getInput_not10[simp]:"¬ is_getInput (prog ! 10)" by(simp add: prog_def)
lemma Output_not10[simp]:"¬ is_Output (prog ! 10)" by(simp add: prog_def)

lemma getInput_not12[simp]:"¬ is_getInput (prog ! 12)" by(simp add: prog_def)
lemma Output_not12[simp]:"¬ is_Output (prog ! 12)" by(simp add: prog_def)

lemma fence[simp]:"prog ! 9 = Fence" by(simp add: prog_def)

lemma nfence[simp]:"prog ! 7 ≠ Fence" by(simp add: prog_def)
(* *)

consts mispred :: "predState ⇒ pcounter list ⇒ bool"
fun resolve :: "predState ⇒ pcounter list ⇒ bool" where
  "resolve p pc = 
  (if (set pc = {4,13} ∨ (7 ∈ set pc ∧ (4 ∈ set pc ∨ 13 ∈ set pc)) ∨ pc = [12,8])
   then True else False)"

lemma resolve_73: "¬resolve p [7,3]" by auto
lemma resolve_74: "resolve p [7,4]" by auto
lemma resolve_713: "resolve p [7,13]" by auto
lemma resolve_127: "¬resolve p [12,7]" by auto
lemma resolve_129: "¬resolve p [12,9]" by auto


consts update :: "predState ⇒ pcounter list ⇒ predState"
consts initPstate :: predState

(* *)
interpretation Prog_Mispred_Init where 
prog = prog and initPstate = initPstate and
mispred = mispred and resolve = resolve and update = update and 
istate = istate
  by (standard, simp add: prog_def)

(* *)

(* Restoring the abbreviations: *)
abbreviation
  stepB_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix "→B" 55)
  where "x →B y == stepB x y"

abbreviation
  stepsB_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix "→B*" 55)
  where "x →B* y == star stepB x y"

abbreviation
  stepM_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix "→MM" 55)
  where "x →MM y == stepM x y"

abbreviation
  stepN_abbrev :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N" 55)
  where "x →N y == stepN x y"

abbreviation
  stepsN_abbrev :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N*" 55)
  where "x →N* y == star stepN x y"

abbreviation
  stepS_abbrev :: "configS ⇒ configS ⇒ bool" (infix "→S" 55)
  where "x →S y == stepS x y"

abbreviation
  stepsS_abbrev :: "configS ⇒ configS ⇒ bool" (infix "→S*" 55)
  where "x →S* y == star stepS x y"

(* *)

lemma endPC[simp]: "endPC = 14"
unfolding endPC_def unfolding prog_def by auto

(* *)
lemma is_getInput_pcOf[simp]: "pcOf cfg < 14 ⟹ is_getInput (prog!(pcOf cfg)) ⟷ pcOf cfg = 4 ∨ pcOf cfg = 5"
  using cases_14[of "pcOf cfg"] by (auto simp: prog_def)

lemma is_Output_pcOf[simp]: "pcOf cfg < 14 ⟹ is_Output (prog!(pcOf cfg)) ⟷ (pcOf cfg = 8 ∨ pcOf cfg = 11 ∨ pcOf cfg = 13)"
using cases_14[of "pcOf cfg"] by (auto simp: prog_def) 

lemma is_Output_T: "is_Output (prog ! 8)"
unfolding is_Output_def prog_def by auto
lemma is_Output: "is_Output (prog ! 11)"
unfolding is_Output_def prog_def by auto
lemma is_Output_1: "is_Output (prog ! 13)"
unfolding is_Output_def prog_def by auto
(* *)

lemma isSecV_pcOf[simp]: 
"isSecV (cfg,ibT,ibUT,ls) ⟷ ¬finalB (cfg,ibT,ibUT)"
using isSecV_def by simp

lemma isSecO_pcOf[simp]: 
"isSecO (pstate,cfg,cfgs,ibT,ibUT,ls) ⟷ 
 ¬finalS (pstate,cfg,cfgs,ibT,ibUT,ls) ∧ cfgs = []"
using isSecO_def by simp

(* *)

lemma getActV_pcOf[simp]: 
"pcOf cfg < 14 ⟹ 
 getActV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 4 then lhd ibUT 
  else if pcOf cfg = 5 then lhd ibT 
  else ⊥)"
apply(subst getActV_simps) unfolding prog_def 
apply simp  
using getActV_simps not_is_getInput_getActV prog_def by auto

lemma getObsV_pcOf[simp]: 
"pcOf cfg < 14 ⟹  
 getObsV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 11 ∨ pcOf cfg = 13 then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsV_simps) 
 apply (simp add: prog_def)
  unfolding getObsV_simps not_is_Output_getObsV is_Output_pcOf prog_def One_nat_def 
  using cases_14[of "pcOf cfg"] by auto

lemma getActO_pcOf[simp]: 
"pcOf cfg < 12 ⟹ 
 getActO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if cfgs = [] then 
  (if pcOf cfg = 4 then lhd ibUT
   else if pcOf cfg = 5 then lhd ibT 
  else ⊥) else ⊥)"
apply(subst getActO_simps)
  apply(cases cfgs, auto)
  unfolding prog_def apply simp 
  apply(cases "pcOf cfg = 4", auto)
  using getActV_simps getActV_pcOf prog_def by simp

lemma getObsO_pcOf[simp]: 
"pcOf cfg < 14 ⟹  
 getObsO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if (pcOf cfg = 11 ∨ pcOf cfg = 13) ∧ cfgs = [] then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsO_simps) 
apply(cases cfgs, auto)
  using getObsV_simps is_Output_pcOf not_is_Output_getObsV prog_def
        One_nat_def 
unfolding prog_def 
  using cases_14[of "pcOf cfg"] 
  by auto


(* *) 

lemma getActTrustedInput:"pc4 = 4 ⟹ pc3 = 4 ⟹ cfgs3 = [] ⟹  cfgs4 = [] ⟹
       getActO (pstate3, Config pc3 (State (Vstore vs3) avst3 h3 p3), [], ib3T, ib3UT, ls3) =
       getActO (pstate4, Config pc4 (State (Vstore vs4) avst4 h4 p4), [], ib4T, ib4UT, ls4)
   ⟹ lhd ib3UT = lhd ib4UT"
  using getActO_pcOf zero_less_numeral by auto

lemma getActUntrustedInput:"pc4 = 5 ⟹ pc3 = 5 ⟹ cfgs3 = [] ⟹  cfgs4 = [] ⟹
       getActO (pstate3, Config pc3 (State (Vstore vs3) avst3 h3 p3), [], ib3T, ib3UT, ls3) =
       getActO (pstate4, Config pc4 (State (Vstore vs4) avst4 h4 p4), [], ib4T, ib4UT, ls4)
   ⟹ lhd ib3T = lhd ib4T"
  using getActO_pcOf zero_less_numeral by auto

(* nextB, nextM and readLocs behavior 
(for nextM we are only interested at branching points, here only program counter 4): *)

lemma nextB_pc0[simp]: 
"nextB (Config 0 s, ibT, ibUT) = (Config 1 s, ibT, ibUT)"
apply(subst nextB_Start_Skip_Fence)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc0[simp]: 
"readLocs (Config 0 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc1[simp]: 
"nextB (Config 1 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 ((Config 2 (State (Vstore (vs(tt := 0))) avst hh p)), ibT, ibUT)"
apply(subst nextB_Assign)
  unfolding endPC_def unfolding prog_def by auto

lemma nextB_pc1'[simp]: 
"nextB (Config (Suc 0) (State (Vstore vs) avst hh p), ibT, ibUT) = 
 ((Config 2 (State (Vstore (vs(tt := 0))) avst hh p)), ibT, ibUT)"
apply(subst nextB_Assign)
  unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc1[simp]: 
"readLocs (Config 1 s) = {}"
  unfolding endPC_def readLocs_def unfolding prog_def by auto

lemma readLocs_pc1'[simp]: 
"readLocs (Config (Suc 0) s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(*  *)

lemma nextB_pc2[simp]: 
"nextB (Config 2 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 ((Config 3 (State (Vstore (vs(xx := 1))) avst hh p)), ibT, ibUT)"
apply(subst nextB_Assign)
  unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc2[simp]: 
"readLocs (Config 2 s) = {}"
  unfolding endPC_def readLocs_def unfolding prog_def by auto

(**)

lemma nextB_pc3_then[simp]: 
"vs xx ≠ 0 ⟹
 nextB (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextB_IfTrue)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextB_pc3_else[simp]: 
"vs xx = 0 ⟹
 nextB (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 13 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextB_IfFalse)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextB_pc3: 
"nextB (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p), ibT, ibUT)"
by(cases "vs xx = 0", auto)

lemma readLocs_pc3[simp]: 
"readLocs (Config 3 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def Eq_def by auto

lemma nextM_pc3_then[simp]: 
"vs xx = 0 ⟹
 nextM (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextM_IfTrue)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextM_pc3_else[simp]: 
"vs xx ≠ 0 ⟹
 nextM (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 13 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextM_IfFalse)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextM_pc3: 
"nextM (Config 3 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config (if vs xx ≠ 0 then 13 else 4) (State (Vstore vs) avst hh p), ibT, ibUT)"
  by(cases "vs xx = 0", auto)

(* *)

lemma nextB_pc4[simp]: 
"ibUT ≠ LNil ⟹ nextB (Config 4 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 5 (State (Vstore (vs(xx := lhd ibUT))) avst hh p), ibT, ltl ibUT)"
apply(subst nextB_getUntrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc4[simp]: 
"readLocs (Config 4 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc5[simp]: 
"ibT ≠ LNil ⟹ nextB (Config 5 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 6 (State (Vstore (vs(yy := lhd ibT))) avst hh p), ltl ibT, ibUT)"
apply(subst nextB_getTrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc5[simp]: 
"readLocs (Config 5 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc6_then[simp]: 
"vs xx < int NN ⟹
 nextB (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 7 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextB_IfTrue)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextB_pc6_else[simp]: 
"vs xx ≥ int NN ⟹
 nextB (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 12 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextB_IfFalse)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextB_pc6: 
"nextB (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config (if vs xx < int NN then 7 else 12) (State (Vstore vs) avst hh p), ibT, ibUT)"
by(cases "vs xx < int NN", auto)

lemma readLocs_pc6[simp]: 
"readLocs (Config 6 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def Eq_def by auto

lemma nextM_pc6_then[simp]: 
"vs xx ≥ int NN ⟹
 nextM (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 7 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextM_IfTrue)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextM_pc6_else[simp]: 
"vs xx < int NN ⟹
 nextM (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config 12 (State (Vstore vs) avst hh p), ibT, ibUT)"
apply(subst nextM_IfFalse)
unfolding endPC_def unfolding prog_def Eq_def by auto

lemma nextM_pc6: 
"nextM (Config 6 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 (Config (if vs xx < int NN then 12 else 7) (State (Vstore vs) avst hh p), ibT, ibUT)"
  by(cases "vs xx < int NN", auto)

(* *)

lemma nextB_pc7[simp]: 
"nextB (Config 7 (State (Vstore vs) avst (Heap hh) p), ibT, ibUT) = 
 (let l = array_loc aa1 (nat (vs xx)) avst 
  in (Config 8 (State (Vstore (vs(vv := hh l))) avst (Heap hh) p)), ibT, ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc7[simp]: 
"readLocs (Config 7 (State (Vstore vs) avst hh p)) = {array_loc aa1 (nat (vs xx)) avst}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)
lemma nextB_pc8[simp]: 
"nextB (Config 8 (State (Vstore vs) avst hh p), ibT, ibUT) = 
 ((Config 9 (State (Vstore vs) avst hh p)), ibT, ibUT)"
apply(subst nextB_Output)
  unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc8[simp]: 
"readLocs (Config 8 s) = {}"
  unfolding endPC_def readLocs_def 
  unfolding prog_def  by auto

(* *)
lemma nextB_pc9[simp]: 
"nextB (Config 9 s, ibT, ibUT) = (Config 10 s, ibT, ibUT)"
apply(subst nextB_Start_Skip_Fence)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc9[simp]: 
"readLocs (Config 9 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc10[simp]:
"nextB (Config 10 (State (Vstore vs) avst (Heap hh) p), ibT, ibUT) =  
  (let l = array_loc aa2 (nat (vs vv * 512)) avst
  in (Config 11 (State (Vstore (vs(tt := hh l))) avst (Heap hh) p)), ibT, ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto


lemma readLocs_pc10[simp]: 
"readLocs (Config 10 (State (Vstore vs) avst hh p)) = {array_loc aa2 (nat (vs vv * 512)) avst}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc11[simp]:
"nextB (Config 11 s, ibT, ibUT) = (Config 12 s, ibT, ibUT)"
apply(subst nextB_Output)
unfolding endPC_def unfolding prog_def by auto 

lemma readLocs_pc11[simp]: 
"readLocs (Config 11 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc12[simp]:
"nextB (Config 12 s, ibT, ibUT) = (Config 3 s, ibT, ibUT)"
apply(subst nextB_Jump)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc12[simp]: 
"readLocs (Config 12 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto


lemma nextB_pc13[simp]: 
"nextB (Config 13 s, ibT, ibUT) = 
 (Config 14 s, ibT, ibUT)"
apply(subst nextB_Output)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc13[simp]: 
"readLocs (Config 13 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(**)
lemma map_L1:"length cfgs = Suc 0 ⟹ 
    pcOf (last cfgs) = y ⟹ map pcOf cfgs = [y]"
  by (smt (verit,del_insts) Suc_length_conv cfgs_map last.simps 
      length_0_conv map_eq_Cons_conv nth_Cons_0 numeral_2_eq_2)

lemma map_L2:"length cfgs = 2 ⟹ 
    pcOf (cfgs ! 0) = x ⟹
    pcOf (last cfgs) = y ⟹ map pcOf cfgs = [x,y]"
  by (smt (verit) Suc_length_conv cfgs_map last.simps 
      length_0_conv map_eq_Cons_conv nth_Cons_0 numeral_2_eq_2)

lemma "length cfgs = 2 ⟹ (cfgs ! 0) = last (butlast cfgs)" 
  by (cases cfgs, auto) 

lemma nextB_stepB_pc: 
"pc < 14 ⟹ (pc = 4 ⟶ ibUT ≠ LNil) ⟹ (pc = 5 ⟶ ibT ≠ LNil) ⟹
(Config pc s, ibT, ibUT) →B nextB (Config pc s, ibT, ibUT)"
apply(cases s) subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
subgoal for vs as h
using cases_14[of pc] apply safe
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)

 (*  *)

  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)  
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)

  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)
  (* *)
  subgoal apply(cases "vs xx = 0")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def Eq_def, auto)  .
  subgoal apply(cases "vs xx = 0")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def, auto)  .
  subgoal apply(cases "vs xx = 0")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def, auto)  .
  subgoal apply(cases "vs xx = 0")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def, auto)  .
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def, metis llist.exhaust_sel)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def, metis llist.exhaust_sel)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def, metis llist.exhaust_sel)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def, metis llist.exhaust_sel)

  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) .
  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) .
  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) .
  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
      by (simp add: prog_def Eq_def) .

  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 

  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)  
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
  by simp_all . . 
  (*  *)

lemma not_finalB: 
"pc < 14 ⟹ (pc = 4 ⟶ ibUT ≠ LNil) ⟹ (pc = 5 ⟶ ibT ≠ LNil) ⟹
 ¬ finalB (Config pc s, ibT, ibUT)"
using nextB_stepB_pc by (simp add: stepB_iff_nextB)


lemma finalB_pc_iff': 
"pc < 14 ⟹
 finalB (Config pc s, ibT, ibUT) ⟷ 
 (pc = 4 ∧ ibUT = LNil) ∨ (pc = 5 ∧ ibT = LNil)"
  apply standard
    subgoal using nextB_stepB_pc[of pc] by (auto simp add: stepB_iff_nextB) 
    unfolding finalB_iff by (elim disjE, simp_all add: prog_def)
  

lemma finalB_pc_iff: 
"pc ≤ 14 ⟹
 finalB (Config pc s, ibT, ibUT) ⟷ 
 (pc = 14 ∨ (pc = 4 ∧ ibUT = LNil) ∨ (pc = 5 ∧ ibT = LNil))"
  using  Prog.finalB_iff endPC finalB_pc_iff' order_le_less finalB_iff
  by metis


lemma finalB_pcOf_iff[simp]:
"pcOf cfg ≤ 14 ⟹ 
 finalB (cfg, ibT, ibUT) ⟷ (pcOf cfg = 14 ∨ (pcOf cfg = 4 ∧ ibUT = LNil) ∨ (pcOf cfg = 5 ∧ ibT = LNil))"
 using config.collapse finalB_pc_iff by metis


lemma finalS_cond:"pcOf cfg < 14 ⟹ noMisSpec cfgs ⟹ ibT ≠ LNil ⟹ ibUT ≠ LNil ⟹ ¬ finalS (pstate, cfg, cfgs, ibT, ibUT, ls)"
  apply(cases cfg)
  subgoal for pc s apply(cases s)
  subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
    subgoal for vs as h
      using cases_14[of pc] apply(elim disjE) unfolding finalS_defs noMisSpec_def
      subgoal using nonspec_normal[of "[]" "Config pc (State (Vstore vs) avst hh p)" 
                                        pstate pstate ibT ibUT 
                                        "Config 1 (State (Vstore vs) avst hh p)" 
                                        ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls]
        using is_If_pc by force


      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT
                                    "Config 2 (State (Vstore (vs(tt:= 0))) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all 

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 3 (State (Vstore (vs(xx:= 1))) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all 

    subgoal apply(cases "mispred pstate [3]")
      subgoal apply(frule nonspec_mispred[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                             pstate "update pstate [pcOf (Config pc (State (Vstore vs) avst hh p))]"
                                             ibT ibUT "Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p)"
                                             ibT ibUT "Config (if vs xx ≠ 0 then 13 else 4) (State (Vstore vs) avst hh p)"
                                             ibT ibUT "[Config (if vs xx ≠ 0 then 13 else 4) (State (Vstore vs) avst hh p)]"
                                             "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
      prefer 9 subgoal by metis by (simp add: finalM_iff)+

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                    pstate pstate ibT ibUT 
                                    "Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
      prefer 7 subgoal by metis by simp_all . 

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 5 (State (Vstore (vs(xx:= lhd ibUT))) avst hh p)" 
                                    ibT "ltl ibUT" "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all 

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 6 (State (Vstore (vs(yy:= lhd ibT))) avst hh p)" 
                                    "ltl ibT" ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all 

    subgoal apply(cases "mispred pstate [6]")
      subgoal apply(frule nonspec_mispred[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                             pstate "update pstate [pcOf (Config pc (State (Vstore vs) avst hh p))]"
                                             ibT ibUT "Config (if vs xx < NN then 7 else 12) (State (Vstore vs) avst hh p)"
                                             ibT ibUT "Config (if vs xx < NN then 12 else 7) (State (Vstore vs) avst hh p)"
                                             ibT ibUT "[Config (if vs xx < NN then 12 else 7) (State (Vstore vs) avst hh p)]"
                                             "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
      prefer 9 subgoal by metis by (simp add: finalM_iff)+

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                    pstate pstate ibT ibUT 
                                    "Config (if vs xx < NN then 7 else 12) (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
      prefer 7 subgoal by metis by simp_all . 

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                         pstate pstate ibT ibUT 
                         "(let l = (array_loc aa1 (nat (vs xx)) (Avstore as)) 
                                in (Config 8 (State (Vstore (vs(vv := h l))) avst hh p)))" 
                         ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
            prefer 7 subgoal by metis by simp_all

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                         pstate pstate ibT ibUT 
                         "(Config 9 (State (Vstore vs) avst hh p))" 
                         ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
            prefer 7 subgoal by metis by simp_all

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 10 (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" ls ls])
            prefer 7 subgoal by metis by simp_all

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                         pstate pstate ibT ibUT 
                         "(let l = (array_loc aa2 (nat (vs vv * 512)) (Avstore as)) 
                                in (Config 11 (State (Vstore (vs(tt := h l))) avst hh p)))" 
                         ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
            prefer 7 subgoal by metis by simp_all

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 12 (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" ls ls])
            prefer 7 subgoal by metis by simp_all

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                    pstate pstate ibT ibUT 
                                    "Config 3 (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
      prefer 7 subgoal by metis by simp_all 

    subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                    pstate pstate ibT ibUT 
                                    "Config 14 (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" ls ls])
            prefer 7 subgoal by metis by simp_all
    by simp_all . . .

lemma finalS_cond':"pcOf cfg < 14 ⟹ cfgs = [] ⟹ ibT ≠ LNil ⟹ ibUT ≠ LNil ⟹
                    ¬ finalS (pstate, cfg, cfgs, ibT, ibUT, ls)"
  using finalS_cond by (simp add: noMisSpec_def)

lemma finalS_while_spec:
      "whileSpeculation cfg (last cfgs) ⟹ 
       length cfgs = Suc 0 ⟹
      ¬ finalS (pstate, cfg, cfgs, ibT, ibUT, ls)"
  apply(unfold whileSpec_defs, cases cfg)
  subgoal for pc s apply(cases s)
  subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
    subgoal for vs as h
      apply(elim disjE, elim conjE) unfolding finalS_defs
      subgoal using stepS_spec_resolve_iff[of cfgs pstate cfg ibT ibUT ls "update pstate (pcOf cfg # map pcOf cfgs)"]
            by (metis (no_types, lifting) cfgs_map empty_set insert_commute less_numeral_extra(3) 
                resolve.simps list.simps(15) list.size(3) numeral_2_eq_2 pos2)
      subgoal apply(elim conjE) 
        using spec_resolve[of cfgs pstate cfg "update pstate (pcOf cfg # map pcOf cfgs)" cfg "[]" ibT ibT ibUT ibUT ls ls ]
        using empty_set  resolve.simps length_0_conv 
              length_1_butlast length_Suc_conv list.simps(9,15) 
              cfgs_map not_Cons_self2 spec_resolve by metis . . . . 

lemma finalS_while_spec_L2:
      "pcOf cfg = 7 ⟹
       whileSpeculation (cfgs!0) (last cfgs) ⟹ 
       length cfgs = 2 ⟹
      ¬ finalS (pstate, cfg, cfgs, ibT, ibUT, ls)"
apply(unfold whileSpec_defs, cases cfg)
  subgoal for pc s apply(cases s)
  subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
    subgoal for vs as h
      apply(elim disjE, elim conjE) unfolding finalS_defs
      subgoal using stepS_spec_resolve_iff[of cfgs pstate cfg ibT ibUT ls "update pstate (pcOf cfg # map pcOf cfgs)"]
        unfolding resolve.simps
        using list.set_intros(1,2) map_L2 zero_neq_numeral
        by fastforce
      subgoal apply(elim conjE) 
        using spec_resolve
        unfolding resolve.simps
        using list.set_intros(1,2) map_L2 zero_neq_numeral
        by (metis (no_types, lifting) Prog_Mispred.spec_resolve Prog_Mispred_axioms list.size(3))
      . . . . 

lemma finalS_if_spec:
      "(pcOf (last cfgs) ∈ inThenIfBeforeOutput ∧ pcOf cfg = 12) ∨ 
       (pcOf (last cfgs) ∈ inElseIf ∧ pcOf cfg = 7) ⟹ 
       length cfgs = Suc 0 ⟹
      ¬ finalS (pstate, cfg, cfgs, ibT, ibUT, ls)"
  unfolding inThenIfBeforeOutput_def inElseIf_def
  apply(simp,cases "last cfgs")
  subgoal for pc s apply(cases s)
  subgoal for vst avst hh p apply(cases vst, cases hh)
    subgoal for vs h
      apply(elim disjE, elim conjE) unfolding finalS_defs
      subgoal apply(elim disjE)
        subgoal apply(rule notI, 
      erule allE[of _ "(pstate,cfg,
                        [Config 8 (State (Vstore (vs(vv := h (array_loc aa1 (nat (vs xx)) avst)))) avst hh p)],
                        ibT,ibUT,ls ∪ readLocs (last cfgs))"])
          by (erule notE, 
        rule spec_normal[of _ _ _ _ _ _"Config 8 (State (Vstore (vs(vv := h (array_loc aa1 (nat (vs xx)) avst)))) avst hh p)"], auto)
        subgoal apply(rule notI, erule allE[of _ "(update pstate (pcOf cfg # map pcOf cfgs),cfg,[],ibT,ibUT,ls ∪ readLocs (last cfgs))"])
          by(erule notE, rule spec_resolve, auto) .
      subgoal apply(elim conjE, elim disjE) 
        subgoal apply(rule notI, erule allE[of _ "
            (pstate, cfg, [Config 3 (State (Vstore vs) avst hh p)], ibT,ibUT,
             ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p)))"])
          by(erule notE, rule spec_normal[of _ _ _ _ _ _"Config 3 (State (Vstore vs) avst hh p)"], auto)

        subgoal apply(cases "mispred pstate [7,3]")
          subgoal apply(rule notI, erule allE[of _ "
            (update pstate (pcOf cfg # map pcOf cfgs),
           cfg,
           [Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p),
            Config (if vs xx ≠ 0 then 13 else 4) (State (Vstore vs) avst hh p)], ibT, ibUT,
           ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p)))"])
                  apply(erule notE, 
        rule spec_mispred[of _ _ _ _ _ _
           "Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p)" _
         _ "Config (if vs xx ≠ 0 then 13 else 4) (State (Vstore vs) avst hh p)" ibT ibUT]) 
            by(auto simp: finalM_iff)

        apply(rule notI, erule allE[of _ "
            (pstate, cfg, [Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p)], ibT,ibUT,
             ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p)))"])
          by (erule notE, 
        rule spec_normal[of _ _ _ _ _ _"Config (if vs xx ≠ 0 then 4 else 13) (State (Vstore vs) avst hh p)"], auto)

        subgoal by (metis resolve_74 stepS_spec_resolve_iff 
                          map_L1 cfgs_Suc_zero not_Cons_self2) 
        subgoal by (metis resolve_713 stepS_spec_resolve_iff 
                          map_L1 cfgs_Suc_zero not_Cons_self2) 
  . . . . .



end