[STATEMENT]
lemma DiamondOne:
fixes
  cfg cfg1 cfg2 :: "('p,'v,'s) configuration" and
  p q :: 'p and
  m m' :: "('p,'v) message"
assumes
  StepP: "cfg \<turnstile> m  \<mapsto> cfg1" and
  PNotQ: "p \<noteq> q" and
  Rec: "isReceiverOf p m" "\<not> (isReceiverOf p m')" and
  Rec': "isReceiverOf q m'" "\<not> (isReceiverOf q m)" and
  StepWithoutP: "cfg \<turnstile> m' \<mapsto> cfg2"
shows
  "\<exists> cfg' :: ('p,'v,'s) configuration . (cfg1 \<turnstile> m' \<mapsto> cfg')
        \<and> (cfg2 \<turnstile> m \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (InMsg p b)
[PROOF STATE]
proof (state)
this:
m = <p, inM b>

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from StepWithoutP ExistsMsg
[PROOF STATE]
proof (chain)
picking this:
cfg \<turnstile> m' \<mapsto> cfg2
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0
[PROOF STEP]
have " m' \<in># (msgs cfg) "
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m' \<mapsto> cfg2
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0

goal (1 subgoal):
 1. m' \<in># msgs cfg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m' \<in># msgs cfg

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence "m' \<in># (msgs cfg1)"
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg

goal (1 subgoal):
 1. m' \<in># msgs cfg1
[PROOF STEP]
using StepP Rec NoMessageLossStep le_neq_implies_less le_antisym
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg
cfg \<turnstile> m \<mapsto> cfg1
isReceiverOf p m
\<not> isReceiverOf p m'
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
\<lbrakk>?m \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. m' \<in># msgs cfg1
[PROOF STEP]
by (metis  gr_implies_not0 neq0_conv)
[PROOF STATE]
proof (state)
this:
m' \<in># msgs cfg1

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence EnM': "enabled cfg1 m'"
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg1

goal (1 subgoal):
 1. enabled cfg1 m'
[PROOF STEP]
using enabled_def
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg1
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg

goal (1 subgoal):
 1. enabled cfg1 m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg1 m'

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from StepP ExistsMsg
[PROOF STATE]
proof (chain)
picking this:
cfg \<turnstile> m \<mapsto> cfg1
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0
[PROOF STEP]
have "m \<in># (msgs cfg) "
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0

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

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence "m \<in># (msgs cfg2)"
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg

goal (1 subgoal):
 1. m \<in># msgs cfg2
[PROOF STEP]
using StepWithoutP Rec' NoMessageLossStep
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'

goal (1 subgoal):
 1. m \<in># msgs cfg2
[PROOF STEP]
by (metis le_0_eq neq0_conv)
[PROOF STATE]
proof (state)
this:
m \<in># msgs cfg2

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence EnM: "enabled cfg2 m"
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg2

goal (1 subgoal):
 1. enabled cfg2 m
[PROOF STEP]
using enabled_def
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg2
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg

goal (1 subgoal):
 1. enabled cfg2 m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg2 m

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
assume CaseM:  "m = <p, inM b>"
[PROOF STATE]
proof (state)
this:
m = <p, inM b>

goal (3 subgoals):
 1. \<And>x11 x12. m = <x11, inM x12> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m = <p, inM b>

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (cases m')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. \<lbrakk>m = <p, inM b>; m' = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (OutMsg b')
[PROOF STATE]
proof (state)
this:
m' = <\<bottom>, outM b'>

goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. \<lbrakk>m = <p, inM b>; m' = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m' = <\<bottom>, outM b'>

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using StepWithoutP
[PROOF STATE]
proof (prove)
using this:
m' = <\<bottom>, outM b'>
cfg \<turnstile> m' \<mapsto> cfg2

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (InMsg q b')
[PROOF STATE]
proof (state)
this:
m' = <q, inM b'>

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
define cfg' where "cfg' = \<lparr>states = \<lambda>s. (
      if s = q then
        trans q (states cfg q) (Bool b')
      else if s = p then
        trans p (states cfg p) (Bool b)
      else
        states cfg s),
      msgs = ((sends q (states cfg q) (Bool b'))
        \<union># (((sends p (states cfg p) (Bool b))
            \<union># ((msgs cfg)-# m)) -# m'))\<rparr> "
[PROOF STATE]
proof (state)
this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m'\<rparr>

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
have StepP': "(cfg1 \<turnstile> m' \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
using StepP  EnM' Rec
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
enabled cfg1 m'
isReceiverOf p m
\<not> isReceiverOf p m'

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
unfolding cfg'_def InMsg CaseM
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> <p, inM b> \<mapsto> cfg1
enabled cfg1 <q, inM b'>
isReceiverOf p <p, inM b>
\<not> isReceiverOf p <q, inM b'>

goal (1 subgoal):
 1. cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from EnM
[PROOF STATE]
proof (chain)
picking this:
enabled cfg2 m
[PROOF STEP]
have "(cfg2 \<turnstile> m \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using InMsg cfg'_def StepP StepP' StepWithoutP NoReceivingNoChange
            Rec' CaseM EnM'
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m
m' = <q, inM b'>
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg \<turnstile> m' \<mapsto> cfg2
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; \<not> isReceiverOf ?p ?m\<rbrakk> \<Longrightarrow> states ?cfg1.0 ?p = states ?cfg2.0 ?p
isReceiverOf q m'
\<not> isReceiverOf q m
m = <p, inM b>
enabled cfg1 m'

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (simp, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
assume msgCfg:
        "msgs cfg1 = (sends p (states cfg p) (Bool b)
                     \<union># (msgs cfg -# <p, inM b>))"
        "msgs cfg2 = (sends q (states cfg q) (Bool b')
                     \<union># (msgs cfg -# <q, inM b'>))"
[PROOF STATE]
proof (state)
this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
have "enabled cfg m" "enabled cfg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
using StepP StepWithoutP CaseM InMsg
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
m = <p, inM b>
m' = <q, inM b'>

goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
with msgCfg
[PROOF STATE]
proof (chain)
picking this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'
[PROOF STEP]
show
        "(sends q (states cfg q) (Bool b') \<union># (msgs cfg1 -# <q, inM b'>)) =
         (sends p (states cfg p) (Bool b) \<union># (msgs cfg2 -# <p, inM b>))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
using CaseM InMsg StepP StepWithoutP Rec' AXc[of "m'" "m" "msgs cfg"
          "sends q (states cfg q) (Bool b')"
          "sends p (states cfg p) (Bool b)"]
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'
m = <p, inM b>
m' = <q, inM b'>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Bool b) \<union># sends q (states cfg q) (Bool b') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
unfolding enabled_def
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
m \<in># msgs cfg
m' \<in># msgs cfg
m = <p, inM b>
m' = <q, inM b'>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Bool b) \<union># sends q (states cfg q) (Bool b') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cfg2 \<turnstile> m \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, inM b>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (Msg q v')
[PROOF STATE]
proof (state)
this:
m' = <q, v'>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
define cfg' where "cfg' = \<lparr>states = \<lambda>s. (
      if s = q then
        trans q (states cfg q) (Value v')
      else if s = p then
        trans p (states cfg p) (Bool b)
      else
        states cfg s),
      msgs = ((sends q (states cfg q) (Value v'))
        \<union># (((sends p (states cfg p) (Bool b))
            \<union># ((msgs cfg)-# m))
            -# m'))\<rparr>"
[PROOF STATE]
proof (state)
this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m'\<rparr>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
have StepP': "(cfg1 \<turnstile> m' \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
using StepP EnM' Rec
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
enabled cfg1 m'
isReceiverOf p m
\<not> isReceiverOf p m'

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
unfolding Msg CaseM cfg'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> <p, inM b> \<mapsto> cfg1
enabled cfg1 <q, v'>
isReceiverOf p <p, inM b>
\<not> isReceiverOf p <q, v'>

goal (1 subgoal):
 1. cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'>\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from EnM
[PROOF STATE]
proof (chain)
picking this:
enabled cfg2 m
[PROOF STEP]
have "(cfg2 \<turnstile> m \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using Msg cfg'_def StepP StepP' StepWithoutP NoReceivingNoChange Rec' CaseM EnM'
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m
m' = <q, v'>
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg \<turnstile> m' \<mapsto> cfg2
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; \<not> isReceiverOf ?p ?m\<rbrakk> \<Longrightarrow> states ?cfg1.0 ?p = states ?cfg2.0 ?p
isReceiverOf q m'
\<not> isReceiverOf q m
m = <p, inM b>
enabled cfg1 m'

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (simp,clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
assume msgCfg1:
        "msgs cfg1 = (sends p (states cfg p) (Bool b)
                      \<union># (msgs cfg -# <p, inM b>))"
        "msgs cfg2 = (sends q (states cfg q) (Value v')
                      \<union># (msgs cfg -# <q,  v'>))"
[PROOF STATE]
proof (state)
this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
have "enabled cfg m" "enabled cfg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
using StepP StepWithoutP CaseM Msg
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
m = <p, inM b>
m' = <q, v'>

goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, inM b>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, inM b>; cfg \<turnstile> <p, inM b> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Bool b) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, inM b>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, inM b>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Bool b)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Bool b) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, inM b>; msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
with msgCfg1
[PROOF STATE]
proof (chain)
picking this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'
[PROOF STEP]
show
        "(sends q (states cfg q) (Value v') \<union># (msgs cfg1 -# <q, v'>)) =
         (sends p (states cfg p) (Bool b) \<union># (msgs cfg2 -# <p, inM b>))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
using CaseM Msg StepP StepWithoutP Rec' AXc[of "m'" "m" "msgs cfg"
          "sends q (states cfg q) (Value v')"
          "sends p (states cfg p) (Bool b)"]
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'
m = <p, inM b>
m' = <q, v'>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Bool b) \<union># sends q (states cfg q) (Value v') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
unfolding enabled_def
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Bool b) \<union># msgs cfg -# <p, inM b>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
m \<in># msgs cfg
m' \<in># msgs cfg
m = <p, inM b>
m' = <q, v'>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Bool b) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Bool b) \<union># sends q (states cfg q) (Value v') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Bool b) \<union># msgs cfg2 -# <p, inM b>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, inM b>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (OutMsg b)
[PROOF STATE]
proof (state)
this:
m = <\<bottom>, outM b>

goal (2 subgoals):
 1. \<And>x2. m = <\<bottom>, outM x2> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b>

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using StepP
[PROOF STATE]
proof (prove)
using this:
m = <\<bottom>, outM b>
cfg \<turnstile> m \<mapsto> cfg1

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (Msg p v)
[PROOF STATE]
proof (state)
this:
m = <p, v>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from StepWithoutP ExistsMsg
[PROOF STATE]
proof (chain)
picking this:
cfg \<turnstile> m' \<mapsto> cfg2
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0
[PROOF STEP]
have " m' \<in># (msgs cfg) "
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m' \<mapsto> cfg2
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0

goal (1 subgoal):
 1. m' \<in># msgs cfg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m' \<in># msgs cfg

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence "m' \<in># (msgs cfg1)"
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg

goal (1 subgoal):
 1. m' \<in># msgs cfg1
[PROOF STEP]
using StepP Rec NoMessageLossStep le_neq_implies_less le_antisym
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg
cfg \<turnstile> m \<mapsto> cfg1
isReceiverOf p m
\<not> isReceiverOf p m'
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
\<lbrakk>?m \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m = ?n

goal (1 subgoal):
 1. m' \<in># msgs cfg1
[PROOF STEP]
by (metis  gr_implies_not0 neq0_conv)
[PROOF STATE]
proof (state)
this:
m' \<in># msgs cfg1

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence EnM': "enabled cfg1 m'"
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg1

goal (1 subgoal):
 1. enabled cfg1 m'
[PROOF STEP]
using enabled_def
[PROOF STATE]
proof (prove)
using this:
m' \<in># msgs cfg1
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg

goal (1 subgoal):
 1. enabled cfg1 m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg1 m'

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from StepP ExistsMsg
[PROOF STATE]
proof (chain)
picking this:
cfg \<turnstile> m \<mapsto> cfg1
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0
[PROOF STEP]
have "m \<in># (msgs cfg) "
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0 \<Longrightarrow> ?m \<in># msgs ?cfg1.0

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

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence "m \<in># (msgs cfg2)"
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg

goal (1 subgoal):
 1. m \<in># msgs cfg2
[PROOF STEP]
using StepWithoutP Rec' NoMessageLossStep
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'\<rbrakk> \<Longrightarrow> msgs ?cfg1.0 ?m' \<le> msgs ?cfg2.0 ?m'

goal (1 subgoal):
 1. m \<in># msgs cfg2
[PROOF STEP]
by (metis le_0_eq neq0_conv)
[PROOF STATE]
proof (state)
this:
m \<in># msgs cfg2

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence EnM: "enabled cfg2 m"
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg2

goal (1 subgoal):
 1. enabled cfg2 m
[PROOF STEP]
using enabled_def
[PROOF STATE]
proof (prove)
using this:
m \<in># msgs cfg2
enabled ?cfg ?msg \<equiv> ?msg \<in># msgs ?cfg

goal (1 subgoal):
 1. enabled cfg2 m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg2 m

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
assume CaseM:  "m = <p, v>"
[PROOF STATE]
proof (state)
this:
m = <p, v>

goal (1 subgoal):
 1. \<And>x31 x32. m = <x31, x32> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m = <p, v>

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (cases m')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. \<lbrakk>m = <p, v>; m' = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (OutMsg b')
[PROOF STATE]
proof (state)
this:
m' = <\<bottom>, outM b'>

goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x2. \<lbrakk>m = <p, v>; m' = <\<bottom>, outM x2>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 3. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m' = <\<bottom>, outM b'>

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using StepWithoutP
[PROOF STATE]
proof (prove)
using this:
m' = <\<bottom>, outM b'>
cfg \<turnstile> m' \<mapsto> cfg2

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (InMsg q b')
[PROOF STATE]
proof (state)
this:
m' = <q, inM b'>

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
define cfg' where "cfg' = \<lparr>states = \<lambda>s. (
      if s = q then
        trans q (states cfg q) (Bool b')
      else if s = p then
        trans p (states cfg p) (Value v)
      else
        states cfg s),
      msgs = ((sends q (states cfg q) (Bool b'))
        \<union># (((sends p (states cfg p) (Value v))
        \<union># ((msgs cfg)-# m))
        -# m'))\<rparr> "
[PROOF STATE]
proof (state)
this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence StepP': "(cfg1 \<turnstile> m' \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
using StepP InMsg EnM' Rec CaseM
[PROOF STATE]
proof (prove)
using this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
m' = <q, inM b'>
enabled cfg1 m'
isReceiverOf p m
\<not> isReceiverOf p m'
m = <p, v>

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from EnM
[PROOF STATE]
proof (chain)
picking this:
enabled cfg2 m
[PROOF STEP]
have "(cfg2 \<turnstile> m \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using InMsg cfg'_def StepP StepP' StepWithoutP NoReceivingNoChange Rec'
            CaseM EnM'
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m
m' = <q, inM b'>
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg \<turnstile> m' \<mapsto> cfg2
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; \<not> isReceiverOf ?p ?m\<rbrakk> \<Longrightarrow> states ?cfg1.0 ?p = states ?cfg2.0 ?p
isReceiverOf q m'
\<not> isReceiverOf q m
m = <p, v>
enabled cfg1 m'

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (simp, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
assume msgCfg:
        "msgs cfg1 = (sends p (states cfg p) (Value v)
          \<union># (msgs cfg -# <p, v>))"
        "msgs cfg2 = (sends q (states cfg q) (Bool b')
          \<union># (msgs cfg -# <q, inM b'>))"
[PROOF STATE]
proof (state)
this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
have "enabled cfg m" "enabled cfg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
using StepP StepWithoutP CaseM InMsg
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
m = <p, v>
m' = <q, inM b'>

goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, inM b'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Bool b') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>\<rparr>; cfg \<turnstile> <q, inM b'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, inM b'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, inM b'>; m' = <q, inM b'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Bool b')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, inM b'>; sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'>; enabled cfg <q, inM b'>; msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>; sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, inM b'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
with msgCfg
[PROOF STATE]
proof (chain)
picking this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'
[PROOF STEP]
show " (sends q (states cfg q) (Bool b')
                         \<union># (msgs cfg1 -# <q, inM b'>))
                       = (sends p (states cfg p) (Value v)
                         \<union># (msgs cfg2 -# <p, v>))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
using CaseM StepP StepWithoutP Rec' InMsg AXc[of "m'" "m" "msgs cfg"
          "sends q (states cfg q) (Bool b')"
          "sends p (states cfg p) (Value v)"]
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
enabled cfg m
enabled cfg m'
m = <p, v>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
m' = <q, inM b'>
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Value v) \<union># sends q (states cfg q) (Bool b') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
unfolding enabled_def
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Bool b') \<union># msgs cfg -# <q, inM b'>
m \<in># msgs cfg
m' \<in># msgs cfg
m = <p, v>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
m' = <q, inM b'>
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Bool b') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Value v) \<union># sends q (states cfg q) (Bool b') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sends q (states cfg q) (Bool b') \<union># msgs cfg1 -# <q, inM b'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cfg2 \<turnstile> m \<mapsto> cfg'

goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>m = <p, v>; m' = <x11, inM x12>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
 2. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
case (Msg q v')
[PROOF STATE]
proof (state)
this:
m' = <q, v'>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
define cfg' where "cfg' = \<lparr>states = \<lambda>s. (
      if s = q then
        trans q (states cfg q) (Value v')
      else if s = p then
        trans p (states cfg p) (Value v)
      else
        states cfg s),
      msgs = ((sends q (states cfg q) (Value v'))
        \<union># (((sends p (states cfg p) (Value v))
        \<union># ((msgs cfg)-# m))
        -# m'))\<rparr> "
[PROOF STATE]
proof (state)
this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
hence StepP': "(cfg1 \<turnstile> m' \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
using StepP Msg EnM' Rec CaseM
[PROOF STATE]
proof (prove)
using this:
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
m' = <q, v'>
enabled cfg1 m'
isReceiverOf p m
\<not> isReceiverOf p m'
m = <p, v>

goal (1 subgoal):
 1. cfg1 \<turnstile> m' \<mapsto> cfg'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> m' \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
from EnM
[PROOF STATE]
proof (chain)
picking this:
enabled cfg2 m
[PROOF STEP]
have "(cfg2 \<turnstile> m \<mapsto> cfg')"
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
using Msg cfg'_def StepP StepP' StepWithoutP NoReceivingNoChange Rec' CaseM EnM'
[PROOF STATE]
proof (prove)
using this:
enabled cfg2 m
m' = <q, v'>
cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m'\<rparr>
cfg \<turnstile> m \<mapsto> cfg1
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg \<turnstile> m' \<mapsto> cfg2
\<lbrakk>?cfg1.0 \<turnstile> ?m \<mapsto> ?cfg2.0; \<not> isReceiverOf ?p ?m\<rbrakk> \<Longrightarrow> states ?cfg1.0 ?p = states ?cfg2.0 ?p
isReceiverOf q m'
\<not> isReceiverOf q m
m = <p, v>
enabled cfg1 m'

goal (1 subgoal):
 1. cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
proof (simp, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
assume msgCfg:
        "msgs cfg1 = (sends p (states cfg p) (Value v)
          \<union># (msgs cfg -# <p, v>))"
        "msgs cfg2 = (sends q (states cfg q) (Value v')
          \<union># (msgs cfg -# <q, v'>))"
[PROOF STATE]
proof (state)
this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
have "enabled cfg m" "enabled cfg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
using StepP StepWithoutP CaseM Msg
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
m = <p, v>
m' = <q, v'>

goal (1 subgoal):
 1. enabled cfg m &&& enabled cfg m'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. \<lbrakk>enabled cfg2 <p, v>; cfg' = \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; q = q; q \<noteq> p; enabled cfg2 <p, v>; cfg \<turnstile> <p, v> \<mapsto> cfg1; cfg1 \<turnstile> <q, v'> \<mapsto> \<lparr>states = \<lambda>s. if s = q then trans q (states cfg q) (Value v') else if s = p then trans p (states cfg p) (Value v) else states cfg s, msgs = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>\<rparr>; cfg \<turnstile> <q, v'> \<mapsto> cfg2; \<And>cfg1 m cfg2 p. \<lbrakk>cfg1 \<turnstile> m \<mapsto> cfg2; \<not> isReceiverOf p m\<rbrakk> \<Longrightarrow> states cfg1 p = states cfg2 p; isReceiverOf q <q, v'>; \<not> isReceiverOf q <p, v>; enabled cfg1 <q, v'>; m' = <q, v'>; m = <p, v>; \<forall>s. (s = p \<longrightarrow> states cfg1 p = trans p (states cfg p) (Value v)) \<and> (s \<noteq> p \<longrightarrow> states cfg1 s = states cfg s); \<forall>s. s \<noteq> q \<longrightarrow> (if s = p then trans p (states cfg p) (Value v) else states cfg s) = states cfg1 s; \<forall>s. (s = q \<longrightarrow> states cfg2 q = trans q (states cfg q) (Value v')) \<and> (s \<noteq> q \<longrightarrow> states cfg2 s = states cfg s); enabled cfg <p, v>; msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>; enabled cfg1 <q, v'>; sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'> = sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'>; enabled cfg <q, v'>; msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>; sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v> -# <q, v'>\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
with msgCfg
[PROOF STATE]
proof (chain)
picking this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'
[PROOF STEP]
show " (sends q (states cfg q) (Value v')
                         \<union># (msgs cfg1 -# <q, v'>))
                       = (sends p (states cfg p) (Value v)
                         \<union># (msgs cfg2 -# <p, v>))"
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
using CaseM StepP StepWithoutP Rec' Msg
          AXc[of "m'" "m" "msgs cfg" "sends q (states cfg q) (Value v')"
          "sends p (states cfg p) (Value v)"]
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
enabled cfg m
enabled cfg m'
m = <p, v>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
m' = <q, v'>
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Value v) \<union># sends q (states cfg q) (Value v') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
unfolding enabled_def
[PROOF STATE]
proof (prove)
using this:
msgs cfg1 = sends p (states cfg p) (Value v) \<union># msgs cfg -# <p, v>
msgs cfg2 = sends q (states cfg q) (Value v') \<union># msgs cfg -# <q, v'>
m \<in># msgs cfg
m' \<in># msgs cfg
m = <p, v>
cfg \<turnstile> m \<mapsto> cfg1
cfg \<turnstile> m' \<mapsto> cfg2
isReceiverOf q m'
\<not> isReceiverOf q m
m' = <q, v'>
\<lbrakk>m' \<noteq> m; m' \<in># msgs cfg; m \<in># msgs cfg\<rbrakk> \<Longrightarrow> sends q (states cfg q) (Value v') \<union># sends p (states cfg p) (Value v) \<union># msgs cfg -# m -# m' = sends p (states cfg p) (Value v) \<union># sends q (states cfg q) (Value v') \<union># msgs cfg -# m' -# m

goal (1 subgoal):
 1. sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
sends q (states cfg q) (Value v') \<union># msgs cfg1 -# <q, v'> = sends p (states cfg p) (Value v) \<union># msgs cfg2 -# <p, v>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>m = <p, v>; m' = <x31, x32>\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> m' \<mapsto> cfg'
cfg2 \<turnstile> m \<mapsto> cfg'

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> m' \<mapsto> cfg' \<and> cfg2 \<turnstile> m \<mapsto> cfg'

goal:
No subgoals!
[PROOF STEP]
qed