[STATEMENT]
lemma weakTransferTauChainFrame:
  fixes \<Psi>\<^sub>F :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   A\<^sub>P :: "name list"
  and   \<Psi>\<^sub>P :: 'b
  and   A\<^sub>F :: "name list"
  and   A\<^sub>G :: "name list"
  and   \<Psi>\<^sub>G :: 'b

  assumes PChain: "\<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
  and     "distinct A\<^sub>P"
  and     FeqG: "\<And>\<Psi>. insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>"
  and     "A\<^sub>F \<sharp>* \<Psi>\<^sub>G"
  and     "A\<^sub>G \<sharp>* \<Psi>"
  and     "A\<^sub>G \<sharp>* \<Psi>\<^sub>F"
  and     "A\<^sub>F \<sharp>* A\<^sub>G"
  and     "A\<^sub>F \<sharp>* P"
  and     "A\<^sub>G \<sharp>* P"
  and     "A\<^sub>P \<sharp>* A\<^sub>F"
  and     "A\<^sub>P \<sharp>* A\<^sub>G"
  and     "A\<^sub>P \<sharp>* \<Psi>\<^sub>F"
  and     "A\<^sub>P \<sharp>* \<Psi>\<^sub>G"
  and     "A\<^sub>P \<sharp>* P"

  shows "\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
using PChain FrP \<open>A\<^sub>F \<sharp>* P\<close> \<open>A\<^sub>G \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* P\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
A\<^sub>P \<sharp>* P

goal (1 subgoal):
 1. \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
