[STATEMENT]
lemma par_qmsg_oreachable:
  assumes "(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
           (is "_ \<in> oreachable _ ?owS _")
      and pinv: "A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>)
                       globala (\<lambda>(\<sigma>, _, \<sigma>'). U (\<sigma> i) (\<sigma>' i))"
      and ustutter: "\<And>\<xi>. U \<xi> \<xi>"
      and sgivesu: "\<And>\<xi> \<xi>'. S \<xi> \<xi>' \<Longrightarrow> U \<xi> \<xi>'"
      and upreservesq: "\<And>\<sigma> \<sigma>' m. \<lbrakk> \<forall>j. U (\<sigma> j) (\<sigma>' j); R \<sigma> m \<rbrakk> \<Longrightarrow> R \<sigma>' m"
  shows "(\<sigma>, fst \<zeta>) \<in> oreachable A ?owS (other U {i})
         \<and> snd \<zeta> \<in> reachable qmsg (recvmsg (R \<sigma>))
         \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R \<sigma> m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R \<sigma> m)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<zeta>) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. (\<sigma>, fst \<zeta>) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd \<zeta> \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd \<zeta>)). R \<sigma> m)
[PROOF STEP]
proof (induction rule: oreachable_pair_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
fix \<sigma> pq
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
assume "(\<sigma>, pq) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)"
[PROOF STATE]
proof (state)
this:
(\<sigma>, pq) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, pq) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
[PROOF STEP]
obtain p ms q where "pq = (p, (ms, q))"
                         and "(\<sigma>, p) \<in> init A"
                         and "(ms, q) \<in> init qmsg"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, pq) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)

goal (1 subgoal):
 1. (\<And>p ms q. \<lbrakk>pq = (p, ms, q); (\<sigma>, p) \<in> init A; (ms, q) \<in> init qmsg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp simp del: \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_simps)
[PROOF STATE]
proof (state)
this:
pq = (p, ms, q)
(\<sigma>, p) \<in> init A
(ms, q) \<in> init qmsg

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, p) \<in> init A
[PROOF STEP]
have "(\<sigma>, p) \<in> oreachable A ?owS (other U {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> init A

goal (1 subgoal):
 1. (\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>(ms, q) \<in> init qmsg\<close>
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> init qmsg
[PROOF STEP]
have "(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> init qmsg

goal (1 subgoal):
 1. (ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>(ms, q) \<in> init qmsg\<close>
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> init qmsg
[PROOF STEP]
have "ms = []"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> init qmsg

goal (1 subgoal):
 1. ms = []
[PROOF STEP]
unfolding \<sigma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_def
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> init \<lparr>init = {([], \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G ())}, trans = seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rparr>

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

goal (3 subgoals):
 1. \<And>\<sigma> p. (\<sigma>, p) \<in> init (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) \<Longrightarrow> (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m)
 2. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 3. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
ms = []
[PROOF STEP]
show "(\<sigma>, fst pq) \<in> oreachable A ?owS (other U {i})
                     \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))
                     \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
ms = []

goal (1 subgoal):
 1. (\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)
[PROOF STEP]
using \<open>pq = (p, (ms, q))\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
ms = []
pq = (p, ms, q)

