[STATEMENT]
lemma swap_vars_typed:
  "\<Gamma> = (\<lambda>_. None) \<Longrightarrow> \<S> = ({},{}) \<Longrightarrow> P = {} \<Longrightarrow>
  \<exists>\<Gamma>' \<S>' P'. has_type \<Gamma> \<S> P swap_vars \<Gamma>' \<S>' P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' \<S>' P'. has_type \<Gamma> \<S> P swap_vars \<Gamma>' \<S>' P'
[PROOF STEP]
apply(intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type \<Gamma> \<S> P swap_vars ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp add: swap_vars_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({}, {}) {} ((Skip@[control_X +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({}, {}) {} (Skip@[control_X +=\<^sub>m AsmNoWrite]) ?\<Gamma>'3 ?\<S>'3 ?P'3
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'3 ?\<S>'3 ?P'3 ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) (add_anno_stable ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'3 ?\<S>'3 ?P'3
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({}, {}) {} (control_X +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'3 ?\<S>'3 ?P'3 ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_X}, {}) {} Skip ?\<Gamma>'3 ?\<S>'3 ?P'3
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({}, {}) {} (control_X +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'3 ?\<S>'3 ?P'3 ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({}, {}) (control_X +=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({}, {}) {} (control_X +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_X}, {}) {} ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_X}, {}) {} ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_X}, {}) {} (Skip@[control_Y +=\<^sub>m AsmNoWrite]) ?\<Gamma>'20 ?\<S>'20 ?P'20
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'20 ?\<S>'20 ?P'20 ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'20 ?\<S>'20 ?P'20
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_X}, {}) {} (control_Y +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'20 ?\<S>'20 ?P'20 ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Y, control_X}, {}) {} Skip ?\<Gamma>'20 ?\<S>'20 ?P'20
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_X}, {}) {} (control_Y +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'20 ?\<S>'20 ?P'20 ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_X}, {}) (control_Y +=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_X}, {}) {} (control_Y +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Y, control_X}, {}) {} ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Y, control_X}, {}) {} ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Y, control_X}, {}) {} (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ?\<Gamma>'37 ?\<S>'37 ?P'37
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'37 ?\<S>'37 ?P'37 ((Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'37 ?\<S>'37 ?P'37
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Y, control_X}, {}) {} (control_Z +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'37 ?\<S>'37 ?P'37 ((Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {}) {} Skip ?\<Gamma>'37 ?\<S>'37 ?P'37
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Y, control_X}, {}) {} (control_Z +=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'37 ?\<S>'37 ?P'37 ((Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Y, control_X}, {}) (control_Z +=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Y, control_X}, {}) {} (control_Z +=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {}) {} ((Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {}) {} ((Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {}) {} (Skip@[X +=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'54 ?\<S>'54 ?P'54
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'54 ?\<S>'54 ?P'54 ((Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'54 ?\<S>'54 ?P'54
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {} (X +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'54 ?\<S>'54 ?P'54 ((Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} Skip ?\<Gamma>'54 ?\<S>'54 ?P'54
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {} (X +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'54 ?\<S>'54 ?P'54 ((Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {}) (X +=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {} (X +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} ((Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} ((Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} (Skip@[Y +=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'75 ?\<S>'75 ?P'75
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'75 ?\<S>'75 ?P'75 ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'75 ?\<S>'75 ?P'75
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} (Y +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'75 ?\<S>'75 ?P'75 ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} Skip ?\<Gamma>'75 ?\<S>'75 ?P'75
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} (Y +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'75 ?\<S>'75 ?P'75 ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) (Y +=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {X}) {} (Y +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'96 ?\<S>'96 ?P'96
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'96 ?\<S>'96 ?P'96 ((Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'96 ?\<S>'96 ?P'96
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} (Z +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'96 ?\<S>'96 ?P'96 ((Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {} Skip ?\<Gamma>'96 ?\<S>'96 ?P'96
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} (Z +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'96 ?\<S>'96 ?P'96 ((Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) (Z +=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Y, X}) {} (Z +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {} ((Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {} ((Z \<leftarrow> Load X) ;; (X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {} (Z \<leftarrow> Load X) ?\<Gamma>'117 ?\<S>'117 ?P'117
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'117 ?\<S>'117 ?P'117 ((X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>2[OF _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] (Load X) ?t120
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t120
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t120 (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> ?t120] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] (Load X) ?t120
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t120
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t120 (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> ?t120] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule type_aexpr_Load')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t120 = the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}] X)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t120
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t120 (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> ?t120] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((X \<leftarrow> Load Y) ;; (Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X \<leftarrow> Load Y) ?\<Gamma>'135 ?\<S>'135 ?P'135
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'135 ?\<S>'135 ?P'135 ((Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>2[OF _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}] (Load Y) ?t138
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t138
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t138 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type X)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> ?t138] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}] (Load Y) ?t138
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t138
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t138 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type X)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> ?t138] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule type_aexpr_Load')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t138 = the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}] Y)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t138
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t138 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type X)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> ?t138] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Y \<leftarrow> Load Z) ;; (control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (Y \<leftarrow> Load Z) ?\<Gamma>'153 ?\<S>'153 ?P'153
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'153 ?\<S>'153 ?P'153 ((control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>2[OF _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}] (Load Z) ?t156
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t156
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t156 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Y)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> ?t156] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}] (Load Z) ?t156
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t156
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t156 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Y)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> ?t156] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule type_aexpr_Load')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t156 = the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}] Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) ?t156
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> subtype ?t156 (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type Y)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> ?t156] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Z \<leftarrow> Load control_X) ;; (control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (control_Z \<leftarrow> Load control_X) ?\<Gamma>'171 ?\<S>'171 ?P'171
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'171 ?\<S>'171 ?P'171 ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>\<C>[OF _ _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_Z \<in> \<C>
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] (Load control_X) ?t174
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ?t174
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Z \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) \<and> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] (Load control_X) ?t174
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ?t174
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Z \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) \<and> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule type_aexpr_Load)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_X \<notin> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type control_X)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Z \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) \<and> subtype (to_total [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] v) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (simp+)[4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post (restrict_preds_to_vars (assign_post {} Z (Load X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) X (Load Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) Y (Load Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) control_Z (Load control_X)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} ((control_X \<leftarrow> Load control_Y) ;; (control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'196 ?\<S>'196 ?P'196
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'196 ?\<S>'196 ?P'196 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule conc'[where x="Z" and t="dma_type Z", OF _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'196 ?\<S>'196 ?P'196
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'196 ?\<S>'196 ?P'196 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule conc'[where x=Y and t="dma_type Z", OF _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'196 ?\<S>'196 ?P'196
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'196 ?\<S>'196 ?P'196 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>\<C>[OF _ _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_X \<in> \<C>
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] (Load control_Y) ?t215
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} ?t215
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]. control_X \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_X \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
A total of 14 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] (Load control_Y) ?t215
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} ?t215
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]. control_X \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_X \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
A total of 13 subgoals...
[PROOF STEP]
apply(rule type_aexpr_Load)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_Y \<notin> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type control_Y)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]. control_X \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_X \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_Z (Load control_X), Same Y (Load Z)} (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] v) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
A total of 13 subgoals...
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv {Eq control_X 0} {Same control_Z (Load control_X), Same Y (Load Z)} {Eq control_Z 0}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: type_wellformed_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: type_wellformed_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_Z (Load control_X), Same Y (Load Z)} control_X (Load control_Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} (control_Y \<leftarrow> Load control_Z) ?\<Gamma>'239 ?\<S>'239 ?P'239
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'239 ?\<S>'239 ?P'239 ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule conc'[where x=X and t="dma_type X" , OF _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} (control_Y \<leftarrow> Load control_Z) ?\<Gamma>'239 ?\<S>'239 ?P'239
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'239 ?\<S>'239 ?P'239 ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule assign\<^sub>\<C>[OF _ _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_Y \<in> \<C>
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] (Load control_Z) ?t250
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} ?t250
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X]. control_Y \<notin> vars_of_type (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Y \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) \<and> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}]
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] (Load control_Z) ?t250
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} ?t250
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X]. control_Y \<notin> vars_of_type (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Y \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) \<and> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}]
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule type_aexpr_Load)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> control_Z \<notin> dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type control_Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X]. control_Y \<notin> vars_of_type (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v. control_Y \<in> \<C>_vars v \<and> v \<notin> snd ({control_Z, control_Y, control_X}, {Z, Y, X}) \<longrightarrow> pred_entailment {Same control_X (Load control_Y), Same Y (Load Z)} (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) \<and> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] v) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}]
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv {Eq control_Y 0} {Same control_X (Load control_Y), Same Y (Load Z)} {Eq control_X 0}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(clarsimp simp: type_wellformed_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'270 ?\<S>'270 ?P'270
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'270 ?\<S>'270 ?P'270 ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'270 ?\<S>'270 ?P'270
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] x) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'270 ?\<S>'270 ?P'270 ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] x) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] x) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) (X -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) ((Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'289 ?\<S>'289 ?P'289
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'289 ?\<S>'289 ?P'289 ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) {v. local.stable (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'289 ?\<S>'289 ?P'289
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x) (restrict_preds_to_vars (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) {v. local.stable (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'289 ?\<S>'289 ?P'289 ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} Skip ?\<Gamma>'289 ?\<S>'289 ?P'289
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x) (restrict_preds_to_vars (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) {v. local.stable (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'289 ?\<S>'289 ?P'289 ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x) (restrict_preds_to_vars (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) {v. local.stable (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) x) (restrict_preds_to_vars (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) {v. local.stable (add_anno_stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (Y -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec (add_anno [X \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Y \<mapsto> {Eq control_Z 0}, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (assign_post {Same control_X (Load control_Y), Same Y (Load Z)} control_Y (Load control_Z)) {v. local.stable ({control_Z, control_Y, control_X}, {Z, Y, X}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (X -=\<^sub>m AsmNoReadOrWrite)) v}) (Y -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} ((Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'310 ?\<S>'310 ?P'310
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'310 ?\<S>'310 ?P'310 ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'310 ?\<S>'310 ?P'310
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [Z \<mapsto> {Eq control_Z 0}] x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'310 ?\<S>'310 ?P'310 ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} Skip ?\<Gamma>'310 ?\<S>'310 ?P'310
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [Z \<mapsto> {Eq control_Z 0}] x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'310 ?\<S>'310 ?P'310 ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [Z \<mapsto> {Eq control_Z 0}] x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total [Z \<mapsto> {Eq control_Z 0}] x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) (Z -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Z 0}] ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y}) {Same control_Y (Load control_Z)} (Z -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (Skip@[control_X -=\<^sub>m AsmNoWrite]) ?\<Gamma>'331 ?\<S>'331 ?P'331
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'331 ?\<S>'331 ?P'331 ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'331 ?\<S>'331 ?P'331
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'331 ?\<S>'331 ?P'331 ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} Skip ?\<Gamma>'331 ?\<S>'331 ?P'331
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'331 ?\<S>'331 ?P'331 ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_X -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (simp add: add_anno_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_X -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ?\<Gamma>'348 ?\<S>'348 ?P'348
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'348 ?\<S>'348 ?P'348 ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'348 ?\<S>'348 ?P'348
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'348 ?\<S>'348 ?P'348 ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>'348 ?\<S>'348 ?P'348
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'348 ?\<S>'348 ?P'348 ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {Same control_Y (Load control_Z)} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Y -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (simp add: add_anno_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X}, {Z, Y, X} - {X} - {Y} - {Z}) {Same control_Y (Load control_Z)} (control_Y -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule seq_type)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ?\<Gamma>'365 ?\<S>'365 ?P'365
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'365 ?\<S>'365 ?P'365 Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'365 ?\<S>'365 ?P'365
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'365 ?\<S>'365 ?P'365 Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>'365 ?\<S>'365 ?P'365
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 3. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'365 ?\<S>'365 ?P'365 Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Skip \<noteq> Stop
 2. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> subtype (to_total Map.empty x) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(fastforce simp: add_anno_def subtype_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) (control_Z -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (simp add: add_anno_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y}, {Z, Y, X} - {X} - {Y} - {Z}) {} (control_Z -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type Map.empty ({control_Z, control_Y, control_X} - {control_X} - {control_Y} - {control_Z}, {Z, Y, X} - {X} - {Y} - {Z}) {} Skip ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(rule skip_type)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done