[STATEMENT]
theorem sterms_maximal_microstep:
  assumes "wellformed \<Gamma>"
    shows "sterms \<Gamma> p = {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> \<not>(\<exists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> p = {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}
 2. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
from \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
[PROOF STEP]
have "sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

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

goal (10 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}; sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
have "sterms \<Gamma> p1 \<subseteq> {q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
assume "p' \<in> sterms \<Gamma> p1"
[PROOF STATE]
proof (state)
this:
p' \<in> sterms \<Gamma> p1

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with IH1
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> p1
[PROOF STEP]
have "p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> p1

goal (1 subgoal):
 1. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
have "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1
[PROOF STEP]
have "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'"
[PROOF STATE]
proof (prove)
using this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1

goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
by - (rule converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
from \<open>wellformed \<Gamma>\<close> and \<open>p' \<in> sterms \<Gamma> p1\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
p' \<in> sterms \<Gamma> p1
[PROOF STEP]
have "sterms \<Gamma> p' = {p'}"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p' \<in> sterms \<Gamma> p1

goal (1 subgoal):
 1. sterms \<Gamma> p' = {p'}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p' = {p'}

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p1 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}
[PROOF STEP]
show "p' \<in> {q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
using this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}

goal (1 subgoal):
 1. p' \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p' \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (10 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}; sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (10 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}; sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
have "sterms \<Gamma> p2 \<subseteq> {q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> p2 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
assume "p' \<in> sterms \<Gamma> p2"
[PROOF STATE]
proof (state)
this:
p' \<in> sterms \<Gamma> p2

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with IH2
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> p2
[PROOF STEP]
have "p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'" and "sterms \<Gamma> p' = {p'}"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> p2

goal (1 subgoal):
 1. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p' &&& sterms \<Gamma> p' = {p'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
have "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2
[PROOF STEP]
have "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'"
[PROOF STATE]
proof (prove)
using this:
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2

goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
by - (rule converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> p2 \<Longrightarrow> x \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with \<open>sterms \<Gamma> p' = {p'}\<close>
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p' = {p'}
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
show "p' \<in> {q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p' = {p'}
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. p' \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p' \<in> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p2 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (10 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> p1 \<subseteq> {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}; sterms \<Gamma> p2 \<subseteq> {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
sterms \<Gamma> p2 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
show "sterms \<Gamma> (p1 \<oplus> p2) \<subseteq> {q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
sterms \<Gamma> p2 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (1 subgoal):
 1. sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
using \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p1 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
sterms \<Gamma> p2 \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
wellformed \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
fix pn
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
assume IH: "sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}\<rbrakk> \<Longrightarrow> sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
show "sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
assume "p' \<in> sterms \<Gamma> (call(pn))"
[PROOF STATE]
proof (state)
this:
p' \<in> sterms \<Gamma> (call(pn))

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
p' \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
have "p' \<in> sterms \<Gamma> (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p' \<in> sterms \<Gamma> (call(pn))

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

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> (\<Gamma> pn)
[PROOF STEP]
have "\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'" and "sterms \<Gamma> p' = {p'}"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> (\<Gamma> pn) \<subseteq> {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
p' \<in> sterms \<Gamma> (\<Gamma> pn)

goal (1 subgoal):
 1. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p' &&& sterms \<Gamma> p' = {p'}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
sterms \<Gamma> p' = {p'}

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
note this(1)
[PROOF STATE]
proof (state)
this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
have "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn
[PROOF STEP]
have "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn

goal (1 subgoal):
 1. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
by - (rule converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. \<And>x. x \<in> sterms \<Gamma> (call(pn)) \<Longrightarrow> x \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
with \<open>sterms \<Gamma> p' = {p'}\<close>
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p' = {p'}
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'
[PROOF STEP]
show "p' \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p' = {p'}
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'

goal (1 subgoal):
 1. p' \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p' \<in> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (call(pn)) \<subseteq> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (8 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p) \<subseteq> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}\<langle>f\<rangle>
p) \<subseteq> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<subseteq> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}}
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}broadcast(fmsg) .
p) \<subseteq> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p) \<subseteq> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}send(fmsg) .
p) \<subseteq> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}deliver(fdata) .
p) \<subseteq> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> sterms \<Gamma> ({l}receive(fmsg) .
p) \<subseteq> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (2 subgoals):
 1. sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}
 2. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
show "sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> \<not>(\<exists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (1 subgoal):
 1. sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}
[PROOF STEP]
by (simp only: no_microsteps_sterms_refl)
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p \<subseteq> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')}

goal (1 subgoal):
 1. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
from \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
[PROOF STEP]
have "{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

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

