[STATEMENT]
lemma weakTransitionClosed[eqvt]:
  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   p    :: "name prm"

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

  shows "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>(p \<bullet> \<alpha>)\<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                           and "\<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. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
hence "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P'') \<longmapsto>(p \<bullet> \<alpha>) \<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P'' \<longmapsto> p \<bullet> \<alpha> \<prec> p \<bullet> P'

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

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

goal:
No subgoals!
[PROOF STEP]
qed