[STATEMENT]
lemma index_states_integer_observable :
  assumes "observable M"
  shows "observable (index_states_integer M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (index_states_integer M)
[PROOF STEP]
using rename_states_observable[of "integer_of_nat \<circ> assign_indices (states M)" M, OF assign_indices_integer_bij_betw assms]
[PROOF STATE]
proof (prove)
using this:
observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))

goal (1 subgoal):
 1. observable (index_states_integer M)
[PROOF STEP]
unfolding index_states_integer.simps
[PROOF STATE]
proof (prove)
using this:
observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))

goal (1 subgoal):
 1. observable (FSM.rename_states M (integer_of_nat \<circ> assign_indices (FSM.states M)))
[PROOF STEP]
.