[STATEMENT]
lemma wellformed_induct
  [consumes 1, case_names ASSIGN CHOICE CALL GUARD UCAST BCAST GCAST SEND DELIVER RECEIVE,
   induct set: wellformed]:
  assumes "wellformed \<Gamma>"
      and ASSIGN:  "\<And>l f p.          wellformed \<Gamma> \<Longrightarrow> P ({l}\<lbrakk>f\<rbrakk> p)"
      and GUARD:   "\<And>l f p.          wellformed \<Gamma> \<Longrightarrow> P ({l}\<langle>f\<rangle> p)"
      and UCAST:   "\<And>l fip fmsg p q. wellformed \<Gamma> \<Longrightarrow> P ({l}unicast(fip, fmsg). p \<triangleright> q)"
      and BCAST:   "\<And>l fmsg p.       wellformed \<Gamma> \<Longrightarrow> P ({l}broadcast(fmsg). p)"
      and GCAST:   "\<And>l fips fmsg p.  wellformed \<Gamma> \<Longrightarrow> P ({l}groupcast(fips, fmsg). p)"
      and SEND:    "\<And>l fmsg p.       wellformed \<Gamma> \<Longrightarrow> P ({l}send(fmsg). p)"
      and DELIVER: "\<And>l fdata p.      wellformed \<Gamma> \<Longrightarrow> P ({l}deliver(fdata). p)"
      and RECEIVE: "\<And>l fmsg p.       wellformed \<Gamma> \<Longrightarrow> P ({l}receive(fmsg). p)"
      and CHOICE:  "\<And>p1 p2.        \<lbrakk> wellformed \<Gamma>; P p1; P p2 \<rbrakk> \<Longrightarrow> P (p1 \<oplus> p2)"
      and CALL:    "\<And>pn.           \<lbrakk> wellformed \<Gamma>; P (\<Gamma> pn) \<rbrakk> \<Longrightarrow> P (call(pn))"
    shows "P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. P a
[PROOF STEP]
unfolding wellformed_defP
[PROOF STATE]
proof (prove)
using this:
wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)

goal (1 subgoal):
 1. P a
[PROOF STEP]
proof (rule wfP_induct_rule, case_tac x, simp_all)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x31 x32. \<lbrakk>\<And>y. (x31
\<oplus>
x32) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = x31
\<oplus>
x32; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (x31
\<oplus>
x32)
 4. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 5. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 6. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 7. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 8. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 9. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 10. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x31 x32. \<lbrakk>\<And>y. (x31
\<oplus>
x32) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = x31
\<oplus>
x32; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (x31
\<oplus>
x32)
 4. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 5. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 6. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 7. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 8. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 9. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 10. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
assume "\<And>q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<Longrightarrow> P q"
[PROOF STATE]
proof (state)
this:
(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> ?q \<Longrightarrow> P ?q

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

goal (1 subgoal):
 1. (\<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro!: microstep.intros)
[PROOF STATE]
proof (state)
this:
P p1
P p2

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

goal (1 subgoal):
 1. P (p1
\<oplus>
p2)
[PROOF STEP]
by (rule CHOICE [OF \<open>wellformed \<Gamma>\<close>])
[PROOF STATE]
proof (state)
this:
P (p1
\<oplus>
p2)

goal (9 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 9. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 9. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
fix pn
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 9. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
assume "\<And>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<Longrightarrow> P q"
[PROOF STATE]
proof (state)
this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> ?q \<Longrightarrow> P ?q

goal (9 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 9. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
hence "P (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> ?q \<Longrightarrow> P ?q

goal (1 subgoal):
 1. P (\<Gamma> pn)
[PROOF STEP]
by (auto intro!: microstep.intros)
[PROOF STATE]
proof (state)
this:
P (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
 9. \<And>x x10. \<lbrakk>\<And>y. (call(x10)) \<leadsto>\<^bsub>\<Gamma>\<^esub> y \<Longrightarrow> P y; x = call(x10); wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P (call(x10))
[PROOF STEP]
thus "P (call(pn))"
[PROOF STATE]
proof (prove)
using this:
P (\<Gamma> pn)

goal (1 subgoal):
 1. P (call(pn))
[PROOF STEP]
by (rule CALL [OF \<open>wellformed \<Gamma>\<close>])
[PROOF STATE]
proof (state)
this:
P (call(pn))

goal (8 subgoals):
 1. \<And>x x11 x12 x13. \<lbrakk>x = {x11}\<langle>x12\<rangle>
x13; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x11}\<langle>x12\<rangle>
x13)
 2. \<And>x x21 x22 x23. \<lbrakk>x = {x21}\<lbrakk>x22\<rbrakk>
x23; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x21}\<lbrakk>x22\<rbrakk>
x23)
 3. \<And>x x41 x42 x43 x44 x45. \<lbrakk>x = {x41}unicast(x42, x43) .