goal (1 subgoal):
 1. (\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
note \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_simps [simp del]
[PROOF STATE]
proof (state)
this:
\<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G () = {()-:0}receive(\<lambda>msg msgs. msgs @ [msg]) .
call(())
\<oplus>
{()-:0}\<langle>\<lambda>msgs. if msgs \<noteq> [] then {msgs} else {}\<rangle>
({()-:1}send(hd) .
({()-:2}\<lbrakk>tl\<rbrakk>
call(())
\<oplus>
{()-:2}receive(\<lambda>msg msgs. tl msgs @ [msg]) .
call(()))
\<oplus>
{()-:1}receive(\<lambda>msg msgs. msgs @ [msg]) .
call(()))

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
case (other \<sigma> pq \<sigma>')
[PROOF STATE]
proof (state)
this:
(\<sigma>, pq) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
other U {i} \<sigma> \<sigma>'
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
hence "(\<sigma>, fst pq) \<in> oreachable A ?owS (other U {i})"
      and "other U {i} \<sigma> \<sigma>'"
      and qr: "snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))"
      and "\<forall>m\<in>set (fst (snd pq)). R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, pq) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
other U {i} \<sigma> \<sigma>'
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)

goal (1 subgoal):
 1. ((\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) &&& other U {i} \<sigma> \<sigma>') &&& snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) &&& \<forall>m\<in>set (fst (snd pq)). R \<sigma> m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
other U {i} \<sigma> \<sigma>'
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))
\<forall>m\<in>set (fst (snd pq)). R \<sigma> m

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>other U {i} \<sigma> \<sigma>'\<close> and ustutter
[PROOF STATE]
proof (chain)
picking this:
other U {i} \<sigma> \<sigma>'
U ?\<xi> ?\<xi>
[PROOF STEP]
have "\<forall>j. U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
other U {i} \<sigma> \<sigma>'
U ?\<xi> ?\<xi>

goal (1 subgoal):
 1. \<forall>j. U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by (clarsimp elim!: otherE) metis
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>other U {i} \<sigma> \<sigma>'\<close>
     and \<open>(\<sigma>, fst pq) \<in> oreachable A ?owS (other U {i})\<close>
[PROOF STATE]
proof (chain)
picking this:
other U {i} \<sigma> \<sigma>'
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
have "(\<sigma>', fst pq) \<in> oreachable A ?owS (other U {i})"
[PROOF STATE]
proof (prove)
using this:
other U {i} \<sigma> \<sigma>'
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. (\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
by - (rule oreachable_other')
[PROOF STATE]
proof (state)
this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
have "\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>set (fst (snd pq)). R \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set (fst (snd pq)) \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set (fst (snd pq)) \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
assume "m \<in> set (fst (snd pq))"
[PROOF STATE]
proof (state)
this:
m \<in> set (fst (snd pq))

goal (1 subgoal):
 1. \<And>m. m \<in> set (fst (snd pq)) \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>m\<in>set (fst (snd pq)). R \<sigma> m\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set (fst (snd pq)). R \<sigma> m
m \<in> set (fst (snd pq))
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set (fst (snd pq)). R \<sigma> m
m \<in> set (fst (snd pq))

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. m \<in> set (fst (snd pq)) \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m
[PROOF STEP]
show "R \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m

goal (1 subgoal):
 1. R \<sigma>' m
[PROOF STEP]
by (rule upreservesq)
[PROOF STATE]
proof (state)
this:
R \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from qr
[PROOF STATE]
proof (chain)
picking this:
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))"
[PROOF STATE]
proof (prove)
using this:
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
assume "recvmsg (R \<sigma>) a"
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) a

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
thus "recvmsg (R \<sigma>') a"
[PROOF STATE]
proof (prove)
using this:
recvmsg (R \<sigma>) a

goal (1 subgoal):
 1. recvmsg (R \<sigma>') a
[PROOF STEP]
proof (rule recvmsgE [where R=R])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. R \<sigma> m \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. R \<sigma> m \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
assume "R \<sigma> m"
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. R \<sigma> m \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m
[PROOF STEP]
show "R \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m

goal (1 subgoal):
 1. R \<sigma>' m
[PROOF STEP]
by (rule upreservesq)
[PROOF STATE]
proof (state)
this:
R \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>') a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (2 subgoals):
 1. \<And>\<sigma> p \<sigma>'. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); other U {i} \<sigma> \<sigma>'\<rbrakk> \<Longrightarrow> (\<sigma>', fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma>' m)
 2. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (1 subgoal):
 1. (\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m)
[PROOF STEP]
using qr
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>'))
snd pq \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<sigma>', fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma>' m)

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
case (local \<sigma> pq \<sigma>' pq' a)
[PROOF STATE]
proof (state)
this:
(\<sigma>, pq) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, pq), a, \<sigma>', pq') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
obtain p ms q p' ms' q' where "pq = (p, (ms, q))"
                              and "pq' = (p', (ms', q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p ms q p' ms' q'. \<lbrakk>pq = (p, ms, q); pq' = (p', ms', q')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases pq, cases pq') metis
