[STATEMENT]
lemma current_independent_of_domain_actions:
assumes current_s_t: "mcurrents s t"
  shows "mcurrents (run n s execs) (run n t execs2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
fix n s execs t execs2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
have "mcurrents s t \<longrightarrow> mcurrents (run n s execs) (run n t execs2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents s t \<longrightarrow> mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
proof (induct n s execs arbitrary: t execs2 rule: run.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s execs t execs2. mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)
 2. \<And>n execs t execs2. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
 3. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 5. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 6. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (1 s execs t execs2)
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. \<And>s execs t execs2. mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)
 2. \<And>n execs t execs2. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
 3. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 5. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 6. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)
[PROOF STEP]
using current_s_t
[PROOF STATE]
proof (prove)
using this:
mcurrents s t

goal (1 subgoal):
 1. mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
mcurrents s t

goal (1 subgoal):
 1. mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents s t \<longrightarrow> mcurrents (run 0 s execs) (run 0 t execs2)

goal (5 subgoals):
 1. \<And>n execs t execs2. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
 2. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 5. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n execs t execs2. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
 2. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 5. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (2 n execs t execs2)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>n execs t execs2. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
 2. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 5. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B2 None t (\<lambda>s t. current s = current t) \<longrightarrow> B2 (run (Suc n) None execs) (run (Suc n) t execs2) (\<lambda>s t. current s = current t)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
mcurrents None t \<longrightarrow> mcurrents (run (Suc n) None execs) (run (Suc n) t execs2)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (3 n s execs t execs2)
[PROOF STATE]
proof (state)
this:
interrupt (Suc n)
mcurrents (Some (cswitch (Suc n) s)) ?t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n ?t ?execs2.0)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume interrupt: "interrupt (Suc n)"
[PROOF STATE]
proof (state)
this:
interrupt (Suc n)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume IH: "(\<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2))"
[PROOF STATE]
proof (state)
this:
mcurrents (Some (cswitch (Suc n) s)) ?t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n ?t ?execs2.0)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mcurrents (Some (cswitch (Suc n) s)) ?t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n ?t ?execs2.0)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
fix t'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume t: "t = (Some t')"
[PROOF STATE]
proof (state)
this:
t = Some t'

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume curr: "mcurrents (Some s) t"
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t curr cswitch_independent_of_state[THEN spec,THEN spec,THEN spec,where x1=s]
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
mcurrents (Some s) t
current s = current ?x \<longrightarrow> current (cswitch ?x2 s) = current (cswitch ?x2 ?x)
[PROOF STEP]
have current_ns_nt: "current (cswitch (Suc n) s) = current (cswitch (Suc n) t')"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
mcurrents (Some s) t
current s = current ?x \<longrightarrow> current (cswitch ?x2 s) = current (cswitch ?x2 ?x)

