[STATEMENT]
lemma no_microsteps_sterms_refl:
  assumes "wellformed \<Gamma>"
  shows "(\<not>(\<exists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)) = (sterms \<Gamma> p = {p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13. p = {x11}\<langle>x12\<rangle>
x13 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 2. \<And>x21 x22 x23. p = {x21}\<lbrakk>x22\<rbrakk>
x23 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 3. \<And>x31 x32. p = x31
\<oplus>
x32 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 4. \<And>x41 x42 x43 x44 x45. p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 5. \<And>x51 x52 x53. p = {x51}broadcast(x52) .
x53 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 6. \<And>x61 x62 x63 x64. p = {x61}groupcast(x62, x63) .
x64 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 7. \<And>x71 x72 x73. p = {x71}send(x72) .
x73 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 8. \<And>x81 x82 x83. p = {x81}deliver(x82) .
x83 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 9. \<And>x91 x92 x93. p = {x91}receive(x92) .
x93 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 10. \<And>x10. p = call(x10) \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13. p = {x11}\<langle>x12\<rangle>
x13 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 2. \<And>x21 x22 x23. p = {x21}\<lbrakk>x22\<rbrakk>
x23 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 3. \<And>x31 x32. p = x31
\<oplus>
x32 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 4. \<And>x41 x42 x43 x44 x45. p = {x41}unicast(x42, x43) .
x44 \<triangleright> x45 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 5. \<And>x51 x52 x53. p = {x51}broadcast(x52) .
x53 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 6. \<And>x61 x62 x63 x64. p = {x61}groupcast(x62, x63) .
x64 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 7. \<And>x71 x72 x73. p = {x71}send(x72) .
x73 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 8. \<And>x81 x82 x83. p = {x81}deliver(x82) .
x83 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 9. \<And>x91 x92 x93. p = {x91}receive(x92) .
x93 \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
 10. \<And>x10. p = call(x10) \<Longrightarrow> (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
assume "p = p1 \<oplus> p2"
[PROOF STATE]
proof (state)
this:
p = p1
\<oplus>
p2

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
using \<open>p = p1 \<oplus> p2\<close>
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> (p1
\<oplus>
p2) \<noteq> {p1
\<oplus>
p2}
\<exists>q. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
p = p1
\<oplus>
p2

goal (1 subgoal):
 1. (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})

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

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

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

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

goal (1 subgoal):
 1. sterms \<Gamma> (call(pn)) \<noteq> {call(pn)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (call(pn)) \<noteq> {call(pn)}

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

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

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

goal (1 subgoal):
 1. (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
using \<open>p = call(pn)\<close>
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> (call(pn)) \<noteq> {call(pn)}
\<exists>q. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
p = call(pn)

goal (1 subgoal):
 1. (\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<nexists>q. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q) = (sterms \<Gamma> p = {p})

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


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

goal (1 subgoal):
 1. sterms \<Gamma> q = {q}
[PROOF STEP]
by (cases q) auto


[STATEMENT]
lemma microstep_rtranscl_equal:
  assumes "not_call p"
      and "not_choice p"
      and "p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q"
    shows "q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = p
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q

goal (1 subgoal):
 1. q = p
[PROOF STEP]
proof (rule converse_rtranclpE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = q \<Longrightarrow> q = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q\<rbrakk> \<Longrightarrow> q = p
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = q \<Longrightarrow> q = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q\<rbrakk> \<Longrightarrow> q = p
[PROOF STEP]
assume "p \<leadsto>\<^bsub>\<Gamma>\<^esub> p'"
[PROOF STATE]
proof (state)
this:
p \<leadsto>\<^bsub>\<Gamma>\<^esub> p'

goal (2 subgoals):
 1. p = q \<Longrightarrow> q = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q\<rbrakk> \<Longrightarrow> q = p
[PROOF STEP]
with assms(1-2)
[PROOF STATE]
proof (chain)
picking this:
not_call p
not_choice p
p \<leadsto>\<^bsub>\<Gamma>\<^esub> p'
[PROOF STEP]
show "q = p"
[PROOF STATE]
proof (prove)
using this:
not_call p
not_choice p
p \<leadsto>\<^bsub>\<Gamma>\<^esub> p'

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

goal (1 subgoal):
 1. p = q \<Longrightarrow> q = p
[PROOF STEP]
qed simp


[STATEMENT]
lemma microstep_rtranscl_singleton [simp]:
  assumes "not_call p"
      and "not_choice p"
    shows "{q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} = {p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} = {p}
[PROOF STEP]
proof (rule set_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}) = (x \<in> {p})
[PROOF STEP]
fix p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}) = (x \<in> {p})
[PROOF STEP]
show "(p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}) = (p' \<in> {p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}) = (p' \<in> {p})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<Longrightarrow> p' \<in> {p}
 2. p' \<in> {p} \<Longrightarrow> p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
assume "p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}"
[PROOF STATE]
proof (state)
this:
p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

goal (2 subgoals):
 1. p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<Longrightarrow> p' \<in> {p}
 2. p' \<in> {p} \<Longrightarrow> p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
hence "(microstep \<Gamma>)\<^sup>*\<^sup>* p p'" and "sterms \<Gamma> p' = {p'}"
[PROOF STATE]
proof (prove)
using this:
p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}

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

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

goal (1 subgoal):
 1. p' = p
[PROOF STEP]
proof (rule converse_rtranclpE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = p' \<Longrightarrow> p' = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = p
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = p' \<Longrightarrow> p' = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = p
[PROOF STEP]
assume "p \<leadsto>\<^bsub>\<Gamma>\<^esub> q"
[PROOF STATE]
proof (state)
this:
p \<leadsto>\<^bsub>\<Gamma>\<^esub> q

goal (2 subgoals):
 1. p = p' \<Longrightarrow> p' = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = p
[PROOF STEP]
with \<open>not_call p\<close> and \<open>not_choice p\<close>
[PROOF STATE]
proof (chain)
picking this:
not_call p
not_choice p
p \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
not_call p
not_choice p
p \<leadsto>\<^bsub>\<Gamma>\<^esub> q

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

goal (2 subgoals):
 1. p = p' \<Longrightarrow> p' = p
 2. \<And>y. \<lbrakk>p \<leadsto>\<^bsub>\<Gamma>\<^esub> y; y \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* p'\<rbrakk> \<Longrightarrow> p' = p
[PROOF STEP]
thus "p' = p"
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. p = p' \<Longrightarrow> p' = p
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
p' = p

goal (2 subgoals):
 1. p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}} \<Longrightarrow> p' \<in> {p}
 2. p' \<in> {p} \<Longrightarrow> p' \<in> {q. p \<leadsto>\<^bsub>\<Gamma>\<^esub>\<^sup>* q \<and> sterms \<Gamma> q = {q}}
[PROOF STEP]
thus "p' \<in> {p}"
[PROOF STATE]
proof (prove)
using this:
p' = p

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed