[STATEMENT]
lemma add_vars_typed:
  "\<Gamma> = (\<lambda>_. None) \<Longrightarrow> \<S> = ({},{}) \<Longrightarrow> P = {} \<Longrightarrow>
  \<exists>\<Gamma>' \<S>' P'. has_type \<Gamma> \<S> P add_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 add_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 add_vars ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(simp add: add_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@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 (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@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 Map.empty ({control_X}, {}) {} ((Skip@[control_Y +=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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>'16 ?\<S>'16 ?P'16
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'16 ?\<S>'16 ?P'16 ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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>'16 ?\<S>'16 ?P'16
 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>'16 ?\<S>'16 ?P'16 ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 (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@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 Map.empty ({control_Y, control_X}, {}) {} ((Skip@[control_Z +=\<^sub>m AsmNoWrite]) ;; (Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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>'29 ?\<S>'29 ?P'29
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'29 ?\<S>'29 ?P'29 ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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>'29 ?\<S>'29 ?P'29
 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>'29 ?\<S>'29 ?P'29 ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 (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@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 Map.empty ({control_Z, control_Y, control_X}, {}) {} ((Skip@[Z +=\<^sub>m AsmNoReadOrWrite]) ;; (Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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@[Z +=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'42 ?\<S>'42 ?P'42
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'42 ?\<S>'42 ?P'42 ((Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'42 ?\<S>'42 ?P'42
 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}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {} (Z +=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'42 ?\<S>'42 ?P'42 ((Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable Map.empty ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {} (Z +=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (Z +=\<^sub>m AsmNoReadOrWrite)) v}) ((Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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}) {} ((Z \<leftarrow> Add X Y) ;; Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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}) {} (Z \<leftarrow> Add X Y) ?\<Gamma>'59 ?\<S>'59 ?P'59
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'59 ?\<S>'59 ?P'59 (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [Z \<mapsto> {Eq control_Z 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_Z 0}] (Add X Y) ?t62
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z}) ?t62
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'59 = restrict_preds_to_vars (assign_post {} Z (Add X Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z}) \<longrightarrow> subtype ?t62 ?P'59 (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> ?t62] ({control_Z, control_Y, control_X}, {Z}) ?P'59 (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 [Z \<mapsto> {Eq control_Z 0}] (Add X Y) ?t62
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z}) ?t62
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'59 = restrict_preds_to_vars (assign_post {} Z (Add X Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z}) \<longrightarrow> subtype ?t62 ?P'59 (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> ?t62] ({control_Z, control_Y, control_X}, {Z}) ?P'59 (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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_Add type_aexpr_Add' type_aexpr_Add'' type_aexpr_Add'''; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z}) (\<Union> {dma_type X, dma_type Y})
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'59 = restrict_preds_to_vars (assign_post {} Z (Add X Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z}) \<longrightarrow> subtype (\<Union> {dma_type X, dma_type Y}) ?P'59 (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P'59 (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'59 = restrict_preds_to_vars (assign_post {} Z (Add X Y)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z}) \<longrightarrow> subtype (\<Union> {dma_type X, dma_type Y}) ?P'59 (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P'59 (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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> Z \<notin> snd ({control_Z, control_Y, control_X}, {Z}) \<longrightarrow> subtype (\<Union> {dma_type X, dma_type Y}) {} (dma_type Z)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) {} (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) {} (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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 (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) {} (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0)) ;; (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_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) {} (Stmt.If (Eq control_X 0) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'78
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 ?P'78 ((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 if_type''[OF _ _ _ _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_bexpr [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Eq control_X 0) ?t81
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'81
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'81 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'81 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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_bexprI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t81 = \<Union> (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ` bexp_vars (Eq control_X 0))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'81
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'81 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'81 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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 (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t81 = {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'81
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'81 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'81 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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 HOL.refl)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'81 {Eq control_X 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'81 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) (Stmt.If (Eq control_Y 0) (control_Z \<leftarrow> Const 0) (control_Z \<leftarrow> Const (Suc 0))) ?\<Gamma>'78 ?\<S>'78 ?P'81
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'81 {Eq control_X 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'81 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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 if_type''[OF _ _ _ _ _ _ HOL.refl])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_bexpr [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Eq control_Y 0) ?t100
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ?t100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (control_Z \<leftarrow> Const 0) ?\<Gamma>'78 ?\<S>'78 ?P'100
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''100
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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_bexprI)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t100 = \<Union> (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ` bexp_vars (Eq control_Y 0))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ?t100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (control_Z \<leftarrow> Const 0) ?\<Gamma>'78 ?\<S>'78 ?P'100
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''100
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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: to_total_def)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t100 = {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ?t100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (control_Z \<leftarrow> Const 0) ?\<Gamma>'78 ?\<S>'78 ?P'100
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''100
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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 HOL.refl)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (control_Z \<leftarrow> Const 0) ?\<Gamma>'78 ?\<S>'78 ?P'100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''100
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v}) {Eq control_X 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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 (8 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (control_Z \<leftarrow> Const 0) ?\<Gamma>'78 ?\<S>'78 ?P'100
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) ?\<Gamma>'78 ?\<S>'78 ?P''81
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v}) {Eq control_X 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'78 ?\<S>'78 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'78 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'78 v}) ((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>)
[PROOF STATE]
proof (prove)
goal (13 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 [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const 0) ?t119
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) ?t119
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'100 = restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 6. \<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}) \<longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P'100 (dma_type v)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
A total of 13 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const 0) ?t119
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) ?t119
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'100 = restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P'100 (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
A total of 12 subgoals...
[PROOF STEP]
apply(rule type_aexpr_Const)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'100 = restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P'100 (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
A total of 11 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P'100 = restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 3. \<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}) \<longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P'100 (dma_type v)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'100 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'100 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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, fast)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<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}) \<longrightarrow> pred_entailment (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (dma_type v)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_Y 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) {bexp.Not (Eq control_Y 0), Eq control_X 0} (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''100
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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>)
[PROOF STATE]
proof (prove)
goal (12 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 [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const (Suc 0)) ?t139
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} ?t139
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''100 = restrict_preds_to_vars (assign_post {bexp.Not (Eq control_Y 0), Eq control_X 0} control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 6. \<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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''100 (dma_type v)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
A total of 12 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const (Suc 0)) ?t139
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} ?t139
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''100 = restrict_preds_to_vars (assign_post {bexp.Not (Eq control_Y 0), Eq control_X 0} control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''100 (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
A total of 11 subgoals...
[PROOF STEP]
apply(rule type_aexpr_Const)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''100 = restrict_preds_to_vars (assign_post {bexp.Not (Eq control_Y 0), Eq control_X 0} control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''100 (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''100 = restrict_preds_to_vars (assign_post {bexp.Not (Eq control_Y 0), Eq control_X 0} control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 3. \<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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''100 (dma_type v)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 auto[1]
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''100 = restrict_preds_to_vars (assign_post {bexp.Not (Eq control_Y 0), Eq control_X 0} control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 2. \<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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''100 (dma_type v)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''100 {bexp_neg (Eq control_Y 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''100 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (7 subgoals):
 1. \<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}) \<longrightarrow> pred_entailment {bexp.Not (Eq control_Y 0), Eq control_X 0} (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} (dma_type v)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} {bexp_neg (Eq control_Y 0)}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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> pred_entailment (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_Y 0}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} {bexp_neg (Eq control_Y 0)}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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: subset_entailment)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} {bexp_neg (Eq control_Y 0)}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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: subset_entailment)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const (Suc 0)) [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) ?P''81
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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>)
[PROOF STATE]
proof (prove)
goal (9 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 [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const (Suc 0)) ?t157
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) ?t157
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''81 = restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 6. \<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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''81 (dma_type v)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (8 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_aexpr [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] (Const (Suc 0)) ?t157
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) ?t157
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''81 = restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''81 (dma_type v)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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_Const)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''81 = restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) 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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''81 (dma_type v)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}]. control_Z \<notin> vars_of_type (the ([Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''81 = restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 3. \<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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''81 (dma_type v)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?P''81 = restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}
 2. \<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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) ?P''81 (dma_type v)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''81 {bexp_neg (Eq control_X 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''81 - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 fast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<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}) \<longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) \<and> subtype (to_total [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] v) (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (dma_type v)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {bexp_neg (Eq control_X 0)}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {Eq control_X 0}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {bexp_neg (Eq control_X 0)}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0))), Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0), Imp (Eq control_Y 0) (Same control_Z (Const 0)), Imp (Eq control_Y 0) (Eq control_X 0)} {Eq control_X 0}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {bexp_neg (Eq control_X 0)}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 intro: pred_entailment_singleton_by_case_distinction simp: image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {bexp_neg (Eq control_X 0)}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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 intro: subset_entailment)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) ((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_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ?\<Gamma>'268 ?\<S>'268 ?P'268
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'268 ?\<S>'268 ?P'268 ((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_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) Skip ?\<Gamma>'268 ?\<S>'268 ?P'268
 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_Y 0, Eq control_X 0}] x) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (Z -=\<^sub>m AsmNoReadOrWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'268 ?\<S>'268 ?P'268 ((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_Y 0, Eq control_X 0}] x) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (Z -=\<^sub>m AsmNoReadOrWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) ((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_Y 0, Eq control_X 0}] x) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) (to_total (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) x)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (Z -=\<^sub>m AsmNoReadOrWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) ((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: subtype_def pred_def add_anno_def pred_entailment_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_stable [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) (Z -=\<^sub>m AsmNoReadOrWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno [Z \<mapsto> {Eq control_Y 0, Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) (restrict_preds_to_vars (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (restrict_preds_to_vars (assign_post (add_pred (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ({control_Z, control_Y, control_X}, {Z}) (Eq control_Y 0)) control_Z (Const 0)) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_Y 0), Eq control_X 0} - {bexp_neg (Eq control_Y 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (restrict_preds_to_vars (assign_post (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) control_Z (Const (Suc 0))) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v} - {bexp_neg (Eq control_X 0)})) {v. local.stable ({control_Z, control_Y, control_X}, {Z}) v}) {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {Z}) (Z -=\<^sub>m AsmNoReadOrWrite)) v}) ((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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} ((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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (Skip@[control_X -=\<^sub>m AsmNoWrite]) ?\<Gamma>'294 ?\<S>'294 ?P'294
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'294 ?\<S>'294 ?P'294 ((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}, {}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'294 ?\<S>'294 ?P'294
 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 {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (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}, {}) (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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (control_X -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'294 ?\<S>'294 ?P'294 ((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 {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (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}, {}) (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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (control_X -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) ((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 {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (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}, {}) (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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (control_X -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) ((Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(clarsimp simp: subtype_def pred_def add_anno_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 -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y, control_X}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (control_X -=\<^sub>m AsmNoWrite)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) ((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}, {}) {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} (control_X -=\<^sub>m AsmNoWrite)
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {Imp (bexp.Not (Eq control_X 0)) (Same control_Z (Const (Suc 0))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Same control_Z (Const (Suc 0)))), Imp (Eq control_X 0) (Imp (bexp.Not (Eq control_Y 0)) (Eq control_X 0)), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Same control_Z (Const 0))), Imp (Eq control_X 0) (Imp (Eq control_Y 0) (Eq control_X 0))} {v. local.stable (add_anno_stable ({control_Z, control_Y, control_X}, {}) (control_X -=\<^sub>m AsmNoWrite)) v}) ((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}, {}) {} ((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}, {}) {} (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ?\<Gamma>'307 ?\<S>'307 ?P'307
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'307 ?\<S>'307 ?P'307 ((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_Y -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y}, {}) (control_Y -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y}, {}) (control_Y -=\<^sub>m AsmNoWrite)) v}) Skip ?\<Gamma>'307 ?\<S>'307 ?P'307
 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_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y}, {}) (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_Y -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y}, {}) {} (control_Y -=\<^sub>m AsmNoWrite)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'307 ?\<S>'307 ?P'307 ((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_Y -=\<^sub>m AsmNoWrite)) v}) (to_total (add_anno Map.empty ({control_Z, control_Y}, {}) (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_Y -=\<^sub>m AsmNoWrite)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> anno_type_sec Map.empty ({control_Z, control_Y}, {}) {} (control_Y -=\<^sub>m AsmNoWrite)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type (add_anno Map.empty ({control_Z, control_Y}, {}) (control_Y -=\<^sub>m AsmNoWrite)) (add_anno_stable ({control_Z, control_Y}, {}) (control_Y -=\<^sub>m AsmNoWrite)) (restrict_preds_to_vars {} {v. local.stable (add_anno_stable ({control_Z, control_Y}, {}) (control_Y -=\<^sub>m AsmNoWrite)) v}) ((Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done