[STATEMENT]
lemma interaction_any_bounded_converter_parallel_converter' [interaction_bound]:
  assumes "interaction_any_bounded_converter conv1 n"
    and "interaction_any_bounded_converter conv2 m"
  shows "interaction_any_bounded_converter (parallel_converter conv1 conv2) (max n m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interaction_any_bounded_converter (parallel_converter conv1 conv2) (max n m)
[PROOF STEP]
by(rule interaction_any_bounded_converter_parallel_converter; rule assms[THEN interaction_any_bounded_converter_mono]; simp)