[STATEMENT]
lemma swap_vars_typed':
  "\<Gamma> = (\<lambda>_. None) \<Longrightarrow> \<S> = ({},{}) \<Longrightarrow> P = {} \<Longrightarrow>
  \<exists>\<Gamma>' \<S>' P'. has_type \<Gamma> \<S> P swap_vars \<Gamma>' \<S>' P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>' \<S>' P'. has_type \<Gamma> \<S> P swap_vars \<Gamma>' \<S>' P'
[PROOF STEP]
apply (has_type_tac prog: swap_vars_def aexpr: type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'243 ?\<S>'243 ?P'243
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'243 ?\<S>'243 ?P'243 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(conc_tac Z Z)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'243 ?\<S>'243 ?P'243
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'243 ?\<S>'243 ?P'243 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(conc_tac Y Z)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Z (Load control_X), Same Y (Load Z)} (control_X \<leftarrow> Load control_Y) ?\<Gamma>'243 ?\<S>'243 ?P'243
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'243 ?\<S>'243 ?P'243 ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Y \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z] Y)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply post_conc_tac
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> Z \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}] Z)) {Same control_Z (Load control_X), Same Y (Load Z)} (dma_type Z)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type Z)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type Z)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} ((control_Y \<leftarrow> Load control_Z) ;; (Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply post_conc_tac
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} (control_Y \<leftarrow> Load control_Z) ?\<Gamma>'291 ?\<S>'291 ?P'291
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'291 ?\<S>'291 ?P'291 ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} (control_Y \<leftarrow> Load control_Z) ?\<Gamma>'291 ?\<S>'291 ?P'291
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'291 ?\<S>'291 ?P'291 ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply(conc_tac X X)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_X (Load control_Y), Same Y (Load Z)} (control_Y \<leftarrow> Load control_Z) ?\<Gamma>'291 ?\<S>'291 ?P'291
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'291 ?\<S>'291 ?P'291 ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> X \<in> dom [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z]
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_equiv (the ([X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z] X)) {Same control_X (Load control_Y), Same Y (Load Z)} (dma_type X)
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_wellformed (dma_type X)
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> type_stable ({control_Z, control_Y, control_X}, {Z, Y, X}) (dma_type X)
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type [X \<mapsto> {Eq control_X 0}, Y \<mapsto> {Eq control_Y 0}, Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> {Eq control_X 0}, X \<mapsto> {Eq control_Y 0}, Y \<mapsto> {Eq control_X 0}, Z \<mapsto> dma_type Z, Y \<mapsto> dma_type Z, X \<mapsto> dma_type X] ({control_Z, control_Y, control_X}, {Z, Y, X}) {Same control_Y (Load control_Z), Same Y (Load Z)} ((Skip@[X -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Y -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[Z -=\<^sub>m AsmNoReadOrWrite]) ;; (Skip@[control_X -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Y -=\<^sub>m AsmNoWrite]) ;; (Skip@[control_Z -=\<^sub>m AsmNoWrite]) ;; Skip) ?\<Gamma>' ?\<S>'1 ?P'2
[PROOF STEP]
apply  (post_conc_tac)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[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 (has_type_no_if_tac
          prog: add_vars_def
          aexpr: type_aexpr_Load' type_aexpr_Load type_aexpr_Add
           type_aexpr_Add' type_aexpr_Add''  type_aexpr_Const
          bexpr:type_bexprI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 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 1)) (control_Z \<leftarrow> Const 1)) ?\<Gamma>'107 ?\<S>'107 ?P'107
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 ?P'107 ((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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] (Eq control_X 0) ?t110
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t110
 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}) (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 1)) ?\<Gamma>'107 ?\<S>'107 ?P'110
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'110 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'110 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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> ?t110 = \<Union> (to_total [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ` bexp_vars (Eq control_X 0))
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t110
 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}) (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 1)) ?\<Gamma>'107 ?\<S>'107 ?P'110
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'110 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'110 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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> ?t110 = {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {} ?t110
 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}) (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 1)) ?\<Gamma>'107 ?\<S>'107 ?P'110
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'110 {Eq control_X 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'110 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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 1)) ?\<Gamma>'107 ?\<S>'107 ?P'110
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'110 {Eq control_X 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'110 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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 1)) ?\<Gamma>'107 ?\<S>'107 ?P'110
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'110 {Eq control_X 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (?P'110 - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] (Eq control_Y 0) ?t129
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ?t129
 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}) (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>'107 ?\<S>'107 ?P'129
 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}) (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 1) ?\<Gamma>'107 ?\<S>'107 ?P''129
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'129 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 7. \<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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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> ?t129 = \<Union> (to_total [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ` 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)) ?t129
 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}) (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>'107 ?\<S>'107 ?P'129
 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}) (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 1) ?\<Gamma>'107 ?\<S>'107 ?P''129
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'129 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 7. \<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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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 (10 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> ?t129 = {}
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (Eq control_X 0)) ?t129
 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}) (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>'107 ?\<S>'107 ?P'129
 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}) (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 1) ?\<Gamma>'107 ?\<S>'107 ?P''129
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'129 {Eq control_Y 0}
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 7. \<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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v}) {Eq control_X 0}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 10. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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>'107 ?\<S>'107 ?P'129
 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}) (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 1) ?\<Gamma>'107 ?\<S>'107 ?P''129
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'129 {Eq control_Y 0}
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 6. \<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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v}) {Eq control_X 0}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 9. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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>'107 ?\<S>'107 ?P'129
 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}) (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 1) ?\<Gamma>'107 ?\<S>'107 ?P''129
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P'129 {Eq control_Y 0}
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 5. \<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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) ?\<Gamma>'107 ?\<S>'107 ?P''110
 6. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v}) {Eq control_X 0}
 7. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''110 {bexp_neg (Eq control_X 0)}
 8. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> has_type ?\<Gamma>'107 ?\<S>'107 (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` (?P'129 - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {bexp_neg (Eq control_Y 0)})) {v. local.stable ?\<S>'107 v} - {Eq control_X 0}) \<union> Imp (bexp_neg (Eq control_X 0)) ` (?P''110 - {bexp_neg (Eq control_X 0)})) {v. local.stable ?\<S>'107 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 (has_type_tac' aexpr: type_aexpr_Const)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 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}) (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 1) [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P''129
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} {Eq control_Y 0}
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment ?P''129 {bexp_neg (Eq control_Y 0)}
 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}) (add_pred {} ({control_Z, control_Y, control_X}, {Z}) (bexp_neg (Eq control_X 0))) (control_Z \<leftarrow> Const 1) [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P''110
 5. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {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''110 {bexp_neg (Eq control_X 0)}
 7. \<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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {Eq control_Y 0}) \<union> Imp (bexp_neg (Eq control_Y 0)) ` (?P''129 - {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''110 - {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 (has_type_tac' aexpr: type_aexpr_Const)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment {Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} {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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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 1) [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P''110
 4. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 {bexp_neg (Eq control_X 0)}
 6. \<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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 - {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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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 1) [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P''110
 3. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 {bexp_neg (Eq control_X 0)}
 5. \<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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 - {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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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 1) [Z \<mapsto> {Eq control_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({control_Z, control_Y, control_X}, {Z}) ?P''110
 2. \<lbrakk>\<Gamma> = Map.empty; \<S> = ({}, {}); P = {}\<rbrakk> \<Longrightarrow> pred_entailment (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 {bexp_neg (Eq control_X 0)}
 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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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''110 - {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 (has_type_tac' aexpr: type_aexpr_Const)
[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) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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 {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} {bexp_neg (Eq control_X 0)}
 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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} - {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 {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} {bexp_neg (Eq control_X 0)}
 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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} - {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 {Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} {bexp_neg (Eq control_X 0)}
 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}) (restrict_preds_to_vars (Imp (Eq control_X 0) ` (restrict_preds_to_vars (Imp (Eq control_Y 0) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} - {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_Z 0}, Z \<mapsto> \<Union> {dma_type X, dma_type Y}] ({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) ` ({Same control_Z (Const 0), Eq control_Y 0, Eq control_X 0} - {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)) ` ({Same control_Z (Const (Suc 0)), bexp.Not (Eq control_X 0)} - {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 (has_type_tac')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem epath_prover_completeness:
  fixes A :: \<open>tm list\<close> and z :: \<open>fm list\<close>
  defines \<open>t \<equiv> secavProver (A, z)\<close>
  shows \<open>(fst (root t) = (A, z) \<and> wf t \<and> tfinite t) \<or>
    (\<exists> steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)\<close>
    (is \<open>?A \<or> ?B\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
assume \<open>\<not> ?A\<close>
[PROOF STATE]
proof (state)
this:
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t)

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
t \<equiv> secavProver (A, z)
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t)
[PROOF STEP]
have \<open>\<not> tfinite (mkTree rules (A, z))\<close>
[PROOF STATE]
proof (prove)
using this:
t \<equiv> secavProver (A, z)
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t)

goal (1 subgoal):
 1. \<not> tfinite (mkTree rules (A, z))
[PROOF STEP]
unfolding secavProver_def
[PROOF STATE]
proof (prove)
using this:
t \<equiv> mkTree rules (A, z)
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t)

goal (1 subgoal):
 1. \<not> tfinite (mkTree rules (A, z))
[PROOF STEP]
using wf_mkTree fair_rules
[PROOF STATE]
proof (prove)
using this:
t \<equiv> mkTree rules (A, z)
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t)
\<lbrakk>?s \<in> UNIV; fair ?rs\<rbrakk> \<Longrightarrow> Prover.wf (mkTree ?rs ?s)
fair rules

goal (1 subgoal):
 1. \<not> tfinite (mkTree rules (A, z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> tfinite (mkTree rules (A, z))

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> tfinite (mkTree rules (A, z))
[PROOF STEP]
obtain steps where \<open>ipath (mkTree rules (A, z)) steps\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> tfinite (mkTree rules (A, z))

goal (1 subgoal):
 1. (\<And>steps. ipath (mkTree rules (A, z)) steps \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Konig
[PROOF STATE]
proof (prove)
using this:
\<not> tfinite (mkTree rules (A, z))
\<not> tfinite ?t \<Longrightarrow> ipath ?t (konig ?t)

goal (1 subgoal):
 1. (\<And>steps. ipath (mkTree rules (A, z)) steps \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ipath (mkTree rules (A, z)) steps

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
t \<equiv> secavProver (A, z)
ipath (mkTree rules (A, z)) steps
[PROOF STEP]
have \<open>fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps\<close>
[PROOF STATE]
proof (prove)
using this:
t \<equiv> secavProver (A, z)
ipath (mkTree rules (A, z)) steps

goal (1 subgoal):
 1. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps
[PROOF STEP]
by (metis UNIV_I fair_rules ipath.cases ipath_mkTree_Saturated mkTree.simps(1) prod.sel(1)
          wf_ipath_epath wf_mkTree)
[PROOF STATE]
proof (state)
this:
fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps
[PROOF STEP]
have ?B
[PROOF STATE]
proof (prove)
using this:
fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps

goal (1 subgoal):
 1. \<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t) \<Longrightarrow> \<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t) \<Longrightarrow> \<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t) \<Longrightarrow> \<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t \<or> (\<exists>steps. fst (shd steps) = (A, z) \<and> epath steps \<and> Saturated steps)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma epath_countermodel:
  assumes \<open>fst (shd steps) = (A, z)\<close> and \<open>epath steps\<close> and \<open>Saturated steps\<close>
  shows \<open>\<not> uvalid z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> uvalid z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
assume \<open>uvalid z\<close>
[PROOF STATE]
proof (state)
this:
uvalid z

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uvalid z

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
have \<open>Hintikka (tree_fms steps)\<close> (is \<open>Hintikka ?S\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hintikka (tree_fms steps)
[PROOF STEP]
using assms escape_path_Hintikka assms
[PROOF STATE]
proof (prove)
using this:
fst (shd steps) = (A, z)
epath steps
Saturated steps
\<lbrakk>epath ?steps; Saturated ?steps\<rbrakk> \<Longrightarrow> Hintikka (tree_fms ?steps)
fst (shd steps) = (A, z)
epath steps
Saturated steps

goal (1 subgoal):
 1. Hintikka (tree_fms steps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Hintikka (tree_fms steps)

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Hintikka (tree_fms steps)

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall>p \<in> set z. p \<in> tree_fms steps\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set z. p \<in> tree_fms steps
[PROOF STEP]
using assms shd_sset
[PROOF STATE]
proof (prove)
using this:
fst (shd steps) = (A, z)
epath steps
Saturated steps
shd ?a \<in> i.R ?a

goal (1 subgoal):
 1. \<forall>p\<in>set z. p \<in> tree_fms steps
[PROOF STEP]
by (metis Pair_inject prod.collapse pseq_def pseq_in_tree_fms)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set z. p \<in> tree_fms steps

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set z. p \<in> tree_fms steps
[PROOF STEP]
have \<open>\<exists>g. \<forall>p \<in> set z. \<not> usemantics (terms ?S) (E ?S) (F ?S) g p\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set z. p \<in> tree_fms steps

goal (1 subgoal):
 1. \<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p
[PROOF STEP]
using calculation(2) Hintikka_counter_model assms
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set z. p \<in> tree_fms steps
Hintikka (tree_fms steps)
Hintikka ?S \<Longrightarrow> (?p \<in> ?S \<longrightarrow> \<not> usemantics (terms ?S) (E ?S) (F ?S) (\<lambda>n ts. Neg (Pre n ts) \<in> ?S) ?p) \<and> (Neg ?p \<in> ?S \<longrightarrow> usemantics (terms ?S) (E ?S) (F ?S) (\<lambda>n ts. Neg (Pre n ts) \<in> ?S) ?p)
fst (shd steps) = (A, z)
epath steps
Saturated steps

goal (1 subgoal):
 1. \<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
have \<open>is_env (terms ?S) (E ?S)\<close> \<open>is_fdenot (terms ?S) (F ?S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_env (terms (tree_fms steps)) (E (tree_fms steps)) &&& is_fdenot (terms (tree_fms steps)) (F (tree_fms steps))
[PROOF STEP]
using is_env_E is_fdenot_F
[PROOF STATE]
proof (prove)
using this:
is_env (terms ?S) (E ?S)
is_fdenot (terms ?S) (F ?S)

goal (1 subgoal):
 1. is_env (terms (tree_fms steps)) (E (tree_fms steps)) &&& is_fdenot (terms (tree_fms steps)) (F (tree_fms steps))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
is_env (terms (tree_fms steps)) (E (tree_fms steps))
is_fdenot (terms (tree_fms steps)) (F (tree_fms steps))

goal (1 subgoal):
 1. uvalid z \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uvalid z
Hintikka (tree_fms steps)
\<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p
is_env (terms (tree_fms steps)) (E (tree_fms steps))
is_fdenot (terms (tree_fms steps)) (F (tree_fms steps))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
uvalid z
Hintikka (tree_fms steps)
\<exists>g. \<forall>p\<in>set z. \<not> usemantics (terms (tree_fms steps)) (E (tree_fms steps)) (F (tree_fms steps)) g p
is_env (terms (tree_fms steps)) (E (tree_fms steps))
is_fdenot (terms (tree_fms steps)) (F (tree_fms steps))

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem prover_completeness_usemantics:
  fixes A :: \<open>tm list\<close>
  assumes \<open>uvalid z\<close>
  defines \<open>t \<equiv> secavProver (A, z)\<close>
  shows \<open>fst (root t) = (A, z) \<and> wf t \<and> tfinite t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t
[PROOF STEP]
using assms epath_prover_completeness epath_countermodel
[PROOF STATE]
proof (prove)
using this:
uvalid z
t \<equiv> secavProver (A, z)
fst (tree.root (secavProver (?A, ?z))) = (?A, ?z) \<and> Prover.wf (secavProver (?A, ?z)) \<and> tfinite (secavProver (?A, ?z)) \<or> (\<exists>steps. fst (shd steps) = (?A, ?z) \<and> epath steps \<and> Saturated steps)
\<lbrakk>fst (shd ?steps) = (?A, ?z); epath ?steps; Saturated ?steps\<rbrakk> \<Longrightarrow> \<not> uvalid ?z

goal (1 subgoal):
 1. fst (tree.root t) = (A, z) \<and> Prover.wf t \<and> tfinite t
[PROOF STEP]
by blast


[STATEMENT]
lemma lbI [Pure.intro]:
  "(\<And>y. y \<in> B \<Longrightarrow> P\<^sup>=\<^sup>= x y) \<Longrightarrow> lb P B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. y \<in> B \<Longrightarrow> P\<^sup>=\<^sup>= x y) \<Longrightarrow> lb P B x
[PROOF STEP]
by (auto simp: lb_def)


[STATEMENT]
lemma glbI [Pure.intro]:
  "lb P B x \<Longrightarrow> (\<And>y. lb P B y \<Longrightarrow> P\<^sup>=\<^sup>= y x) \<Longrightarrow> glb P B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lb P B x; \<And>y. lb P B y \<Longrightarrow> P\<^sup>=\<^sup>= y x\<rbrakk> \<Longrightarrow> glb P B x
[PROOF STEP]
by (auto simp: glb_def)


[STATEMENT]
lemma glb_unique:
  "antisymp_on P A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> glb P B x \<Longrightarrow> glb P B y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>antisymp_on P A; x \<in> A; y \<in> A; glb P B x; glb P B y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (auto simp: glb_def antisymp_on_def)


[STATEMENT]
lemma openI [Pure.intro]:
  "(\<And>C. chain C \<Longrightarrow> C \<noteq> {} \<Longrightarrow> \<exists>x\<in>A. glb (\<sqsubset>) C x \<and> Q x \<Longrightarrow> \<exists>y\<in>C. Q y) \<Longrightarrow> open Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>chain_on (\<sqsubset>) C A; C \<noteq> {}; \<exists>x\<in>A. glb (\<sqsubset>) C x \<and> Q x\<rbrakk> \<Longrightarrow> \<exists>y\<in>C. Q y) \<Longrightarrow> open Q
[PROOF STEP]
by (auto simp: open_def)


[STATEMENT]
lemma open_glb:
  "\<lbrakk>chain C; C \<noteq> {}; open Q; \<forall>x\<in>C. \<not> Q x; x \<in> A; glb (\<sqsubset>) C x\<rbrakk> \<Longrightarrow> \<not> Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>chain_on (\<sqsubset>) C A; C \<noteq> {}; open Q; \<forall>x\<in>C. \<not> Q x; x \<in> A; glb (\<sqsubset>) C x\<rbrakk> \<Longrightarrow> \<not> Q x
[PROOF STEP]
by (auto simp: open_def)


[STATEMENT]
lemma downward_completeI [Pure.intro]:
  assumes "\<And>C. chain C \<Longrightarrow> C \<noteq> {} \<Longrightarrow> \<exists>x\<in>A. glb (\<sqsubset>) C x"
  shows "downward_complete"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. downward_complete
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>chain_on (\<sqsubset>) ?C A; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. glb (\<sqsubset>) ?C x

goal (1 subgoal):
 1. downward_complete
[PROOF STEP]
by (auto simp: downward_complete_def)


[STATEMENT]
lemma dc_onI [Pure.intro]:
  assumes "\<And>C. chain_on P C A \<Longrightarrow> C \<noteq> {} \<Longrightarrow> \<exists>x\<in>A. glb P C x"
  shows "dc_on P A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dc_on P A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>chain_on P ?C A; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. glb P ?C x

goal (1 subgoal):
 1. dc_on P A
[PROOF STEP]
by (auto simp: dc_on_def)


[STATEMENT]
lemma open_onI [Pure.intro]:
  "(\<And>C. chain_on P C A \<Longrightarrow> C \<noteq> {} \<Longrightarrow> \<exists>x\<in>A. glb P C x \<and> Q x \<Longrightarrow> \<exists>y\<in>C. Q y) \<Longrightarrow> open_on P Q A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>chain_on P C A; C \<noteq> {}; \<exists>x\<in>A. glb P C x \<and> Q x\<rbrakk> \<Longrightarrow> \<exists>y\<in>C. Q y) \<Longrightarrow> open_on P Q A
[PROOF STEP]
by (auto simp: open_on_def)


[STATEMENT]
lemma chain_on_reflclp:
  "chain_on P\<^sup>=\<^sup>= A C \<longleftrightarrow> chain_on P A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_on P\<^sup>=\<^sup>= A C = chain_on P A C
[PROOF STEP]
by (auto simp: pred_on.chain_def)


[STATEMENT]
lemma lb_reflclp:
  "lb P\<^sup>=\<^sup>= B x \<longleftrightarrow> lb P B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lb P\<^sup>=\<^sup>= B x = lb P B x
[PROOF STEP]
by (auto simp: lb_def)


[STATEMENT]
lemma glb_reflclp:
  "glb P\<^sup>=\<^sup>= B x \<longleftrightarrow> glb P B x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. glb P\<^sup>=\<^sup>= B x = glb P B x
[PROOF STEP]
by (auto simp: glb_def lb_reflclp)


[STATEMENT]
lemma dc_on_reflclp:
  "dc_on P\<^sup>=\<^sup>= A \<longleftrightarrow> dc_on P A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dc_on P\<^sup>=\<^sup>= A = dc_on P A
[PROOF STEP]
by (auto simp: dc_on_def chain_on_reflclp glb_reflclp)


[STATEMENT]
lemma open_induct_on [consumes 4, case_names less]:
  assumes qo: "qo_on P A" and "dc_on P A" and "open_on P Q A"
    and "x \<in> A"
    and ind: "\<And>x. \<lbrakk>x \<in> A; \<And>y. \<lbrakk>y \<in> A; strict P y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x"
  shows "Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
assume "\<not> Q x"
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
let ?B = "{x\<in>A. \<not> Q x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
have "?B \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A. \<not> Q x} \<subseteq> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x \<in> A. \<not> Q x} \<subseteq> A

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
interpret B: pred_on ?B P
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
from B.Hausdorff
[PROOF STATE]
proof (chain)
picking this:
Ex B.maxchain
[PROOF STEP]
obtain M
    where chain: "B.chain M"
    and max: "\<And>C. B.chain C \<Longrightarrow> M \<subseteq> C \<Longrightarrow> M = C"
[PROOF STATE]
proof (prove)
using this:
Ex B.maxchain

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>chain_on P M {x \<in> A. \<not> Q x}; \<And>C. \<lbrakk>chain_on P C {x \<in> A. \<not> Q x}; M \<subseteq> C\<rbrakk> \<Longrightarrow> M = C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: B.maxchain_def)
[PROOF STATE]
proof (state)
this:
chain_on P M {x \<in> A. \<not> Q x}
\<lbrakk>chain_on P ?C {x \<in> A. \<not> Q x}; M \<subseteq> ?C\<rbrakk> \<Longrightarrow> M = ?C

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chain_on P M {x \<in> A. \<not> Q x}
\<lbrakk>chain_on P ?C {x \<in> A. \<not> Q x}; M \<subseteq> ?C\<rbrakk> \<Longrightarrow> M = ?C
[PROOF STEP]
have "M \<subseteq> ?B"
[PROOF STATE]
proof (prove)
using this:
chain_on P M {x \<in> A. \<not> Q x}
\<lbrakk>chain_on P ?C {x \<in> A. \<not> Q x}; M \<subseteq> ?C\<rbrakk> \<Longrightarrow> M = ?C

goal (1 subgoal):
 1. M \<subseteq> {x \<in> A. \<not> Q x}
[PROOF STEP]
by (auto simp: B.chain_def)
[PROOF STATE]
proof (state)
this:
M \<subseteq> {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "M = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M = {} \<Longrightarrow> False
 2. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "M = {}"
[PROOF STATE]
proof (state)
this:
M = {}

goal (2 subgoals):
 1. M = {} \<Longrightarrow> False
 2. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M = {}

goal (2 subgoals):
 1. M = {} \<Longrightarrow> False
 2. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "B.chain {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_on P {x} {x \<in> A. \<not> Q x}
[PROOF STEP]
using \<open>x \<in> A\<close> and \<open>\<not> Q x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> A
\<not> Q x

goal (1 subgoal):
 1. chain_on P {x} {x \<in> A. \<not> Q x}
[PROOF STEP]
by (simp add: B.chain_def)
[PROOF STATE]
proof (state)
this:
chain_on P {x} {x \<in> A. \<not> Q x}

goal (2 subgoals):
 1. M = {} \<Longrightarrow> False
 2. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
M = {}
chain_on P {x} {x \<in> A. \<not> Q x}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
M = {}
chain_on P {x} {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. False
[PROOF STEP]
using max
[PROOF STATE]
proof (prove)
using this:
M = {}
chain_on P {x} {x \<in> A. \<not> Q x}
\<lbrakk>chain_on P ?C {x \<in> A. \<not> Q x}; M \<subseteq> ?C\<rbrakk> \<Longrightarrow> M = ?C

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
interpret A: pred_on A P
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "M \<noteq> {}"
[PROOF STATE]
proof (state)
this:
M \<noteq> {}

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "A.chain M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_on P M A
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
chain_on P M {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. chain_on P M A
[PROOF STEP]
by (auto simp: A.chain_def B.chain_def)
[PROOF STATE]
proof (state)
this:
chain_on P M A

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
chain_on P M A

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with \<open>dc_on P A\<close> and \<open>M \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
A.downward_complete
M \<noteq> {}
chain_on P M A
[PROOF STEP]
obtain m
      where "m \<in> A" and "glb P M m"
[PROOF STATE]
proof (prove)
using this:
A.downward_complete
M \<noteq> {}
chain_on P M A

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<in> A; glb P M m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: A.downward_complete_def)
[PROOF STATE]
proof (state)
this:
m \<in> A
glb P M m

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
chain_on P M A
m \<in> A
glb P M m
[PROOF STEP]
have "\<not> Q m" and "m \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
chain_on P M A
m \<in> A
glb P M m

goal (1 subgoal):
 1. \<not> Q m &&& m \<in> {x \<in> A. \<not> Q x}
[PROOF STEP]
using A.open_glb [OF _ \<open>M \<noteq> {}\<close> \<open>open_on P Q A\<close> _ _ \<open>glb P M m\<close>]
      and \<open>M \<subseteq> ?B\<close>
[PROOF STATE]
proof (prove)
using this:
chain_on P M A
m \<in> A
glb P M m
\<lbrakk>chain_on P M A; \<forall>x\<in>M. \<not> Q x; m \<in> A\<rbrakk> \<Longrightarrow> \<not> Q m
M \<subseteq> {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. \<not> Q m &&& m \<in> {x \<in> A. \<not> Q x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> Q m
m \<in> {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from ind [OF \<open>m \<in> A\<close>] and \<open>\<not> Q m\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<And>y. \<lbrakk>y \<in> A; strict P y m\<rbrakk> \<Longrightarrow> Q y) \<Longrightarrow> Q m
\<not> Q m
[PROOF STEP]
obtain y
      where "y \<in> A" and "strict P y m" and "\<not> Q y"
[PROOF STATE]
proof (prove)
using this:
(\<And>y. \<lbrakk>y \<in> A; strict P y m\<rbrakk> \<Longrightarrow> Q y) \<Longrightarrow> Q m
\<not> Q m

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> A; strict P y m; \<not> Q y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> A
strict P y m
\<not> Q y

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> A
strict P y m
\<not> Q y
[PROOF STEP]
have "P y m" and "y \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
y \<in> A
strict P y m
\<not> Q y

goal (1 subgoal):
 1. P y m &&& y \<in> {x \<in> A. \<not> Q x}
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
P y m
y \<in> {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from transp_on_subset [OF \<open>?B \<subseteq> A\<close> qo_on_imp_transp_on [OF qo]]
[PROOF STATE]
proof (chain)
picking this:
transp_on P {x \<in> A. \<not> Q x}
[PROOF STEP]
have "transp_on P ?B"
[PROOF STATE]
proof (prove)
using this:
transp_on P {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. transp_on P {x \<in> A. \<not> Q x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
transp_on P {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from B.chain_glb [OF this chain \<open>glb P M m\<close> \<open>m \<in> ?B\<close> \<open>y \<in> ?B\<close> \<open>P y m\<close>]
[PROOF STATE]
proof (chain)
picking this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}
[PROOF STEP]
have "B.chain ({y} \<union> M)"
[PROOF STATE]
proof (prove)
using this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. M \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>glb P M m\<close> and \<open>strict P y m\<close>
[PROOF STATE]
proof (prove)
using this:
chain_on P ({y} \<union> M) {x \<in> A. \<not> Q x}
glb P M m
strict P y m

goal (1 subgoal):
 1. False
[PROOF STEP]
by (cases "y \<in> M") (auto dest: max simp: glb_def lb_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst3_simp[simp]: "fst3 (a,b,c) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst3 (a, b, c) = a
[PROOF STEP]
unfolding fst3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (a, b, c) = a
[PROOF STEP]
by simp


[STATEMENT]
lemma snd3_simp[simp]: "snd3 (a,b,c) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd3 (a, b, c) = b
[PROOF STEP]
unfolding snd3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst \<circ> snd) (a, b, c) = b
[PROOF STEP]
by simp


[STATEMENT]
lemma trd3_simp[simp]: "trd3 (a,b,c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trd3 (a, b, c) = c
[PROOF STEP]
unfolding trd3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snd \<circ> snd) (a, b, c) = c
[PROOF STEP]
by simp


[STATEMENT]
lemma fst3_snd3_trd3: "abc = (fst3 abc, snd3 abc, trd3 abc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abc = (fst3 abc, snd3 abc, trd3 abc)
[PROOF STEP]
unfolding fst3_def snd3_def trd3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abc = (fst abc, (fst \<circ> snd) abc, (snd \<circ> snd) abc)
[PROOF STEP]
by auto


[STATEMENT]
lemma fst3_snd3_trd3_rev[simp]:
"(fst3 abc, snd3 abc, trd3 abc) = abc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst3 abc, snd3 abc, trd3 abc) = abc
[PROOF STEP]
using fst3_snd3_trd3[of abc]
[PROOF STATE]
proof (prove)
using this:
abc = (fst3 abc, snd3 abc, trd3 abc)

goal (1 subgoal):
 1. (fst3 abc, snd3 abc, trd3 abc) = abc
[PROOF STEP]
by simp


[STATEMENT]
lemma map_id[simp]: "map id l = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map id l = l
[PROOF STEP]
unfolding id_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. x) l = l
[PROOF STEP]
by simp


[STATEMENT]
lemma ext2:
"(f \<noteq> g) = (\<exists> x. f x \<noteq> g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<noteq> g) = (\<exists>x. f x \<noteq> g x)
[PROOF STEP]
using ext
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. (f \<noteq> g) = (\<exists>x. f x \<noteq> g x)
[PROOF STEP]
by auto


[STATEMENT]
lemma not_equals_and_not_equals_not_in:
"(y \<noteq> x \<and> y \<noteq> x' \<and> phi) =
 (y \<notin> {x,x'} \<and> phi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<noteq> x \<and> y \<noteq> x' \<and> phi) = (y \<notin> {x, x'} \<and> phi)
[PROOF STEP]
by simp


[STATEMENT]
lemma mp2:
assumes "!! x y. phi x y \<Longrightarrow> chi x y" and "phi x y"
shows "chi x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chi x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
phi ?x ?y \<Longrightarrow> chi ?x ?y
phi x y

goal (1 subgoal):
 1. chi x y
[PROOF STEP]
by simp


[STATEMENT]
lemma mp3:
assumes "!! x y z. phi x y z \<Longrightarrow> chi x y z" and "phi x y z"
shows "chi x y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chi x y z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
phi ?x ?y ?z \<Longrightarrow> chi ?x ?y ?z
phi x y z

goal (1 subgoal):
 1. chi x y z
[PROOF STEP]
by simp


[STATEMENT]
lemma all_lt_Suc:
"(\<forall> i < Suc n. phi i) = ((\<forall> i < n. phi i) \<and> phi n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<Suc n. phi i) = ((\<forall>i<n. phi i) \<and> phi n)
[PROOF STEP]
using less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

goal (1 subgoal):
 1. (\<forall>i<Suc n. phi i) = ((\<forall>i<n. phi i) \<and> phi n)
[PROOF STEP]
by auto


[STATEMENT]
lemma tl_last[simp]:
assumes "tl L \<noteq> []"
shows "last (tl L) = last L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (tl L) = last L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
tl L \<noteq> []

goal (1 subgoal):
 1. last (tl L) = last L
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl L \<noteq> [] \<Longrightarrow> last (tl L) = last L
[PROOF STEP]
by(induct L, auto)


[STATEMENT]
lemma tl_last_hd:
assumes "L \<noteq> []" and "tl L = []"
shows "last L = hd L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last L = hd L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
L \<noteq> []
tl L = []

goal (1 subgoal):
 1. last L = hd L
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>L \<noteq> []; tl L = []\<rbrakk> \<Longrightarrow> last L = hd L
[PROOF STEP]
by(induct L, auto)


[STATEMENT]
lemma wf_lt2:
"wf lt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf lt2
[PROOF STEP]
unfolding lt2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (less_than <*lex*> less_than)
[PROOF STEP]
by auto


[STATEMENT]
lemma wf_lt3:
"wf lt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf lt3
[PROOF STEP]
unfolding lt3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (less_than <*lex*> lt2)
[PROOF STEP]
by (auto simp add: wf_lt2)


[STATEMENT]
lemma lt2[intro]:
"!! k1 k2 j1 j2. k1 < j1 \<Longrightarrow> ((k1,k2),(j1,j2)) \<in> lt2"
"!! k1 k2 j1 j2. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1,k2),(j1,j2)) \<in> lt2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k1 k2 j1 j2. k1 < j1 \<Longrightarrow> ((k1, k2), j1, j2) \<in> lt2) &&& (\<And>k1 k2 j1 j2. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1, k2), j1, j2) \<in> lt2)
[PROOF STEP]
unfolding lt2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k1 k2 j1 j2. k1 < j1 \<Longrightarrow> ((k1, k2), j1, j2) \<in> less_than <*lex*> less_than) &&& (\<And>k1 k2 j1 j2. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1, k2), j1, j2) \<in> less_than <*lex*> less_than)
[PROOF STEP]
by auto


[STATEMENT]
lemma lt3[intro]:
"!! k1 k2 k3 j1 j2 j3. k1 < j1 \<Longrightarrow> ((k1,k2,k3),(j1,j2,j3)) \<in> lt3"
"!! k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1,k2,k3),(j1,j2,j3)) \<in> lt3"
"!! k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 \<le> j2; k3 < j3\<rbrakk> \<Longrightarrow> ((k1,k2,k3),(j1,j2,j3)) \<in> lt3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k1 k2 k3 j1 j2 j3. k1 < j1 \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> lt3) &&& (\<And>k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> lt3) &&& (\<And>k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 \<le> j2; k3 < j3\<rbrakk> \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> lt3)
[PROOF STEP]
unfolding lt3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k1 k2 k3 j1 j2 j3. k1 < j1 \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> less_than <*lex*> lt2) &&& (\<And>k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 < j2\<rbrakk> \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> less_than <*lex*> lt2) &&& (\<And>k1 k2 k3 j1 j2 j3. \<lbrakk>k1 \<le> j1; k2 \<le> j2; k3 < j3\<rbrakk> \<Longrightarrow> ((k1, k2, k3), j1, j2, j3) \<in> less_than <*lex*> lt2)
[PROOF STEP]
by auto


[STATEMENT]
lemma measure_lex2_induct:
fixes h1 :: "'a1 \<Rightarrow> nat" and h2 :: "'a2 \<Rightarrow> nat"
assumes
"!! x1 x2.
  \<lbrakk>(!! y1 y2. h1 y1 < h1 x1 \<Longrightarrow> phi y1 y2);
   (!! y1 y2. \<lbrakk>h1 y1 \<le> h1 x1; h2 y2 < h2 x2\<rbrakk> \<Longrightarrow> phi y1 y2)\<rbrakk>
  \<Longrightarrow> phi x1 x2"
shows "phi x1 x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
let ?chi = "%(n1,n2). ALL x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
fix n1 n2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
have "?chi (n1,n2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (n1, n2) of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2
[PROOF STEP]
apply(rule wf_induct[of lt2 ?chi])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf lt2
 2. \<And>x. \<forall>y. (y, x) \<in> lt2 \<longrightarrow> (case y of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2) \<Longrightarrow> case x of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2
[PROOF STEP]
using wf_lt2 assms
[PROOF STATE]
proof (prove)
using this:
wf lt2
\<lbrakk>\<And>y1 y2. h1 y1 < h1 ?x1.0 \<Longrightarrow> phi y1 y2; \<And>y1 y2. \<lbrakk>h1 y1 \<le> h1 ?x1.0; h2 y2 < h2 ?x2.0\<rbrakk> \<Longrightarrow> phi y1 y2\<rbrakk> \<Longrightarrow> phi ?x1.0 ?x2.0

goal (2 subgoals):
 1. wf lt2
 2. \<And>x. \<forall>y. (y, x) \<in> lt2 \<longrightarrow> (case y of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2) \<Longrightarrow> case x of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
case (n1, n2) of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2

goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
case (?n1.2, ?n2.2) of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2

goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
case (?n1.2, ?n2.2) of (n1, n2) \<Rightarrow> \<forall>x1 x2. h1 x1 = n1 \<and> h2 x2 = n2 \<longrightarrow> phi x1 x2

goal (1 subgoal):
 1. phi x1 x2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
phi x1 x2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measure_lex3_induct:
fixes h1 :: "'a1 \<Rightarrow> nat" and h2 :: "'a2 \<Rightarrow> nat" and h3 :: "'a3 \<Rightarrow> nat"
assumes
"!! x1 x2 x3.
  \<lbrakk>(!! y1 y2 y3. h1 y1 < h1 x1 \<Longrightarrow> phi y1 y2 y3);
   (!! y1 y2 y3. \<lbrakk>h1 y1 \<le> h1 x1; h2 y2 < h2 x2\<rbrakk> \<Longrightarrow> phi y1 y2 y3);
   (!! y1 y2 y3. \<lbrakk>h1 y1 \<le> h1 x1; h2 y2 \<le> h2 x2; h3 y3 < h3 x3\<rbrakk> \<Longrightarrow> phi y1 y2 y3)\<rbrakk>
  \<Longrightarrow> phi x1 x2 x3"
shows "phi x1 x2 x3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
let ?chi = "%(n1,n2,n3). ALL x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
fix n1 n2 n3
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
have "?chi (n1,n2,n3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (n1, n2, n3) of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3
[PROOF STEP]
apply(rule wf_induct[of lt3 ?chi])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf lt3
 2. \<And>x. \<forall>y. (y, x) \<in> lt3 \<longrightarrow> (case y of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3) \<Longrightarrow> case x of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3
[PROOF STEP]
using wf_lt3 assms
[PROOF STATE]
proof (prove)
using this:
wf lt3
\<lbrakk>\<And>y1 y2 y3. h1 y1 < h1 ?x1.0 \<Longrightarrow> phi y1 y2 y3; \<And>y1 y2 y3. \<lbrakk>h1 y1 \<le> h1 ?x1.0; h2 y2 < h2 ?x2.0\<rbrakk> \<Longrightarrow> phi y1 y2 y3; \<And>y1 y2 y3. \<lbrakk>h1 y1 \<le> h1 ?x1.0; h2 y2 \<le> h2 ?x2.0; h3 y3 < h3 ?x3.0\<rbrakk> \<Longrightarrow> phi y1 y2 y3\<rbrakk> \<Longrightarrow> phi ?x1.0 ?x2.0 ?x3.0

goal (2 subgoals):
 1. wf lt3
 2. \<And>x. \<forall>y. (y, x) \<in> lt3 \<longrightarrow> (case y of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3) \<Longrightarrow> case x of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
case (n1, n2, n3) of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3

goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
case (?n1.2, ?n2.2, ?n3.2) of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3

goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
case (?n1.2, ?n2.2, ?n3.2) of (n1, n2, n3) \<Rightarrow> \<forall>x1 x2 x3. h1 x1 = n1 \<and> h2 x2 = n2 \<and> h3 x3 = n3 \<longrightarrow> phi x1 x2 x3

goal (1 subgoal):
 1. phi x1 x2 x3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
phi x1 x2 x3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_None: "(lift h inp i = None) = (inp i = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lift h inp i = None) = (inp i = None)
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h v)) = None) = (inp i = None)
[PROOF STEP]
by (cases "inp i", auto)


[STATEMENT]
lemma lift_Some:
"(\<exists> v. lift h inp i = Some v) = (\<exists> v'. inp i = Some v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. lift h inp i = Some v) = (\<exists>v'. inp i = Some v')
[PROOF STEP]
using lift_None[of h inp i]
[PROOF STATE]
proof (prove)
using this:
(lift h inp i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<exists>v. lift h inp i = Some v) = (\<exists>v'. inp i = Some v')
[PROOF STEP]
by force


[STATEMENT]
lemma lift_cong[fundef_cong]:
assumes "\<And> i v. inp i = Some v \<Longrightarrow>  h v = h' v"
shows "lift h inp = lift h' inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift h inp = lift h' inp
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h v)) = (\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h' v))
[PROOF STEP]
apply(rule ext)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h v)) = (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h' v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inp ?i = Some ?v \<Longrightarrow> h ?v = h' ?v

goal (1 subgoal):
 1. \<And>i. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h v)) = (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (h' v))
[PROOF STEP]
by (case_tac "inp i", auto)