177 | "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"

   177 | "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"

   178 | "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"

   178 | "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"

   179 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"

   179 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"

   180 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"

   180 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"

   181 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"

   181 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"

   182   apply(auto simp add: piMix_distinct piMix_eq_iff)

   183   apply(auto simp add: piMix_distinct piMix_eq_iff)

   183   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")

   184   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")

   184   unfolding eqvt_def

   185   unfolding eqvt_def

   185   apply(rule allI)

   186   apply(rule allI)

   186   apply(simp only: permute_fun_def)

   187   apply(simp only: permute_fun_def)

   292   apply(blast)

   293   apply(blast)

   293   apply(simp)

   294   apply(simp)

   294   apply(case_tac ba)

   295   apply(case_tac ba)

   295   apply(simp)

   296   apply(simp)

   296   apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))

   297   apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))

   297   apply(auto simp add: fresh_star_def)[1]

   299   apply(auto simp add: fresh_star_def)[1]

   298   apply(blast)

   300   apply(blast)

   299   apply(blast)

   301   apply(blast)

   300   apply(blast)

   302   apply(blast)

   301   apply(auto simp add: fresh_star_def)[1]

   304   apply(auto simp add: fresh_star_def)[1]

   302   apply(blast)

   305   apply(blast)

   303   apply(simp)

   306   apply(simp)

   304   apply(blast)

   307   apply(blast)

   305   --"compatibility"

   308   --"compatibility"