proof(induct rule: tauChainInduct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
 2. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
case TauBase
[PROOF STATE]
proof (state)
this:
extractFrame P_ = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>F \<sharp>* P_
A\<^sub>G \<sharp>* P_
A\<^sub>P \<sharp>* P_

goal (2 subgoals):
 1. \<And>P. \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
 2. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extractFrame P_ = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>F \<sharp>* P_
A\<^sub>G \<sharp>* P_
A\<^sub>P \<sharp>* P_

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
case(TauStep P P' P'')
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''
\<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
A\<^sub>P \<sharp>* P

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
have FrP: "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
have PChain: "\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
using \<open>A\<^sub>F \<sharp>* P\<close> \<open>A\<^sub>G \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* P\<close>
[PROOF STATE]
proof (prove)
using this:
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
A\<^sub>P \<sharp>* P

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
obtain A\<^sub>P' \<Psi>\<^sub>P' \<Psi>' where FrP': "extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>" and "\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'"
                            and "A\<^sub>P' \<sharp>* A\<^sub>F" and "A\<^sub>P' \<sharp>* A\<^sub>G" and "A\<^sub>P' \<sharp>* \<Psi>\<^sub>F" and "A\<^sub>P' \<sharp>* \<Psi>\<^sub>G"
                            and "distinct A\<^sub>P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. (\<And>A\<^sub>P' \<Psi>\<^sub>P' \<Psi>'. \<lbrakk>extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; \<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; A\<^sub>P' \<sharp>* A\<^sub>F; A\<^sub>P' \<sharp>* A\<^sub>G; A\<^sub>P' \<sharp>* \<Psi>\<^sub>F; A\<^sub>P' \<sharp>* \<Psi>\<^sub>G; distinct A\<^sub>P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using FrP \<open>distinct A\<^sub>P\<close> \<open>A\<^sub>P \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>F\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>G\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>F\<close> \<open>A\<^sub>P \<sharp>* \<Psi>\<^sub>G\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
distinct A\<^sub>P
A\<^sub>P \<sharp>* P
A\<^sub>P \<sharp>* A\<^sub>F
A\<^sub>P \<sharp>* A\<^sub>G
A\<^sub>P \<sharp>* \<Psi>\<^sub>F
A\<^sub>P \<sharp>* \<Psi>\<^sub>G

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
from PChain \<open>A\<^sub>F \<sharp>* P\<close> \<open>A\<^sub>G \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
[PROOF STEP]
have "A\<^sub>F \<sharp>* P'" and "A\<^sub>G \<sharp>* P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P

goal (1 subgoal):
 1. A\<^sub>F \<sharp>* P' &&& A\<^sub>G \<sharp>* P'
[PROOF STEP]
by(blast dest: tauChainFreshChain)+
[PROOF STATE]
proof (state)
this:
A\<^sub>F \<sharp>* P'
A\<^sub>G \<sharp>* P'

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
with \<open>A\<^sub>F \<sharp>* P\<close> \<open>A\<^sub>G \<sharp>* P\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>F\<close> \<open>A\<^sub>P \<sharp>* A\<^sub>G\<close>\<open>A\<^sub>P' \<sharp>* A\<^sub>F\<close> \<open>A\<^sub>P' \<sharp>* A\<^sub>G\<close> FrP FrP'
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
A\<^sub>P \<sharp>* A\<^sub>F
A\<^sub>P \<sharp>* A\<^sub>G
A\<^sub>P' \<sharp>* A\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>G
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
A\<^sub>F \<sharp>* P'
A\<^sub>G \<sharp>* P'
[PROOF STEP]
have "A\<^sub>F \<sharp>* \<Psi>\<^sub>P" and "A\<^sub>G \<sharp>* \<Psi>\<^sub>P" and "A\<^sub>F \<sharp>* \<Psi>\<^sub>P'" and "A\<^sub>G \<sharp>* \<Psi>\<^sub>P'"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>F \<sharp>* P
A\<^sub>G \<sharp>* P
A\<^sub>P \<sharp>* A\<^sub>F
A\<^sub>P \<sharp>* A\<^sub>G
A\<^sub>P' \<sharp>* A\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>G
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
A\<^sub>F \<sharp>* P'
A\<^sub>G \<sharp>* P'

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
from FeqG
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) ?\<Psi> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) ?\<Psi>
[PROOF STEP]
have FeqG: "insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) ?\<Psi> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) ?\<Psi>

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
obtain p::"name prm" where "(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F" and  "(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P" and "(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'" and "(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'"
                         and Sp: "(set p) \<subseteq> set A\<^sub>F \<times> set(p \<bullet> A\<^sub>F)" and "distinctPerm p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'; set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F); distinctPerm p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac xvec=A\<^sub>F and c="(\<Psi>\<^sub>F, \<Psi>\<^sub>P, \<Psi>', \<Psi>\<^sub>P')" in name_list_avoiding) auto
[PROOF STATE]
proof (state)
this:
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'
set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)
distinctPerm p

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
obtain q::"name prm" where "(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G" and  "(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P" and "(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'" and "(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'"
                         and Sq: "(set q) \<subseteq> set A\<^sub>G \<times> set(q \<bullet> A\<^sub>G)" and "distinctPerm q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'; set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G); distinctPerm q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac xvec=A\<^sub>G and c="(\<Psi>\<^sub>G, \<Psi>\<^sub>P, \<Psi>', \<Psi>\<^sub>P')" in name_list_avoiding) auto
[PROOF STATE]
proof (state)
this:
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'
set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G)
distinctPerm q

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
from \<open>\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'
[PROOF STEP]
have "\<langle>(p \<bullet> A\<^sub>F), ((p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P')\<rangle> \<simeq>\<^sub>F \<langle>(p \<bullet> A\<^sub>F), (p \<bullet> \<Psi>\<^sub>F) \<otimes> (\<Psi>\<^sub>P \<otimes> \<Psi>')\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
hence "\<langle>(p \<bullet> A\<^sub>F), (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<simeq>\<^sub>F \<langle>(p \<bullet> A\<^sub>F), \<Psi>' \<otimes> ((p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P)\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<simeq>\<^sub>F \<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>'\<rangle>

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<simeq>\<^sub>F \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
from FeqG \<open>A\<^sub>F \<sharp>* \<Psi>\<^sub>P\<close> \<open>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P\<close> \<open>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F\<close> \<open>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'\<close> Sp
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'
A\<^sub>F \<sharp>* \<Psi>\<^sub>P
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'
set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)
[PROOF STEP]
have "\<langle>(p \<bullet> A\<^sub>F), \<Psi>' \<otimes> ((p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P)\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'
A\<^sub>F \<sharp>* \<Psi>\<^sub>P
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'
set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)