x44 \<triangleright> x45; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x41}unicast(x42, x43) .
x44 \<triangleright> x45)
 4. \<And>x x51 x52 x53. \<lbrakk>x = {x51}broadcast(x52) .
x53; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x51}broadcast(x52) .
x53)
 5. \<And>x x61 x62 x63 x64. \<lbrakk>x = {x61}groupcast(x62, x63) .
x64; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x61}groupcast(x62, x63) .
x64)
 6. \<And>x x71 x72 x73. \<lbrakk>x = {x71}send(x72) .
x73; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x71}send(x72) .
x73)
 7. \<And>x x81 x82 x83. \<lbrakk>x = {x81}deliver(x82) .
x83; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x81}deliver(x82) .
x83)
 8. \<And>x x91 x92 x93. \<lbrakk>x = {x91}receive(x92) .
x93; wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)\<rbrakk> \<Longrightarrow> P ({x91}receive(x92) .
x93)
[PROOF STEP]
qed (auto intro: assms)


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


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


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


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


[STATEMENT]
lemma stermsl_commute:
  "stermsl (p1 \<oplus> p2) = stermsl (p2 \<oplus> p1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stermsl (p1
\<oplus>
p2) = stermsl (p2
\<oplus>
p1)
[PROOF STEP]
by simp (rule Un_commute)


[STATEMENT]
lemma stermsl_not_empty:
  "stermsl p \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stermsl p \<noteq> {}
[PROOF STEP]
by (induct p) auto


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


[STATEMENT]
lemma stermsl_in_wfpf:
  assumes AA: "A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A"
      and *: "p \<in> A"
    shows "\<exists>r\<in>stermsl p. r \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>stermsl p. r \<in> A
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
p \<in> A

goal (1 subgoal):
 1. \<exists>r\<in>stermsl p. r \<in> A
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
assume IH1: "p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A"
       and IH2: "p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A"
       and *: "p1 \<oplus> p2 \<in> A"
[PROOF STATE]
proof (state)
this:
p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A
p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A
p1
\<oplus>
p2 \<in> A

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
from * and AA
[PROOF STATE]
proof (chain)
picking this:
p1
\<oplus>
p2 \<in> A
A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A
[PROOF STEP]
have "p1 \<oplus> p2 \<in> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A"
[PROOF STATE]
proof (prove)
using this:
p1
\<oplus>
p2 \<in> A
A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A

goal (1 subgoal):
 1. p1
\<oplus>
p2 \<in> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1
\<oplus>
p2 \<in> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
hence "p1 \<in> A \<or> p2 \<in> A"
[PROOF STATE]
proof (prove)
using this:
p1
\<oplus>
p2 \<in> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A

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

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
hence "(\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> A \<or> p2 \<in> A

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

goal (2 subgoals):
 1. p1 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
 2. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
hence "\<exists>r\<in>stermsl p1. r \<in> A"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> A

goal (1 subgoal):
 1. \<exists>r\<in>stermsl p1. r \<in> A
[PROOF STEP]
by (rule IH1)
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>stermsl p1. r \<in> A

goal (2 subgoals):
 1. p1 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
 2. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>stermsl p1. r \<in> A

goal (1 subgoal):
 1. (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)

goal (1 subgoal):
 1. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
assume "p2 \<in> A"
[PROOF STATE]
proof (state)
this:
p2 \<in> A

goal (1 subgoal):
 1. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
hence "\<exists>r\<in>stermsl p2. r \<in> A"
[PROOF STATE]
proof (prove)
using this:
p2 \<in> A

goal (1 subgoal):
 1. \<exists>r\<in>stermsl p2. r \<in> A
[PROOF STEP]
by (rule IH2)
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>stermsl p2. r \<in> A

