[STATEMENT]
lemma caseWeakSimPres:
  fixes \<Psi>    :: 'b
  and   CsP  :: "('c \<times> ('a, 'b, 'c) psi) list"
  and   Rel  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   CsQ  :: "('c \<times> ('a, 'b, 'c) psi) list"
  and   M    :: 'a
  and   N    :: 'a

  assumes PRelQ: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> Eq \<Psi> P Q"
  and     Sim:   "\<And>\<Psi>' P Q. (\<Psi>', P, Q) \<in> Rel \<Longrightarrow> \<Psi>' \<rhd> P \<leadsto><Rel> Q"
  and     EqRel: "\<And>\<Psi>' P Q. Eq \<Psi>' P Q \<Longrightarrow> (\<Psi>', P, Q) \<in> Rel"
  and     EqSim: "\<And>\<Psi>' P Q. Eq \<Psi>' P Q \<Longrightarrow> \<Psi>' \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q"

  shows "\<Psi> \<rhd> Cases CsP \<leadsto><Rel> Cases CsQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> Cases CsP \<leadsto><Rel> Cases CsQ
[PROOF STEP]
proof(induct rule: weakSimI2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* (Cases CsP); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cAct \<Psi>' \<alpha> Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* (Cases CsP)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* (Cases CsP); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>bn \<alpha> \<sharp>* (Cases CsP)\<close>
[PROOF STATE]
proof (chain)
picking this:
bn \<alpha> \<sharp>* (Cases CsP)
[PROOF STEP]
have "bn \<alpha> \<sharp>* CsP"
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* (Cases CsP)

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* CsP
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* CsP

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* (Cases CsP); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> Cases CsQ \<longmapsto>\<alpha> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
proof(induct rule: caseCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
case(cCase \<phi> Q)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
(\<phi>, Q) mem CsQ
\<Psi> \<turnstile> \<phi>
guarded Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>(\<phi>, Q) mem CsQ\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>, Q) mem CsQ
[PROOF STEP]
obtain P where "(\<phi>, P) mem CsP" and "guarded P" and "Eq \<Psi> P Q"
[PROOF STATE]
proof (prove)
using this:
(\<phi>, Q) mem CsQ

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>(\<phi>, P) mem CsP; guarded P; Eq \<Psi> P Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis PRelQ)
[PROOF STATE]
proof (state)
this:
(\<phi>, P) mem CsP
guarded P
Eq \<Psi> P Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>Eq \<Psi> P Q\<close>
[PROOF STATE]
proof (chain)
picking this:
Eq \<Psi> P Q
[PROOF STEP]
have "\<Psi> \<rhd> P \<leadsto><Rel> Q"
[PROOF STATE]
proof (prove)
using this:
Eq \<Psi> P Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
by(metis EqRel Sim)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<leadsto><Rel> Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<leadsto><Rel> Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
note \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>bn \<alpha> \<sharp>* CsP\<close> \<open>(\<phi>, P) mem CsP\<close>
[PROOF STATE]
proof (chain)
picking this:
bn \<alpha> \<sharp>* CsP
(\<phi>, P) mem CsP
[PROOF STEP]
have "bn \<alpha> \<sharp>* P"
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* CsP
(\<phi>, P) mem CsP

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* P
[PROOF STEP]
by(auto dest: memFreshChain)
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* P

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''"
                               and P''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