goal (1 subgoal):
 1. current (cswitch (Suc n) s) = current (cswitch (Suc n) t')
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
t = Some t'
B2 (Some s) t (\<lambda>s t. current s = current t)
current s = current ?x \<longrightarrow> current (cswitch ?x2 s) = current (cswitch ?x2 ?x)

goal (1 subgoal):
 1. current (cswitch (Suc n) s) = current (cswitch (Suc n) t')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
current (cswitch (Suc n) s) = current (cswitch (Suc n) t')

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from current_ns_nt IH[where t="Some (cswitch (Suc n) t')" and ?execs2.0=execs2]
[PROOF STATE]
proof (chain)
picking this:
current (cswitch (Suc n) s) = current (cswitch (Suc n) t')
mcurrents (Some (cswitch (Suc n) s)) (Some (cswitch (Suc n) t')) \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)
[PROOF STEP]
have mcurrents_ns_nt: "mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)"
[PROOF STATE]
proof (prove)
using this:
current (cswitch (Suc n) s) = current (cswitch (Suc n) t')
mcurrents (Some (cswitch (Suc n) s)) (Some (cswitch (Suc n) t')) \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)

goal (1 subgoal):
 1. mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
current (cswitch (Suc n) s) = current (cswitch (Suc n) t')
B2 (Some (cswitch (Suc n) s)) (Some (cswitch (Suc n) t')) (\<lambda>s t. current s = current t) \<longrightarrow> B2 (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2) (\<lambda>s t. current s = current t)

goal (1 subgoal):
 1. B2 (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2) (\<lambda>s t. current s = current t)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from mcurrents_ns_nt interrupt t
[PROOF STATE]
proof (chain)
picking this:
mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)
interrupt (Suc n)
t = Some t'
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n (Some (cswitch (Suc n) t')) execs2)
interrupt (Suc n)
t = Some t'

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def B2_def B_def
[PROOF STATE]
proof (prove)
using this:
case run n (Some (cswitch (Suc n) s)) execs of None \<Rightarrow> True | Some a \<Rightarrow> case run n (Some (cswitch (Suc n) t')) execs2 of None \<Rightarrow> True | Some aa \<Rightarrow> current a = current aa
interrupt (Suc n)
t = Some t'

goal (1 subgoal):
 1. case run (Suc n) (Some s) execs of None \<Rightarrow> True | Some a \<Rightarrow> case run (Suc n) t execs2 of None \<Rightarrow> True | Some aa \<Rightarrow> current a = current aa
[PROOF STEP]
by(cases "run n (Some (cswitch (Suc n) s)) execs", cases "run (Suc n) t execs2",auto)
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (4 subgoals):
 1. \<And>n s execs t execs2. \<lbrakk>interrupt (Suc n); \<And>t execs2. mcurrents (Some (cswitch (Suc n) s)) t \<longrightarrow> mcurrents (run n (Some (cswitch (Suc n) s)) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 4. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def B2_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b))\<rbrakk> \<Longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))

goal (1 subgoal):
 1. Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b)) \<longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))
[PROOF STEP]
by(cases t,auto)
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (4 n execs s t execs2)
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)
thread_empty (execs (current s))
mcurrents (Some s) ?t \<longrightarrow> mcurrents (run n (Some s) execs) (run n ?t ?execs2.0)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_interrupt: "\<not>interrupt (Suc n)"
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume thread_empty_s: "thread_empty(execs (current s))"
[PROOF STATE]
proof (state)
this:
thread_empty (execs (current s))

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume IH: "(\<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2))"
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) ?t \<longrightarrow> mcurrents (run n (Some s) execs) (run n ?t ?execs2.0)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) ?t \<longrightarrow> mcurrents (run n (Some s) execs) (run n ?t ?execs2.0)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
fix t'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume t: "t = (Some t')"
[PROOF STATE]
proof (state)
this:
t = Some t'

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume curr: "mcurrents (Some s) t"
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume thread_empty_t: "thread_empty(execs2 (current t'))"
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t'))

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t curr not_interrupt thread_empty_s this IH[where ?execs2.0=execs2 and t="Some t'"]
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
mcurrents (Some s) t
\<not> interrupt (Suc n)
thread_empty (execs (current s))
thread_empty (execs2 (current t'))
mcurrents (Some s) (Some t') \<longrightarrow> mcurrents (run n (Some s) execs) (run n (Some t') execs2)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
mcurrents (Some s) t
\<not> interrupt (Suc n)
thread_empty (execs (current s))
thread_empty (execs2 (current t'))
mcurrents (Some s) (Some t') \<longrightarrow> mcurrents (run n (Some s) execs) (run n (Some t') execs2)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_prec_t: "\<not>thread_empty(execs2 (current t')) \<and> \<not>precondition (next_state t' execs2) (next_action t' execs2)"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t this not_interrupt
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)

goal (1 subgoal):
 1. B2 (run (Suc n) (Some s) execs) (run (Suc n) t execs2) (\<lambda>s t. current s = current t)
[PROOF STEP]
by (simp add: rewrite_B2_cases)
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume step_t: "\<not>thread_empty(execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
have "mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
using step_atomicity curr t current_next_state
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
mcurrents (Some s) t
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some s) (Some (step (next_state t' execs2) (next_action t' execs2))) (\<lambda>s t. current s = current t)
[PROOF STEP]
unfolding step_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some s) (Some (case next_action t' execs2 of None \<Rightarrow> next_state t' execs2 | Some a \<Rightarrow> kstep (next_state t' execs2) a)) (\<lambda>s t. current s = current t)
[PROOF STEP]
by (cases "next_action t' execs2",auto)
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t step_t curr not_interrupt thread_empty_s this IH[where ?execs2.0="next_execs t' execs2" and t="Some (step (next_state t' execs2) (next_action t' execs2))"]
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)
mcurrents (Some s) t
\<not> interrupt (Suc n)
thread_empty (execs (current s))
mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))
mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2))) \<longrightarrow> mcurrents (run n (Some s) execs) (run n (Some (step (next_state t' execs2) (next_action t' execs2))) (next_execs t' execs2))
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)
mcurrents (Some s) t
\<not> interrupt (Suc n)
thread_empty (execs (current s))
mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2)))
mcurrents (Some s) (Some (step (next_state t' execs2) (next_action t' execs2))) \<longrightarrow> mcurrents (run n (Some s) execs) (run n (Some (step (next_state t' execs2) (next_action t' execs2))) (next_execs t' execs2))

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (3 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); thread_empty (execs (current s)); \<And>t execs2. mcurrents (Some s) t \<longrightarrow> mcurrents (run n (Some s) execs) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 3. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def B2_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b))\<rbrakk> \<Longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))