goal (10 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
 9. \<And>p1 p2. \<lbrakk>wellformed \<Gamma>; {q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p1; {q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p2\<rbrakk> \<Longrightarrow> {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (p1
\<oplus>
p2)
 10. \<And>pn. \<lbrakk>wellformed \<Gamma>; {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
show "{q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
proof (rule, drule CollectD, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
fix q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
assume "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
           and "sterms \<Gamma> q' = {q'}"
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}
[PROOF STEP]
have "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}

goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'
[PROOF STEP]
by (auto dest!: rtranclpD sterms_no_choice)
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
hence "p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<or> p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
[PROOF STATE]
proof (prove)
using this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'

goal (1 subgoal):
 1. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<or> p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
[PROOF STEP]
by (auto dest: tranclpD)
[PROOF STATE]
proof (state)
this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<or> p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
thus "q' \<in> sterms \<Gamma> (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
using this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<or> p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

goal (1 subgoal):
 1. q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
 2. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
assume "p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
[PROOF STATE]
proof (state)
this:
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

goal (2 subgoals):
 1. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
 2. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
with IH1 and \<open>sterms \<Gamma> q' = {q'}\<close>
[PROOF STATE]
proof (chain)
picking this:
{q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p1
sterms \<Gamma> q' = {q'}
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
[PROOF STEP]
have "q' \<in> sterms \<Gamma> p1"
[PROOF STATE]
proof (prove)
using this:
{q. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p1
sterms \<Gamma> q' = {q'}
p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

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

goal (2 subgoals):
 1. p1 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
 2. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> p1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> p1

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

goal (1 subgoal):
 1. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
assume "p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
[PROOF STATE]
proof (state)
this:
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

goal (1 subgoal):
 1. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
with IH2 and \<open>sterms \<Gamma> q' = {q'}\<close>
[PROOF STATE]
proof (chain)
picking this:
{q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p2
sterms \<Gamma> q' = {q'}
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
[PROOF STEP]
have "q' \<in> sterms \<Gamma> p2"
[PROOF STATE]
proof (prove)
using this:
{q. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p2
sterms \<Gamma> q' = {q'}
p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

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

goal (1 subgoal):
 1. p2 \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q' \<Longrightarrow> q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> p2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
q' \<in> sterms \<Gamma> (p1
\<oplus>
p2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (p1
\<oplus>
p2)

goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
fix pn
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
assume IH: "{q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
{q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
 9. \<And>pn. \<lbrakk>wellformed \<Gamma>; {q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)\<rbrakk> \<Longrightarrow> {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
show   "{q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))
[PROOF STEP]
proof (rule, drule CollectD, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
fix q'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
assume "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
           and "sterms \<Gamma> q' = {q'}"
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}
[PROOF STEP]
have "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
sterms \<Gamma> q' = {q'}

goal (1 subgoal):
 1. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'
[PROOF STEP]
by (auto dest!: rtranclpD sterms_no_call)
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
have "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn
[PROOF STEP]
have "\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'"
[PROOF STATE]
proof (prove)
using this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>+ q'
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> \<Gamma> pn

goal (1 subgoal):
 1. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
[PROOF STEP]
by (auto dest!: tranclpD)
[PROOF STATE]
proof (state)
this:
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
with \<open>sterms \<Gamma> q' = {q'}\<close> and IH
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> q' = {q'}
{q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'
[PROOF STEP]
have "q' \<in> sterms \<Gamma> (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> q' = {q'}
{q. \<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (\<Gamma> pn)
\<Gamma> pn \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q'

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* x; sterms \<Gamma> x = {x}\<rbrakk> \<Longrightarrow> x \<in> sterms \<Gamma> (call(pn))
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> (\<Gamma> pn)
[PROOF STEP]
show "q' \<in> sterms \<Gamma> (call(pn))"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
q' \<in> sterms \<Gamma> (\<Gamma> pn)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> (call(pn))

goal (8 subgoals):
 1. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<lbrakk>f\<rbrakk>
p)
 2. \<And>l f p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}\<langle>f\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}\<langle>f\<rangle>
p)
 3. \<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> {qa. ({l}unicast(fip, fmsg) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* qa \<and> sterms \<Gamma> qa = {qa}} \<subseteq> sterms \<Gamma> ({l}unicast(fip, fmsg) .
p \<triangleright> q)
 4. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}broadcast(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}broadcast(fmsg) .
p)
 5. \<And>l fips fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}groupcast(fips, fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}groupcast(fips, fmsg) .
p)
 6. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}send(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}send(fmsg) .
p)
 7. \<And>l fdata p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}deliver(fdata) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}deliver(fdata) .
