theory ADT_IF

lemma small_step_irq_state_next_irq:
  "\<lbrakk> invs_if s1; (s',evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1;
     (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1;
     snd s1 = KernelExit; interrupted_modes (snd s2) \<rbrakk>
     \<Longrightarrow> next_irq_state_of_state (internal_state_if s1) = irq_state_of_state (internal_state_if s2)" apply (subgoal_tac "invs_if s'") apply (rule step_out_equivalent[where f="\<lambda>(states,mask). (next_irq_state (Suc states) mask,mask)"
                                     and g="\<lambda>s. (irq_state_of_state (internal_state_if s),
                                                 irq_masks_of_state (internal_state_if s))",
                                   simplified, THEN conjunct1]) apply assumption apply assumption apply (rule conjI) apply (rule ADT_A_if_Step_measure_if''[THEN conjunct2,rule_format],assumption+) apply (rule ADT_A_if_sub_big_steps_measuref_if,assumption+) apply (frule sub_big_steps_not_related) apply (simp add: big_step_R_def) apply simp apply (rule ADT_A_if_Step_irq_masks,assumption+) apply clarsimp apply (subgoal_tac "invs_if ((a,b),ba)") apply (rule_tac b=b and a=a and c=ba in irq_state_back) apply (rule_tac b=bb and a=aa and c=bc in irq_state_back) apply (rule conjI) apply (rule sym) apply (rule ADT_A_if_Step_measure_if'[THEN conjunct2,rule_format],assumption+) apply (rule ADT_A_if_sub_big_steps_measuref_if,assumption+) apply (drule sub_big_steps_not_related)+ apply (simp add: big_step_R_def) apply (simp add: big_step_R_def) apply (rule sym) apply (rule ADT_A_if_Step_irq_masks,assumption+) apply (simp add: invs_if_sub_big_steps_ADT_A_if)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if s1) = irq_state_of_state (internal_state_if s2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if s1) = irq_state_of_state (internal_state_if s2)
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> (?s'2, ?as2) \<in> sub_big_steps ?A2 ?R2 s1
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> (?s'2, s2) \<in> Step ?A2 ?a2
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_state_of_state (internal_state_if s2) = next_irq_state_of_state (internal_state_if ?s'2) \<and> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if ?s'2)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps ?A2 ?R2 s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step ?A2 ab) \<longrightarrow> \<not> ?R2 s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> (s', s2) \<in> Step (ADT_A_if utf) ?a2
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_state_of_state (internal_state_if s2) = next_irq_state_of_state (internal_state_if s') \<and> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_state_of_state (internal_state_if s2) = next_irq_state_of_state (internal_state_if s') \<and> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_state_of_state (internal_state_if s2) = next_irq_state_of_state (internal_state_if s')
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> 0 < measuref_if ?y27 s'
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd s')
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> interrupted_modes (snd s2)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 6. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd s')
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> interrupted_modes (snd s2)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; \<not> big_step_R s1 s'\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd s')
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> interrupted_modes (snd s2)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> interrupted_modes (snd s2)
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s2) = irq_masks_of_state (internal_state_if s')
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'\<rbrakk> \<Longrightarrow> \<forall>a b ba. (\<exists>as. (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1) \<longrightarrow> (\<forall>aa bb bc. (\<exists>ab. (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) ab) \<longrightarrow> \<not> big_step_R s1 ((aa, bb), bc) \<longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb)
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> next_irq_state_of_state b = next_irq_state_of_state bb \<and> irq_masks_of_state b = irq_masks_of_state bb
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if ((a, b), ba)) = next_irq_state_of_state bb \<and> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state bb
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if ((a, b), ba)) = next_irq_state_of_state (internal_state_if ((aa, bb), bc)) \<and> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if ((a, b), ba)) = next_irq_state_of_state (internal_state_if ((aa, bb), bc))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if ((aa, bb), bc)) = next_irq_state_of_state (internal_state_if ((a, b), ba))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (6 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> 0 < measuref_if (?y68 a b ba as aa bb bc) ((a, b), ba)
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((a, b), ba))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((aa, bb), bc))
 4. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 5. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 6. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (5 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((a, b), ba))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((aa, bb), bc))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 4. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (5 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba); \<not> big_step_R s1 s'; \<not> big_step_R s1 ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((a, b), ba))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((aa, bb), bc))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 4. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 5. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (4 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> \<not> interrupted_modes (snd ((aa, bb), bc))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 3. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 4. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((a, b), ba)) = irq_masks_of_state (internal_state_if ((aa, bb), bc))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (3 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc); invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if ((aa, bb), bc)) = irq_masks_of_state (internal_state_if ((a, b), ba))
 2. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 3. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as aa bb bc. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) (); big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2); invs_if s'; (((a, b), ba), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (((a, b), ba), (aa, bb), bc) \<in> Step (ADT_A_if utf) (); \<not> big_step_R s1 ((aa, bb), bc)\<rbrakk> \<Longrightarrow> invs_if ((a, b), ba)
 2. \<lbrakk>invs_if s1; (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1; (s', s2) \<in> Step (ADT_A_if utf) a; big_step_R\<^sup>*\<^sup>* s0 s1; snd s1 = KernelExit; interrupted_modes (snd s2)\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal:
No subgoals!