[STATEMENT]
lemma dterms_ctermsl [intro]:
  assumes "q \<in> dterms \<Gamma> p"
      and "wellformed \<Gamma>"
    shows "q \<in> ctermsl p \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> ctermsl p \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
using assms(1-2)
[PROOF STATE]
proof (prove)
using this:
q \<in> dterms \<Gamma> p
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> ctermsl p \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
proof (induction p rule: dterms_pinduct [OF \<open>wellformed \<Gamma>\<close>])
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>\<Gamma> l g p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<langle>g\<rangle>
p); q \<in> dterms \<Gamma> ({l}\<langle>g\<rangle>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<langle>g\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> p1 p2. \<lbrakk>dterms_dom (\<Gamma>, p1
\<oplus>
p2); \<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); \<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (p1
\<oplus>
p2); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (p1
\<oplus>
p2) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 9. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 10. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
fix \<Gamma> l fg p
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>\<Gamma> l g p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<langle>g\<rangle>
p); q \<in> dterms \<Gamma> ({l}\<langle>g\<rangle>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<langle>g\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> p1 p2. \<lbrakk>dterms_dom (\<Gamma>, p1
\<oplus>
p2); \<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); \<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (p1
\<oplus>
p2); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (p1
\<oplus>
p2) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 9. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 10. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
assume "q \<in> dterms \<Gamma> ({l}\<langle>fg\<rangle> p)"
       and "wellformed \<Gamma>"
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> ({l}\<langle>fg\<rangle>
p)
wellformed \<Gamma>

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

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

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

goal (1 subgoal):
 1. q \<in> stermsl p \<or> (\<exists>pn. q \<in> stermsl (\<Gamma> pn))
[PROOF STEP]
using \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> sterms \<Gamma> p
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> stermsl p \<or> (\<exists>pn. q \<in> stermsl (\<Gamma> pn))
[PROOF STEP]
by (rule sterms_stermsl)
[PROOF STATE]
proof (state)
this:
q \<in> stermsl p \<or> (\<exists>pn. q \<in> stermsl (\<Gamma> pn))

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

goal (1 subgoal):
 1. q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> stermsl p \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
assume "q \<in> stermsl p"
[PROOF STATE]
proof (state)
this:
q \<in> stermsl p

goal (2 subgoals):
 1. q \<in> stermsl p \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
hence "q \<in> ctermsl p"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl p

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

goal (2 subgoals):
 1. q \<in> stermsl p \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
hence "q \<in> ctermsl ({l}\<langle>fg\<rangle> p)"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl p

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

goal (2 subgoals):
 1. q \<in> stermsl p \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl ({l}\<langle>fg\<rangle>
p)

goal (1 subgoal):
 1. q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))

goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
assume "\<exists>pn. q \<in> stermsl (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
\<exists>pn. q \<in> stermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>pn. q \<in> stermsl (\<Gamma> pn)
[PROOF STEP]
obtain pn where "q \<in> stermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
\<exists>pn. q \<in> stermsl (\<Gamma> pn)

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

goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
hence "q \<in> ctermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (\<Gamma> pn)

goal (1 subgoal):
 1. q \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
by (rule stermsl_ctermsl)
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
hence "\<exists>pn. q \<in> ctermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
q \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<exists>pn. q \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>pn. q \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<exists>pn. q \<in> stermsl (\<Gamma> pn) \<Longrightarrow> q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>pn. q \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
q \<in> ctermsl ({l}\<langle>fg\<rangle>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))