p)
 8. \<And>l fmsg p. wellformed \<Gamma> \<Longrightarrow> {q. ({l}receive(fmsg) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> ({l}receive(fmsg) .
p)
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p

goal (1 subgoal):
 1. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
with \<open>wellformed \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
show "{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> \<not>(\<exists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<subseteq> sterms \<Gamma> p

goal (1 subgoal):
 1. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p
[PROOF STEP]
by (simp only: no_microsteps_sterms_refl)
[PROOF STATE]
proof (state)
this:
{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> (\<nexists>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')} \<subseteq> sterms \<Gamma> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dterms_dom_basic [simp]:
  assumes "not_call p"
      and "not_choice p"
    shows "dterms_dom (\<Gamma>, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
proof (rule accpI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. dterms_rel y (\<Gamma>, p) \<Longrightarrow> dterms_dom y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. dterms_rel y (\<Gamma>, p) \<Longrightarrow> dterms_dom y
[PROOF STEP]
assume "dterms_rel y (\<Gamma>, p)"
[PROOF STATE]
proof (state)
this:
dterms_rel y (\<Gamma>, p)

goal (1 subgoal):
 1. \<And>y. dterms_rel y (\<Gamma>, p) \<Longrightarrow> dterms_dom y
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
not_call p
not_choice p
dterms_rel y (\<Gamma>, p)
[PROOF STEP]
show "dterms_dom y"
[PROOF STATE]
proof (prove)
using this:
not_call p
not_choice p
dterms_rel y (\<Gamma>, p)

goal (1 subgoal):
 1. dterms_dom y
[PROOF STEP]
by (cases p) (auto simp: dterms_rel.simps)
[PROOF STATE]
proof (state)
this:
dterms_dom y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dterms_termination:
  assumes "wellformed \<Gamma>"
    shows "dterms_dom (\<Gamma>, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
have dterms_rel': "dterms_rel = (\<lambda>gq gp. (gq, gp) \<in> {((\<Gamma>, q), (\<Gamma>', p)). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dterms_rel = (\<lambda>gq gp. (gq, gp) \<in> {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q})
[PROOF STEP]
by (rule ext)+ (auto simp: dterms_rel.simps elim: microstep.cases)
[PROOF STATE]
proof (state)
this:
dterms_rel = (\<lambda>gq gp. (gq, gp) \<in> {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q})

goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
from \<open>wellformed(\<Gamma>)\<close>
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
[PROOF STEP]
have "\<forall>x. x \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. \<forall>x. x \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
unfolding wellformed_def
[PROOF STATE]
proof (prove)
using this:
wf {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. \<forall>x. x \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
by (simp add: wf_acc_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
hence "p \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. p \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
hence "(\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}"
[PROOF STATE]
proof (prove)
using this:
p \<in> Wellfounded.acc {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. (\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
by (rule acc_induct) (auto intro: accI)
[PROOF STATE]
proof (state)
this:
(\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
thus "dterms_dom (\<Gamma>, p)"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. dterms_dom (\<Gamma>, p)
[PROOF STEP]
unfolding dterms_rel'
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}

goal (1 subgoal):
 1. Wellfounded.accp (\<lambda>gq gp. (gq, gp) \<in> {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}) (\<Gamma>, p)
[PROOF STEP]
by (subst accp_acc_eq)
[PROOF STATE]
proof (state)
this:
dterms_dom (\<Gamma>, p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sterms_after_dterms [simp]:
  assumes "wellformed \<Gamma>"
  shows "(\<Union>x\<in>dterms \<Gamma> p. sterms \<Gamma> x) = dterms \<Gamma> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (sterms \<Gamma> ` dterms \<Gamma> p) = dterms \<Gamma> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. \<Union> (sterms \<Gamma> ` dterms \<Gamma> p) = dterms \<Gamma> p
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma sterms_before_dterms [simp]:
  assumes "wellformed \<Gamma>"
  shows "(\<Union>x\<in>sterms \<Gamma> p. dterms \<Gamma> x) = dterms \<Gamma> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (dterms \<Gamma> ` sterms \<Gamma> p) = dterms \<Gamma> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. \<Union> (dterms \<Gamma> ` sterms \<Gamma> p) = dterms \<Gamma> p
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma dterms_choice_disj [simp]:
  assumes "wellformed \<Gamma>"
    shows "p \<in> dterms \<Gamma> (p1 \<oplus> p2) = (p \<in> dterms \<Gamma> p1 \<or> p \<in> dterms \<Gamma> p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<in> dterms \<Gamma> (p1
\<oplus>
p2)) = (p \<in> dterms \<Gamma> p1 \<or> p \<in> dterms \<Gamma> p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. (p \<in> dterms \<Gamma> (p1
\<oplus>
p2)) = (p \<in> dterms \<Gamma> p1 \<or> p \<in> dterms \<Gamma> p2)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma dterms_in_branch:
  assumes "wellformed \<Gamma>"
      and "p \<in> dterms \<Gamma> (p1 \<oplus> p2)"
      and "p \<in> dterms \<Gamma> p1 \<Longrightarrow> P"
      and "p \<in> dterms \<Gamma> p2 \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p \<in> dterms \<Gamma> (p1
\<oplus>
p2)
p \<in> dterms \<Gamma> p1 \<Longrightarrow> P
p \<in> dterms \<Gamma> p2 \<Longrightarrow> P

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


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

goal (1 subgoal):
 1. p1
\<oplus>
p2 \<notin> dterms \<Gamma> p
[PROOF STEP]
by induction simp_all


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

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

goal (1 subgoal):
 1. \<forall>p1 p2. q \<noteq> p1
\<oplus>
p2
[PROOF STEP]
by (auto dest: dterms_no_choice)


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

goal (1 subgoal):
 1. call(pn) \<notin> dterms \<Gamma> p
[PROOF STEP]
by induction simp_all


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

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

goal (1 subgoal):
 1. \<forall>pn. q \<noteq> call(pn)
[PROOF STEP]
by (auto dest: dterms_no_call)