[STATEMENT]
lemma weakComm1:
  fixes \<Psi>   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   A\<^sub>Q   :: "name list"
  and   \<Psi>\<^sub>Q   :: 'b

  assumes PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'"
  and     FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>"
  and     QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'"
  and     FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>"
  and     MeqK: "\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K"
  and     "A\<^sub>R \<sharp>* \<Psi>"
  and     "A\<^sub>R \<sharp>* P"
  and     "A\<^sub>R \<sharp>* Q"
  and     "A\<^sub>R \<sharp>* R"
  and     "A\<^sub>R \<sharp>* M"
  and     "A\<^sub>R \<sharp>* A\<^sub>Q"
  and     "A\<^sub>Q \<sharp>* \<Psi>"
  and     "A\<^sub>Q \<sharp>* P"
  and     "A\<^sub>Q \<sharp>* Q"
  and     "A\<^sub>Q \<sharp>* R"
  and     "A\<^sub>Q \<sharp>* K"
  and     "xvec \<sharp>* P"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from \<open>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* R\<close> \<open>A\<^sub>Q \<sharp>* K\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>Q\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* Q
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q
[PROOF STEP]
obtain A\<^sub>Q' where FrQ': "extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>" and "distinct A\<^sub>Q'" and "A\<^sub>Q' \<sharp>* \<Psi>" and "A\<^sub>Q' \<sharp>* P"
               and "A\<^sub>Q' \<sharp>* Q" and "A\<^sub>Q' \<sharp>* R" and "A\<^sub>Q' \<sharp>* K" and "A\<^sub>R \<sharp>* A\<^sub>Q'"
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* Q
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q

goal (1 subgoal):
 1. (\<And>A\<^sub>Q'. \<lbrakk>extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q'; A\<^sub>Q' \<sharp>* \<Psi>; A\<^sub>Q' \<sharp>* P; A\<^sub>Q' \<sharp>* Q; A\<^sub>Q' \<sharp>* R; A\<^sub>Q' \<sharp>* K; A\<^sub>R \<sharp>* A\<^sub>Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, P, Q, R, K, A\<^sub>R)" in distinctFrame) auto
[PROOF STATE]
proof (state)
this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
                           and RimpP'': "insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)"
                           and P''Trans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto>M\<lparr>N\<rparr> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q); \<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PChain \<open>A\<^sub>Q' \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
A\<^sub>Q' \<sharp>* P
[PROOF STEP]
have "A\<^sub>Q' \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
A\<^sub>Q' \<sharp>* P

goal (1 subgoal):
 1. A\<^sub>Q' \<sharp>* P''
[PROOF STEP]
by(rule tauChainFreshChain)
[PROOF STATE]
proof (state)
this:
A\<^sub>Q' \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
obtain A\<^sub>P'' \<Psi>\<^sub>P'' where FrP'': "extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>" and "A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)" and "distinct A\<^sub>P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>P'' \<Psi>\<^sub>P''. \<lbrakk>extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>; A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec); distinct A\<^sub>P''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule freshFrame)
[PROOF STATE]
proof (state)
this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)
distinct A\<^sub>P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
hence "A\<^sub>P'' \<sharp>* \<Psi>" and "A\<^sub>P'' \<sharp>* A\<^sub>Q'" and "A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q" and "A\<^sub>P'' \<sharp>* M" and "A\<^sub>P'' \<sharp>* R" and "A\<^sub>P'' \<sharp>* Q"
    and "A\<^sub>P'' \<sharp>* N" and "A\<^sub>P'' \<sharp>* K" and "A\<^sub>P'' \<sharp>* A\<^sub>R" and "A\<^sub>P'' \<sharp>* P''" and "A\<^sub>P'' \<sharp>* xvec" and "A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)
distinct A\<^sub>P''

