[STATEMENT]
lemma state_rank_in_function_set:
  shows "(\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and>
      (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
assume "x \<notin> reach \<Sigma> \<delta> q\<^sub>0"
[PROOF STATE]
proof (state)
this:
x \<notin> reach \<Sigma> \<delta> q\<^sub>0

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
hence "\<And>token. x \<noteq> token_run token t"
[PROOF STATE]
proof (prove)
using this:
x \<notin> reach \<Sigma> \<delta> q\<^sub>0

goal (1 subgoal):
 1. \<And>token. x \<noteq> token_run token t
[PROOF STEP]
unfolding reach_def token_run.simps
[PROOF STATE]
proof (prove)
using this:
x \<notin> {run \<delta> q\<^sub>0 w n |w n. range w \<subseteq> \<Sigma>}

goal (1 subgoal):
 1. \<And>token. x \<noteq> run \<delta> q\<^sub>0 (suffix token w) (t - token)
[PROOF STEP]
using bounded_w
[PROOF STATE]
proof (prove)
using this:
x \<notin> {run \<delta> q\<^sub>0 w n |w n. range w \<subseteq> \<Sigma>}
range w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. \<And>token. x \<noteq> run \<delta> q\<^sub>0 (suffix token w) (t - token)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<noteq> token_run ?token t

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
hence "state_rank x t = None"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> token_run ?token t

goal (1 subgoal):
 1. state_rank x t = None
[PROOF STEP]
using pull_up_configuration_state_rank
[PROOF STATE]
proof (prove)
using this:
x \<noteq> token_run ?token t
configuration ?q ?n = {} \<Longrightarrow> state_rank ?q ?n = None

goal (1 subgoal):
 1. state_rank x t = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
state_rank x t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
with state_rank_range
[PROOF STATE]
proof (chain)
picking this:
state_rank ?q ?n \<in> {None} \<union> Some ` {0..<max_rank}
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_rank ?q ?n \<in> {None} \<union> Some ` {0..<max_rank}
?x2 \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<Longrightarrow> state_rank ?x2 t = None

goal (1 subgoal):
 1. (\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>q. state_rank q t) \<in> {f. (\<forall>x. x \<notin> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x = None) \<and> (\<forall>x. x \<in> reach \<Sigma> \<delta> q\<^sub>0 \<longrightarrow> f x \<in> {None} \<union> Some ` {0..<max_rank})}

goal:
No subgoals!
[PROOF STEP]
qed