[PROOF STATE]
proof (state)
this:
pq = (p, ms, q)
pq' = (p', ms', q')

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
with local.hyps local.IH
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, pq) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, pq), a, \<sigma>', pq') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)
pq = (p, ms, q)
pq' = (p', ms', q')
[PROOF STEP]
have pqtr: "((\<sigma>, (p, (ms, q))), a, (\<sigma>', (p', (ms', q'))))
                    \<in> oparp_sos i (trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)"
        and por: "(\<sigma>, p) \<in> oreachable A ?owS (other U {i})"
        and qr: "(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))"
        and "\<forall>m\<in>set ms. R \<sigma> m"
        and "?owS \<sigma> \<sigma>' a"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, pq) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, pq), a, \<sigma>', pq') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg)
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
(\<sigma>, fst pq) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd pq)). R \<sigma> m)
pq = (p, ms, q)
pq' = (p', ms', q')

goal (1 subgoal):
 1. (((\<sigma>, p, ms, q), a, \<sigma>', p', ms', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G) &&& (\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})) &&& (ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>)) &&& \<forall>m\<in>set ms. R \<sigma> m &&& otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
[PROOF STEP]
by (simp_all del: \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_simps)
[PROOF STATE]
proof (state)
this:
((\<sigma>, p, ms, q), a, \<sigma>', p', ms', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
\<forall>m\<in>set ms. R \<sigma> m
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (chain)
picking this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
[PROOF STEP]
have "\<forall>j. j\<noteq>i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. \<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by (clarsimp dest!: otherwith_syncD)
[PROOF STATE]
proof (state)
this:
\<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
with sgivesu
[PROOF STATE]
proof (chain)
picking this:
S ?\<xi> ?\<xi>' \<Longrightarrow> U ?\<xi> ?\<xi>'
\<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
have "\<forall>j. j\<noteq>i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
S ?\<xi> ?\<xi>' \<Longrightarrow> U ?\<xi> ?\<xi>'
\<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (chain)
picking this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
[PROOF STEP]
have "orecvmsg R \<sigma> a"
[PROOF STATE]
proof (prove)
using this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. orecvmsg R \<sigma> a
[PROOF STEP]
by (rule otherwithE)
[PROOF STATE]
proof (state)
this:
orecvmsg R \<sigma> a

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
hence "recvmsg (R \<sigma>) a"
[PROOF STATE]
proof (prove)
using this:
orecvmsg R \<sigma> a

goal (1 subgoal):
 1. recvmsg (R \<sigma>) a
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) a

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
from pqtr
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, p, ms, q), a, \<sigma>', p', ms', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)
[PROOF STEP]
have "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})
                  \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
                  \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p, ms, q), a, \<sigma>', p', ms', q') \<in> oparp_sos i (automaton.trans A) (seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G)

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
assume "((\<sigma>, p), a, (\<sigma>', p')) \<in> trans A"
         and "\<And>m. a \<noteq> receive m"
         and "(ms', q') = (ms, q)"
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
a \<noteq> receive ?m1
(ms', q') = (ms, q)

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
[PROOF STEP]
have ptr: "((\<sigma>, p), a, (\<sigma>', p')) \<in> trans A"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A