goal (1 subgoal):
 1. ((A\<^sub>P'' \<sharp>* \<Psi> &&& A\<^sub>P'' \<sharp>* A\<^sub>Q' &&& A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q) &&& A\<^sub>P'' \<sharp>* M &&& A\<^sub>P'' \<sharp>* R &&& A\<^sub>P'' \<sharp>* Q) &&& (A\<^sub>P'' \<sharp>* N &&& A\<^sub>P'' \<sharp>* K &&& A\<^sub>P'' \<sharp>* A\<^sub>R) &&& A\<^sub>P'' \<sharp>* P'' &&& A\<^sub>P'' \<sharp>* xvec &&& A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* M
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* N
A\<^sub>P'' \<sharp>* K
A\<^sub>P'' \<sharp>* A\<^sub>R
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* xvec
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from FrR \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>Q' \<sharp>* R\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* R
[PROOF STEP]
have "A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* R

goal (1 subgoal):
 1. A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R
[PROOF STEP]
by(drule_tac extractFrameFreshChain) auto
[PROOF STATE]
proof (state)
this:
A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from FrQ' \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>R \<sharp>* Q\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* Q
[PROOF STEP]
have "A\<^sub>R \<sharp>* \<Psi>\<^sub>Q"
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* Q

goal (1 subgoal):
 1. A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
[PROOF STEP]
by(drule_tac extractFrameFreshChain) auto
[PROOF STATE]
proof (state)
this:
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PChain \<open>xvec \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
xvec \<sharp>* P
[PROOF STEP]
have "xvec \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
xvec \<sharp>* P

goal (1 subgoal):
 1. xvec \<sharp>* P''
[PROOF STEP]
by(force intro: tauChainFreshChain)+
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
have "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
[PROOF STEP]
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
with RimpP'' FrP'' FrR \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>Q\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
[PROOF STEP]
have "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
[PROOF STEP]
using freshCompChain
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?\<Psi>'\<rbrakk> \<Longrightarrow> ?xvec \<sharp>* (?\<Psi> \<otimes> ?\<Psi>')
\<lbrakk>?Xs \<sharp>* ?\<Psi>; ?Xs \<sharp>* ?\<Psi>'\<rbrakk> \<Longrightarrow> ?Xs \<sharp>* (?\<Psi> \<otimes> ?\<Psi>')

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
[PROOF STEP]
by(simp add: freshChainSimps)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
have "\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
have RImpP'': "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
by(rule FrameStatEqImpCompose)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PChain FrQ' \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P
[PROOF STEP]
have "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
by(rule tauChainPar1)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' \<open>distinct A\<^sub>P''\<close> \<open>distinct A\<^sub>Q'\<close> \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close>
        \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P''\<close> \<open>A\<^sub>Q' \<sharp>* Q\<close> \<open>A\<^sub>Q' \<sharp>* R\<close> \<open>A\<^sub>Q' \<sharp>* K\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* R\<close> \<open>A\<^sub>P'' \<sharp>* Q\<close>
        \<open>A\<^sub>P'' \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* M\<close> \<open>A\<^sub>Q \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* Q\<close> \<open>A\<^sub>R \<sharp>* M\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto> K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>P''
distinct A\<^sub>Q'
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* M
A\<^sub>Q \<sharp>* R
A\<^sub>R \<sharp>* Q
A\<^sub>R \<sharp>* M
[PROOF STEP]
obtain K' where "\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto>K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'" and "\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'" and "A\<^sub>Q' \<sharp>* K'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto> K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>P''
distinct A\<^sub>Q'
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* M
A\<^sub>Q \<sharp>* R
A\<^sub>R \<sharp>* Q
A\<^sub>R \<sharp>* M