goal (1 subgoal):
 1. p2 \<in> A \<Longrightarrow> (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>stermsl p2. r \<in> A

goal (1 subgoal):
 1. (\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)

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

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
hence "\<exists>r\<in>stermsl p1 \<union> stermsl p2. r \<in> A"
[PROOF STATE]
proof (prove)
using this:
(\<exists>r\<in>stermsl p1. r \<in> A) \<or> (\<exists>r\<in>stermsl p2. r \<in> A)

goal (1 subgoal):
 1. \<exists>r\<in>stermsl p1 \<union> stermsl p2. r \<in> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>stermsl p1 \<union> stermsl p2. r \<in> A

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl (p1
\<oplus>
p2). r \<in> A
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 10. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
thus "\<exists>r\<in>stermsl (p1 \<oplus> p2). r \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>stermsl p1 \<union> stermsl p2. r \<in> A

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

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 9. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 9. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
case UCAST
[PROOF STATE]
proof (state)
this:
p1_ \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1_. r \<in> A
p2_ \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2_. r \<in> A
{x1_}unicast(x2_, x3_) .
p1_ \<triangleright> p2_ \<in> A

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p1. r \<in> A; p2 \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p2. r \<in> A; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2). r \<in> A
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 9. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
from UCAST.prems
[PROOF STATE]
proof (chain)
picking this:
{x1_}unicast(x2_, x3_) .
p1_ \<triangleright> p2_ \<in> A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{x1_}unicast(x2_, x3_) .
p1_ \<triangleright> p2_ \<in> A

goal (1 subgoal):
 1. \<exists>r\<in>stermsl ({x1_}unicast(x2_, x3_) .
p1_ \<triangleright> p2_). r \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>stermsl ({x1_}unicast(x2_, x3_) .
p1_ \<triangleright> p2_). r \<in> A

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<langle>x2\<rangle>
p). r \<in> A
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}\<lbrakk>x2\<rbrakk>
p). r \<in> A
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}broadcast(x2) .
p). r \<in> A
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}groupcast(x2, x3) .
p). r \<in> A
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}send(x2) .
p). r \<in> A
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}deliver(x2) .
p). r \<in> A
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl p. r \<in> A; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> \<exists>r\<in>stermsl ({x1}receive(x2) .
p). r \<in> A
 8. \<And>x. call(x) \<in> A \<Longrightarrow> \<exists>r\<in>stermsl (call(x)). r \<in> A
[PROOF STEP]
qed auto


[STATEMENT]
lemma nocall_stermsl_max:
  assumes "r \<in> stermsl p"
      and "not_call r"
    shows "\<not> (r \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> r \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<in> stermsl p
not_call r

goal (1 subgoal):
 1. \<not> r \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (induction p) auto


[STATEMENT]
theorem wf_no_direct_calls[intro]:
    fixes \<Gamma> :: "('s, 'm, 'p, 'l) seqp_env"
  assumes no_calls: "\<And>pn. \<forall>pn'. call(pn') \<notin> stermsl(\<Gamma>(pn))"
    shows "wellformed \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed \<Gamma>
[PROOF STEP]
unfolding wellformed_def wfP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
proof (rule wfI_pf)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A \<Longrightarrow> A = {}
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A \<Longrightarrow> A = {}
[PROOF STEP]
assume ARA: "A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A"
[PROOF STATE]
proof (state)
this:
A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A

goal (1 subgoal):
 1. \<And>A. A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A \<Longrightarrow> A = {}
[PROOF STEP]
hence hasnext: "\<And>p. p \<in> A \<Longrightarrow> \<exists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A

goal (1 subgoal):
 1. \<And>p. p \<in> A \<Longrightarrow> \<exists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?p \<in> A \<Longrightarrow> \<exists>q. ?p \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

goal (1 subgoal):
 1. \<And>A. A \<subseteq> {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} `` A \<Longrightarrow> A = {}
