[STATEMENT]
lemma [intro]:
  "composable_tm (tm_copy_begin_orig, 0)"
  "composable_tm (tm_copy_loop_orig, 0)"
  "composable_tm (tm_copy_end_new, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composable_tm0 tm_copy_begin_orig &&& composable_tm0 tm_copy_loop_orig &&& composable_tm0 tm_copy_end_new
[PROOF STEP]
by (auto simp: composable_tm.simps tm_copy_end_new_def tm_copy_loop_orig_def tm_copy_begin_orig_def)