goal (1 subgoal):
 1. \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'
[PROOF STEP]
apply(erule_tac rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A\<^sub>F \<sharp>* \<Psi>\<^sub>P; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F; (p \<bullet> A\<^sub>F) \<sharp>* \<Psi>'; set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)\<rbrakk> \<Longrightarrow> insertAssertion (\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<longrightarrow> \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'
[PROOF STEP]
by(subst frameChainAlpha) (auto simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
hence "\<langle>(p \<bullet> A\<^sub>F), \<Psi>' \<otimes> ((p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P)\<rangle> \<hookrightarrow>\<^sub>F  (\<langle>(q \<bullet> A\<^sub>G), \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'

goal (1 subgoal):
 1. \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
using \<open>A\<^sub>G \<sharp>* \<Psi>\<^sub>P\<close> \<open>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P\<close> \<open>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G\<close> \<open>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'\<close> Sq
[PROOF STATE]
proof (prove)
using this:
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>'
A\<^sub>G \<sharp>* \<Psi>\<^sub>P
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'
set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G)

goal (1 subgoal):
 1. \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
apply(erule_tac rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A\<^sub>G \<sharp>* \<Psi>\<^sub>P; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G; (q \<bullet> A\<^sub>G) \<sharp>* \<Psi>'; set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G)\<rbrakk> \<Longrightarrow> \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F insertAssertion (\<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P\<rangle>) \<Psi>' \<longrightarrow> \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>
[PROOF STEP]
by(subst frameChainAlpha) (auto simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
have "\<langle>(q \<bullet> A\<^sub>G), \<Psi>' \<otimes> ((q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P)\<rangle> \<simeq>\<^sub>F \<langle>(q \<bullet> A\<^sub>G), (q \<bullet> \<Psi>\<^sub>G) \<otimes> (\<Psi>\<^sub>P \<otimes> \<Psi>')\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>'\<rangle>
[PROOF STEP]
by(metis frameIntAssociativity FrameStatEqTrans frameIntCommutativity FrameStatEqSym)
[PROOF STATE]
proof (state)
this:
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>'\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
hence "\<langle>(q \<bullet> A\<^sub>G), \<Psi>' \<otimes> ((q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P)\<rangle> \<simeq>\<^sub>F \<langle>(q \<bullet> A\<^sub>G), (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>'\<rangle>

goal (1 subgoal):
 1. \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
using \<open>\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'\<close>
[PROOF STATE]
proof (prove)
using this:
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P \<otimes> \<Psi>'\<rangle>
\<Psi>\<^sub>P \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'

goal (1 subgoal):
 1. \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
by(blast intro: FrameStatEqTrans frameIntCompositionSym)
[PROOF STATE]
proof (state)
this:
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<simeq>\<^sub>F \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle>
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
have "\<langle>(p \<bullet> A\<^sub>F), (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>(q \<bullet> A\<^sub>G), (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<simeq>\<^sub>F \<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle>
\<langle>p \<bullet> A\<^sub>F, \<Psi>' \<otimes> (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle>
\<langle>q \<bullet> A\<^sub>G, \<Psi>' \<otimes> (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P\<rangle> \<simeq>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
with \<open>A\<^sub>F \<sharp>* \<Psi>\<^sub>P'\<close> \<open>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'\<close> \<open>(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F\<close> Sp
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>F \<sharp>* \<Psi>\<^sub>P'
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F
set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>(q \<bullet> A\<^sub>G), (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>F \<sharp>* \<Psi>\<^sub>P'
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>P'
(p \<bullet> A\<^sub>F) \<sharp>* \<Psi>\<^sub>F
set p \<subseteq> set A\<^sub>F \<times> set (p \<bullet> A\<^sub>F)
\<langle>p \<bullet> A\<^sub>F, (p \<bullet> \<Psi>\<^sub>F) \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>

goal (1 subgoal):
 1. \<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
by(subst frameChainAlpha) (auto simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
with \<open>A\<^sub>G \<sharp>* \<Psi>\<^sub>P'\<close> \<open>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'\<close> \<open>(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G\<close> Sq
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>G \<sharp>* \<Psi>\<^sub>P'
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G
set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G)
\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
have "\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>G \<sharp>* \<Psi>\<^sub>P'
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>P'
(q \<bullet> A\<^sub>G) \<sharp>* \<Psi>\<^sub>G
set q \<subseteq> set A\<^sub>G \<times> set (q \<bullet> A\<^sub>G)
\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>q \<bullet> A\<^sub>G, (q \<bullet> \<Psi>\<^sub>G) \<otimes> \<Psi>\<^sub>P'\<rangle>

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

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
with \<open>\<Psi>\<^sub>F \<rhd> P' \<longmapsto>\<tau> \<prec> P''\<close> FrP' \<open>distinct A\<^sub>P'\<close>
       \<open>A\<^sub>F \<sharp>* P'\<close> \<open>A\<^sub>G \<sharp>* P'\<close> \<open>A\<^sub>F \<sharp>* \<Psi>\<^sub>G\<close> \<open>A\<^sub>G \<sharp>* \<Psi>\<^sub>F\<close> \<open>A\<^sub>P' \<sharp>* A\<^sub>F\<close> \<open>A\<^sub>P' \<sharp>* A\<^sub>G\<close> \<open>A\<^sub>P' \<sharp>* \<Psi>\<^sub>F\<close> \<open>A\<^sub>P' \<sharp>* \<Psi>\<^sub>G\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
distinct A\<^sub>P'
A\<^sub>F \<sharp>* P'
A\<^sub>G \<sharp>* P'
A\<^sub>F \<sharp>* \<Psi>\<^sub>G
A\<^sub>G \<sharp>* \<Psi>\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>G
A\<^sub>P' \<sharp>* \<Psi>\<^sub>F
A\<^sub>P' \<sharp>* \<Psi>\<^sub>G
\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P'\<rangle>
[PROOF STEP]
have "\<Psi>\<^sub>G \<rhd> P' \<longmapsto>\<tau> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''
extractFrame P' = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>
distinct A\<^sub>P'
A\<^sub>F \<sharp>* P'
A\<^sub>G \<sharp>* P'
A\<^sub>F \<sharp>* \<Psi>\<^sub>G
A\<^sub>G \<sharp>* \<Psi>\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>F
A\<^sub>P' \<sharp>* A\<^sub>G
A\<^sub>P' \<sharp>* \<Psi>\<^sub>F
A\<^sub>P' \<sharp>* \<Psi>\<^sub>G
\<langle>A\<^sub>F, \<Psi>\<^sub>F \<otimes> \<Psi>\<^sub>P'\<rangle> \<hookrightarrow>\<^sub>F \<langle>A\<^sub>G, \<Psi>\<^sub>G \<otimes> \<Psi>\<^sub>P'\<rangle>

goal (1 subgoal):
 1. \<Psi>\<^sub>G \<rhd> P' \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
by(rule_tac transferTauFrame)
[PROOF STATE]
proof (state)
this:
\<Psi>\<^sub>G \<rhd> P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. \<And>P P' P''. \<lbrakk>\<Psi>\<^sub>F \<rhd> P' \<longmapsto> \<tau> \<prec> P''; \<Psi>\<^sub>F \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; \<lbrakk>extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; A\<^sub>F \<sharp>* P; A\<^sub>G \<sharp>* P; A\<^sub>P \<sharp>* P\<rbrakk> \<Longrightarrow> \<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
with PChain
[PROOF STATE]
proof (chain)
picking this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi>\<^sub>G \<rhd> P' \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi>\<^sub>G \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi>\<^sub>G \<rhd> P' \<longmapsto> \<tau> \<prec> P''

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

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes "quiet P"

  shows "insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quiet P

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
[PROOF STEP]
by(erule_tac quiet.cases) force


[STATEMENT]
lemma quietTransition:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Rs :: "('a, 'b, 'c) residual"

  assumes "quiet P"
  and     "\<Psi> \<rhd> P \<longmapsto> Rs"

  obtains P' where "Rs = \<tau> \<prec> P'" and "quiet P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quiet P
\<Psi> \<rhd> P \<longmapsto> Rs

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule_tac quiet.cases) force


[STATEMENT]
lemma quietEqvt:
  fixes P :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  assumes "quiet P"

  shows "quiet(p \<bullet> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quiet (p \<bullet> P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quiet (p \<bullet> P)
[PROOF STEP]
let ?X = "\<lambda>P. \<exists>p::name prm. quiet(p \<bullet> P)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quiet (p \<bullet> P)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
quiet P
[PROOF STEP]
have "?X (p \<bullet> P)"
[PROOF STATE]
proof (prove)
using this:
quiet P

goal (1 subgoal):
 1. \<exists>pa. quiet (pa \<bullet> p \<bullet> P)
[PROOF STEP]
by(rule_tac x="rev p" in exI) auto
[PROOF STATE]
proof (state)
this:
\<exists>pa. quiet (pa \<bullet> p \<bullet> P)

goal (1 subgoal):
 1. quiet (p \<bullet> P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>pa. quiet (pa \<bullet> p \<bullet> P)

goal (1 subgoal):
 1. quiet (p \<bullet> P)
[PROOF STEP]
apply coinduct
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>p. quiet (p \<bullet> x) \<Longrightarrow> \<exists>P. x = P \<and> (\<forall>\<Psi>. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle> \<and> (\<forall>Rs. \<Psi> \<rhd> P \<longmapsto> Rs \<longrightarrow> (\<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P'))))
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p. quiet (p \<bullet> x) \<Longrightarrow> \<exists>P. x = P \<and> (\<forall>\<Psi>. insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle> \<and> (\<forall>Rs. \<Psi> \<rhd> P \<longmapsto> Rs \<longrightarrow> (\<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P'))))
[PROOF STEP]
apply(rule_tac x=x in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p. quiet (p \<bullet> x) \<Longrightarrow> x = x \<and> (\<forall>\<Psi>. insertAssertion (extractFrame x) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle> \<and> (\<forall>Rs. \<Psi> \<rhd> x \<longmapsto> Rs \<longrightarrow> (\<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P'))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi>. quiet (p \<bullet> x) \<Longrightarrow> insertAssertion (extractFrame x) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
 2. \<And>x p \<Psi> Rs. \<lbrakk>quiet (p \<bullet> x); \<Psi> \<rhd> x \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(drule_tac \<Psi>="p \<bullet> \<Psi>" in quietFrame)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi>. insertAssertion (extractFrame (p \<bullet> x)) (p \<bullet> \<Psi>) \<simeq>\<^sub>F \<langle>\<epsilon>, p \<bullet> \<Psi>\<rangle> \<Longrightarrow> insertAssertion (extractFrame x) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
 2. \<And>x p \<Psi> Rs. \<lbrakk>quiet (p \<bullet> x); \<Psi> \<rhd> x \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(drule_tac p="rev p" in FrameStatEqClosed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi>. rev p \<bullet> insertAssertion (extractFrame (p \<bullet> x)) (p \<bullet> \<Psi>) \<simeq>\<^sub>F rev p \<bullet> \<langle>\<epsilon>, p \<bullet> \<Psi>\<rangle> \<Longrightarrow> insertAssertion (extractFrame x) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
 2. \<And>x p \<Psi> Rs. \<lbrakk>quiet (p \<bullet> x); \<Psi> \<rhd> x \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(simp add: eqvts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs. \<lbrakk>quiet (p \<bullet> x); \<Psi> \<rhd> x \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(drule_tac pi=p in semantics.eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs. \<lbrakk>quiet (p \<bullet> x); p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> p \<bullet> Rs\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(erule_tac quietTransition)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi> Rs. p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> p \<bullet> Rs \<Longrightarrow> ?\<Psi>12 x p \<Psi> Rs \<rhd> p \<bullet> x \<longmapsto> ?Rs12 x p \<Psi> Rs
 2. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> p \<bullet> Rs; ?Rs12 x p \<Psi> Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> p \<bullet> Rs; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> \<exists>P'. Rs = \<tau> \<prec> P' \<and> ((\<exists>p. quiet (p \<bullet> P')) \<or> quiet P')
[PROOF STEP]
apply(rule_tac x="rev p \<bullet> P'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> p \<bullet> Rs; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> Rs = \<tau> \<prec> rev p \<bullet> P' \<and> ((\<exists>pa. quiet (pa \<bullet> rev p \<bullet> P')) \<or> quiet (rev p \<bullet> P'))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'\<rbrakk> \<Longrightarrow> Rs = \<tau> \<prec> rev p \<bullet> P'
 2. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'; \<not> quiet (rev p \<bullet> P')\<rbrakk> \<Longrightarrow> \<exists>pa. quiet (pa \<bullet> rev p \<bullet> P')
[PROOF STEP]
apply(drule_tac pi="rev p" in pt_bij3)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; quiet P'; rev p \<bullet> p \<bullet> Rs = rev p \<bullet> \<tau> \<prec> P'\<rbrakk> \<Longrightarrow> Rs = \<tau> \<prec> rev p \<bullet> P'
 2. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'; \<not> quiet (rev p \<bullet> P')\<rbrakk> \<Longrightarrow> \<exists>pa. quiet (pa \<bullet> rev p \<bullet> P')
[PROOF STEP]
apply(simp add: eqvts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'; \<not> quiet (rev p \<bullet> P')\<rbrakk> \<Longrightarrow> \<exists>pa. quiet (pa \<bullet> rev p \<bullet> P')
[PROOF STEP]
apply(rule_tac x=p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p \<Psi> Rs P'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> x \<longmapsto> \<tau> \<prec> P'; p \<bullet> Rs = \<tau> \<prec> P'; quiet P'; \<not> quiet (rev p \<bullet> P')\<rbrakk> \<Longrightarrow> quiet (p \<bullet> rev p \<bullet> P')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
quiet (p \<bullet> P)

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes "\<Psi> \<rhd> P \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     "quiet P"

  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
quiet P

goal (1 subgoal):
 1. False
[PROOF STEP]
apply(erule_tac quiet.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Pa. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'; P = Pa; \<forall>\<Psi>. insertAssertion (extractFrame Pa) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle> \<and> (\<forall>Rs. \<Psi> \<rhd> Pa \<longmapsto> Rs \<longrightarrow> (\<exists>P'. Rs = \<tau> \<prec> P' \<and> quiet P'))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(force simp add: residualInject)


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

  assumes "\<Psi> \<rhd> P \<longmapsto>M\<lparr>N\<rparr> \<prec> P'"
  and     "quiet P"

  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
quiet P

goal (1 subgoal):
 1. False
[PROOF STEP]
by(erule_tac quiet.cases) (force simp add: residualInject)


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

  assumes "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'"
  and     "insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>"
  and     "quiet P"

  shows "quiet P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quiet P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
insertAssertion (extractFrame P) \<Psi> \<simeq>\<^sub>F \<langle>\<epsilon>, \<Psi>\<rangle>
quiet P

goal (1 subgoal):
 1. quiet P'
[PROOF STEP]
by(erule_tac quiet.cases) (force simp add: residualInject)


[STATEMENT]
lemma tauChainCases[consumes 1, case_names TauBase TauStep]:
  fixes \<Psi>  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "P = P' \<Longrightarrow> Prop"
  and     "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P' \<Longrightarrow> Prop"

  shows Prop
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
P = P' \<Longrightarrow> Prop
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P' \<Longrightarrow> Prop

goal (1 subgoal):
 1. Prop
[PROOF STEP]
by(blast elim: rtranclE dest: rtrancl_into_trancl1)


[STATEMENT]
lemma Gauss_Jordan_in_ij_unfold:
  assumes "\<exists>n. A $ n $ j \<noteq> 0 \<and> i \<le> n"
  obtains n :: "'n::{finite, wellorder}" and interchange_A and A'
  where
    "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) = n"
    and "A $ n $ j \<noteq> 0"
    and "i \<le> n"
    and "interchange_A = interchange_rows A i n"
    and "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)"
    and "Gauss_Jordan_in_ij A i j = vec_lambda (\<lambda>s. if s = i then A' $ s
      else (row_add A' s i (- (interchange_A $ s $ j))) $ s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n
[PROOF STEP]
obtain m where Anj: "A $ m $ j \<noteq> 0 \<and> i \<le> m"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n

goal (1 subgoal):
 1. (\<And>m. A $ m $ j \<noteq> (0::'a) \<and> i \<le> m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define n where "n = (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)"
[PROOF STATE]
proof (state)
this:
n = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)
[PROOF STEP]
have P1: "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) = n"
[PROOF STATE]
proof (prove)
using this:
n = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)

goal (1 subgoal):
 1. (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n
[PROOF STEP]
have P2: "A $ n $ j \<noteq> 0" and P3: "i \<le> n"
[PROOF STATE]
proof (prove)
using this:
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n

goal (1 subgoal):
 1. A $ n $ j \<noteq> (0::'a) &&& i \<le> n
[PROOF STEP]
using LeastI [of "\<lambda>n. A $ n $ j \<noteq> 0 \<and> i \<le> n" m]
[PROOF STATE]
proof (prove)
using this:
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n
A $ m $ j \<noteq> (0::'a) \<and> i \<le> m \<Longrightarrow> A $ (LEAST x. A $ x $ j \<noteq> (0::'a) \<and> i \<le> x) $ j \<noteq> (0::'a) \<and> i \<le> (LEAST x. A $ x $ j \<noteq> (0::'a) \<and> i \<le> x)

goal (1 subgoal):
 1. A $ n $ j \<noteq> (0::'a) &&& i \<le> n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
A $ n $ j \<noteq> (0::'a)
i \<le> n

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define interchange_A where "interchange_A = interchange_rows A i n"
[PROOF STATE]
proof (state)
this:
interchange_A = interchange_rows A i n

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interchange_A = interchange_rows A i n
[PROOF STEP]
have P4: "interchange_A = interchange_rows A i n"
[PROOF STATE]
proof (prove)
using this:
interchange_A = interchange_rows A i n

goal (1 subgoal):
 1. interchange_A = interchange_rows A i n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interchange_A = interchange_rows A i n

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define A' where "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)"
[PROOF STATE]
proof (state)
this:
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)
[PROOF STEP]
have P5: "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)"
[PROOF STATE]
proof (prove)
using this:
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)

goal (1 subgoal):
 1. A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have P6: "Gauss_Jordan_in_ij A i j = vec_lambda (\<lambda>s. if s = i then A' $ s
    else (row_add A' s i (- (interchange_A $ s $ j))) $ s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)
[PROOF STEP]
by (simp only: Gauss_Jordan_in_ij_def P1 P4 [symmetric] P5 [symmetric] Let_def)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)

goal (1 subgoal):
 1. (\<And>n interchange_A A'. \<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n; A $ n $ j \<noteq> (0::'a); i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from P1 P2 P3 P4 P5 P6 that
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n
A $ n $ j \<noteq> (0::'a)
i \<le> n
interchange_A = interchange_rows A i n
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)
Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)
\<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = ?n; A $ ?n $ j \<noteq> (0::'a); i \<le> ?n; ?interchange_A = interchange_rows A i ?n; ?A' = mult_row ?interchange_A i ((1::'a) / ?interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then ?A' $ s else row_add ?A' s i (- ?interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = n
A $ n $ j \<noteq> (0::'a)
i \<le> n
interchange_A = interchange_rows A i n
A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j)
Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s)
\<lbrakk>(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = ?n; A $ ?n $ j \<noteq> (0::'a); i \<le> ?n; ?interchange_A = interchange_rows A i ?n; ?A' = mult_row ?interchange_A i ((1::'a) / ?interchange_A $ i $ j); Gauss_Jordan_in_ij A i j = (\<chi>s. if s = i then ?A' $ s else row_add ?A' s i (- ?interchange_A $ s $ j) $ s)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greatest_plus_one_eq_0:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A"
  shows "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
have "to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = card (UNIV::'rows set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = CARD('rows)

goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
thus "(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
using to_nat_plus_one_less_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST R. \<not> is_zero_row_upt_k R k A) + 1 = CARD('rows)
\<forall>a. a + (1::?'a) \<noteq> (0::?'a) \<longrightarrow> mod_type_class.to_nat a + 1 < CARD(?'a)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma from_nat_to_nat_greatest:
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows::{mod_type}"
  shows "from_nat (Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A))) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A))) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
unfolding Suc_eq_plus1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
unfolding to_nat_1[where ?'a='rows, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + mod_type_class.to_nat (1::'rows)) = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
unfolding add_to_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + mod_type_class.to_nat (1::'rows)) = mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + mod_type_class.to_nat (1::'rows))
[PROOF STEP]
..


[STATEMENT]
lemma greatest_less_zero_row:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and zero_i: "is_zero_row_upt_k i k A"
  and not_all_zero: "\<not> (\<forall>a. is_zero_row_upt_k a k A)"
  shows "(GREATEST m. \<not> is_zero_row_upt_k m k A) < i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k A) < i
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i \<Longrightarrow> False
[PROOF STEP]
assume not_less_i: "\<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i"
[PROOF STATE]
proof (state)
this:
\<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i

goal (1 subgoal):
 1. \<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i \<Longrightarrow> False
[PROOF STEP]
have i_less_greatest: "i < (GREATEST m. \<not> is_zero_row_upt_k m k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < (GREATEST m. \<not> is_zero_row_upt_k m k A)
[PROOF STEP]
by (metis (mono_tags, lifting) GreatestI neqE not_all_zero not_less_i zero_i)
[PROOF STATE]
proof (state)
this:
i < (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. \<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i \<Longrightarrow> False
[PROOF STEP]
have "is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A
[PROOF STEP]
using r zero_i i_less_greatest
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k
is_zero_row_upt_k i k A
i < (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))
is_zero_row_upt_k i k A
i < (GREATEST m. \<not> is_zero_row_upt_k m k A)

goal (1 subgoal):
 1. is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A

goal (1 subgoal):
 1. \<not> (GREATEST m. \<not> is_zero_row_upt_k m k A) < i \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A

goal (1 subgoal):
 1. False
[PROOF STEP]
using GreatestI_ex not_all_zero
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (GREATEST m. \<not> is_zero_row_upt_k m k A) k A
\<exists>x. ?P x \<Longrightarrow> ?P (Greatest ?P)
\<not> (\<forall>a. is_zero_row_upt_k a k A)

goal (1 subgoal):
 1. False
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed