[STATEMENT]
lemma weakOutput:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   K    :: 'a
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<turnstile> M \<leftrightarrow> K"
  and     Qeq\<Psi>: "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"

  shows "\<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
have "\<Psi> \<rhd>  M\<langle>N\<rangle>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<langle>N\<rangle>.P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<langle>N\<rangle>.P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<langle>N\<rangle>.P

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

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
from Qeq\<Psi>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
have "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame(M\<langle>N\<rangle>.P)) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi>

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

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
have "insertAssertion (extractFrame(M\<langle>N\<rangle>.P)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame(M\<langle>N\<rangle>.P)) \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<langle>N\<rangle>.P)) \<Psi>

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

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
from \<open>\<Psi> \<turnstile> M \<leftrightarrow> K\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<turnstile> M \<leftrightarrow> K
[PROOF STEP]
have "\<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto>K\<langle>N\<rangle> \<prec> P"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<turnstile> M \<leftrightarrow> K

goal (1 subgoal):
 1. \<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto> K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
by(rule Output)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<langle>N\<rangle>.P \<longmapsto> K\<langle>N\<rangle> \<prec> P

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

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P
[PROOF STEP]
by(rule_tac weakTransitionI) auto
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> M\<langle>N\<rangle>.P \<Longrightarrow>K\<langle>N\<rangle> \<prec> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertGuardedAssertion:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "insertAssertion(extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[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>"
[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>\<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>

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
from \<open>guarded P\<close> FrP
[PROOF STATE]
proof (chain)
picking this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>P \<simeq> \<one>" and "supp \<Psi>\<^sub>P = ({}::name set)"
[PROOF STATE]
proof (prove)
using this:
guarded P
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>P \<simeq> \<one> &&& supp \<Psi>\<^sub>P = {}
[PROOF STEP]
by(blast dest: guardedStatEq)+
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>P \<simeq> \<one>
supp \<Psi>\<^sub>P = {}

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

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by simp (metis frameIntCompositionSym)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>

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

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

goal (1 subgoal):
 1. \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(rule_tac frameResFreshChain) auto
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle>
\<langle>A\<^sub>P, \<Psi> \<otimes> \<one>\<rangle> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
by(rule FrameStatEqTrans)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCase:
  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   R    :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "(\<phi>, P) mem CsP"
  and     "\<Psi> \<turnstile> \<phi>"
  and     "guarded P"
  and     RImpQ: "insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>"
  and     ImpR: "insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>"

  shows "\<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> Cases CsP \<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> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
proof(case_tac "P = P''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume "P = P''"
[PROOF STATE]
proof (state)
this:
P = P''

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
have "\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> Cases CsP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> Cases CsP
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> Cases CsP

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> Cases CsP

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from ImpR AssertionStatEq_def
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
?\<Psi> \<simeq> ?\<Psi>' \<equiv> ?\<Psi> \<hookrightarrow> ?\<Psi>' \<and> ?\<Psi>' \<hookrightarrow> ?\<Psi>
[PROOF STEP]
have "insertAssertion(extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame(Cases CsP)) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
?\<Psi> \<simeq> ?\<Psi>' \<equiv> ?\<Psi> \<hookrightarrow> ?\<Psi>' \<and> ?\<Psi>' \<hookrightarrow> ?\<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (Cases CsP)) \<Psi>
[PROOF STEP]
by(rule_tac FrameStatImpTrans) (auto intro: Identity)+
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (Cases CsP)) \<Psi>

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (Cases CsP)) \<Psi>

goal (2 subgoals):
 1. P = P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
 2. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
from P''Trans \<open>(\<phi>, P) mem CsP\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close> \<open>P = P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
P = P''
[PROOF STEP]
have "\<Psi> \<rhd> Cases CsP \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
P = P''

goal (1 subgoal):
 1. \<Psi> \<rhd> Cases CsP \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
by(blast intro: Case)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsP \<longmapsto> \<alpha> \<prec> P'

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

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

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
assume "P \<noteq> P''"
[PROOF STATE]
proof (state)
this:
P \<noteq> P''

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
with PChain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
P \<noteq> P''
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
P \<noteq> P''

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

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P''
[PROOF STEP]
using \<open>(\<phi>, P) mem CsP\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P''
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P

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

goal (1 subgoal):
 1. P \<noteq> P'' \<Longrightarrow> \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
hence "\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P''

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

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

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

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

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

goal (1 subgoal):
 1. \<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
