[STATEMENT]
lemma dterms_subterms:
  assumes wf: "wellformed \<Gamma>"
      and "\<exists>pn. p \<in> subterms (\<Gamma> pn)"
      and "q \<in> dterms \<Gamma> p"
    shows "\<exists>pn. q \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
\<exists>pn. p \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> p

goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
proof (induct p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
assume IH1: "\<exists>pn. p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> q \<in> dterms \<Gamma> p1 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)"
       and IH2: "\<exists>pn. p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)"
       and *: "\<exists>pn. p1 \<oplus> p2 \<in> subterms (\<Gamma> pn)"
       and "q \<in> dterms \<Gamma> (p1 \<oplus> p2)"
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
\<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
\<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> (p1
\<oplus>
p2)

goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
\<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
obtain pn where "p1 \<oplus> p2 \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
\<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. (\<And>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
hence "p1 \<in> subterms (\<Gamma> pn)" and "p2 \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. p1 \<in> subterms (\<Gamma> pn) &&& p2 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1 \<in> subterms (\<Gamma> pn)
p2 \<in> subterms (\<Gamma> pn)

goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
from \<open>q \<in> dterms \<Gamma> (p1 \<oplus> p2)\<close> wf
[PROOF STATE]
proof (chain)
picking this:
q \<in> dterms \<Gamma> (p1
\<oplus>
p2)
wellformed \<Gamma>
[PROOF STEP]
have "q \<in> dterms \<Gamma> p1 \<or> q \<in> dterms \<Gamma> p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> dterms \<Gamma> (p1
\<oplus>
p2)
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p1 \<or> q \<in> dterms \<Gamma> p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> p1 \<or> q \<in> dterms \<Gamma> p2

goal (10 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pn. p1 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p1\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<lbrakk>\<exists>pn. p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> p2\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pn. p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> (p1
\<oplus>
p2)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
thus "\<exists>pn. q \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
q \<in> dterms \<Gamma> p1 \<or> q \<in> dterms \<Gamma> p2

goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> dterms \<Gamma> p1 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
assume "q \<in> dterms \<Gamma> p1"
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> p1

goal (2 subgoals):
 1. q \<in> dterms \<Gamma> p1 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
with \<open>p1 \<in> subterms (\<Gamma> pn)\<close>
[PROOF STATE]
proof (chain)
picking this:
p1 \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> p1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p1 \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> p1

goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by (auto intro: IH1)
[PROOF STATE]
proof (state)
this:
\<exists>pn. q \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
assume "q \<in> dterms \<Gamma> p2"
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> p2

goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p2 \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
with \<open>p2 \<in> subterms (\<Gamma> pn)\<close>
[PROOF STATE]
proof (chain)
picking this:
p2 \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p2 \<in> subterms (\<Gamma> pn)
q \<in> dterms \<Gamma> p2

goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by (auto intro: IH2)
[PROOF STATE]
proof (state)
this:
\<exists>pn. q \<in> subterms (\<Gamma> pn)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pn. q \<in> subterms (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<lbrakk>f\<rbrakk>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 2. \<And>l f p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}\<langle>f\<rangle>
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}\<langle>f\<rangle>
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 3. \<And>l fip fmsg p qa. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}unicast(fip, fmsg) .
p \<triangleright> qa \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> qa)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 4. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}broadcast(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}broadcast(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 5. \<And>l fips fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}groupcast(fips, fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 6. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}send(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}send(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 7. \<And>l fdata p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}deliver(fdata) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}deliver(fdata) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 8. \<And>l fmsg p. \<lbrakk>wellformed \<Gamma>; \<exists>pn. {l}receive(fmsg) .
p \<in> subterms (\<Gamma> pn); q \<in> dterms \<Gamma> ({l}receive(fmsg) .
p)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; \<lbrakk>\<exists>pna. \<Gamma> pn \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn); \<exists>pna. call(pn) \<in> subterms (\<Gamma> pna); q \<in> dterms \<Gamma> (call(pn))\<rbrakk> \<Longrightarrow> \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
qed auto


[STATEMENT]
lemma cterms_not_choice [simp]:
  assumes "wellformed \<Gamma>"
      and "p \<in> cterms \<Gamma>"
    shows "not_choice p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_choice p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. not_choice p
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_choice p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_choice p
 3. \<And>x31 x32. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> not_choice p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_choice p
 5. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_choice p
 6. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_choice p
 7. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_choice p
 8. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_choice p
 9. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_choice p
 10. \<And>x10. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = call(x10)\<rbrakk> \<Longrightarrow> not_choice p