goal (1 subgoal):
 1. Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b)) \<longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))
[PROOF STEP]
by(cases t,auto)
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (5 n execs s t execs2)
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
\<not> precondition (next_state s execs) (next_action s execs)

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_interrupt_s: "\<not>interrupt (Suc n)"
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume thread_not_empty_s: "\<not>thread_empty(execs (current s))"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs (current s))

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_prec_s: "\<not> precondition (next_state s execs) (next_action s execs)"
[PROOF STATE]
proof (state)
this:
\<not> precondition (next_state s execs) (next_action s execs)

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
hence "run (Suc n) (Some s) execs = None"
[PROOF STATE]
proof (prove)
using this:
\<not> precondition (next_state s execs) (next_action s execs)

goal (1 subgoal):
 1. run (Suc n) (Some s) execs = None
[PROOF STEP]
using not_interrupt_s thread_not_empty_s
[PROOF STATE]
proof (prove)
using this:
\<not> precondition (next_state s execs) (next_action s execs)
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))

goal (1 subgoal):
 1. run (Suc n) (Some s) execs = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
run (Suc n) (Some s) execs = None

goal (2 subgoals):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); \<not> precondition (next_state s execs) (next_action s execs)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
 2. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
run (Suc n) (Some s) execs = None

goal (1 subgoal):
 1. mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
run (Suc n) (Some s) execs = None

goal (1 subgoal):
 1. B2 (Some s) t (\<lambda>s t. current s = current t) \<longrightarrow> B2 (run (Suc n) (Some s) execs) (run (Suc n) t execs2) (\<lambda>s t. current s = current t)
[PROOF STEP]
by(simp add:option.splits)
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
case (6 n execs s t execs2)
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
precondition (next_state s execs) (next_action s execs)
mcurrents (Some (step (next_state s execs) (next_action s execs))) ?t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n ?t ?execs2.0)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_interrupt: "\<not>interrupt (Suc n)"
[PROOF STATE]
proof (state)
this:
\<not> interrupt (Suc n)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume thread_not_empty_s: "\<not>thread_empty(execs (current s))"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs (current s))

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume prec_s: "precondition (next_state s execs) (next_action s execs)"
[PROOF STATE]
proof (state)
this:
precondition (next_state s execs) (next_action s execs)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume IH: "(\<And>t execs2.
           mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow>
           mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2))"
[PROOF STATE]
proof (state)
this:
mcurrents (Some (step (next_state s execs) (next_action s execs))) ?t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n ?t ?execs2.0)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mcurrents (Some (step (next_state s execs) (next_action s execs))) ?t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n ?t ?execs2.0)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
fix t'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume t: "t = (Some t')"
[PROOF STATE]
proof (state)
this:
t = Some t'

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume curr: "mcurrents (Some s) t"
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume thread_empty_t: "thread_empty(execs2 (current t'))"
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t'))

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
have "mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')
[PROOF STEP]
using step_atomicity curr t current_next_state
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
mcurrents (Some s) t
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some (step (next_state s execs) (next_action s execs))) (Some t') (\<lambda>s t. current s = current t)
[PROOF STEP]
unfolding step_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some (case next_action s execs of None \<Rightarrow> next_state s execs | Some a \<Rightarrow> kstep (next_state s execs) a)) (Some t') (\<lambda>s t. current s = current t)
[PROOF STEP]
by (cases "next_action s execs",auto)
[PROOF STATE]
proof (state)
this:
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t curr not_interrupt thread_not_empty_s prec_s thread_empty_t this IH[where ?execs2.0=execs2 and t="Some t'"]
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
mcurrents (Some s) t
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
precondition (next_state s execs) (next_action s execs)
thread_empty (execs2 (current t'))
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t') \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n (Some t') execs2)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
mcurrents (Some s) t
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
precondition (next_state s execs) (next_action s execs)
thread_empty (execs2 (current t'))
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t')
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some t') \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n (Some t') execs2)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume not_prec_t: "\<not>thread_empty(execs2 (current t')) \<and> \<not>precondition (next_state t' execs2) (next_action t' execs2)"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from t this not_interrupt
[PROOF STATE]
proof (chain)
picking this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def B2_def
[PROOF STATE]
proof (prove)
using this:
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2)
\<not> interrupt (Suc n)

