[STATEMENT]
lemma SAStates_notmem_Chi [simp]:
  "\<lbrakk> S \<in> States SA; T \<in> States SA;
     SA \<in> SAs A \<rbrakk> \<Longrightarrow> T \<notin> Chi A S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A\<rbrakk> \<Longrightarrow> T \<notin> Chi A S
[PROOF STEP]
apply (unfold Chi_def restrict_def, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAa. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAa \<in> the (CompFun A S); T \<in> States SAa\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac SAA)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac HA="A" in MutuallyDistinct_HA)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; MutuallyDistinct (SAs A)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold MutuallyDistinct_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; \<forall>a\<in>SAs A. \<forall>b\<in>SAs A. a \<noteq> b \<longrightarrow> States a \<inter> States b = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x="SAA" in ballE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; \<forall>b\<in>SAs A. SAA \<noteq> b \<longrightarrow> States SAA \<inter> States b = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x="SA" in ballE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<noteq> SA \<longrightarrow> States SAA \<inter> States SA = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 3. \<And>SAA. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<in> HAStates A; SAA \<in> the (CompFun A S); T \<in> States SAA; SAA \<notin> SAs A\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> HAStates A; T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold HAStates_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<in> States SA; T \<in> States SA; SA \<in> SAs A; S \<notin> \<Union> (States ` SAs A); T \<in> (SOME y. True)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done