[PROOF STEP]
case CHOICE
[PROOF STATE]
proof (state)
this:
p = x31_
\<oplus>
x32_

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_choice p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_choice p
 3. \<And>x31 x32. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> not_choice p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_choice p
 5. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_choice p
 6. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_choice p
 7. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_choice p
 8. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_choice p
 9. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_choice p
 10. \<And>x10. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = call(x10)\<rbrakk> \<Longrightarrow> not_choice p
[PROOF STEP]
from \<open>p \<in> cterms \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> cterms \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. not_choice p
[PROOF STEP]
using \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>
wellformed \<Gamma>

goal (1 subgoal):
 1. not_choice p
[PROOF STEP]
by cases simp_all
[PROOF STATE]
proof (state)
this:
not_choice p

goal (9 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_choice p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_choice p
 3. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_choice p
 4. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_choice p
 5. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_choice p
 6. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_choice p
 7. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_choice p
 8. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_choice p
 9. \<And>x10. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = call(x10)\<rbrakk> \<Longrightarrow> not_choice p
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma cterms_no_choice [simp]:
  assumes "wellformed \<Gamma>"
    shows "p1 \<oplus> p2 \<notin> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1
\<oplus>
p2 \<notin> cterms \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. p1
\<oplus>
p2 \<notin> cterms \<Gamma>
[PROOF STEP]
by (auto dest: cterms_not_choice)


[STATEMENT]
lemma cterms_not_call [simp]:
  assumes "wellformed \<Gamma>"
      and "p \<in> cterms \<Gamma>"
    shows "not_call p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_call p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. not_call p
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_call p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_call p
 3. \<And>x31 x32. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> not_call p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_call p
 5. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_call p
 6. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_call p
 7. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_call p
 8. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_call p
 9. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_call p
 10. \<And>x10. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = call(x10)\<rbrakk> \<Longrightarrow> not_call p
[PROOF STEP]
case CALL
[PROOF STATE]
proof (state)
this:
p = call(x10_)

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_call p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_call p
 3. \<And>x31 x32. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> not_call p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_call p
 5. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_call p
 6. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_call p
 7. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_call p
 8. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_call p
 9. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_call p
 10. \<And>x10. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = call(x10)\<rbrakk> \<Longrightarrow> not_call p
[PROOF STEP]
from \<open>p \<in> cterms \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> cterms \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. not_call p
[PROOF STEP]
using \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>
wellformed \<Gamma>

goal (1 subgoal):
 1. not_call p
[PROOF STEP]
by cases simp_all
[PROOF STATE]
proof (state)
this:
not_call p

goal (9 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> not_call p
 2. \<And>x21 x22 x23. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> not_call p
 3. \<And>x31 x32. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> not_call p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> not_call p
 5. \<And>x51 x52 x53. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> not_call p
 6. \<And>x61 x62 x63 x64. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> not_call p
 7. \<And>x71 x72 x73. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> not_call p
 8. \<And>x81 x82 x83. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> not_call p
 9. \<And>x91 x92 x93. \<lbrakk>wellformed \<Gamma>; p \<in> cterms \<Gamma>; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> not_call p
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma cterms_no_call [simp]:
  assumes "wellformed \<Gamma>"
    shows "call(pn) \<notin> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. call(pn) \<notin> cterms \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. call(pn) \<notin> cterms \<Gamma>
[PROOF STEP]
by (auto dest: cterms_not_call)


[STATEMENT]
lemma sterms_cterms [elim]:
  assumes "p \<in> cterms \<Gamma>"
      and "q \<in> sterms \<Gamma> p"
      and "wellformed \<Gamma>"
    shows "q \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>
q \<in> sterms \<Gamma> p
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
by - (cases p, auto)


[STATEMENT]
lemma dterms_cterms [elim]:
  assumes "p \<in> cterms \<Gamma>"
      and "q \<in> dterms \<Gamma> p"
      and "wellformed \<Gamma>"
    shows "q \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>
q \<in> dterms \<Gamma> p
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma derivs_in_cterms [simp]:
  "\<And>l f p. {l}\<langle>f\<rangle> p \<in> cterms \<Gamma>                            \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l f p. {l}\<lbrakk>f\<rbrakk> p \<in> cterms \<Gamma>                           \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l fip fmsg q p. {l}unicast(fip, fmsg). p \<triangleright> q \<in> cterms \<Gamma>
                            \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma> \<and> sterms \<Gamma> q \<subseteq> cterms \<Gamma>"
  "\<And>l fmsg p.      {l}broadcast(fmsg).p \<in> cterms \<Gamma>       \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l fips fmsg p. {l}groupcast(fips, fmsg).p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l fmsg p.      {l}send(fmsg).p \<in> cterms \<Gamma>            \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l fdata p.     {l}deliver(fdata).p \<in> cterms \<Gamma>        \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
  "\<And>l fmsg p.      {l}receive(fmsg).p \<in> cterms \<Gamma>         \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>l f p. {l}\<langle>f\<rangle>
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>) &&& (\<And>l f p. {l}\<lbrakk>f\<rbrakk>
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>)) &&& (\<And>l fip fmsg q p. {l}unicast(fip, fmsg) .
p \<triangleright> q \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma> \<and> sterms \<Gamma> q \<subseteq> cterms \<Gamma>) &&& (\<And>l fmsg p. {l}broadcast(fmsg) .
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>)) &&& ((\<And>l fips fmsg p. {l}groupcast(fips, fmsg) .
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>) &&& (\<And>l fmsg p. {l}send(fmsg) .
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>)) &&& (\<And>l fdata p. {l}deliver(fdata) .
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>) &&& (\<And>l fmsg p. {l}receive(fmsg) .
p \<in> cterms \<Gamma> \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>)
[PROOF STEP]
by (auto simp: dterms.psimps)