goal (1 subgoal):
 1. run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
assume step_t: "\<not>thread_empty(execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)"
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
have "mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
using step_atomicity curr t current_next_state
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
mcurrents (Some s) t
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))
[PROOF STEP]
unfolding mcurrents_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2))) (\<lambda>s t. current s = current t)
[PROOF STEP]
unfolding step_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s a. current (kstep s a) = current s
B2 (Some s) t (\<lambda>s t. current s = current t)
t = Some t'
\<forall>s execs. current (next_state s execs) = current s

goal (1 subgoal):
 1. B2 (Some (case next_action s execs of None \<Rightarrow> next_state s execs | Some a \<Rightarrow> kstep (next_state s execs) a)) (Some (case next_action t' execs2 of None \<Rightarrow> next_state t' execs2 | Some a \<Rightarrow> kstep (next_state t' execs2) a)) (\<lambda>s t. current s = current t)
[PROOF STEP]
by (cases "next_action s execs",simp,cases "next_action t' execs2",simp,simp,cases "next_action t' execs2",simp,simp)
[PROOF STATE]
proof (state)
this:
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
from current_next_state t step_t curr not_interrupt thread_not_empty_s prec_s this IH[where ?execs2.0="next_execs t' execs2" and t="Some (step (next_state t' execs2) (next_action t' execs2))"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>s execs. current (next_state s execs) = current s
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)
mcurrents (Some s) t
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
precondition (next_state s execs) (next_action s execs)
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2))) \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n (Some (step (next_state t' execs2) (next_action t' execs2))) (next_execs t' execs2))
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>s execs. current (next_state s execs) = current s
t = Some t'
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2)
mcurrents (Some s) t
\<not> interrupt (Suc n)
\<not> thread_empty (execs (current s))
precondition (next_state s execs) (next_action s execs)
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2)))
mcurrents (Some (step (next_state s execs) (next_action s execs))) (Some (step (next_state t' execs2) (next_action t' execs2))) \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n (Some (step (next_state t' execs2) (next_action t' execs2))) (next_execs t' execs2))

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
have "mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)"
[PROOF STATE]
proof (prove)
using this:
thread_empty (execs2 (current t')) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> \<not> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
\<not> thread_empty (execs2 (current t')) \<and> precondition (next_state t' execs2) (next_action t' execs2) \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. \<And>n execs s t execs2. \<lbrakk>\<not> interrupt (Suc n); \<not> thread_empty (execs (current s)); precondition (next_state s execs) (next_action s execs); \<And>t execs2. mcurrents (Some (step (next_state s execs) (next_action s execs))) t \<longrightarrow> mcurrents (run n (Some (step (next_state s execs) (next_action s execs))) (next_execs s execs)) (run n t execs2)\<rbrakk> \<Longrightarrow> mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; mcurrents (Some s) t\<rbrakk> \<Longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal (1 subgoal):
 1. mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)
[PROOF STEP]
unfolding mcurrents_def B2_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = Some ?t'2; Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b))\<rbrakk> \<Longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))

goal (1 subgoal):
 1. Some s \<rightharpoonup> (\<lambda>a. t \<rightharpoonup> (\<lambda>b. current a = current b)) \<longrightarrow> run (Suc n) (Some s) execs \<rightharpoonup> (\<lambda>a. run (Suc n) t execs2 \<rightharpoonup> (\<lambda>b. current a = current b))
[PROOF STEP]
by(cases t,auto)
[PROOF STATE]
proof (state)
this:
mcurrents (Some s) t \<longrightarrow> mcurrents (run (Suc n) (Some s) execs) (run (Suc n) t execs2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mcurrents s t \<longrightarrow> mcurrents (run n s execs) (run n t execs2)

goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
mcurrents ?sa2 ?ta2 \<longrightarrow> mcurrents (run ?na2 ?sa2 ?execsa2) (run ?na2 ?ta2 ?execs2a2)

goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mcurrents ?sa2 ?ta2 \<longrightarrow> mcurrents (run ?na2 ?sa2 ?execsa2) (run ?na2 ?ta2 ?execs2a2)

goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
using current_s_t
[PROOF STATE]
proof (prove)
using this:
mcurrents ?sa2 ?ta2 \<longrightarrow> mcurrents (run ?na2 ?sa2 ?execsa2) (run ?na2 ?ta2 ?execs2a2)
mcurrents s t

goal (1 subgoal):
 1. mcurrents (run n s execs) (run n t execs2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mcurrents (run n s execs) (run n t execs2)

goal:
No subgoals!
[PROOF STEP]
qed