[STATEMENT]
lemma succs_iexec1:
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
  shows "fst c' \<in> succs P 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst c' \<in> succs P 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c' = iexec (P !! i) (i, s, stk)
0 \<le> i
i < size P

goal (1 subgoal):
 1. fst c' \<in> succs P 0
[PROOF STEP]
by (auto simp: succs_def isuccs_def split: instr.split)