goal (9 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> p1 p2. \<lbrakk>dterms_dom (\<Gamma>, p1
\<oplus>
p2); \<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); \<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (p1
\<oplus>
p2); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (p1
\<oplus>
p2) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 9. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> p1 p2. \<lbrakk>dterms_dom (\<Gamma>, p1
\<oplus>
p2); \<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); \<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (p1
\<oplus>
p2); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (p1
\<oplus>
p2) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 9. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
fix \<Gamma> p1 p2
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> p1 p2. \<lbrakk>dterms_dom (\<Gamma>, p1
\<oplus>
p2); \<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); \<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (p1
\<oplus>
p2); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (p1
\<oplus>
p2) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 9. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
assume "q \<in> dterms \<Gamma> (p1 \<oplus> p2)"
       and IH1: "\<lbrakk> q \<in> dterms \<Gamma> p1; wellformed \<Gamma> \<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))"
       and IH2: "\<lbrakk> q \<in> dterms \<Gamma> p2; wellformed \<Gamma> \<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))"
       and "wellformed \<Gamma>"
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> (p1
\<oplus>
p2)
\<lbrakk>q \<in> dterms \<Gamma> p1; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p1 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
\<lbrakk>q \<in> dterms \<Gamma> p2; wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl p2 \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
wellformed \<Gamma>

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

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

goal (8 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
fix \<Gamma> pn
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 8. \<And>\<Gamma> pn. \<lbrakk>dterms_dom (\<Gamma>, call(pn)); \<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn)); q \<in> dterms \<Gamma> (call(pn)); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (call(pn)) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
assume "q \<in> dterms \<Gamma> (call(pn))"
       and "wellformed \<Gamma>"
       and "\<lbrakk> q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma> \<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))"
[PROOF STATE]
proof (state)
this:
q \<in> dterms \<Gamma> (call(pn))
wellformed \<Gamma>
\<lbrakk>q \<in> dterms \<Gamma> (\<Gamma> pn); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl (\<Gamma> pn) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))

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

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

goal (7 subgoals):
 1. \<And>\<Gamma> l u p. \<lbrakk>dterms_dom (\<Gamma>, {l}\<lbrakk>u\<rbrakk>
p); q \<in> dterms \<Gamma> ({l}\<lbrakk>u\<rbrakk>
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}\<lbrakk>u\<rbrakk>
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 2. \<And>\<Gamma> l s\<^sub>i\<^sub>p s\<^sub>m\<^sub>s\<^sub>g p qa. \<lbrakk>dterms_dom (\<Gamma>, {l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); q \<in> dterms \<Gamma> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> qa) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 3. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 4. \<And>\<Gamma> l s\<^sub>i\<^sub>p\<^sub>s s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 5. \<And>\<Gamma> l s\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 6. \<And>\<Gamma> l s\<^sub>d\<^sub>a\<^sub>t\<^sub>a p. \<lbrakk>dterms_dom (\<Gamma>, {l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); q \<in> dterms \<Gamma> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
 7. \<And>\<Gamma> l u\<^sub>m\<^sub>s\<^sub>g p. \<lbrakk>dterms_dom (\<Gamma>, {l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); q \<in> dterms \<Gamma> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p); wellformed \<Gamma>\<rbrakk> \<Longrightarrow> q \<in> ctermsl ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<or> (\<exists>pn. q \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
qed (simp_all, (metis sterms_stermsl stermsl_ctermsl)+)


[STATEMENT]
lemma ctermsl_cterms [elim]:
  assumes "q \<in> ctermsl p"
      and "not_call q"
      and "sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
      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:
q \<in> ctermsl p
not_call q
sterms \<Gamma> p \<subseteq> cterms \<Gamma>
wellformed \<Gamma>

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


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


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


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


[STATEMENT]
lemma dtermsl_choice_disj [simp]:
  "p \<in> dtermsl (p1 \<oplus> p2) = (p \<in> dtermsl p1 \<or> p \<in> dtermsl p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> dtermsl (p1
\<oplus>
p2)) = (p \<in> dtermsl p1 \<or> p \<in> dtermsl p2)
[PROOF STEP]
by simp


[STATEMENT]
lemma dtermsl_in_branch [elim]:
  "\<lbrakk>p \<in> dtermsl (p1 \<oplus> p2); p \<in> dtermsl p1 \<Longrightarrow> P; p \<in> dtermsl p2 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> dtermsl (p1
\<oplus>
p2); p \<in> dtermsl p1 \<Longrightarrow> P; p \<in> dtermsl p2 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by auto


[STATEMENT]
lemma ctermsl_dtermsl [elim]:
  assumes "q \<in> dtermsl 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> dtermsl p

goal (1 subgoal):
 1. q \<in> ctermsl p