[STATEMENT]
lemma ctermsl_refl [intro]: "not_choice p \<Longrightarrow> p \<in> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_choice p \<Longrightarrow> p \<in> ctermsl p
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma ctermsl_subterms:
  "ctermsl p = {q. q \<in> subterms p \<and> not_choice q }" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ctermsl p = {q \<in> subterms p. not_choice q}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ctermsl p \<subseteq> {q \<in> subterms p. not_choice q}
 2. {q \<in> subterms p. not_choice q} \<subseteq> ctermsl p
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ctermsl p \<subseteq> {q \<in> subterms p. not_choice q}
[PROOF STEP]
by (induct p, auto)
[PROOF STATE]
proof (state)
this:
ctermsl p \<subseteq> {q \<in> subterms p. not_choice q}

goal (1 subgoal):
 1. {q \<in> subterms p. not_choice q} \<subseteq> ctermsl p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {q \<in> subterms p. not_choice q} \<subseteq> ctermsl p
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> subterms p. not_choice q} \<subseteq> ctermsl p
[PROOF STEP]
by (induct p, auto)
[PROOF STATE]
proof (state)
this:
{q \<in> subterms p. not_choice q} \<subseteq> ctermsl p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ctermsl_trans [elim]:
  assumes "q \<in> ctermsl p"
      and "r \<in> ctermsl q"
    shows "r \<in> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p
r \<in> ctermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
proof (induction p rule: ctermsl_induct)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>l g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<langle>g\<rangle>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<langle>g\<rangle>
p)
 2. \<And>l u p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p)
 3. \<And>l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; \<lbrakk>q \<in> ctermsl qa; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl qa; q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa)
 4. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 5. \<And>l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p)
 6. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 7. \<And>l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p)
 8. \<And>l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p)
 9. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> ctermsl p1; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> ctermsl p2; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> ctermsl (p1
\<oplus>
p2); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 10. \<And>pn. \<lbrakk>q \<in> ctermsl (call(pn)); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(pn))
[PROOF STEP]
case (CHOICE p1 p2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>q \<in> ctermsl p1; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1
\<lbrakk>q \<in> ctermsl p2; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2
q \<in> ctermsl (p1
\<oplus>
p2)
r \<in> ctermsl q

goal (10 subgoals):
 1. \<And>l g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<langle>g\<rangle>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<langle>g\<rangle>
p)
 2. \<And>l u p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p)
 3. \<And>l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; \<lbrakk>q \<in> ctermsl qa; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl qa; q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa)
 4. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 5. \<And>l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p)
 6. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 7. \<And>l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p)
 8. \<And>l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p)
 9. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> ctermsl p1; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> ctermsl p2; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> ctermsl (p1
\<oplus>
p2); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 10. \<And>pn. \<lbrakk>q \<in> ctermsl (call(pn)); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(pn))
[PROOF STEP]
have "(q \<in> ctermsl p1) \<or> (q \<in> ctermsl p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl p1 \<or> q \<in> ctermsl p2
[PROOF STEP]
using CHOICE.prems(1)
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl (p1
\<oplus>
p2)

goal (1 subgoal):
 1. q \<in> ctermsl p1 \<or> q \<in> ctermsl p2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl p1 \<or> q \<in> ctermsl p2

goal (10 subgoals):
 1. \<And>l g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<langle>g\<rangle>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<langle>g\<rangle>
