[STATEMENT]
lemma TSnopaid: "(snd (fst (snd (rTS initH) is q))) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (snd (rTS initH) is q)) = []
[PROOF STEP]
unfolding rTS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (snd (\<lambda>s. initH, TS_step_d) is q)) = []
[PROOF STEP]
by(simp add: TS_step_d_def)