[STATEMENT]
lemma trace_callee_conv_trace_callee_aux:
  "trace_callee callee p xs a = bind_spmf (trace_callee_aux callee p xs) (\<lambda>s. map_spmf fst (callee s a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_callee callee p xs a = trace_callee_aux callee p xs \<bind> (\<lambda>s. map_spmf fst (callee s a))
[PROOF STEP]
by(induction xs arbitrary: p)(auto simp add: split_def)