[PROOF STEP]
by (induct p) (simp_all, (metis stermsl_ctermsl)+)


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

goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> dtermsl p
not_call q
wellformed \<Gamma>
q \<in> dtermsl p
not_call q
wellformed \<Gamma>

goal (1 subgoal):
 1. q \<in> dterms \<Gamma> p
[PROOF STEP]
by (induct p) (simp_all, (metis stermsl_sterms)+)


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

goal (1 subgoal):
 1. q \<in> stermsl p \<or> (\<exists>p'\<in>dtermsl p. q \<in> ctermsl p')
[PROOF STEP]
by (induct p) (auto dest: ctermsl_ex_stermsl)


[STATEMENT]
lemma dtermsl_add_stermsl_beforeD:
  assumes "q \<in> dtermsl p"
    shows "\<exists>ps\<in>stermsl p. q \<in> dtermsl ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ps\<in>stermsl p. q \<in> dtermsl ps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ps\<in>stermsl p. q \<in> dtermsl ps
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
q \<in> dtermsl p
[PROOF STEP]
have "q \<in> (\<Union>x\<in>stermsl p. dtermsl x)"
[PROOF STATE]
proof (prove)
using this:
q \<in> dtermsl p

goal (1 subgoal):
 1. q \<in> \<Union> (dtermsl ` stermsl p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> \<Union> (dtermsl ` stermsl p)

