[STATEMENT]
lemma \<oo>_Shuffle[simp]:
  "\<oo> (Shuffle r s) = (\<oo> r \<and> \<oo> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Shuffle r s) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
unfolding Shuffle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times_Plus (ShuffleLR r s)) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
by simp