goal (1 subgoal):
 1. (\<And>K'. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'; \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'; A\<^sub>Q' \<sharp>* K'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac comm1Aux) (assumption | simp)+
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
with P''Trans FrP''
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto>\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
using FrQ' \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P''\<close> \<open>A\<^sub>Q' \<sharp>* Q\<close>
    \<open>xvec \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* Q\<close> \<open>A\<^sub>P'' \<sharp>* M\<close>  \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q'\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
xvec \<sharp>* P''
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* M
A\<^sub>P'' \<sharp>* A\<^sub>Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
by(rule_tac Comm1)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
by(drule_tac tauActTauStepChain) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakComm2:
  fixes \<Psi>   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   A\<^sub>Q   :: "name list"
  and   \<Psi>\<^sub>Q   :: 'b

  assumes PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>"
  and     QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'"
  and     FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>"
  and     MeqK: "\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K"
  and     "A\<^sub>R \<sharp>* \<Psi>"
  and     "A\<^sub>R \<sharp>* P"
  and     "A\<^sub>R \<sharp>* Q"
  and     "A\<^sub>R \<sharp>* R"
  and     "A\<^sub>R \<sharp>* M"
  and     "A\<^sub>R \<sharp>* A\<^sub>Q"
  and     "A\<^sub>Q \<sharp>* \<Psi>"
  and     "A\<^sub>Q \<sharp>* P"
  and     "A\<^sub>Q \<sharp>* Q"
  and     "A\<^sub>Q \<sharp>* R"
  and     "A\<^sub>Q \<sharp>* K"
  and     "xvec \<sharp>* Q"
  and     "xvec \<sharp>* M"
  and     "xvec \<sharp>* A\<^sub>Q"
  and     "xvec \<sharp>* A\<^sub>R"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> (\<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from \<open>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* R\<close> \<open>A\<^sub>Q \<sharp>* K\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>Q\<close> \<open>xvec \<sharp>* A\<^sub>Q\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* Q
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q
xvec \<sharp>* A\<^sub>Q
[PROOF STEP]
obtain A\<^sub>Q' where FrQ': "extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>" and "distinct A\<^sub>Q'" and "A\<^sub>Q' \<sharp>* \<Psi>" and "A\<^sub>Q' \<sharp>* P"
               and "A\<^sub>Q' \<sharp>* Q" and "A\<^sub>Q' \<sharp>* R" and "A\<^sub>Q' \<sharp>* K" and "A\<^sub>R \<sharp>* A\<^sub>Q'" and "A\<^sub>Q' \<sharp>* xvec"
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* Q
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q
xvec \<sharp>* A\<^sub>Q

goal (1 subgoal):
 1. (\<And>A\<^sub>Q'. \<lbrakk>extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>; distinct A\<^sub>Q'; A\<^sub>Q' \<sharp>* \<Psi>; A\<^sub>Q' \<sharp>* P; A\<^sub>Q' \<sharp>* Q; A\<^sub>Q' \<sharp>* R; A\<^sub>Q' \<sharp>* K; A\<^sub>R \<sharp>* A\<^sub>Q'; A\<^sub>Q' \<sharp>* xvec\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, P, Q, R, K, A\<^sub>R, xvec)" in distinctFrame) auto
[PROOF STATE]
proof (state)
this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* xvec

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
                           and RimpP'': "insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)"
                           and P''Trans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q); \<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PChain \<open>A\<^sub>Q' \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
A\<^sub>Q' \<sharp>* P
[PROOF STEP]
have "A\<^sub>Q' \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
A\<^sub>Q' \<sharp>* P

goal (1 subgoal):
 1. A\<^sub>Q' \<sharp>* P''
[PROOF STEP]
by(rule tauChainFreshChain)
[PROOF STATE]
proof (state)
this:
A\<^sub>Q' \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
obtain A\<^sub>P'' \<Psi>\<^sub>P'' where FrP'': "extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>" and "A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)" and "distinct A\<^sub>P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>P'' \<Psi>\<^sub>P''. \<lbrakk>extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>; A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec); distinct A\<^sub>P''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule freshFrame)
[PROOF STATE]
proof (state)
this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)
distinct A\<^sub>P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
hence "A\<^sub>P'' \<sharp>* \<Psi>" and "A\<^sub>P'' \<sharp>* A\<^sub>Q'" and "A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q" and "A\<^sub>P'' \<sharp>* M" and "A\<^sub>P'' \<sharp>* R" and "A\<^sub>P'' \<sharp>* Q"
    and "A\<^sub>P'' \<sharp>* N" and "A\<^sub>P'' \<sharp>* K" and "A\<^sub>P'' \<sharp>* A\<^sub>R" and "A\<^sub>P'' \<sharp>* P''" and "A\<^sub>P'' \<sharp>* xvec" and "A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>P'' \<sharp>* (\<Psi>, A\<^sub>Q', \<Psi>\<^sub>Q, A\<^sub>R, \<Psi>\<^sub>R, M, N, K, R, Q, P'', xvec)
distinct A\<^sub>P''

goal (1 subgoal):
 1. ((A\<^sub>P'' \<sharp>* \<Psi> &&& A\<^sub>P'' \<sharp>* A\<^sub>Q' &&& A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q) &&& A\<^sub>P'' \<sharp>* M &&& A\<^sub>P'' \<sharp>* R &&& A\<^sub>P'' \<sharp>* Q) &&& (A\<^sub>P'' \<sharp>* N &&& A\<^sub>P'' \<sharp>* K &&& A\<^sub>P'' \<sharp>* A\<^sub>R) &&& A\<^sub>P'' \<sharp>* P'' &&& A\<^sub>P'' \<sharp>* xvec &&& A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* M
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* N
A\<^sub>P'' \<sharp>* K
A\<^sub>P'' \<sharp>* A\<^sub>R
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* xvec
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>R

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from FrR \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>Q' \<sharp>* R\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* R
[PROOF STEP]
have "A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* R

goal (1 subgoal):
 1. A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R
[PROOF STEP]
by(drule_tac extractFrameFreshChain) auto
[PROOF STATE]
proof (state)
this:
A\<^sub>Q' \<sharp>* \<Psi>\<^sub>R

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from FrQ' \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>R \<sharp>* Q\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* Q
[PROOF STEP]
have "A\<^sub>R \<sharp>* \<Psi>\<^sub>Q"
[PROOF STATE]
proof (prove)
using this:
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* Q

goal (1 subgoal):
 1. A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
[PROOF STEP]
by(drule_tac extractFrameFreshChain) auto
[PROOF STATE]
proof (state)
this:
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
have "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
[PROOF STEP]
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
with RimpP'' FrP'' FrR \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>Q\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
[PROOF STEP]
have "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
[PROOF STEP]
using freshCompChain
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<lbrakk>?xvec \<sharp>* ?\<Psi>; ?xvec \<sharp>* ?\<Psi>'\<rbrakk> \<Longrightarrow> ?xvec \<sharp>* (?\<Psi> \<otimes> ?\<Psi>')
\<lbrakk>?Xs \<sharp>* ?\<Psi>; ?Xs \<sharp>* ?\<Psi>'\<rbrakk> \<Longrightarrow> ?Xs \<sharp>* (?\<Psi> \<otimes> ?\<Psi>')

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
[PROOF STEP]
by(simp add: freshChainSimps)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
have "\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
have RImpP'': "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle>
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle>
\<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<otimes> \<Psi>\<^sub>P''\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
by(rule FrameStatEqImpCompose)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from PChain FrQ' \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P
[PROOF STEP]
have "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
[PROOF STEP]
by(rule tauChainPar1)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' \<open>distinct A\<^sub>P''\<close> \<open>distinct A\<^sub>Q'\<close> \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q'\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>Q'\<close>
        \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P''\<close> \<open>A\<^sub>Q' \<sharp>* Q\<close> \<open>A\<^sub>Q' \<sharp>* R\<close> \<open>A\<^sub>Q' \<sharp>* K\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* R\<close> \<open>A\<^sub>P'' \<sharp>* Q\<close>
        \<open>A\<^sub>P'' \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* M\<close> \<open>A\<^sub>Q \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* Q\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>xvec \<sharp>* A\<^sub>R\<close> \<open>xvec \<sharp>* M\<close> \<open>A\<^sub>Q' \<sharp>* xvec\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto> K\<lparr>N\<rparr> \<prec> Q'
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>P''
distinct A\<^sub>Q'
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* M
A\<^sub>Q \<sharp>* R
A\<^sub>R \<sharp>* Q
A\<^sub>R \<sharp>* M
xvec \<sharp>* A\<^sub>R
xvec \<sharp>* M
A\<^sub>Q' \<sharp>* xvec
[PROOF STEP]
obtain K' where "\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto>K'\<lparr>N\<rparr> \<prec> Q'" and "\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'" and "A\<^sub>Q' \<sharp>* K'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> Q \<longmapsto> K\<lparr>N\<rparr> \<prec> Q'
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', (\<Psi> \<otimes> \<Psi>\<^sub>P'') \<otimes> \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
distinct A\<^sub>P''
distinct A\<^sub>Q'
A\<^sub>P'' \<sharp>* A\<^sub>Q'
A\<^sub>R \<sharp>* A\<^sub>Q'
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
A\<^sub>Q' \<sharp>* R
A\<^sub>Q' \<sharp>* K
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* R
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* M
A\<^sub>Q \<sharp>* R
A\<^sub>R \<sharp>* Q
A\<^sub>R \<sharp>* M
xvec \<sharp>* A\<^sub>R
xvec \<sharp>* M
A\<^sub>Q' \<sharp>* xvec

goal (1 subgoal):
 1. (\<And>K'. \<lbrakk>\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>N\<rparr> \<prec> Q'; \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'; A\<^sub>Q' \<sharp>* K'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac comm2Aux) (assumption | simp)+
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>N\<rparr> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
with P''Trans FrP''
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>N\<rparr> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto>\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(P' \<parallel> Q')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>N\<rparr> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
using FrQ' \<open>A\<^sub>Q' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q' \<sharp>* P''\<close> \<open>A\<^sub>Q' \<sharp>* Q\<close>
    \<open>xvec \<sharp>* Q\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* P''\<close> \<open>A\<^sub>P'' \<sharp>* Q\<close> \<open>A\<^sub>P'' \<sharp>* M\<close>  \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q'\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<rhd> Q \<longmapsto> K'\<lparr>N\<rparr> \<prec> Q'
\<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K'
A\<^sub>Q' \<sharp>* K'
extractFrame Q = \<langle>A\<^sub>Q', \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q' \<sharp>* \<Psi>
A\<^sub>Q' \<sharp>* P''
A\<^sub>Q' \<sharp>* Q
xvec \<sharp>* Q
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* P''
A\<^sub>P'' \<sharp>* Q
A\<^sub>P'' \<sharp>* M
A\<^sub>P'' \<sharp>* A\<^sub>Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
by(rule_tac Comm2)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'
[PROOF STEP]
by(drule_tac tauActTauStepChain) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P' \<parallel> Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frameImpIntComposition:
  fixes \<Psi>  :: 'b
  and   \<Psi>' :: 'b
  and   A\<^sub>F :: "name list"
  and   \<Psi>\<^sub>F :: 'b

  assumes "\<Psi> \<simeq> \<Psi>'"

  shows "\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
by(rule frameIntComposition)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
by(simp add: FrameStatEq_def)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertAssertionStatImp:
  fixes F  :: "'b frame"
  and   \<Psi>  :: 'b
  and   G  :: "'b frame"
  and   \<Psi>' :: 'b

  assumes FeqG: "insertAssertion F \<Psi> \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>"
  and     "\<Psi> \<simeq> \<Psi>'"

  shows "insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
obtain A\<^sub>F \<Psi>\<^sub>F where FrF: "F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>" and "A\<^sub>F \<sharp>* \<Psi>" and "A\<^sub>F \<sharp>* \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>F \<Psi>\<^sub>F. \<lbrakk>F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>; A\<^sub>F \<sharp>* \<Psi>; A\<^sub>F \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, \<Psi>')" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
A\<^sub>F \<sharp>* \<Psi>
A\<^sub>F \<sharp>* \<Psi>'

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
obtain A\<^sub>G \<Psi>\<^sub>G where FrG: "G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>" and "A\<^sub>G \<sharp>* \<Psi>" and "A\<^sub>G \<sharp>* \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>G \<Psi>\<^sub>G. \<lbrakk>G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>; A\<^sub>G \<sharp>* \<Psi>; A\<^sub>G \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, \<Psi>')" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>G \<sharp>* \<Psi>
A\<^sub>G \<sharp>* \<Psi>'

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
from \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>
[PROOF STEP]
by (metis frameIntComposition FrameStatEqSym)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
from \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
by(rule frameIntComposition)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>
\<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>
\<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
using FeqG FrF FrG \<open>A\<^sub>F \<sharp>* \<Psi>\<close> \<open>A\<^sub>G \<sharp>* \<Psi>\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>F, \<Psi> \<otimes> \<Psi>\<^sub>F\<rangle>
\<langle>A\<^sub>G, \<Psi> \<otimes> \<Psi>\<^sub>G\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
insertAssertion F \<Psi> \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>
A\<^sub>G \<sharp>* \<Psi>
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
by(force simp add: FrameStatEq_def dest: FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
with FrF FrG \<open>A\<^sub>F \<sharp>* \<Psi>'\<close> \<open>A\<^sub>G \<sharp>* \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>'
A\<^sub>G \<sharp>* \<Psi>'
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>'
A\<^sub>G \<sharp>* \<Psi>'
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insertAssertion F \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion G \<Psi>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertAssertionStatEq:
  fixes F  :: "'b frame"
  and   \<Psi>  :: 'b
  and   G  :: "'b frame"
  and   \<Psi>' :: 'b

  assumes FeqG: "insertAssertion F \<Psi> \<simeq>\<^sub>F insertAssertion G \<Psi>"
  and     "\<Psi> \<simeq> \<Psi>'"

  shows "insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
obtain A\<^sub>F \<Psi>\<^sub>F where FrF: "F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>" and "A\<^sub>F \<sharp>* \<Psi>" and "A\<^sub>F \<sharp>* \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>F \<Psi>\<^sub>F. \<lbrakk>F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>; A\<^sub>F \<sharp>* \<Psi>; A\<^sub>F \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, \<Psi>')" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
A\<^sub>F \<sharp>* \<Psi>
A\<^sub>F \<sharp>* \<Psi>'

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
obtain A\<^sub>G \<Psi>\<^sub>G where FrG: "G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>" and "A\<^sub>G \<sharp>* \<Psi>" and "A\<^sub>G \<sharp>* \<Psi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>G \<Psi>\<^sub>G. \<lbrakk>G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>; A\<^sub>G \<sharp>* \<Psi>; A\<^sub>G \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, \<Psi>')" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>G \<sharp>* \<Psi>
A\<^sub>G \<sharp>* \<Psi>'

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
from FeqG FrF FrG \<open>A\<^sub>F \<sharp>* \<Psi>\<close> \<open>A\<^sub>G \<sharp>* \<Psi>\<close> \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion F \<Psi> \<simeq>\<^sub>F insertAssertion G \<Psi>
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>
A\<^sub>G \<sharp>* \<Psi>
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion F \<Psi> \<simeq>\<^sub>F insertAssertion G \<Psi>
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>
A\<^sub>G \<sharp>* \<Psi>
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
by simp (metis frameIntComposition FrameStatEqTrans FrameStatEqSym)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
with FrF FrG \<open>A\<^sub>F \<sharp>* \<Psi>'\<close> \<open>A\<^sub>G \<sharp>* \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>'
A\<^sub>G \<sharp>* \<Psi>'
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F = \<langle>A\<^sub>F, \<Psi>\<^sub>F\<rangle>
G = \<langle>A\<^sub>G, \<Psi>\<^sub>G\<rangle>
A\<^sub>F \<sharp>* \<Psi>'
A\<^sub>G \<sharp>* \<Psi>'
\<langle>A\<^sub>F, \<Psi>' \<otimes> \<Psi>\<^sub>F\<rangle> \<simeq>\<^sub>F \<langle>A\<^sub>G, \<Psi>' \<otimes> \<Psi>\<^sub>G\<rangle>

goal (1 subgoal):
 1. insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insertAssertion F \<Psi>' \<simeq>\<^sub>F insertAssertion G \<Psi>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakTransitionStatEq:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   \<Psi>'  :: 'b

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "\<Psi> \<simeq> \<Psi>'"

  shows "\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
                           and QeqP'': "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                           and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from PChain \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
by(rule tauChainStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from QeqP'' \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'
[PROOF STEP]
by(rule insertAssertionStatImp)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from P''Trans \<open>\<Psi> \<simeq> \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
\<Psi> \<simeq> \<Psi>'
[PROOF STEP]
have "\<Psi>' \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
by(rule statEqTransition)
[PROOF STATE]
proof (state)
this:
\<Psi>' \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'
\<Psi>' \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>'
\<Psi>' \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi>' : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transitionWeakTransition:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<longmapsto>\<alpha> \<prec> P'"
  and     "insertAssertion(extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame P) \<Psi>"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P) \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(fastforce intro: weakTransitionI)


[STATEMENT]
lemma weakPar1Guarded:
  fixes \<Psi>  :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "bn \<alpha> \<sharp>* Q"
  and     "guarded Q"

  shows "\<Psi> : (R \<parallel> Q) \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
obtain A\<^sub>Q \<Psi>\<^sub>Q where FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>" and "A\<^sub>Q \<sharp>* \<Psi>" and "A\<^sub>Q \<sharp>* P" and "A\<^sub>Q \<sharp>* \<alpha>" and "A\<^sub>Q \<sharp>* R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A\<^sub>Q \<Psi>\<^sub>Q. \<lbrakk>extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>; A\<^sub>Q \<sharp>* \<Psi>; A\<^sub>Q \<sharp>* P; A\<^sub>Q \<sharp>* \<alpha>; A\<^sub>Q \<sharp>* R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(\<Psi>, P, \<alpha>, R)" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* \<alpha>
A\<^sub>Q \<sharp>* R

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
from \<open>guarded Q\<close> FrQ
[PROOF STATE]
proof (chain)
picking this:
guarded Q
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>Q \<simeq> \<one>"
[PROOF STATE]
proof (prove)
using this:
guarded Q
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>Q \<simeq> \<one>
[PROOF STEP]
by(blast dest: guardedStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>Q \<simeq> \<one>

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
\<Psi>\<^sub>Q \<simeq> \<one>
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
\<Psi>\<^sub>Q \<simeq> \<one>

goal (1 subgoal):
 1. \<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(metis weakTransitionStatEq Identity AssertionStatEqSym compositionSym)
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
using FrQ \<open>bn \<alpha> \<sharp>* Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* P\<close> \<open>A\<^sub>Q \<sharp>* \<alpha>\<close> \<open>A\<^sub>Q \<sharp>* R\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
bn \<alpha> \<sharp>* Q
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P
A\<^sub>Q \<sharp>* \<alpha>
A\<^sub>Q \<sharp>* R

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
by(rule weakPar1)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q

goal:
No subgoals!
[PROOF STEP]
qed