>P \<sharp>* be; A\<^sub>P \<sharp>* bf; A\<^sub>P \<sharp>* bc; distinct (bn bb)\<rbrakk> \<Longrightarrow> thesis; x \<in> supp N; x \<sharp> \<Psi>; x \<sharp> M; x \<sharp> A\<^sub>P; x \<sharp> xvec; x \<sharp> yvec; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* M; A\<^sub>P \<sharp>* N; A\<^sub>P \<sharp>* P'; A\<^sub>P \<sharp>* xvec; A\<^sub>P \<sharp>* yvec; xvec \<sharp>* yvec; distinct xvec; distinct yvec; xvec \<sharp>* \<Psi>; xvec \<sharp>* P; xvec \<sharp>* M; xvec \<sharp>* \<Psi>\<^sub>P; yvec \<sharp>* \<Psi>\<^sub>P; yvec \<sharp>* \<Psi>; yvec \<sharp>* P; yvec \<sharp>* M; A\<^sub>P \<sharp>* C; A\<^sub>P \<sharp>* C'; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'a; A\<^sub>P \<sharp>* X; A\<^sub>P \<sharp>* Y; A\<^sub>P \<sharp>* Z; x \<sharp> C; x \<sharp> C'; x \<sharp> \<alpha>; x \<sharp> P'a; x \<sharp> X; x \<sharp> Y; x \<sharp> Z; xvec \<sharp>* C; xvec \<sharp>* C'; xvec \<sharp>* \<alpha>; xvec \<sharp>* P'a; xvec \<sharp>* X; xvec \<sharp>* Y; xvec \<sharp>* Z; yvec \<sharp>* C; yvec \<sharp>* C'; yvec \<sharp>* \<alpha>; yvec \<sharp>* P'a; yvec \<sharp>* X; yvec \<sharp>* Y; yvec \<sharp>* Z; M\<lparr>\<nu>*(xvec @ x # yvec)\<rparr>\<langle>N\<rangle> \<prec> P' = \<alpha> \<prec> P'a; \<And>p \<Psi>' \<Psi>\<^sub>P' A\<^sub>P'. \<lbrakk>set p \<subseteq> set (bn \<alpha>) \<times> set (bn (p \<bullet> \<alpha>)); (p \<bullet> \<Psi>\<^sub>P) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; distinctPerm p; extractFrame P'a = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; A\<^sub>P' \<sharp>* P'a; A\<^sub>P' \<sharp>* \<alpha>; A\<^sub>P' \<sharp>* (p \<bullet> \<alpha>); A\<^sub>P' \<sharp>* C; bn (p \<bullet> \<alpha>) \<sharp>* C'; bn (p \<bullet> \<alpha>) \<sharp>* \<alpha>; bn (p \<bullet> \<alpha>) \<sharp>* P'a; A\<^sub>P' \<sharp>* X; A\<^sub>P' \<sharp>* Y; A\<^sub>P' \<sharp>* Z; distinct A\<^sub>P'; bn (p \<bullet> \<alpha>) \<sharp>* X; bn (p \<bullet> \<alpha>) \<sharp>* Y; bn (p \<bullet> \<alpha>) \<sharp>* Z\<rbrakk> \<Longrightarrow> thesis; bn \<alpha> \<sharp>* subject \<alpha>; (x # A\<^sub>P) \<sharp>* \<lparr>\<nu>x\<rparr>P; (x # A\<^sub>P) \<sharp>* \<alpha>; (x # A\<^sub>P) \<sharp>* C; (x # A\<^sub>P) \<sharp>* C'; bn \<alpha> \<sharp>* \<lparr>\<nu>x\<rparr>P; bn \<alpha> \<sharp>* C'; \<alpha> \<noteq> \<tau>; bn \<alpha> \<sharp>* X; bn \<alpha> \<sharp>* Y; bn \<alpha> \<sharp>* Z; (x # A\<^sub>P) \<sharp>* X; (x # A\<^sub>P) \<sharp>* Y; (x # A\<^sub>P) \<sharp>* Z; (x # A\<^sub>P) \<sharp>* P'a; distinct (bn \<alpha>)\<rbrakk> \<Longrightarrow> thesis
 5. \<And>\<Psi> P \<alpha> P' x A\<^sub>P \<Psi>\<^sub>P C C' \<alpha>' P'a X Y Z thesis. \<lbrakk>\<Psi> \<rhd> P \<longmapsto> \<alpha> \<prec> P'; extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>; distinct A\<^sub>P; \<And>b ba bb bc bd be bf thesis. \<lbrakk>\<alpha> \<prec> P' = bb \<prec> bc; \<And>p \<Psi>' \<Psi>\<^sub>P' A\<^sub>P'. \<lbrakk>set p \<subseteq> set (bn bb) \<times> set (bn (p \<bullet> bb)); (p \<bullet> \<Psi>\<^sub>P) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>P'; distinctPerm p; extractFrame bc = \<langle>A\<^sub>P', \<Psi>\<^sub>P'\<rangle>; A\<^sub>P' \<sharp>* bc; A\<^sub>P' \<sharp>* bb; A\<^sub>P' \<sharp>* (p \<bullet> bb); A\<^sub>P' \<sharp>* b; bn (p \<bullet> bb) \<sharp>* ba; bn (p \<bullet> bb) \<sharp>* bb; bn (p \<bullet> bb) \<sharp>* bc; A\<^sub>P' \<sharp>* bd; A\<^sub>P' \<sharp>* be; A\<^sub>P' \<sharp>* bf; distinct A\<^sub>P'; bn (p \<bullet> bb) \<sharp>* bd; bn (p \<bullet> bb) \<sharp>* be; bn (p \<bullet> bb) \<sharp>* bf\<rbrakk> \<Longrightarrow> thesis; bn bb \<sharp>* subject bb; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* bb; A\<^sub>P \<sharp>* b; A\<^sub>P \<sharp>* ba; bn bb \<sharp>* P; bn bb \<sharp>* ba; bb \<noteq> \<tau>; bn bb \<sharp>* bd; bn bb \<sharp>* be; bn bb \<sharp>* bf; A\<^sub>P \<sharp>* bd; A\<^sub>P \<sharp>* be; A\<^sub>P \<sharp>* bf; A\<^sub>P \<sharp>* bc; distinct (bn bb)\<rbrakk> \<Longrightarrow> thesis; x \<sharp> \<Psi>; x \<sharp> \<alpha>; x \<sharp> A\<^sub>P; A\<^sub>P \<sharp>* \<Psi>; A\<^sub>P \<sharp>* P; A\<^sub>P \<sharp>* \<alpha>; A\<^sub>P \<sharp>* P'; distinct (bn \<alpha>); bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* \<Psi>\<^sub>P; A\<^sub>P \<sharp>* C; A\<^sub>P \<sharp>* C'; A\<^sub>P \<sharp>* \<alpha>'; A\<^sub>P \<sharp>* P'a; A\<^sub>P \<sharp>* X; A\<^sub>P \<sharp>* Y; A\<^sub>P \<sharp>* Z; x \<sharp> C; x \<sharp> C'; x \<sharp> \<alpha>'; x \<sharp> P'a; x \<sharp