note PTrans \<open>(\<phi>, P) mem CsP\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close>
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>guarded Q\<close>
[PROOF STATE]
proof (chain)
picking this:
guarded Q
[PROOF STEP]
have "insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
guarded Q

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

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
hence "insertAssertion (extractFrame(Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>
[PROOF STEP]
by(auto simp add: FrameStatEq_def)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from Identity
[PROOF STATE]
proof (chain)
picking this:
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>
[PROOF STEP]
have "insertAssertion (extractFrame(Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>"
[PROOF STATE]
proof (prove)
using this:
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
[PROOF STEP]
by(auto simp add: AssertionStatEq_def)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
[PROOF STEP]
have "\<Psi> : (Cases CsQ) \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q) \<Psi>
insertAssertion (extractFrame (Cases CsQ)) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>

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

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
with P''Chain P'RelQ'
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
\<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
\<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P''

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Cases CsQ \<rhd> Cases CsP \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> Cases CsQ \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
proof(induct rule: caseCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cCase \<phi> Q)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
(\<phi>, Q) mem CsQ
\<Psi> \<turnstile> \<phi>
guarded Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>(\<phi>, Q) mem CsQ\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>, Q) mem CsQ
[PROOF STEP]
obtain P where "(\<phi>, P) mem CsP" and "guarded P" and "Eq \<Psi> P Q"
[PROOF STATE]
proof (prove)
using this:
(\<phi>, Q) mem CsQ

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>(\<phi>, P) mem CsP; guarded P; Eq \<Psi> P Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis PRelQ)
[PROOF STATE]
proof (state)
this:
(\<phi>, P) mem CsP
guarded P
Eq \<Psi> P Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>Eq \<Psi> P Q\<close> \<open>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
Eq \<Psi> P Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Eq \<Psi> P Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: EqSim weakCongSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PChain \<open>(\<phi>, P) mem CsP\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
[PROOF STEP]
have "\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P'"
[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. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[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 add: trancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with P'RelQ'
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongSimCasePres:
  fixes \<Psi>    :: 'b
  and   CsP  :: "('c \<times> ('a, 'b, 'c) psi) list"
  and   Rel  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   CsQ  :: "('c \<times> ('a, 'b, 'c) psi) list"
  and   M    :: 'a
  and   N    :: 'a

  assumes PRelQ: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> Eq \<Psi> P Q"
  and     EqSim: "\<And>\<Psi>' P Q. Eq \<Psi>' P Q \<Longrightarrow> \<Psi>' \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q"

  shows "\<Psi> \<rhd> Cases CsP \<leadsto>\<guillemotleft>Rel\<guillemotright> Cases CsQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> Cases CsP \<leadsto>\<guillemotleft>Rel\<guillemotright> Cases CsQ
[PROOF STEP]
proof(induct rule: weakCongSimI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<Psi> \<rhd> Cases CsQ \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Cases CsQ \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
proof(induct rule: caseCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cCase \<phi> Q)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
(\<phi>, Q) mem CsQ
\<Psi> \<turnstile> \<phi>
guarded Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>(\<phi>, Q) mem CsQ\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>, Q) mem CsQ
[PROOF STEP]
obtain P where "(\<phi>, P) mem CsP" and "guarded P" and "Eq \<Psi> P Q"
[PROOF STATE]
proof (prove)
using this:
(\<phi>, Q) mem CsQ

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>(\<phi>, P) mem CsP; guarded P; Eq \<Psi> P Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(metis PRelQ)
[PROOF STATE]
proof (state)
this:
(\<phi>, P) mem CsP
guarded P
Eq \<Psi> P Q

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>Eq \<Psi> P Q\<close> \<open>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
Eq \<Psi> P Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Eq \<Psi> P Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: EqSim weakCongSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PChain \<open>(\<phi>, P) mem CsP\<close> \<open>\<Psi> \<turnstile> \<phi>\<close> \<open>guarded P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<phi>, P) mem CsP
\<Psi> \<turnstile> \<phi>
guarded P
[PROOF STEP]
have "\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P'"
[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. \<And>\<phi> P. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> Q'; (\<phi>, P) mem CsQ; \<Psi> \<turnstile> \<phi>; guarded P\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with P'RelQ'
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
\<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> Cases CsP \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongSimResPres:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   x    :: name
  and   Rel' :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q"
  and     "eqvt Rel'"
  and     "x \<sharp> \<Psi>"
  and     "Rel \<subseteq> Rel'"
  and     C1: "\<And>\<Psi>' R S x. \<lbrakk>(\<Psi>', R, S) \<in> Rel; x \<sharp> \<Psi>'\<rbrakk> \<Longrightarrow> (\<Psi>', \<lparr>\<nu>x\<rparr>R, \<lparr>\<nu>x\<rparr>S) \<in> Rel'"

  shows   "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<leadsto>\<guillemotleft>Rel'\<guillemotright> \<lparr>\<nu>x\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<leadsto>\<guillemotleft>Rel'\<guillemotright> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
proof(induct rule: weakCongSimI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel'
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel'
[PROOF STEP]
from \<open>\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
have "x \<sharp> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. x \<sharp> Q'
[PROOF STEP]
by(auto dest: tauFreshDerivative simp add: abs_fresh)
[PROOF STATE]
proof (state)
this:
x \<sharp> Q'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel'
[PROOF STEP]
with  \<open>\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto>\<tau> \<prec> Q'\<close> \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q'
x \<sharp> \<Psi>
x \<sharp> Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>Q \<longmapsto> \<tau> \<prec> Q'
x \<sharp> \<Psi>
x \<sharp> Q'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel'
[PROOF STEP]
proof(induct rule: resTauCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
case(cRes Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
from PSimQ \<open>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakCongSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
from PChain \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> \<Psi>
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> \<Psi>

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

goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'

goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
from P'RelQ' \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
x \<sharp> \<Psi>
[PROOF STEP]
have "(\<Psi>, \<lparr>\<nu>x\<rparr>P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
x \<sharp> \<Psi>

goal (1 subgoal):
 1. (\<Psi>, \<lparr>\<nu>x\<rparr>P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'
[PROOF STEP]
by(rule C1)
[PROOF STATE]
proof (state)
this:
(\<Psi>, \<lparr>\<nu>x\<rparr>P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'

goal (1 subgoal):
 1. \<And>P'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> P' \<Longrightarrow> \<exists>P'a. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P'a \<and> (\<Psi>, P'a, \<lparr>\<nu>x\<rparr>P') \<in> Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
(\<Psi>, \<lparr>\<nu>x\<rparr>P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
(\<Psi>, \<lparr>\<nu>x\<rparr>P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', \<lparr>\<nu>x\<rparr>Q') \<in> Rel'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongSimResChainPres:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes PSimQ: "\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q"
  and     "eqvt Rel"
  and     "xvec \<sharp>* \<Psi>"
  and     C1:    "\<And>\<Psi>' R S xvec. \<lbrakk>(\<Psi>', R, S) \<in> Rel; xvec \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow> (\<Psi>', \<lparr>\<nu>*xvec\<rparr>R, \<lparr>\<nu>*xvec\<rparr>S) \<in> Rel"

  shows   "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
[PROOF STEP]
using \<open>xvec \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
[PROOF STEP]
proof(induct xvec)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*[]\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*[]\<rparr>Q
 2. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<sharp>* \<Psi>

goal (2 subgoals):
 1. [] \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*[]\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*[]\<rparr>Q
 2. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
from PSimQ
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*[]\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*[]\<rparr>Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>*[]\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*[]\<rparr>Q

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
case(Cons x xvec)
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
(x # xvec) \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
from \<open>(x#xvec) \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
(x # xvec) \<sharp>* \<Psi>
[PROOF STEP]
have "x \<sharp> \<Psi>" and "xvec \<sharp>* \<Psi>"
[PROOF STATE]
proof (prove)
using this:
(x # xvec) \<sharp>* \<Psi>

goal (1 subgoal):
 1. x \<sharp> \<Psi> &&& xvec \<sharp>* \<Psi>
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<sharp> \<Psi>
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
from \<open>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q\<close> \<open>xvec \<sharp>* \<Psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
xvec \<sharp>* \<Psi>
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
note \<open>eqvt Rel\<close> \<open>x \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (state)
this:
eqvt Rel
x \<sharp> \<Psi>

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt Rel
x \<sharp> \<Psi>

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
have "Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel \<subseteq> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
have "\<And>\<Psi> P Q x. \<lbrakk>(\<Psi>, P, Q) \<in> Rel; x \<sharp> \<Psi>\<rbrakk> \<Longrightarrow> (\<Psi>, \<lparr>\<nu>*[x]\<rparr>P, \<lparr>\<nu>*[x]\<rparr>Q) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Psi> P Q x. \<lbrakk>(\<Psi>, P, Q) \<in> Rel; x \<sharp> \<Psi>\<rbrakk> \<Longrightarrow> (\<Psi>, \<lparr>\<nu>*[x]\<rparr>P, \<lparr>\<nu>*[x]\<rparr>Q) \<in> Rel
[PROOF STEP]
by(rule_tac xvec="[x]" in C1) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?\<Psi>, ?P, ?Q) \<in> Rel; ?x \<sharp> ?\<Psi>\<rbrakk> \<Longrightarrow> (?\<Psi>, \<lparr>\<nu>*[?x]\<rparr>?P, \<lparr>\<nu>*[?x]\<rparr>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
hence "\<And>\<Psi> P Q x. \<lbrakk>(\<Psi>, P, Q) \<in> Rel; x \<sharp> \<Psi>\<rbrakk> \<Longrightarrow> (\<Psi>, \<lparr>\<nu>x\<rparr>P, \<lparr>\<nu>x\<rparr>Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?\<Psi>, ?P, ?Q) \<in> Rel; ?x \<sharp> ?\<Psi>\<rbrakk> \<Longrightarrow> (?\<Psi>, \<lparr>\<nu>*[?x]\<rparr>?P, \<lparr>\<nu>*[?x]\<rparr>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>\<Psi> P Q x. \<lbrakk>(\<Psi>, P, Q) \<in> Rel; x \<sharp> \<Psi>\<rbrakk> \<Longrightarrow> (\<Psi>, \<lparr>\<nu>x\<rparr>P, \<lparr>\<nu>x\<rparr>Q) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?\<Psi>, ?P, ?Q) \<in> Rel; ?x \<sharp> ?\<Psi>\<rbrakk> \<Longrightarrow> (?\<Psi>, \<lparr>\<nu>?x\<rparr>?P, \<lparr>\<nu>?x\<rparr>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
eqvt Rel
x \<sharp> \<Psi>
Rel \<subseteq> Rel
\<lbrakk>(?\<Psi>, ?P, ?Q) \<in> Rel; ?x \<sharp> ?\<Psi>\<rbrakk> \<Longrightarrow> (?\<Psi>, \<lparr>\<nu>?x\<rparr>?P, \<lparr>\<nu>?x\<rparr>?Q) \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>Q)"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q
eqvt Rel
x \<sharp> \<Psi>
Rel \<subseteq> Rel
\<lbrakk>(?\<Psi>, ?P, ?Q) \<in> Rel; ?x \<sharp> ?\<Psi>\<rbrakk> \<Longrightarrow> (?\<Psi>, \<lparr>\<nu>?x\<rparr>?P, \<lparr>\<nu>?x\<rparr>?Q) \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>Q)
[PROOF STEP]
by(rule weakCongSimResPres)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>Q)

goal (1 subgoal):
 1. \<And>a xvec. \<lbrakk>xvec \<sharp>* \<Psi> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*xvec\<rparr>Q; (a # xvec) \<sharp>* \<Psi>\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>*(a # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(a # xvec)\<rparr>Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>P) \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>x\<rparr>(\<lparr>\<nu>*xvec\<rparr>Q)

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*(x # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(x # xvec)\<rparr>Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>*(x # xvec)\<rparr>P \<leadsto>\<guillemotleft>Rel\<guillemotright> \<lparr>\<nu>*(x # xvec)\<rparr>Q

goal:
No subgoals!
[PROOF STEP]
qed