[STATEMENT]
lemma next_execs_subset:
shows "\<forall>s execs u . actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
fix s execs u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
have "actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
unfolding Kernel.next_execs_def actions_in_execution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. \<exists>aseq\<in>set ((execs(current s := fst (snd (CISK_control s (current s) (execs (current s)))))) u). a \<in> set aseq} \<subseteq> {a. \<exists>aseq\<in>set (execs u). a \<in> set aseq}
[PROOF STEP]
by (cases "(s,(current s),execs (current s))" rule: CISK_control.cases,auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
actions_in_execution (next_execs ?s2 ?execs2 ?u2) \<subseteq> actions_in_execution (?execs2 ?u2)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
actions_in_execution (next_execs ?s2 ?execs2 ?u2) \<subseteq> actions_in_execution (?execs2 ?u2)

goal (1 subgoal):
 1. \<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s execs u. actions_in_execution (next_execs s execs u) \<subseteq> actions_in_execution (execs u)

goal:
No subgoals!
[PROOF STEP]
qed