goal (1 subgoal):
 1. \<exists>ps\<in>stermsl p. q \<in> dtermsl ps
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> \<Union> (dtermsl ` stermsl p)

goal (1 subgoal):
 1. \<exists>ps\<in>stermsl p. q \<in> dtermsl ps
[PROOF STEP]
by (rule UN_E) auto
[PROOF STATE]
proof (state)
this:
\<exists>ps\<in>stermsl p. q \<in> dtermsl ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma call_dtermsl_empty [elim]:
 "q \<in> dtermsl p \<Longrightarrow> not_call p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> dtermsl p \<Longrightarrow> not_call p
[PROOF STEP]
by (cases p) simp_all


[STATEMENT]
theorem cterms_def':
  assumes wfg: "wellformed \<Gamma>"
    shows "cterms \<Gamma> = { p |p pn. p \<in> ctermsl (\<Gamma> pn) \<and> not_call p }"
          (is "_ = ?ctermsl_set")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cterms \<Gamma> = {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
proof (rule iffI [THEN set_eqI])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> cterms \<Gamma> \<Longrightarrow> x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> cterms \<Gamma> \<Longrightarrow> x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
assume "p \<in> cterms \<Gamma>"
[PROOF STATE]
proof (state)
this:
p \<in> cterms \<Gamma>

goal (2 subgoals):
 1. \<And>x. x \<in> cterms \<Gamma> \<Longrightarrow> x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
thus "p \<in> ?ctermsl_set"
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
fix p pn
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
assume "p \<in> sterms \<Gamma> (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
p \<in> sterms \<Gamma> (\<Gamma> pn)

goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> sterms \<Gamma> (\<Gamma> pn)
[PROOF STEP]
obtain pn' where "p \<in> stermsl (\<Gamma> pn')"
[PROOF STATE]
proof (prove)
using this:
p \<in> sterms \<Gamma> (\<Gamma> pn)

goal (1 subgoal):
 1. (\<And>pn'. p \<in> stermsl (\<Gamma> pn') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfg
[PROOF STATE]
proof (prove)
using this:
p \<in> sterms \<Gamma> (\<Gamma> pn)
wellformed \<Gamma>

goal (1 subgoal):
 1. (\<And>pn'. p \<in> stermsl (\<Gamma> pn') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: sterms_stermsl_heads)
[PROOF STATE]
proof (state)
this:
p \<in> stermsl (\<Gamma> pn')

goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
hence "p \<in> ctermsl (\<Gamma> pn')"
[PROOF STATE]
proof (prove)
using this:
p \<in> stermsl (\<Gamma> pn')

goal (1 subgoal):
 1. p \<in> ctermsl (\<Gamma> pn')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl (\<Gamma> pn')

goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl (\<Gamma> pn')

goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
from \<open>p \<in> sterms \<Gamma> (\<Gamma> pn)\<close> wfg
[PROOF STATE]
proof (chain)
picking this:
p \<in> sterms \<Gamma> (\<Gamma> pn)
wellformed \<Gamma>
[PROOF STEP]
have "not_call p"
[PROOF STATE]
proof (prove)
using this:
p \<in> sterms \<Gamma> (\<Gamma> pn)
wellformed \<Gamma>

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

goal (2 subgoals):
 1. \<And>p pn. p \<in> sterms \<Gamma> (\<Gamma> pn) \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
 2. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<in> ctermsl (\<Gamma> pn')
not_call p
[PROOF STEP]
show "p \<in> ?ctermsl_set"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl (\<Gamma> pn')
not_call p

goal (1 subgoal):
 1. p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
fix pp p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
assume "pp \<in> cterms \<Gamma>"
         and IH: "pp \<in> ?ctermsl_set"
         and *: "p \<in> dterms \<Gamma> pp"
[PROOF STATE]
proof (state)
this:
pp \<in> cterms \<Gamma>
pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
p \<in> dterms \<Gamma> pp

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
p \<in> dterms \<Gamma> pp
[PROOF STEP]
have "p \<in> ctermsl pp \<or> (\<exists>pn. p \<in> ctermsl (\<Gamma> pn))"
[PROOF STATE]
proof (prove)
using this:
p \<in> dterms \<Gamma> pp

goal (1 subgoal):
 1. p \<in> ctermsl pp \<or> (\<exists>pn. p \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
using wfg
[PROOF STATE]
proof (prove)
using this:
p \<in> dterms \<Gamma> pp
wellformed \<Gamma>

goal (1 subgoal):
 1. p \<in> ctermsl pp \<or> (\<exists>pn. p \<in> ctermsl (\<Gamma> pn))
[PROOF STEP]
by (rule dterms_ctermsl)
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl pp \<or> (\<exists>pn. p \<in> ctermsl (\<Gamma> pn))

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
hence "\<exists>pn. p \<in> ctermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl pp \<or> (\<exists>pn. p \<in> ctermsl (\<Gamma> pn))

goal (1 subgoal):
 1. \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> ctermsl pp \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
 2. \<exists>pn. p \<in> ctermsl (\<Gamma> pn) \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
assume "p \<in> ctermsl pp"
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl pp

goal (2 subgoals):
 1. p \<in> ctermsl pp \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
 2. \<exists>pn. p \<in> ctermsl (\<Gamma> pn) \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
from \<open>pp \<in> cterms \<Gamma>\<close> and IH
[PROOF STATE]
proof (chain)
picking this:
pp \<in> cterms \<Gamma>
pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
obtain pn' where "pp \<in> ctermsl (\<Gamma> pn')"
[PROOF STATE]
proof (prove)
using this:
pp \<in> cterms \<Gamma>
pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. (\<And>pn'. pp \<in> ctermsl (\<Gamma> pn') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pp \<in> ctermsl (\<Gamma> pn')

goal (2 subgoals):
 1. p \<in> ctermsl pp \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
 2. \<exists>pn. p \<in> ctermsl (\<Gamma> pn) \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
with \<open>p \<in> ctermsl pp\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> ctermsl pp
pp \<in> ctermsl (\<Gamma> pn')
[PROOF STEP]
have "p \<in> ctermsl (\<Gamma> pn')"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl pp
pp \<in> ctermsl (\<Gamma> pn')

goal (1 subgoal):
 1. p \<in> ctermsl (\<Gamma> pn')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl (\<Gamma> pn')

goal (2 subgoals):
 1. p \<in> ctermsl pp \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
 2. \<exists>pn. p \<in> ctermsl (\<Gamma> pn) \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
thus "\<exists>pn. p \<in> ctermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl (\<Gamma> pn')

goal (1 subgoal):
 1. \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>pn. p \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<exists>pn. p \<in> ctermsl (\<Gamma> pn) \<Longrightarrow> \<exists>pn. p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
qed -
[PROOF STATE]
proof (state)
this:
\<exists>pn. p \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>pn. p \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
from \<open>p \<in> dterms \<Gamma> pp\<close> wfg
[PROOF STATE]
proof (chain)
picking this:
p \<in> dterms \<Gamma> pp
wellformed \<Gamma>
[PROOF STEP]
have "not_call p"
[PROOF STATE]
proof (prove)
using this:
p \<in> dterms \<Gamma> pp
wellformed \<Gamma>

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

goal (1 subgoal):
 1. \<And>pp p. \<lbrakk>pp \<in> cterms \<Gamma>; pp \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}; p \<in> dterms \<Gamma> pp\<rbrakk> \<Longrightarrow> p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>pn. p \<in> ctermsl (\<Gamma> pn)
not_call p
[PROOF STEP]
show "p \<in> ?ctermsl_set"
[PROOF STATE]
proof (prove)
using this:
\<exists>pn. p \<in> ctermsl (\<Gamma> pn)
not_call p

goal (1 subgoal):
 1. p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
assume "p \<in> ?ctermsl_set"
[PROOF STATE]
proof (state)
this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}
[PROOF STEP]
obtain pn where *: "p \<in> ctermsl (\<Gamma> pn)" and "not_call p"
[PROOF STATE]
proof (prove)
using this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. (\<And>pn. \<lbrakk>p \<in> ctermsl (\<Gamma> pn); not_call p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> ctermsl (\<Gamma> pn)
not_call p

goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
p \<in> ctermsl (\<Gamma> pn)
[PROOF STEP]
have "p \<in> stermsl (\<Gamma> pn) \<or> (\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p')"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl (\<Gamma> pn)

goal (1 subgoal):
 1. p \<in> stermsl (\<Gamma> pn) \<or> (\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p')
[PROOF STEP]
by (rule ctermsl_stermsl_or_dtermsl)
[PROOF STATE]
proof (state)
this:
p \<in> stermsl (\<Gamma> pn) \<or> (\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p')

goal (1 subgoal):
 1. \<And>x. x \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p} \<Longrightarrow> x \<in> cterms \<Gamma>
[PROOF STEP]
thus "p \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p \<in> stermsl (\<Gamma> pn) \<or> (\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p')

goal (1 subgoal):
 1. p \<in> cterms \<Gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> stermsl (\<Gamma> pn) \<Longrightarrow> p \<in> cterms \<Gamma>
 2. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
assume "p \<in> stermsl (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
p \<in> stermsl (\<Gamma> pn)

goal (2 subgoals):
 1. p \<in> stermsl (\<Gamma> pn) \<Longrightarrow> p \<in> cterms \<Gamma>
 2. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
hence "p \<in> sterms \<Gamma> (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p \<in> stermsl (\<Gamma> pn)

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

goal (1 subgoal):
 1. p \<in> sterms \<Gamma> (\<Gamma> pn)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> sterms \<Gamma> (\<Gamma> pn)

goal (2 subgoals):
 1. p \<in> stermsl (\<Gamma> pn) \<Longrightarrow> p \<in> cterms \<Gamma>
 2. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
thus "p \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p \<in> sterms \<Gamma> (\<Gamma> pn)

goal (1 subgoal):
 1. p \<in> cterms \<Gamma>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
assume "\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p'"
[PROOF STATE]
proof (state)
this:
\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p'

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p'
[PROOF STEP]
obtain p' where p'1: "p' \<in> dtermsl (\<Gamma> pn)"
                       and p'2: "p \<in> ctermsl p'"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p'

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' \<in> dtermsl (\<Gamma> pn); p \<in> ctermsl p'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p' \<in> dtermsl (\<Gamma> pn)
p \<in> ctermsl p'

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
from p'2 and \<open>not_call p\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> ctermsl p'
not_call p
[PROOF STEP]
have "not_call p'"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl p'
not_call p

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

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
from p'1
[PROOF STATE]
proof (chain)
picking this:
p' \<in> dtermsl (\<Gamma> pn)
[PROOF STEP]
obtain ps where ps1: "ps \<in> stermsl (\<Gamma> pn)"
                           and ps2: "p' \<in> dtermsl ps"
[PROOF STATE]
proof (prove)
using this:
p' \<in> dtermsl (\<Gamma> pn)

goal (1 subgoal):
 1. (\<And>ps. \<lbrakk>ps \<in> stermsl (\<Gamma> pn); p' \<in> dtermsl ps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: dtermsl_add_stermsl_beforeD)
[PROOF STATE]
proof (state)
this:
ps \<in> stermsl (\<Gamma> pn)
p' \<in> dtermsl ps

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
from ps2
[PROOF STATE]
proof (chain)
picking this:
p' \<in> dtermsl ps
[PROOF STEP]
have "not_call ps"
[PROOF STATE]
proof (prove)
using this:
p' \<in> dtermsl ps

goal (1 subgoal):
 1. not_call ps
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
not_call ps

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
with ps1
[PROOF STATE]
proof (chain)
picking this:
ps \<in> stermsl (\<Gamma> pn)
not_call ps
[PROOF STEP]
have "ps \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
ps \<in> stermsl (\<Gamma> pn)
not_call ps

goal (1 subgoal):
 1. ps \<in> cterms \<Gamma>
[PROOF STEP]
using wfg
[PROOF STATE]
proof (prove)
using this:
ps \<in> stermsl (\<Gamma> pn)
not_call ps
wellformed \<Gamma>

goal (1 subgoal):
 1. ps \<in> cterms \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps \<in> cterms \<Gamma>

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
with \<open>p' \<in> dtermsl ps\<close> and \<open>not_call p'\<close>
[PROOF STATE]
proof (chain)
picking this:
p' \<in> dtermsl ps
not_call p'
ps \<in> cterms \<Gamma>
[PROOF STEP]
have "p' \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p' \<in> dtermsl ps
not_call p'
ps \<in> cterms \<Gamma>

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

goal (1 subgoal):
 1. p' \<in> cterms \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p' \<in> cterms \<Gamma>

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
hence "sterms \<Gamma> p' \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p' \<in> cterms \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> p' \<subseteq> cterms \<Gamma>
[PROOF STEP]
using wfg
[PROOF STATE]
proof (prove)
using this:
p' \<in> cterms \<Gamma>
wellformed \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> p' \<subseteq> cterms \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p' \<subseteq> cterms \<Gamma>

goal (1 subgoal):
 1. \<exists>p'\<in>dtermsl (\<Gamma> pn). p \<in> ctermsl p' \<Longrightarrow> p \<in> cterms \<Gamma>
[PROOF STEP]
with \<open>p \<in> ctermsl p'\<close> \<open>not_call p\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> ctermsl p'
not_call p
sterms \<Gamma> p' \<subseteq> cterms \<Gamma>
[PROOF STEP]
show "p \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl p'
not_call p
sterms \<Gamma> p' \<subseteq> cterms \<Gamma>

goal (1 subgoal):
 1. p \<in> cterms \<Gamma>
[PROOF STEP]
using wfg
[PROOF STATE]
proof (prove)
using this:
p \<in> ctermsl p'
not_call p
sterms \<Gamma> p' \<subseteq> cterms \<Gamma>
wellformed \<Gamma>

goal (1 subgoal):
 1. p \<in> cterms \<Gamma>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> cterms \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> cterms \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ctermsE [elim]:
  assumes "wellformed \<Gamma>"
      and "p \<in> cterms \<Gamma>"
  obtains pn where "p \<in> ctermsl (\<Gamma> pn)"
               and "not_call p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pn. \<lbrakk>p \<in> ctermsl (\<Gamma> pn); not_call p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
p \<in> cterms \<Gamma>

goal (1 subgoal):
 1. (\<And>pn. \<lbrakk>p \<in> ctermsl (\<Gamma> pn); not_call p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cterms_def' [OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> ctermsl (\<Gamma> pn) \<and> not_call p}

goal (1 subgoal):
 1. (\<And>pn. \<lbrakk>p \<in> ctermsl (\<Gamma> pn); not_call p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


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

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

goal (1 subgoal):
 1. p \<in> {uu_. \<exists>p pn. uu_ = p \<and> p \<in> subterms (\<Gamma> pn) \<and> not_call p \<and> not_choice p}
[PROOF STEP]
by auto