[STATEMENT]
lemma exec_1I: "execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> Predicate.eval (exec_1 P t \<sigma>) (ta, \<sigma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> pred.eval (exec_1 P t \<sigma>) (ta, \<sigma>')
[PROOF STEP]
by(erule execute.exec_1.cases)(simp add: exec_1_def exec_def)