[STATEMENT]
lemma non_interference_induct_case_sub2: 
assumes a1: 
"(user_seq_exe n s1 \<and>
          user_seq_exe n s2 \<longrightarrow>
          (\<exists>t1. Some t1 = SEQ n s1 \<and>
               (\<exists>t2. Some t2 = SEQ n s2 \<and>
                     (((get_S (cpu_reg_val PSR t1)))::word1) = 0 \<and>
    (((get_S (cpu_reg_val PSR t2)))::word1) = 0 \<and> low_equal t1 t2))) \<and>
user_seq_exe (Suc n) s1 \<and>
         user_seq_exe (Suc n) s2"
shows "\<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and>
              (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and>
                    (((get_S (cpu_reg_val PSR t1)))::word1) = 0 \<and>
    (((get_S (cpu_reg_val PSR t2)))::word1) = 0 \<and> low_equal t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2)
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
(user_seq_exe n s1 \<and> user_seq_exe n s2 \<longrightarrow> (\<exists>t1. Some t1 = SEQ n s1 \<and> (\<exists>t2. Some t2 = SEQ n s2 \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2))) \<and> user_seq_exe (Suc n) s1 \<and> user_seq_exe (Suc n) s2

goal (1 subgoal):
 1. \<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2)
[PROOF STEP]
by (simp add: non_interference_induct_case user_seq_exe_def)