goal (1 subgoal):
 1. ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with pinv por and \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). U (\<sigma> i) (\<sigma>' i))
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
[PROOF STEP]
have "U (\<sigma> i) (\<sigma>' i)"
[PROOF STATE]
proof (prove)
using this:
A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). U (\<sigma> i) (\<sigma>' i))
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A

goal (1 subgoal):
 1. U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
by (auto dest!: ostep_invariantD)
[PROOF STATE]
proof (state)
this:
U (\<sigma> i) (\<sigma>' i)

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with \<open>\<forall>j. j\<noteq>i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
have "\<forall>j. U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)

goal (1 subgoal):
 1. \<forall>j. U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
hence recvmsg': "\<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
by (auto elim!: recvmsgE [where R=R] upreservesq)
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) ?a1 \<Longrightarrow> recvmsg (R \<sigma>') ?a1

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from por ptr \<open>?owS \<sigma> \<sigma>' a\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a
[PROOF STEP]
have "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
by - (rule oreachable_local')
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
from qr and \<open>(ms', q') = (ms, q)\<close>
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
(ms', q') = (ms, q)
[PROOF STEP]
have "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
(ms', q') = (ms, q)

goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
by (rule reachable_weakenE) (erule recvmsg')
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "\<forall>m\<in>set ms'. R \<sigma>' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
assume "m\<in>set ms'"
[PROOF STATE]
proof (state)
this:
m \<in> set ms'

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>(ms', q') = (ms, q)\<close>
[PROOF STATE]
proof (chain)
picking this:
(ms', q') = (ms, q)
m \<in> set ms'
[PROOF STEP]
have "m\<in>set ms"
[PROOF STATE]
proof (prove)
using this:
(ms', q') = (ms, q)
m \<in> set ms'

goal (1 subgoal):
 1. m \<in> set ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m \<in> set ms

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>m\<in>set ms. R \<sigma> m\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set ms. R \<sigma> m
m \<in> set ms
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set ms. R \<sigma> m
m \<in> set ms

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m
[PROOF STEP]
show "R \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m

goal (1 subgoal):
 1. R \<sigma>' m
[PROOF STEP]
by (rule upreservesq)
[PROOF STATE]
proof (state)
this:
R \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>set ms'. R \<sigma>' m

goal (3 subgoals):
 1. \<lbrakk>((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans A; \<And>m. a \<noteq> receive m; (ms', q') = (ms, q)\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 3. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
show
        "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})
          \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
          \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
assume qtr: "((ms, q), a, (ms', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G"
         and "\<And>m. a \<noteq> send m"
         and "p' = p"
         and "\<sigma>' i = \<sigma> i"
[PROOF STATE]
proof (state)
this:
((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
a \<noteq> send ?m1
p' = p
\<sigma>' i = \<sigma> i

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from this(4) and \<open>\<And>\<xi>. U \<xi> \<xi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<sigma>' i = \<sigma> i
U ?\<xi> ?\<xi>
[PROOF STEP]
have "U (\<sigma> i) (\<sigma>' i)"
[PROOF STATE]
proof (prove)
using this:
\<sigma>' i = \<sigma> i
U ?\<xi> ?\<xi>

goal (1 subgoal):
 1. U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U (\<sigma> i) (\<sigma>' i)

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with \<open>\<forall>j. j\<noteq>i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
have "\<forall>j. U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)

goal (1 subgoal):
 1. \<forall>j. U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
hence recvmsg': "\<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
by (auto elim!: recvmsgE [where R=R] upreservesq)
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) ?a1 \<Longrightarrow> recvmsg (R \<sigma>') ?a1

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from qtr
[PROOF STATE]
proof (chain)
picking this:
((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
[PROOF STEP]
have tqtr: "((ms, q), a, (ms', q')) \<in> trans qmsg"
[PROOF STATE]
proof (prove)
using this:
((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. ((ms, q), a, ms', q') \<in> automaton.trans qmsg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((ms, q), a, ms', q') \<in> automaton.trans qmsg

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close> and  \<open>\<sigma>' i = \<sigma> i\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
\<sigma>' i = \<sigma> i
[PROOF STEP]
have "other U {i} \<sigma> \<sigma>'"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
\<sigma>' i = \<sigma> i

goal (1 subgoal):
 1. other U {i} \<sigma> \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
other U {i} \<sigma> \<sigma>'

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with por and \<open>p' = p\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
p' = p
other U {i} \<sigma> \<sigma>'
[PROOF STEP]
have "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
p' = p
other U {i} \<sigma> \<sigma>'

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
by (auto dest: oreachable_other)
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
proof (rule reachable_weakenE [where P="recvmsg (R \<sigma>)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
 2. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
from qr tqtr \<open>recvmsg (R \<sigma>) a\<close>
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
((ms, q), a, ms', q') \<in> automaton.trans qmsg
recvmsg (R \<sigma>) a
[PROOF STEP]
show "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
((ms, q), a, ms', q') \<in> automaton.trans qmsg
recvmsg (R \<sigma>) a

goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
qed (rule recvmsg')
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "\<forall>m\<in>set ms'. R \<sigma>' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
assume "m \<in> set ms'"
[PROOF STATE]
proof (state)
this:
m \<in> set ms'

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<in> set ms'

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
have "case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
from qr
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "(ms, q) \<in> reachable qmsg TT"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (ms, q) \<in> reachable qmsg TT
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
using tqtr
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg TT
((ms, q), a, ms', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
by (auto dest!: step_invariantD [OF qmsg_queue_contents])
[PROOF STATE]
proof (state)
this:
case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<in> set ms'
case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
m \<in> set ms'
case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
using \<open>\<forall>m\<in>set ms. R \<sigma> m\<close> and \<open>orecvmsg R \<sigma> a\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> set ms'
case a of receive m \<Rightarrow> set ms' \<subseteq> set (ms @ [m]) | _ \<Rightarrow> set ms' \<subseteq> set ms
\<forall>m\<in>set ms. R \<sigma> m
orecvmsg R \<sigma> a

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m
[PROOF STEP]
show "R \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m

goal (1 subgoal):
 1. R \<sigma>' m
[PROOF STEP]
by (rule upreservesq)
[PROOF STATE]
proof (state)
this:
R \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>set ms'. R \<sigma>' m

goal (2 subgoals):
 1. \<lbrakk>((ms, q), a, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G; \<And>m. a \<noteq> send m; p' = p; \<sigma>' i = \<sigma> i\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
 2. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
show "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})
                     \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
                     \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
assume "a = \<tau>"
         and "((\<sigma>, p), receive m, (\<sigma>', p')) \<in> trans A"
         and "((ms, q), send m, (ms', q')) \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G"
[PROOF STATE]
proof (state)
this:
a = \<tau>
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from this(2-3)
[PROOF STATE]
proof (chain)
picking this:
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G
[PROOF STEP]
have ptr: "((\<sigma>, p), receive m, (\<sigma>', p')) \<in> trans A"
         and qtr: "((ms, q), send m, (ms', q')) \<in> trans qmsg"
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G

goal (1 subgoal):
 1. ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A &&& ((ms, q), send m, ms', q') \<in> automaton.trans qmsg
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
((ms, q), send m, ms', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from qr
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "(ms, q) \<in> reachable qmsg TT"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (ms, q) \<in> reachable qmsg TT
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with qtr
[PROOF STATE]
proof (chain)
picking this:
((ms, q), send m, ms', q') \<in> automaton.trans qmsg
(ms, q) \<in> reachable qmsg TT
[PROOF STEP]
have "m \<in> set ms"
[PROOF STATE]
proof (prove)
using this:
((ms, q), send m, ms', q') \<in> automaton.trans qmsg
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. m \<in> set ms
[PROOF STEP]
by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
[PROOF STATE]
proof (state)
this:
m \<in> set ms

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with \<open>\<forall>m\<in>set ms. R \<sigma> m\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set ms. R \<sigma> m
m \<in> set ms
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set ms. R \<sigma> m
m \<in> set ms

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
hence "orecvmsg R \<sigma> (receive m)"
[PROOF STATE]
proof (prove)
using this:
R \<sigma> m

goal (1 subgoal):
 1. orecvmsg R \<sigma> (receive m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
orecvmsg R \<sigma> (receive m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with \<open>\<forall>j. j\<noteq>i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)
orecvmsg R \<sigma> (receive m)
[PROOF STEP]
have "?owS \<sigma> \<sigma>' (receive m)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. j \<noteq> i \<longrightarrow> S (\<sigma> j) (\<sigma>' j)
orecvmsg R \<sigma> (receive m)

goal (1 subgoal):
 1. otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)
[PROOF STEP]
by (auto intro!: otherwithI)
[PROOF STATE]
proof (state)
this:
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with pinv por ptr
[PROOF STATE]
proof (chain)
picking this:
A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). U (\<sigma> i) (\<sigma>' i))
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)
[PROOF STEP]
have "U (\<sigma> i) (\<sigma>' i)"
[PROOF STATE]
proof (prove)
using this:
A \<Turnstile>\<^sub>A (otherwith S {i} (orecvmsg R), other U {i} \<rightarrow>) globala (\<lambda>(\<sigma>, uu_, \<sigma>'). U (\<sigma> i) (\<sigma>' i))
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)

goal (1 subgoal):
 1. U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
by (auto dest!: ostep_invariantD)
[PROOF STATE]
proof (state)
this:
U (\<sigma> i) (\<sigma>' i)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
with \<open>\<forall>j. j\<noteq>i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)
[PROOF STEP]
have "\<forall>j. U (\<sigma> j) (\<sigma>' j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. j \<noteq> i \<longrightarrow> U (\<sigma> j) (\<sigma>' j)
U (\<sigma> i) (\<sigma>' i)

goal (1 subgoal):
 1. \<forall>j. U (\<sigma> j) (\<sigma>' j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
hence recvmsg': "\<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
by (auto elim!: recvmsgE [where R=R] upreservesq)
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) ?a1 \<Longrightarrow> recvmsg (R \<sigma>') ?a1

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
from por ptr
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
[PROOF STEP]
have "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
using \<open>?owS \<sigma> \<sigma>' (receive m)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A
otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' (receive m)

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
[PROOF STEP]
by - (erule(1) oreachable_local, simp)
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
[PROOF STEP]
proof (rule reachable_weakenE [where P="recvmsg (R \<sigma>)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
 2. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
have "recvmsg (R \<sigma>) (send m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recvmsg (R \<sigma>) (send m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recvmsg (R \<sigma>) (send m)

goal (2 subgoals):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
 2. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
with qr qtr
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
((ms, q), send m, ms', q') \<in> automaton.trans qmsg
recvmsg (R \<sigma>) (send m)
[PROOF STEP]
show "(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
((ms, q), send m, ms', q') \<in> automaton.trans qmsg
recvmsg (R \<sigma>) (send m)

goal (1 subgoal):
 1. (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. \<And>a. recvmsg (R \<sigma>) a \<Longrightarrow> recvmsg (R \<sigma>') a
[PROOF STEP]
qed (rule recvmsg')
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
have "\<forall>m\<in>set ms'. R \<sigma>' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
assume "m \<in> set ms'"
[PROOF STATE]
proof (state)
this:
m \<in> set ms'

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<in> set ms'

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
have "set ms' \<subseteq> set ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ms' \<subseteq> set ms
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set ms' \<subseteq> set ms
[PROOF STEP]
from qr
[PROOF STATE]
proof (chain)
picking this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))
[PROOF STEP]
have "(ms, q) \<in> reachable qmsg TT"
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg (recvmsg (R \<sigma>))

goal (1 subgoal):
 1. (ms, q) \<in> reachable qmsg TT
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. set ms' \<subseteq> set ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg TT

goal (1 subgoal):
 1. set ms' \<subseteq> set ms
[PROOF STEP]
using qtr
[PROOF STATE]
proof (prove)
using this:
(ms, q) \<in> reachable qmsg TT
((ms, q), send m__, ms', q') \<in> automaton.trans qmsg

goal (1 subgoal):
 1. set ms' \<subseteq> set ms
[PROOF STEP]
by (auto dest!: step_invariantD [OF qmsg_queue_contents])
[PROOF STATE]
proof (state)
this:
set ms' \<subseteq> set ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set ms' \<subseteq> set ms

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<in> set ms'
set ms' \<subseteq> set ms
[PROOF STEP]
have "R \<sigma> m"
[PROOF STATE]
proof (prove)
using this:
m \<in> set ms'
set ms' \<subseteq> set ms

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
using \<open>\<forall>m\<in>set ms. R \<sigma> m\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> set ms'
set ms' \<subseteq> set ms
\<forall>m\<in>set ms. R \<sigma> m

goal (1 subgoal):
 1. R \<sigma> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R \<sigma> m

goal (1 subgoal):
 1. \<And>m. m \<in> set ms' \<Longrightarrow> R \<sigma>' m
[PROOF STEP]
with \<open>\<forall>j. U (\<sigma> j) (\<sigma>' j)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m
[PROOF STEP]
show "R \<sigma>' m"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. U (\<sigma> j) (\<sigma>' j)
R \<sigma> m

goal (1 subgoal):
 1. R \<sigma>' m
[PROOF STEP]
by (rule upreservesq)
[PROOF STATE]
proof (state)
this:
R \<sigma>' m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>set ms'. R \<sigma>' m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>a = \<tau>; ((\<sigma>, p), receive m, \<sigma>', p') \<in> automaton.trans A; ((ms, q), send m, ms', q') \<in> seqp_sos \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G\<rbrakk> \<Longrightarrow> (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m
[PROOF STEP]
show "(\<sigma>', p') \<in> oreachable A ?owS (other U {i})
                     \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
                     \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})
(ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>'))
\<forall>m\<in>set ms'. R \<sigma>' m

goal (1 subgoal):
 1. (\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)

goal (1 subgoal):
 1. \<And>\<sigma> p \<sigma>' p' a. \<lbrakk>(\<sigma>, p) \<in> oreachable (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg) (otherwith S {i} (orecvmsg R)) (other U {i}); (\<sigma>, fst p) \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p \<in> reachable qmsg (recvmsg (R \<sigma>)) \<and> (\<forall>m\<in>set (fst (snd p)). R \<sigma> m); ((\<sigma>, p), a, \<sigma>', p') \<in> automaton.trans (A \<langle>\<langle>\<^bsub>i\<^esub> qmsg); otherwith S {i} (orecvmsg R) \<sigma> \<sigma>' a\<rbrakk> \<Longrightarrow> (\<sigma>', fst p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd p' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd p')). R \<sigma>' m)
[PROOF STEP]
with \<open>pq = (p, (ms, q))\<close> and \<open>pq' = (p', (ms', q'))\<close>
[PROOF STATE]
proof (chain)
picking this:
pq = (p, ms, q)
pq' = (p', ms', q')
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pq = (p, ms, q)
pq' = (p', ms', q')
(\<sigma>', p') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> (ms', q') \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set ms'. R \<sigma>' m)

goal (1 subgoal):
 1. (\<sigma>', fst pq') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd pq')). R \<sigma>' m)
[PROOF STEP]
by (simp_all del: \<Gamma>\<^sub>Q\<^sub>M\<^sub>S\<^sub>G_simps)
[PROOF STATE]
proof (state)
this:
(\<sigma>', fst pq') \<in> oreachable A (otherwith S {i} (orecvmsg R)) (other U {i}) \<and> snd pq' \<in> reachable qmsg (recvmsg (R \<sigma>')) \<and> (\<forall>m\<in>set (fst (snd pq')). R \<sigma>' m)

goal:
No subgoals!
[PROOF STEP]
qed