p)
 2. \<And>l u p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p)
 3. \<And>l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; \<lbrakk>q \<in> ctermsl qa; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl qa; q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa)
 4. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 5. \<And>l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p)
 6. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 7. \<And>l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p)
 8. \<And>l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p)
 9. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> ctermsl p1; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> ctermsl p2; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> ctermsl (p1
\<oplus>
p2); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 10. \<And>pn. \<lbrakk>q \<in> ctermsl (call(pn)); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(pn))
[PROOF STEP]
hence "r \<in> ctermsl p1 \<or> r \<in> ctermsl p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p1 \<or> q \<in> ctermsl p2

goal (1 subgoal):
 1. r \<in> ctermsl p1 \<or> r \<in> ctermsl p2
[PROOF STEP]
proof (rule disj_forward)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> ctermsl p1 \<Longrightarrow> r \<in> ctermsl p1
 2. q \<in> ctermsl p2 \<Longrightarrow> r \<in> ctermsl p2
[PROOF STEP]
assume "q \<in> ctermsl p1"
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl p1

goal (2 subgoals):
 1. q \<in> ctermsl p1 \<Longrightarrow> r \<in> ctermsl p1
 2. q \<in> ctermsl p2 \<Longrightarrow> r \<in> ctermsl p2
[PROOF STEP]
thus "r \<in> ctermsl p1"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p1

goal (1 subgoal):
 1. r \<in> ctermsl p1
[PROOF STEP]
using \<open>r \<in> ctermsl q\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p1
r \<in> ctermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p1
[PROOF STEP]
by (rule CHOICE.IH)
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl p1

goal (1 subgoal):
 1. q \<in> ctermsl p2 \<Longrightarrow> r \<in> ctermsl p2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> ctermsl p2 \<Longrightarrow> r \<in> ctermsl p2
[PROOF STEP]
assume "q \<in> ctermsl p2"
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl p2

goal (1 subgoal):
 1. q \<in> ctermsl p2 \<Longrightarrow> r \<in> ctermsl p2
[PROOF STEP]
thus "r \<in> ctermsl p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p2

goal (1 subgoal):
 1. r \<in> ctermsl p2
[PROOF STEP]
using \<open>r \<in> ctermsl q\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p2
r \<in> ctermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p2
[PROOF STEP]
by (rule CHOICE.IH)
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl p2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl p1 \<or> r \<in> ctermsl p2

goal (10 subgoals):
 1. \<And>l g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<langle>g\<rangle>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<langle>g\<rangle>
p)
 2. \<And>l u p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p)
 3. \<And>l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; \<lbrakk>q \<in> ctermsl qa; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl qa; q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa)
 4. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 5. \<And>l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p)
 6. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 7. \<And>l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p)
 8. \<And>l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p)
 9. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> ctermsl p1; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> ctermsl p2; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> ctermsl (p1
\<oplus>
p2); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 10. \<And>pn. \<lbrakk>q \<in> ctermsl (call(pn)); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(pn))
[PROOF STEP]
thus "r \<in> ctermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
using this:
r \<in> ctermsl p1 \<or> r \<in> ctermsl p2

goal (1 subgoal):
 1. r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl (p1
\<oplus>
p2)

goal (9 subgoals):
 1. \<And>l g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<langle>g\<rangle>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<langle>g\<rangle>
p)
 2. \<And>l u p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p)
 3. \<And>l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; \<lbrakk>q \<in> ctermsl qa; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl qa; q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa)
 4. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 5. \<And>l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p)
 6. \<And>l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p)
 7. \<And>l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p)
 8. \<And>l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>\<lbrakk>q \<in> ctermsl p; r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p)
 9. \<And>pn. \<lbrakk>q \<in> ctermsl (call(pn)); r \<in> ctermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(pn))
[PROOF STEP]
qed auto


[STATEMENT]
lemma ctermsl_ex_trans [elim]:
  assumes "\<exists>q \<in> ctermsl p. r \<in> ctermsl q"
    shows "r \<in> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>q\<in>ctermsl p. r \<in> ctermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
by auto


[STATEMENT]
lemma call_ctermsl_empty [elim]:
  "\<lbrakk> p \<in> ctermsl p'; not_call p \<rbrakk> \<Longrightarrow> not_call p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> ctermsl p'; not_call p\<rbrakk> \<Longrightarrow> not_call p'
[PROOF STEP]
unfolding not_call_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> ctermsl p'; \<forall>pn. p \<noteq> call(pn)\<rbrakk> \<Longrightarrow> \<forall>pn. p' \<noteq> call(pn)
[PROOF STEP]
by (cases p) auto