using P''Trans
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakOpen:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     "x \<in> supp N"
  and     "x \<sharp> \<Psi>"
  and     "x \<sharp> M"
  and     "x \<sharp> xvec"
  and     "x \<sharp> yvec"

  shows "\<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<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>M\<lparr>\<nu>*(xvec@yvec)\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<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> M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<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> M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from PChain \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> \<Psi>
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> \<Psi>

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

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P''

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from QeqP'' \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
x \<sharp> \<Psi>
[PROOF STEP]
have "insertAssertion (extractFrame(\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame(\<lparr>\<nu>x\<rparr>P'')) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
x \<sharp> \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>
[PROOF STEP]
by(force intro: frameImpResPres)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from P''Trans \<open>x \<in> supp N\<close> \<open>x \<sharp> \<Psi>\<close> \<open>x \<sharp> M\<close> \<open>x \<sharp> xvec\<close> \<open>x \<sharp> yvec\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
x \<in> supp N
x \<sharp> \<Psi>
x \<sharp> M
x \<sharp> xvec
x \<sharp> yvec
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P'' \<longmapsto>M\<lparr>\<nu>*(xvec@x#yvec)\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
x \<in> supp N
x \<sharp> \<Psi>
x \<sharp> M
x \<sharp> xvec
x \<sharp> yvec

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
by(rule Open)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P''
insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P''
insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P'' \<longmapsto> M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakScope:
  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 PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "x \<sharp> \<Psi>"
  and     "x \<sharp> \<alpha>"

  shows "\<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<alpha> \<prec> \<lparr>\<nu>x\<rparr>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> : \<lparr>\<nu>x\<rparr>Q \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<alpha> \<prec> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
from PChain \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> \<Psi>
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> \<Psi>

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

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

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>
[PROOF STEP]
by(force intro: frameImpResPres)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (\<lparr>\<nu>x\<rparr>P'')) \<Psi>

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakPar1:
  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>\<alpha> \<prec> P'"
  and     FrQ: "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>"
  and     "bn \<alpha> \<sharp>* Q"
  and     "A\<^sub>Q \<sharp>* \<Psi>"
  and     "A\<^sub>Q \<sharp>* P"
  and     "A\<^sub>Q \<sharp>* \<alpha>"
  and     "A\<^sub>Q \<sharp>* R"

  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]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
                           and ReqP'': "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>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q : R \<rhd> P \<Longrightarrow>\<alpha> \<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> \<alpha> \<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> \<alpha> \<prec> P'

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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>* A\<^sub>Q" and "A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q" and "A\<^sub>P'' \<sharp>* \<Psi>"
[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>* A\<^sub>Q; A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q; A\<^sub>P'' \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(A\<^sub>Q, \<Psi>\<^sub>Q, \<Psi>)" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>P'' \<sharp>* A\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[PROOF STEP]
from FrR FrP'' \<open>A\<^sub>Q \<sharp>* R\<close> \<open>A\<^sub>Q \<sharp>* P''\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* P''
A\<^sub>R \<sharp>* A\<^sub>Q
A\<^sub>P'' \<sharp>* A\<^sub>Q
[PROOF STEP]
have "A\<^sub>Q \<sharp>* \<Psi>\<^sub>R" and "A\<^sub>Q \<sharp>* \<Psi>\<^sub>P''"
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>Q \<sharp>* R
A\<^sub>Q \<sharp>* P''
A\<^sub>R \<sharp>* A\<^sub>Q
A\<^sub>P'' \<sharp>* A\<^sub>Q

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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 frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[PROOF STEP]
from ReqP'' FrR FrP'' \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<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 R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
[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 R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q

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 R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
\<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 auto
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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 frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[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 "\<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(force dest: FrameStatImpTrans simp add: FrameStatEq_def)
[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. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[PROOF STEP]
hence "\<langle>(A\<^sub>R@A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P''@A\<^sub>Q), \<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> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>P'', \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. \<langle>(A\<^sub>R @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P'' @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
apply(simp add: frameChainAppend)
[PROOF STATE]
proof (prove)
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> \<Longrightarrow> \<lparr>\<nu>*A\<^sub>R\<rparr>\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>P''\<rparr>\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
apply(drule_tac xvec=A\<^sub>Q in frameImpResChainPres)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>*A\<^sub>Q\<rparr>\<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>Q\<rparr>\<langle>A\<^sub>P'', \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle> \<Longrightarrow> \<lparr>\<nu>*A\<^sub>R\<rparr>\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>P''\<rparr>\<langle>A\<^sub>Q, \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
by(metis frameImpChainComm FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
\<langle>(A\<^sub>R @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P'' @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
[PROOF STEP]
with FrR FrQ FrP'' \<open>A\<^sub>R \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>R\<close> \<open>A\<^sub>P'' \<sharp>* A\<^sub>Q\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<^sub>P''\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>P'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q \<sharp>* \<Psi>\<close> ReqP''
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
A\<^sub>Q \<sharp>* \<Psi>\<^sub>R
A\<^sub>P'' \<sharp>* A\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>Q \<sharp>* \<Psi>\<^sub>P''
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* \<Psi>
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
\<langle>(A\<^sub>R @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P'' @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
extractFrame P'' = \<langle>A\<^sub>P'', \<Psi>\<^sub>P''\<rangle>
A\<^sub>R \<sharp>* A\<^sub>Q
A\<^sub>R \<sharp>* \<Psi>\<^sub>Q
A\<^sub>Q \<sharp>* \<Psi>\<^sub>R
A\<^sub>P'' \<sharp>* A\<^sub>Q
A\<^sub>P'' \<sharp>* \<Psi>\<^sub>Q
A\<^sub>Q \<sharp>* \<Psi>\<^sub>P''
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>P'' \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* \<Psi>
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>Q) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') (\<Psi> \<otimes> \<Psi>\<^sub>Q)
\<langle>(A\<^sub>R @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P'' @ A\<^sub>Q), \<Psi> \<otimes> \<Psi>\<^sub>P'' \<otimes> \<Psi>\<^sub>Q\<rangle>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>

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

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
from P''Trans 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>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> \<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>
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto>\<alpha> \<prec> (P' \<parallel> Q)"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P'' \<longmapsto> \<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>

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

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'' \<parallel> Q
insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<alpha> \<prec> 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
insertAssertion (extractFrame (R \<parallel> Q)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P'' \<parallel> Q)) \<Psi>
\<Psi> \<rhd> P'' \<parallel> Q \<longmapsto> \<alpha> \<prec> P' \<parallel> Q

goal (1 subgoal):
 1. \<Psi> : R \<parallel> Q \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
by(rule weakTransitionI)
[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


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

  assumes QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>P : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q'"
  and     FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
  and     "bn \<alpha> \<sharp>* P"
  and     "A\<^sub>P \<sharp>* \<Psi>"
  and     "A\<^sub>P \<sharp>* Q"
  and     "A\<^sub>P \<sharp>* \<alpha>"
  and     "A\<^sub>P \<sharp>* R"

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

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

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

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

goal (1 subgoal):
 1. \<Psi> : P \<parallel> R \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P \<parallel> Q'
[PROOF STEP]
from QChain FrP \<open>A\<^sub>P \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
A\<^sub>P \<sharp>* Q
[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>P \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
A\<^sub>P \<sharp>* Q

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

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
[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>* A\<^sub>P" and "A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P" and "A\<^sub>Q'' \<sharp>* \<Psi>"
[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>* A\<^sub>P; A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P; A\<^sub>Q'' \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac C="(A\<^sub>P, \<Psi>\<^sub>P, \<Psi>)" in freshFrame) auto
[PROOF STATE]
proof (state)
this:
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>Q'' \<sharp>* A\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
[PROOF STEP]
from FrR FrQ'' \<open>A\<^sub>P \<sharp>* R\<close> \<open>A\<^sub>P \<sharp>* Q''\<close> \<open>A\<^sub>R \<sharp>* A\<^sub>P\<close> \<open>A\<^sub>Q'' \<sharp>* A\<^sub>P\<close>
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>P \<sharp>* R
A\<^sub>P \<sharp>* Q''
A\<^sub>R \<sharp>* A\<^sub>P
A\<^sub>Q'' \<sharp>* A\<^sub>P
[PROOF STEP]
have "A\<^sub>P \<sharp>* \<Psi>\<^sub>R" and "A\<^sub>P \<sharp>* \<Psi>\<^sub>Q''"
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>P \<sharp>* R
A\<^sub>P \<sharp>* Q''
A\<^sub>R \<sharp>* A\<^sub>P
A\<^sub>Q'' \<sharp>* A\<^sub>P

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

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

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
[PROOF STEP]
from ReqQ'' FrR FrQ'' \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>P\<close> \<open>A\<^sub>Q'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P\<close>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>P) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') (\<Psi> \<otimes> \<Psi>\<^sub>P)
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P
[PROOF STEP]
have "\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>Q''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>P) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') (\<Psi> \<otimes> \<Psi>\<^sub>P)
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P

goal (1 subgoal):
 1. \<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
using freshCompChain
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>P) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') (\<Psi> \<otimes> \<Psi>\<^sub>P)
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>R \<sharp>* \<Psi>\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P
\<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>P) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>R, (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', (\<Psi> \<otimes> \<Psi>\<^sub>P) \<otimes> \<Psi>\<^sub>Q''\<rangle>

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

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

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

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

goal (1 subgoal):
 1. insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
[PROOF STEP]
hence "\<langle>(A\<^sub>P@A\<^sub>R), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P@A\<^sub>Q''), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>

goal (1 subgoal):
 1. \<langle>(A\<^sub>P @ A\<^sub>R), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P @ A\<^sub>Q''), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
apply(simp add: frameChainAppend)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>Q'', \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle> \<Longrightarrow> \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>Q'', \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
apply(drule_tac xvec=A\<^sub>P in frameImpResChainPres)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>Q'', \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle> \<Longrightarrow> \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>R, \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<lparr>\<nu>*A\<^sub>P\<rparr>\<langle>A\<^sub>Q'', \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
by(metis frameImpChainComm FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
\<langle>(A\<^sub>P @ A\<^sub>R), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P @ A\<^sub>Q''), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
[PROOF STEP]
with FrR FrP FrQ'' \<open>A\<^sub>R \<sharp>* A\<^sub>P\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>R\<close> \<open>A\<^sub>Q'' \<sharp>* A\<^sub>P\<close> \<open>A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>Q''\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>Q'' \<sharp>* \<Psi>\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<close> ReqQ''
[PROOF STATE]
proof (chain)
picking this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>R \<sharp>* A\<^sub>P
A\<^sub>R \<sharp>* \<Psi>\<^sub>P
A\<^sub>P \<sharp>* \<Psi>\<^sub>R
A\<^sub>Q'' \<sharp>* A\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P
A\<^sub>P \<sharp>* \<Psi>\<^sub>Q''
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>Q'' \<sharp>* \<Psi>
A\<^sub>P \<sharp>* \<Psi>
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>P) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') (\<Psi> \<otimes> \<Psi>\<^sub>P)
\<langle>(A\<^sub>P @ A\<^sub>R), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P @ A\<^sub>Q''), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
extractFrame Q'' = \<langle>A\<^sub>Q'', \<Psi>\<^sub>Q''\<rangle>
A\<^sub>R \<sharp>* A\<^sub>P
A\<^sub>R \<sharp>* \<Psi>\<^sub>P
A\<^sub>P \<sharp>* \<Psi>\<^sub>R
A\<^sub>Q'' \<sharp>* A\<^sub>P
A\<^sub>Q'' \<sharp>* \<Psi>\<^sub>P
A\<^sub>P \<sharp>* \<Psi>\<^sub>Q''
A\<^sub>R \<sharp>* \<Psi>
A\<^sub>Q'' \<sharp>* \<Psi>
A\<^sub>P \<sharp>* \<Psi>
insertAssertion (extractFrame R) (\<Psi> \<otimes> \<Psi>\<^sub>P) \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') (\<Psi> \<otimes> \<Psi>\<^sub>P)
\<langle>(A\<^sub>P @ A\<^sub>R), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>R\<rangle> \<hookrightarrow>\<^sub>F \<langle>(A\<^sub>P @ A\<^sub>Q''), \<Psi> \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>\<^sub>Q''\<rangle>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>

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

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

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q'' \<longmapsto> \<alpha> \<prec> P \<parallel> Q'
[PROOF STEP]
by(rule_tac Par2) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<parallel> Q'' \<longmapsto> \<alpha> \<prec> P \<parallel> Q'

goal (1 subgoal):
 1. \<Psi> : P \<parallel> R \<rhd> P \<parallel> Q \<Longrightarrow>\<alpha> \<prec> P \<parallel> Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P \<parallel> Q''
insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
\<Psi> \<rhd> P \<parallel> Q'' \<longmapsto> \<alpha> \<prec> 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''
insertAssertion (extractFrame (P \<parallel> R)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (P \<parallel> Q'')) \<Psi>
\<Psi> \<rhd> P \<parallel> Q'' \<longmapsto> \<alpha> \<prec> P \<parallel> Q'

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

goal:
No subgoals!
[PROOF STEP]
qed