[STATEMENT]
lemma parp_sos_cases [elim]:
  assumes "((s, t), a, (s', t')) \<in> parp_sos S T"
      and "\<lbrakk> (s, a, s') \<in> S; \<And>m. a \<noteq> receive m; t' = t \<rbrakk> \<Longrightarrow> P"
      and "\<lbrakk> (t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s \<rbrakk> \<Longrightarrow> P"
      and "\<And>m. \<lbrakk> (s, receive m, s') \<in> S; (t, send m, t') \<in> T \<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((s, t), a, s', t') \<in> parp_sos S T
\<lbrakk>(s, a, s') \<in> S; \<And>m. a \<noteq> receive m; t' = t\<rbrakk> \<Longrightarrow> P
\<lbrakk>(t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s\<rbrakk> \<Longrightarrow> P
\<lbrakk>(s, receive ?m, s') \<in> S; (t, send ?m, t') \<in> T\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by cases auto