[STATEMENT]
lemma stermsl_ctermsl_choice1 [simp]:
  assumes "q \<in> stermsl p1"
    shows "q \<in> ctermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl p1

goal (1 subgoal):
 1. q \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by (induction p1) auto


[STATEMENT]
lemma stermsl_ctermsl_choice2 [simp]:
  assumes "q \<in> stermsl p2"
    shows "q \<in> ctermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl p2

goal (1 subgoal):
 1. q \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by (induction p2) auto


[STATEMENT]
lemma stermsl_ctermsl [elim]:
  assumes "q \<in> stermsl p"
    shows "q \<in> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl p

goal (1 subgoal):
 1. q \<in> ctermsl p
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x31 x32. \<lbrakk>q \<in> stermsl p; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 10. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
case (CHOICE p1 p2)
[PROOF STATE]
proof (state)
this:
p = p1
\<oplus>
p2

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x31 x32. \<lbrakk>q \<in> stermsl p; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 10. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
hence "q \<in> stermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
using this:
p = p1
\<oplus>
p2

goal (1 subgoal):
 1. q \<in> stermsl (p1
\<oplus>
p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p = p1
\<oplus>
p2
q \<in> stermsl p

goal (1 subgoal):
 1. q \<in> stermsl (p1
\<oplus>
p2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> stermsl (p1
\<oplus>
p2)

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x31 x32. \<lbrakk>q \<in> stermsl p; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 10. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
hence "q \<in> stermsl p1 \<or> q \<in> stermsl p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (p1
\<oplus>
p2)

goal (1 subgoal):
 1. q \<in> stermsl p1 \<or> q \<in> stermsl p2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> stermsl p1 \<or> q \<in> stermsl p2

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x31 x32. \<lbrakk>q \<in> stermsl p; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 10. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
hence "q \<in> ctermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl p1 \<or> q \<in> stermsl p2

goal (1 subgoal):
 1. q \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by (rule) (simp_all del: ctermsl.simps)
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl (p1
\<oplus>
p2)

goal (10 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x31 x32. \<lbrakk>q \<in> stermsl p; p = x31
\<oplus>
x32\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 10. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
thus  "q \<in> ctermsl p"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl (p1
\<oplus>
p2)

goal (1 subgoal):
 1. q \<in> ctermsl p
[PROOF STEP]
using CHOICE
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl (p1
\<oplus>
p2)
p = p1
\<oplus>
p2

goal (1 subgoal):
 1. q \<in> ctermsl p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl p

goal (9 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>q \<in> stermsl p; p = {x11}\<langle>x12\<rangle>
x13\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 2. \<And>x21 x22 x23. \<lbrakk>q \<in> stermsl p; p = {x21}\<lbrakk>x22\<rbrakk>
x23\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 3. \<And>x41 x42 x43 x44 x45. \<lbrakk>q \<in> stermsl p; p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 4. \<And>x51 x52 x53. \<lbrakk>q \<in> stermsl p; p = {x51}broadcast(x52) .
x53\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 5. \<And>x61 x62 x63 x64. \<lbrakk>q \<in> stermsl p; p = {x61}groupcast(x62, x63) .
x64\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 6. \<And>x71 x72 x73. \<lbrakk>q \<in> stermsl p; p = {x71}send(x72) .
x73\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 7. \<And>x81 x82 x83. \<lbrakk>q \<in> stermsl p; p = {x81}deliver(x82) .
x83\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 8. \<And>x91 x92 x93. \<lbrakk>q \<in> stermsl p; p = {x91}receive(x92) .
x93\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
 9. \<And>x10. \<lbrakk>q \<in> stermsl p; p = call(x10)\<rbrakk> \<Longrightarrow> q \<in> ctermsl p
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma stermsl_after_ctermsl [simp]:
  "(\<Union>x\<in>ctermsl p. stermsl x) = ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (stermsl ` ctermsl p) = ctermsl p
[PROOF STEP]
by (induct p) auto


[STATEMENT]
lemma stermsl_before_ctermsl [simp]:
  "(\<Union>x\<in>stermsl p. ctermsl x) = ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (ctermsl ` stermsl p) = ctermsl p
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
lemma ctermsl_no_choice: "p1 \<oplus> p2 \<notin> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1
\<oplus>
p2 \<notin> ctermsl p
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
lemma ctermsl_ex_stermsl: "q \<in> ctermsl p \<Longrightarrow> \<exists>ps\<in>stermsl p. q \<in> ctermsl ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl p \<Longrightarrow> \<exists>ps\<in>stermsl p. q \<in> ctermsl ps
[PROOF STEP]
by (induct p) auto