[PROOF STEP]
show "A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = {}
[PROOF STEP]
proof (rule Set.equals0I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> A \<Longrightarrow> False
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> A \<Longrightarrow> False
[PROOF STEP]
assume "p \<in> A"
[PROOF STATE]
proof (state)
this:
p \<in> A

goal (1 subgoal):
 1. \<And>y. y \<in> A \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
p \<in> A

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (induction p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 10. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
fix l f p'
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 10. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
assume *: "{l}\<langle>f\<rangle> p' \<in> A"
[PROOF STATE]
proof (state)
this:
{l}\<langle>f\<rangle>
p' \<in> A

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 10. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
from hasnext [OF *]
[PROOF STATE]
proof (chain)
picking this:
\<exists>q. ({l}\<langle>f\<rangle>
p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A
[PROOF STEP]
have "\<exists>q. ({l}\<langle>f\<rangle> p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. ({l}\<langle>f\<rangle>
p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

goal (1 subgoal):
 1. \<exists>q. ({l}\<langle>f\<rangle>
p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>q. ({l}\<langle>f\<rangle>
p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<langle>x2\<rangle>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 10. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. ({l}\<langle>f\<rangle>
p') \<leadsto>\<^bsub>\<Gamma>\<^esub> q

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

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
assume *: "p1 \<oplus> p2 \<in> A"
         and IH1: "p1 \<in> A \<Longrightarrow> False"
         and IH2: "p2 \<in> A \<Longrightarrow> False"
[PROOF STATE]
proof (state)
this:
p1
\<oplus>
p2 \<in> A
p1 \<in> A \<Longrightarrow> False
p2 \<in> A \<Longrightarrow> False

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
have "\<exists>q. (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A
[PROOF STEP]
by (rule hasnext [OF *])
[PROOF STATE]
proof (state)
this:
\<exists>q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
hence "p1 \<in> A \<or> p2 \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

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

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; p1
\<oplus>
p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 9. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> A \<or> p2 \<in> A

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest: IH1 IH2)
[PROOF STATE]
proof (state)
this:
False

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
fix pn
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
assume "call(pn) \<in> A"
[PROOF STATE]
proof (state)
this:
call(pn) \<in> A

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A"
[PROOF STATE]
proof (prove)
using this:
call(pn) \<in> A

goal (1 subgoal):
 1. \<exists>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A
[PROOF STEP]
by (rule hasnext)
[PROOF STATE]
proof (state)
this:
\<exists>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
hence "\<Gamma>(pn) \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q \<and> q \<in> A

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

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
with ARA [THEN stermsl_in_wfpf]
[PROOF STATE]
proof (chain)
picking this:
?p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl ?p. r \<in> A
\<Gamma> pn \<in> A
[PROOF STEP]
obtain q where "q\<in>stermsl (\<Gamma> pn)" and "q \<in> A"
[PROOF STATE]
proof (prove)
using this:
?p \<in> A \<Longrightarrow> \<exists>r\<in>stermsl ?p. r \<in> A
\<Gamma> pn \<in> A

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

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
hence "not_call q"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (\<Gamma> pn)
q \<in> A

goal (1 subgoal):
 1. not_call q
[PROOF STEP]
using no_calls [of pn]
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (\<Gamma> pn)
q \<in> A
\<forall>pn'. call(pn') \<notin> stermsl (\<Gamma> pn)

goal (1 subgoal):
 1. not_call q
[PROOF STEP]
unfolding not_call_def
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (\<Gamma> pn)
q \<in> A
\<forall>pn'. call(pn') \<notin> stermsl (\<Gamma> pn)

goal (1 subgoal):
 1. \<forall>pn. q \<noteq> call(pn)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
not_call q

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
from hasnext [OF \<open>q \<in> A\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>qa. q \<leadsto>\<^bsub>\<Gamma>\<^esub> qa \<and> qa \<in> A
[PROOF STEP]
obtain q' where "q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'"
[PROOF STATE]
proof (prove)
using this:
\<exists>qa. q \<leadsto>\<^bsub>\<Gamma>\<^esub> qa \<and> qa \<in> A

goal (1 subgoal):
 1. (\<And>q'. q \<leadsto>\<^bsub>\<Gamma>\<^esub> q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
from  \<open>q \<in> stermsl (\<Gamma> pn)\<close> \<open>not_call q\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<in> stermsl (\<Gamma> pn)
not_call q
[PROOF STEP]
have "\<not> (q \<leadsto>\<^bsub>\<Gamma>\<^esub> q')"
[PROOF STATE]
proof (prove)
using this:
q \<in> stermsl (\<Gamma> pn)
not_call q

goal (1 subgoal):
 1. \<not> q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'
[PROOF STEP]
by (rule nocall_stermsl_max)
[PROOF STATE]
proof (state)
this:
\<not> q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 8. \<And>x. call(x) \<in> A \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'
\<not> q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'
\<not> q \<leadsto>\<^bsub>\<Gamma>\<^esub> q'

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

goal (7 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}\<lbrakk>x2\<rbrakk>
p \<in> A\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> A \<Longrightarrow> False; p2 \<in> A \<Longrightarrow> False; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> A\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}broadcast(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}groupcast(x2, x3) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}send(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}deliver(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x2 p. \<lbrakk>p \<in> A \<Longrightarrow> False; {x1}receive(x2) .
p \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed (auto dest: hasnext)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = {}

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sterms_termination:
  assumes "wellformed \<Gamma>"
    shows "sterms_dom (\<Gamma>, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms_dom (\<Gamma>, p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sterms_dom (\<Gamma>, p)
[PROOF STEP]
have sterms_rel':
      "sterms_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. sterms_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: sterms_rel.simps elim: microstep.cases)
[PROOF STATE]
proof (state)
this:
sterms_rel = (\<lambda>gq gp. (gq, gp) \<in> {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q})

goal (1 subgoal):
 1. sterms_dom (\<Gamma>, p)
[PROOF STEP]
from assms
[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. sterms_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. sterms_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. sterms_dom (\<Gamma>, p)
[PROOF STEP]
thus "sterms_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. sterms_dom (\<Gamma>, p)
[PROOF STEP]
unfolding sterms_rel' accp_acc_eq
[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. (\<Gamma>, p) \<in> Wellfounded.acc {((\<Gamma>, q), \<Gamma>', p). \<Gamma> = \<Gamma>' \<and> p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sterms_dom (\<Gamma>, p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sterms_reflD [dest]:
  assumes "q \<in> sterms \<Gamma> p"
      and "not_choice p" "not_call p"
    shows "q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> sterms \<Gamma> p
not_choice p
not_call p

goal (1 subgoal):
 1. q = p
[PROOF STEP]
by (cases p) auto


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

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


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

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


[STATEMENT]
lemma sterms_not_choice [simp]:
  assumes "wellformed \<Gamma>"
      and "q \<in> sterms \<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> sterms \<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> sterms \<Gamma> p

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


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

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


[STATEMENT]
lemma sterms_not_call [simp]:
  assumes "wellformed \<Gamma>"
      and "q \<in> sterms \<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> sterms \<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> sterms \<Gamma> p

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


[STATEMENT]
lemma sterms_in_branch:
  assumes "wellformed \<Gamma>"
      and "p \<in> sterms \<Gamma> (p1 \<oplus> p2)"
      and "p \<in> sterms \<Gamma> p1 \<Longrightarrow> P"
      and "p \<in> sterms \<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> sterms \<Gamma> (p1
\<oplus>
p2)
p \<in> sterms \<Gamma> p1 \<Longrightarrow> P
p \<in> sterms \<Gamma> p2 \<Longrightarrow> P

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


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

goal (1 subgoal):
 1. sterms \<Gamma> (p1
\<oplus>
p2) = sterms \<Gamma> (p2
\<oplus>
p1)
[PROOF STEP]
by simp (rule Un_commute)


[STATEMENT]
lemma sterms_not_empty:
  assumes "wellformed \<Gamma>"
    shows "sterms \<Gamma> p \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> p \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> p \<noteq> {}
[PROOF STEP]
by (induct p rule: sterms_pinduct [OF \<open>wellformed \<Gamma>\<close>]) simp_all


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

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


[STATEMENT]
lemma sterms_stermsl:
  assumes "ps \<in> sterms \<Gamma> p"
      and "wellformed \<Gamma>"
    shows "ps \<in> stermsl p \<or> (\<exists>pn. ps \<in> stermsl (\<Gamma> pn))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<in> stermsl p \<or> (\<exists>pn. ps \<in> stermsl (\<Gamma> pn))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ps \<in> sterms \<Gamma> p
wellformed \<Gamma>

goal (1 subgoal):
 1. ps \<in> stermsl p \<or> (\<exists>pn. ps \<in> stermsl (\<Gamma> pn))
[PROOF STEP]
by (induction p rule: sterms_pinduct [OF \<open>wellformed \<Gamma>\<close>]) auto


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

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


[STATEMENT]
lemma sterms_stermsl_heads:
  assumes "ps \<in> sterms \<Gamma> (\<Gamma> pn)"
      and "wellformed \<Gamma>"
    shows "\<exists>pn. ps \<in> stermsl (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pn. ps \<in> stermsl (\<Gamma> pn)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>pn. ps \<in> stermsl (\<Gamma> pn)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
ps \<in> sterms \<Gamma> (\<Gamma> pn)
wellformed \<Gamma>
[PROOF STEP]
have "ps \<in> stermsl (\<Gamma> pn) \<or> (\<exists>pn'. ps \<in> stermsl (\<Gamma> pn'))"
[PROOF STATE]
proof (prove)
using this:
ps \<in> sterms \<Gamma> (\<Gamma> pn)
wellformed \<Gamma>

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

goal (1 subgoal):
 1. \<exists>pn. ps \<in> stermsl (\<Gamma> pn)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ps \<in> stermsl (\<Gamma> pn) \<or> (\<exists>pn'. ps \<in> stermsl (\<Gamma> pn'))

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<exists>pn. q \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by (induct p) auto