[STATEMENT]
theorem ate_termination:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and commR: "\<forall>r. (SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine)
                                     \<Rightarrow> (Proc HO) \<Rightarrow> (Proc HO) \<Rightarrow> bool)
                  Ate_M (HOs r) (SHOs r)"
  and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "\<exists>r v. decide (rho r p) = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from commG
[PROOF STATE]
proof (chain)
picking this:
SHOcommGlobal Ate_M HOs SHOs
[PROOF STEP]
obtain r' \<pi>1 \<pi>2
    where \<pi>ea: "card \<pi>1 > E - \<alpha>"
      and \<pi>t: "card \<pi>2 > T"
      and  hosho: "\<forall>p \<in> \<pi>1. (HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2)"
[PROOF STATE]
proof (prove)
using this:
SHOcommGlobal Ate_M HOs SHOs

goal (1 subgoal):
 1. (\<And>\<pi>1 \<pi>2 r'. \<lbrakk>E - \<alpha> < card \<pi>1; T < card \<pi>2; \<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card \<pi>1
T < card \<pi>2
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
obtain v where
    P1: "\<forall>pp. card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} > E - \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>p \<in> \<pi>1. \<forall>q \<in> \<pi>1. x (rho (Suc r') p) = x (rho (Suc r') q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>\<pi>1. \<forall>q\<in>\<pi>1. x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
assume p: "p \<in> \<pi>1" and q: "q \<in> \<pi>1"
[PROOF STATE]
proof (state)
this:
p \<in> \<pi>1
q \<in> \<pi>1

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>p
        where nxtp: "nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)"
          and mup: "\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>p. \<lbrakk>nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p); \<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>q
        where nxtq: "nextState Ate_M r' q (rho r' q) \<mu>q (rho (Suc r') q)"
          and muq: "\<mu>q \<in> SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>q. \<lbrakk>nextState Ate_M r' q (rho r' q) \<mu>q (rho (Suc r') q); \<mu>q \<in> SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M r' q (rho r' q) \<mu>q (rho (Suc r') q)
\<mu>q \<in> SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
from mup muq p q
[PROOF STATE]
proof (chain)
picking this:
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)
\<mu>q \<in> SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)
p \<in> \<pi>1
q \<in> \<pi>1
[PROOF STEP]
have "{qq. \<mu>q qq \<noteq> None}  = HOs r' q"
        and 2:"{qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
               \<supseteq> SHOs r' q \<inter> HOs r' q"
        and "{qq. \<mu>p qq \<noteq> None}  = HOs r' p"
        and 4:"{qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
               \<supseteq> SHOs r' p \<inter> HOs r' p"
[PROOF STATE]
proof (prove)
using this:
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)
\<mu>q \<in> SHOmsgVectors Ate_M r' q (rho r') (HOs r' q) (SHOs r' q)
p \<in> \<pi>1
q \<in> \<pi>1

goal (1 subgoal):
 1. ({qq. \<mu>q qq \<noteq> None} = HOs r' q &&& SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}) &&& {qq. \<mu>p qq \<noteq> None} = HOs r' p &&& SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def)
[PROOF STATE]
proof (state)
this:
{qq. \<mu>q qq \<noteq> None} = HOs r' q
SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
{qq. \<mu>p qq \<noteq> None} = HOs r' p
SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
with p q hosho
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
{qq. \<mu>q qq \<noteq> None} = HOs r' q
SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
{qq. \<mu>p qq \<noteq> None} = HOs r' p
SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
[PROOF STEP]
have aa:"\<pi>2 = {qq. \<mu>q qq \<noteq> None}"
        and cc:"\<pi>2 = {qq. \<mu>p qq \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
{qq. \<mu>q qq \<noteq> None} = HOs r' q
SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
{qq. \<mu>p qq \<noteq> None} = HOs r' p
SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}

goal (1 subgoal):
 1. \<pi>2 = {qq. \<mu>q qq \<noteq> None} &&& \<pi>2 = {qq. \<mu>p qq \<noteq> None}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
\<pi>2 = {qq. \<mu>p qq \<noteq> None}

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
from p q hosho 2
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
[PROOF STEP]
have bb:"{qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))} \<supseteq> \<pi>2"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
SHOs r' q \<inter> HOs r' q \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}

goal (1 subgoal):
 1. \<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
from p q hosho 4
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
[PROOF STEP]
have dd:"{qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))} \<supseteq> \<pi>2"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<pi>1
q \<in> \<pi>1
\<forall>p\<in>\<pi>1. HOs r' p = \<pi>2 \<and> SHOs r' p \<inter> HOs r' p = \<pi>2
SHOs r' p \<inter> HOs r' p \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}

goal (1 subgoal):
 1. \<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
have "Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
have "\<forall>qq. sendMsg Ate_M r' qq p (rho r' qq)
                   = sendMsg Ate_M r' qq q (rho r' qq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qq. sendMsg Ate_M r' qq p (rho r' qq) = sendMsg Ate_M r' qq q (rho r' qq)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M r' qq p (rho r' qq) = sendMsg Ate_M r' qq q (rho r' qq)

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
with aa bb cc dd
[PROOF STATE]
proof (chain)
picking this:
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
\<forall>qq. sendMsg Ate_M r' qq p (rho r' qq) = sendMsg Ate_M r' qq q (rho r' qq)
[PROOF STEP]
have "\<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq"
[PROOF STATE]
proof (prove)
using this:
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
\<forall>qq. sendMsg Ate_M r' qq p (rho r' qq) = sendMsg Ate_M r' qq q (rho r' qq)

goal (1 subgoal):
 1. \<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
from aa bb cc dd
[PROOF STATE]
proof (chain)
picking this:
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}
[PROOF STEP]
have "{qq. \<mu>p qq \<noteq> None} = {qq. \<mu>q qq \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>q qq = Some (sendMsg Ate_M r' qq q (rho r' qq))}
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
\<pi>2 \<subseteq> {qq. \<mu>p qq = Some (sendMsg Ate_M r' qq p (rho r' qq))}

goal (1 subgoal):
 1. {qq. \<mu>p qq \<noteq> None} = {qq. \<mu>q qq \<noteq> None}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. \<mu>p qq \<noteq> None} = {qq. \<mu>q qq \<noteq> None}

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
hence "\<forall>qq. \<mu>p qq = None \<longleftrightarrow> \<mu>q qq = None"
[PROOF STATE]
proof (prove)
using this:
{qq. \<mu>p qq \<noteq> None} = {qq. \<mu>q qq \<noteq> None}

goal (1 subgoal):
 1. \<forall>qq. (\<mu>p qq = None) = (\<mu>q qq = None)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>qq. (\<mu>p qq = None) = (\<mu>q qq = None)

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
hence "\<forall>qq. \<mu>p qq = None \<longrightarrow> \<mu>p qq = \<mu>q qq"
[PROOF STATE]
proof (prove)
using this:
\<forall>qq. (\<mu>p qq = None) = (\<mu>q qq = None)

goal (1 subgoal):
 1. \<forall>qq. \<mu>p qq = None \<longrightarrow> \<mu>p qq = \<mu>q qq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>qq. \<mu>p qq = None \<longrightarrow> \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq
\<forall>qq. \<mu>p qq = None \<longrightarrow> \<mu>p qq = \<mu>q qq
[PROOF STEP]
have "\<forall>qq. \<mu>p qq = \<mu>q qq"
[PROOF STATE]
proof (prove)
using this:
\<forall>qq. \<mu>p qq \<noteq> None \<longrightarrow> \<mu>p qq = \<mu>q qq
\<forall>qq. \<mu>p qq = None \<longrightarrow> \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. \<forall>qq. \<mu>p qq = \<mu>q qq
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>qq. \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>qq. \<mu>p qq = \<mu>q qq

goal (1 subgoal):
 1. Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
by (auto simp: mostOftenRcvd_def)
[PROOF STATE]
proof (state)
this:
Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> \<pi>1; q \<in> \<pi>1\<rbrakk> \<Longrightarrow> x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
with \<pi>t aa nxtq \<pi>t cc nxtp
[PROOF STATE]
proof (chain)
picking this:
T < card \<pi>2
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
nextState Ate_M r' q (rho r' q) \<mu>q (rho (Suc r') q)
T < card \<pi>2
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)
[PROOF STEP]
show "x (rho (Suc r') p) = x (rho (Suc r') q)"
[PROOF STATE]
proof (prove)
using this:
T < card \<pi>2
\<pi>2 = {qq. \<mu>q qq \<noteq> None}
nextState Ate_M r' q (rho r' q) \<mu>q (rho (Suc r') q)
T < card \<pi>2
\<pi>2 = {qq. \<mu>p qq \<noteq> None}
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
Min (mostOftenRcvd \<mu>p) = Min (mostOftenRcvd \<mu>q)

goal (1 subgoal):
 1. x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
x (rho (Suc r') p) = x (rho (Suc r') q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>\<pi>1. \<forall>q\<in>\<pi>1. x (rho (Suc r') p) = x (rho (Suc r') q)

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>\<pi>1. \<forall>q\<in>\<pi>1. x (rho (Suc r') p) = x (rho (Suc r') q)
[PROOF STEP]
obtain v where Pv:"\<forall>p \<in> \<pi>1. x (rho (Suc r') p) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>\<pi>1. \<forall>q\<in>\<pi>1. x (rho (Suc r') p) = x (rho (Suc r') q)

goal (1 subgoal):
 1. (\<And>v. \<forall>p\<in>\<pi>1. x (rho (Suc r') p) = v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>\<pi>1. x (rho (Suc r') p) = v

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>\<pi>1. x (rho (Suc r') p) = v

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from Pv
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>\<pi>1. x (rho (Suc r') p) = v
[PROOF STEP]
have "\<forall>p \<in> \<pi>1. sendMsg Ate_M (Suc r') p pp (rho (Suc r') p) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>\<pi>1. x (rho (Suc r') p) = v

goal (1 subgoal):
 1. \<forall>p\<in>\<pi>1. sendMsg Ate_M (Suc r') p pp (rho (Suc r') p) = v
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>\<pi>1. sendMsg Ate_M (Suc r') p pp (rho (Suc r') p) = v

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "card \<pi>1 \<le> card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>\<pi>1. sendMsg Ate_M (Suc r') p pp (rho (Suc r') p) = v

goal (1 subgoal):
 1. card \<pi>1 \<le> card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}
[PROOF STEP]
by (auto intro: card_mono)
[PROOF STATE]
proof (state)
this:
card \<pi>1 \<le> card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<pi>ea
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card \<pi>1
card \<pi>1 \<le> card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card \<pi>1
card \<pi>1 \<le> card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq ?pp7 (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. (\<And>v. \<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = ?v5} \<Longrightarrow> thesis
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq ?pp7 (rho (Suc r') qq) = v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = ?v5} \<Longrightarrow> thesis
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq ?pp7 (rho (Suc r') qq) = v}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
fix k pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}"
      (is "?P k")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + 0) qq pp (rho (Suc r' + 0) qq) = v}
 2. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}
[PROOF STEP]
show "?P 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>pp. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r') qq pp (rho (Suc r') qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + 0) qq pp (rho (Suc r' + 0) qq) = v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + 0) qq pp (rho (Suc r' + 0) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
assume ih: "?P k"
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
from commR
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine)
                               \<Rightarrow> (Proc HO) \<Rightarrow> (Proc HO) \<Rightarrow> bool)
                Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
from ih
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. x (rho (Suc r' + k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (Suc r' + k) qq) = v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
E - \<alpha> < card {qq. x (rho (Suc r' + k) qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. x (rho (Suc r' + Suc k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
E - \<alpha> < card {qq. x (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. x (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
by (rule common_x_induct[OF run])
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. x (rho (Suc r' + Suc k) qq) = v}

goal (1 subgoal):
 1. \<And>k. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v} \<Longrightarrow> E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
thus "?P (Suc k)"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. x (rho (Suc r' + Suc k) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + Suc k) qq pp (rho (Suc r' + Suc k) qq) = v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
note P2 = this
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
fix k pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
assume ppupdatex: "x (rho (Suc r' + Suc k) pp) \<noteq> x (rho (Suc r' + k) pp)"
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k) pp) \<noteq> x (rho (Suc r' + k) pp)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from commR
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val) SHOMachine)
                            \<Rightarrow> (Proc HO) \<Rightarrow> (Proc HO) \<Rightarrow> bool)
              Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>pp
      where nxt:"nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp
                           (rho (Suc r' + Suc k) pp)"
        and mu: "\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k))
                           (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>pp. \<lbrakk>nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp); \<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from nxt ppupdatex
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
x (rho (Suc r' + Suc k) pp) \<noteq> x (rho (Suc r' + k) pp)
[PROOF STEP]
have threshold_T: "card {qq. \<mu>pp qq \<noteq> None} > T"
      and xsmall: "x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
x (rho (Suc r' + Suc k) pp) \<noteq> x (rho (Suc r' + k) pp)

goal (1 subgoal):
 1. T < card {qq. \<mu>pp qq \<noteq> None} &&& x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
T < card {qq. \<mu>pp qq \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T < card {qq. \<mu>pp qq \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)
T < card {qq. \<mu>pp qq \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
have "mostOftenRcvd \<mu>pp = {v}"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)
T < card {qq. \<mu>pp qq \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>pp = {v}
[PROOF STEP]
by (auto dest!: mostOftenRcvd_v)
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>pp = {v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
with xsmall
[PROOF STATE]
proof (chain)
picking this:
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
mostOftenRcvd \<mu>pp = {v}
[PROOF STEP]
have "x (rho (Suc r' + Suc k) pp) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
mostOftenRcvd \<mu>pp = {v}

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k) pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc ?k7) ?pp7) \<noteq> x (rho (Suc r' + ?k7) ?pp7) \<Longrightarrow> x (rho (Suc r' + Suc ?k7) ?pp7) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
note P3 = this
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc ?k7) ?pp7) \<noteq> x (rho (Suc r' + ?k7) ?pp7) \<Longrightarrow> x (rho (Suc r' + Suc ?k7) ?pp7) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
have P4:"\<forall>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
fix pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
from commG
[PROOF STATE]
proof (chain)
picking this:
SHOcommGlobal Ate_M HOs SHOs
[PROOF STEP]
have "\<exists>r'' > r'. card (HOs r'' pp) > T"
[PROOF STATE]
proof (prove)
using this:
SHOcommGlobal Ate_M HOs SHOs

goal (1 subgoal):
 1. \<exists>r''>r'. T < card (HOs r'' pp)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)
[PROOF STATE]
proof (state)
this:
\<exists>r''>r'. T < card (HOs r'' pp)

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r''>r'. T < card (HOs r'' pp)
[PROOF STEP]
obtain k where "Suc r' + k > r'" and t:"card (HOs (Suc r' + k) pp) > T"
[PROOF STATE]
proof (prove)
using this:
\<exists>r''>r'. T < card (HOs r'' pp)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>r' < Suc r' + k; T < card (HOs (Suc r' + k) pp)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: less_imp_Suc_add)
[PROOF STATE]
proof (state)
this:
r' < Suc r' + k
T < card (HOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r' < Suc r' + k
T < card (HOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>pp
      where nxt: "nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp
                                  (rho (Suc r' + Suc k) pp)"
        and mu: "\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k))
                                  (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>pp. \<lbrakk>nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp); \<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
have "x (rho (Suc r' + Suc k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
from commR
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "(SHOcommPerRd::((Proc, 'val::linorder pstate, 'val::linorder) SHOMachine)
                                \<Rightarrow> (Proc HO) \<Rightarrow> (Proc HO) \<Rightarrow> bool)
                Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
from mu
[PROOF STATE]
proof (chain)
picking this:
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)
[PROOF STEP]
have "HOs (Suc r' + k) pp = {q. \<mu>pp q \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. HOs (Suc r' + k) pp = {q. \<mu>pp q \<noteq> None}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def)
[PROOF STATE]
proof (state)
this:
HOs (Suc r' + k) pp = {q. \<mu>pp q \<noteq> None}

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
with nxt t
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
T < card (HOs (Suc r' + k) pp)
HOs (Suc r' + k) pp = {q. \<mu>pp q \<noteq> None}
[PROOF STEP]
have threshold_T: "card {q. \<mu>pp q \<noteq> None} > T"
        and xsmall: "x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
T < card (HOs (Suc r' + k) pp)
HOs (Suc r' + k) pp = {q. \<mu>pp q \<noteq> None}

goal (1 subgoal):
 1. T < card {q. \<mu>pp q \<noteq> None} &&& x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
T < card {q. \<mu>pp q \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T < card {q. \<mu>pp q \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}
[PROOF STEP]
have "E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + ?k7) qq ?pp7 (rho (Suc r' + ?k7) qq) = v}

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
T < card {q. \<mu>pp q \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
[PROOF STEP]
have "mostOftenRcvd \<mu>pp = {v}"
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
T < card {q. \<mu>pp q \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}

goal (1 subgoal):
 1. mostOftenRcvd \<mu>pp = {v}
[PROOF STEP]
using nxt mu
[PROOF STATE]
proof (prove)
using this:
SHOcommPerRd Ate_M (HOs (Suc r' + k)) (SHOs (Suc r' + k))
T < card {q. \<mu>pp q \<noteq> None}
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
E - \<alpha> < card {qq. sendMsg Ate_M (Suc r' + k) qq pp (rho (Suc r' + k) qq) = v}
nextState Ate_M (Suc r' + k) pp (rho (Suc r' + k) pp) \<mu>pp (rho (Suc r' + Suc k) pp)
\<mu>pp \<in> SHOmsgVectors Ate_M (Suc r' + k) pp (rho (Suc r' + k)) (HOs (Suc r' + k) pp) (SHOs (Suc r' + k) pp)

goal (1 subgoal):
 1. mostOftenRcvd \<mu>pp = {v}
[PROOF STEP]
by (auto dest!: mostOftenRcvd_v)
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>pp = {v}

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
with xsmall
[PROOF STATE]
proof (chain)
picking this:
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
mostOftenRcvd \<mu>pp = {v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r' + Suc k) pp) = Min (mostOftenRcvd \<mu>pp)
mostOftenRcvd \<mu>pp = {v}

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k) pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k) pp) = v

goal (1 subgoal):
 1. \<And>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
thus "\<exists>k. x (rho (Suc r' + Suc k) pp) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r' + Suc k) pp) = v

goal (1 subgoal):
 1. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>k. x (rho (Suc r' + Suc k) pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
have P5a: "\<forall>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
fix pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
\<forall>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v
[PROOF STEP]
obtain rk where
      xrrv: "x (rho (Suc r' + Suc rk) pp) = v" (is "x (rho ?rr pp) = v")
[PROOF STATE]
proof (prove)
using this:
\<forall>pp. \<exists>k. x (rho (Suc r' + Suc k) pp) = v

goal (1 subgoal):
 1. (\<And>rk. x (rho (Suc r' + Suc rk) pp) = v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk) pp) = v

goal (1 subgoal):
 1. \<And>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
have "\<forall>k. x (rho (?rr + k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. x (rho (Suc r' + Suc rk + k) pp) = v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v
[PROOF STEP]
show "x (rho (?rr + k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + k) pp) = v
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x (rho (Suc r' + Suc rk + 0) pp) = v
 2. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
from xrrv
[PROOF STATE]
proof (chain)
picking this:
x (rho (Suc r' + Suc rk) pp) = v
[PROOF STEP]
show "x (rho (?rr + 0) pp) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r' + Suc rk) pp) = v

goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + 0) pp) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk + 0) pp) = v

goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
assume ih: "x (rho (?rr + k) pp) = v"
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk + k) pp) = v

goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
obtain k' where rrk: "Suc r' + k' = ?rr + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. Suc r' + k' = Suc r' + Suc rk + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc r' + k' = Suc r' + Suc rk + k

goal (1 subgoal):
 1. \<And>k. x (rho (Suc r' + Suc rk + k) pp) = v \<Longrightarrow> x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
show "x (rho (?rr + Suc k) pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + Suc k) pp) = v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v \<Longrightarrow> False
[PROOF STEP]
assume nv: "x (rho (?rr + Suc k) pp) \<noteq> v"
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v

goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with rrk ih
[PROOF STATE]
proof (chain)
picking this:
Suc r' + k' = Suc r' + Suc rk + k
x (rho (Suc r' + Suc rk + k) pp) = v
x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v
[PROOF STEP]
have "x (rho (Suc r' + Suc k') pp) \<noteq> x (rho (Suc r' + k') pp)"
[PROOF STATE]
proof (prove)
using this:
Suc r' + k' = Suc r' + Suc rk + k
x (rho (Suc r' + Suc rk + k) pp) = v
x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k') pp) \<noteq> x (rho (Suc r' + k') pp)
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k') pp) \<noteq> x (rho (Suc r' + k') pp)

goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v \<Longrightarrow> False
[PROOF STEP]
hence "x (rho (Suc r' + Suc k') pp) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r' + Suc k') pp) \<noteq> x (rho (Suc r' + k') pp)

goal (1 subgoal):
 1. x (rho (Suc r' + Suc k') pp) = v
[PROOF STEP]
by (rule P3)
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc k') pp) = v

goal (1 subgoal):
 1. x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with rrk nv
[PROOF STATE]
proof (chain)
picking this:
Suc r' + k' = Suc r' + Suc rk + k
x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v
x (rho (Suc r' + Suc k') pp) = v
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Suc r' + k' = Suc r' + Suc rk + k
x (rho (Suc r' + Suc rk + Suc k) pp) \<noteq> v
x (rho (Suc r' + Suc k') pp) = v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk + Suc k) pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x (rho (Suc r' + Suc rk + k) pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k. x (rho (Suc r' + Suc rk + k) pp) = v

goal (1 subgoal):
 1. \<And>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
thus "\<exists>rr. \<forall>k. x (rho (rr + k) pp) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. x (rho (Suc r' + Suc rk + k) pp) = v

goal (1 subgoal):
 1. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>rr. \<forall>k. x (rho (rr + k) pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from P5a
[PROOF STATE]
proof (chain)
picking this:
\<forall>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v
[PROOF STEP]
have "\<exists>F. \<forall>pp k. x (rho (F pp + k) pp) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>pp. \<exists>rr. \<forall>k. x (rho (rr + k) pp) = v

goal (1 subgoal):
 1. \<exists>F. \<forall>pp k. x (rho (F pp + k) pp) = v
[PROOF STEP]
by (rule choice)
[PROOF STATE]
proof (state)
this:
\<exists>F. \<forall>pp k. x (rho (F pp + k) pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>F. \<forall>pp k. x (rho (F pp + k) pp) = v
[PROOF STEP]
obtain R::"(Proc \<Rightarrow> nat)"
    where imgR: "R ` (UNIV::Proc set) \<noteq> {}"
      and R: "\<forall>pp k. x (rho (R pp + k) pp) = v"
[PROOF STATE]
proof (prove)
using this:
\<exists>F. \<forall>pp k. x (rho (F pp + k) pp) = v

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>range R \<noteq> {}; \<forall>pp k. x (rho (R pp + k) pp) = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
range R \<noteq> {}
\<forall>pp k. x (rho (R pp + k) pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define rr where "rr = Max (R ` UNIV)"
[PROOF STATE]
proof (state)
this:
rr = Max (range R)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
have P5: "\<forall>r' > rr. \<forall>pp. x (rho r' pp) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r'>rr. \<forall>pp. x (rho r' pp) = v
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r' pp. rr < r' \<Longrightarrow> x (rho r' pp) = v
[PROOF STEP]
fix r' pp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r' pp. rr < r' \<Longrightarrow> x (rho r' pp) = v
[PROOF STEP]
assume r': "r' > rr"
[PROOF STATE]
proof (state)
this:
rr < r'

goal (1 subgoal):
 1. \<And>r' pp. rr < r' \<Longrightarrow> x (rho r' pp) = v
[PROOF STEP]
hence "r' > R pp"
[PROOF STATE]
proof (prove)
using this:
rr < r'

goal (1 subgoal):
 1. R pp < r'
[PROOF STEP]
by (auto simp: rr_def)
[PROOF STATE]
proof (state)
this:
R pp < r'

goal (1 subgoal):
 1. \<And>r' pp. rr < r' \<Longrightarrow> x (rho r' pp) = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R pp < r'
[PROOF STEP]
obtain i where "r' = R pp + i"
[PROOF STATE]
proof (prove)
using this:
R pp < r'

goal (1 subgoal):
 1. (\<And>i. r' = R pp + i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: less_imp_Suc_add)
[PROOF STATE]
proof (state)
this:
r' = R pp + i

goal (1 subgoal):
 1. \<And>r' pp. rr < r' \<Longrightarrow> x (rho r' pp) = v
[PROOF STEP]
with R
[PROOF STATE]
proof (chain)
picking this:
\<forall>pp k. x (rho (R pp + k) pp) = v
r' = R pp + i
[PROOF STEP]
show "x (rho r' pp) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>pp k. x (rho (R pp + k) pp) = v
r' = R pp + i

goal (1 subgoal):
 1. x (rho r' pp) = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x (rho r' pp) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r'>rr. \<forall>pp. x (rho r' pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from commG
[PROOF STATE]
proof (chain)
picking this:
SHOcommGlobal Ate_M HOs SHOs
[PROOF STEP]
have "\<exists>r' > rr. card (SHOs r' p \<inter> HOs r' p) > E"
[PROOF STATE]
proof (prove)
using this:
SHOcommGlobal Ate_M HOs SHOs

goal (1 subgoal):
 1. \<exists>r'>rr. E < card (SHOs r' p \<inter> HOs r' p)
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commGlobal_def)
[PROOF STATE]
proof (state)
this:
\<exists>r'>rr. E < card (SHOs r' p \<inter> HOs r' p)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
with P5
[PROOF STATE]
proof (chain)
picking this:
\<forall>r'>rr. \<forall>pp. x (rho r' pp) = v
\<exists>r'>rr. E < card (SHOs r' p \<inter> HOs r' p)
[PROOF STEP]
obtain r'
    where "r' > rr"
      and "card (SHOs r' p \<inter> HOs r' p) > E"
      and "\<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>r'>rr. \<forall>pp. x (rho r' pp) = v
\<exists>r'>rr. E < card (SHOs r' p \<inter> HOs r' p)

goal (1 subgoal):
 1. (\<And>r'. \<lbrakk>rr < r'; E < card (SHOs r' p \<inter> HOs r' p); \<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
rr < r'
E < card (SHOs r' p \<inter> HOs r' p)
\<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rr < r'
E < card (SHOs r' p \<inter> HOs r' p)
\<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>p
    where nxt: "nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)"
      and mu: "\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

goal (1 subgoal):
 1. (\<And>\<mu>p. \<lbrakk>nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p); \<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq)
[PROOF STATE]
proof (state)
this:
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from mu
[PROOF STATE]
proof (chain)
picking this:
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)
[PROOF STEP]
have "card (SHOs r' p \<inter> HOs r' p)
        \<le> card {q. \<mu>p q = Some (sendMsg Ate_M r' q p (rho r' q))}"
[PROOF STATE]
proof (prove)
using this:
\<mu>p \<in> SHOmsgVectors Ate_M r' p (rho r') (HOs r' p) (SHOs r' p)

goal (1 subgoal):
 1. card (SHOs r' p \<inter> HOs r' p) \<le> card {q. \<mu>p q = Some (sendMsg Ate_M r' q p (rho r' q))}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def intro: card_mono)
[PROOF STATE]
proof (state)
this:
card (SHOs r' p \<inter> HOs r' p) \<le> card {q. \<mu>p q = Some (sendMsg Ate_M r' q p (rho r' q))}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rr < r'
E < card (SHOs r' p \<inter> HOs r' p)
\<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v
card (SHOs r' p \<inter> HOs r' p) \<le> card {q. \<mu>p q = Some (sendMsg Ate_M r' q p (rho r' q))}
[PROOF STEP]
have threshold_E: "card {q. \<mu>p q = Some v} > E"
[PROOF STATE]
proof (prove)
using this:
rr < r'
E < card (SHOs r' p \<inter> HOs r' p)
\<forall>pp. sendMsg Ate_M r' pp p (rho r' pp) = v
card (SHOs r' p \<inter> HOs r' p) \<le> card {q. \<mu>p q = Some (sendMsg Ate_M r' q p (rho r' q))}

goal (1 subgoal):
 1. E < card {q. \<mu>p q = Some v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E < card {q. \<mu>p q = Some v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
with nxt
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
E < card {q. \<mu>p q = Some v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M r' p (rho r' p) \<mu>p (rho (Suc r') p)
E < card {q. \<mu>p q = Some v}

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def nextState_def Ate_nextState_def)
[PROOF STATE]
proof (state)
this:
\<exists>r v. decide (rho r p) = Some v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ate_weak_consensus:
  assumes run: "SHORun Ate_M rho HOs SHOs"
      and commR: "\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "weak_consensus (x \<circ> (rho 0)) decide rho"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_consensus (x \<circ> rho 0) decide rho
[PROOF STEP]
unfolding weak_consensus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>v. (\<forall>p. (x \<circ> rho 0) p = v) \<longrightarrow> (\<forall>n p w. decide (rho n p) = Some w \<longrightarrow> w = v)) \<and> (\<forall>m n p q v w. decide (rho m p) = Some v \<and> decide (rho n q) = Some w \<longrightarrow> v = w) \<and> (\<forall>p. \<exists>n. decide (rho n p) \<noteq> None)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
SHOcommGlobal Ate_M HOs SHOs

goal (1 subgoal):
 1. (\<forall>v. (\<forall>p. (x \<circ> rho 0) p = v) \<longrightarrow> (\<forall>n p w. decide (rho n p) = Some w \<longrightarrow> w = v)) \<and> (\<forall>m n p q v w. decide (rho m p) = Some v \<and> decide (rho n q) = Some w \<longrightarrow> v = w) \<and> (\<forall>p. \<exists>n. decide (rho n p) \<noteq> None)
[PROOF STEP]
by (auto elim: ate_validity ate_agreement ate_termination)


[STATEMENT]
theorem ate_weak_consensus_fg:
  assumes run: "fg_run Ate_M rho HOs SHOs (\<lambda>r q. undefined)"
      and commR: "\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ate_M HOs SHOs"
  shows "weak_consensus (\<lambda>p. x (state (rho 0) p)) decide (state \<circ> rho)"
    (is "weak_consensus ?inits _ _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_consensus (\<lambda>p. x (state (rho 0) p)) decide (state \<circ> rho)
[PROOF STEP]
proof (rule local_property_reduction[OF run weak_consensus_is_local])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>crho. \<lbrakk>CSHORun Ate_M crho HOs SHOs (\<lambda>r q. undefined); crho 0 = state (rho 0)\<rbrakk> \<Longrightarrow> weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crho
[PROOF STEP]
fix crun
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>crho. \<lbrakk>CSHORun Ate_M crho HOs SHOs (\<lambda>r q. undefined); crho 0 = state (rho 0)\<rbrakk> \<Longrightarrow> weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crho
[PROOF STEP]
assume crun: "CSHORun Ate_M crun HOs SHOs (\<lambda>r q. undefined)"
     and init: "crun 0 = state (rho 0)"
[PROOF STATE]
proof (state)
this:
CSHORun Ate_M crun HOs SHOs (\<lambda>r q. undefined)
crun 0 = state (rho 0)

goal (1 subgoal):
 1. \<And>crho. \<lbrakk>CSHORun Ate_M crho HOs SHOs (\<lambda>r q. undefined); crho 0 = state (rho 0)\<rbrakk> \<Longrightarrow> weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crho
[PROOF STEP]
from crun
[PROOF STATE]
proof (chain)
picking this:
CSHORun Ate_M crun HOs SHOs (\<lambda>r q. undefined)
[PROOF STEP]
have "SHORun Ate_M crun HOs SHOs"
[PROOF STATE]
proof (prove)
using this:
CSHORun Ate_M crun HOs SHOs (\<lambda>r q. undefined)

goal (1 subgoal):
 1. SHORun Ate_M crun HOs SHOs
[PROOF STEP]
by (unfold SHORun_def)
[PROOF STATE]
proof (state)
this:
SHORun Ate_M crun HOs SHOs

goal (1 subgoal):
 1. \<And>crho. \<lbrakk>CSHORun Ate_M crho HOs SHOs (\<lambda>r q. undefined); crho 0 = state (rho 0)\<rbrakk> \<Longrightarrow> weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crho
[PROOF STEP]
from this commR commG
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M crun HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
SHOcommGlobal Ate_M HOs SHOs
[PROOF STEP]
have "weak_consensus (x \<circ> (crun 0)) decide crun"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M crun HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
SHOcommGlobal Ate_M HOs SHOs

goal (1 subgoal):
 1. weak_consensus (x \<circ> crun 0) decide crun
[PROOF STEP]
by (rule ate_weak_consensus)
[PROOF STATE]
proof (state)
this:
weak_consensus (x \<circ> crun 0) decide crun

goal (1 subgoal):
 1. \<And>crho. \<lbrakk>CSHORun Ate_M crho HOs SHOs (\<lambda>r q. undefined); crho 0 = state (rho 0)\<rbrakk> \<Longrightarrow> weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crho
[PROOF STEP]
with init
[PROOF STATE]
proof (chain)
picking this:
crun 0 = state (rho 0)
weak_consensus (x \<circ> crun 0) decide crun
[PROOF STEP]
show "weak_consensus ?inits decide crun"
[PROOF STATE]
proof (prove)
using this:
crun 0 = state (rho 0)
weak_consensus (x \<circ> crun 0) decide crun

goal (1 subgoal):
 1. weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crun
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
weak_consensus (\<lambda>p. x (state (rho 0) p)) decide crun

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]:
  "NullPointer \<in> sys_xcpts \<and>
   OutOfMemory \<in> sys_xcpts \<and>
   ClassCast \<in> sys_xcpts \<and>
   ArrayIndexOutOfBounds \<in> sys_xcpts \<and>
   ArrayStore \<in> sys_xcpts \<and>
   NegativeArraySize \<in> sys_xcpts \<and>
   IllegalMonitorState \<in> sys_xcpts \<and>
   IllegalThreadState \<in> sys_xcpts \<and>
   InterruptedException \<in> sys_xcpts \<and>
   ArithmeticException \<in> sys_xcpts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NullPointer \<in> sys_xcpts \<and> OutOfMemory \<in> sys_xcpts \<and> ClassCast \<in> sys_xcpts \<and> ArrayIndexOutOfBounds \<in> sys_xcpts \<and> ArrayStore \<in> sys_xcpts \<and> NegativeArraySize \<in> sys_xcpts \<and> IllegalMonitorState \<in> sys_xcpts \<and> IllegalThreadState \<in> sys_xcpts \<and> InterruptedException \<in> sys_xcpts \<and> ArithmeticException \<in> sys_xcpts
[PROOF STEP]
by(simp add: sys_xcpts_def sys_xcpts_list_def)


[STATEMENT]
lemma sys_xcpts_cases [consumes 1, cases set]:
  "\<lbrakk> C \<in> sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast;
     P ArrayIndexOutOfBounds; P ArrayStore; P NegativeArraySize;
     P ArithmeticException;
     P IllegalMonitorState; P IllegalThreadState; P InterruptedException \<rbrakk>
  \<Longrightarrow> P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast; P ArrayIndexOutOfBounds; P ArrayStore; P NegativeArraySize; P ArithmeticException; P IllegalMonitorState; P IllegalThreadState; P InterruptedException\<rbrakk> \<Longrightarrow> P C
[PROOF STEP]
by (auto simp add: sys_xcpts_def sys_xcpts_list_def)


[STATEMENT]
lemma OutOfMemory_not_Object[simp]: "OutOfMemory \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OutOfMemory \<noteq> Object
[PROOF STEP]
by(simp add: OutOfMemory_def Object_def)


[STATEMENT]
lemma ClassCast_not_Object[simp]: "ClassCast \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ClassCast \<noteq> Object
[PROOF STEP]
by(simp add: ClassCast_def Object_def)


[STATEMENT]
lemma NullPointer_not_Object[simp]: "NullPointer \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NullPointer \<noteq> Object
[PROOF STEP]
by(simp add: NullPointer_def Object_def)


[STATEMENT]
lemma ArrayIndexOutOfBounds_not_Object[simp]: "ArrayIndexOutOfBounds \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ArrayIndexOutOfBounds \<noteq> Object
[PROOF STEP]
by(simp add: ArrayIndexOutOfBounds_def Object_def)


[STATEMENT]
lemma ArrayStore_not_Object[simp]: "ArrayStore \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ArrayStore \<noteq> Object
[PROOF STEP]
by(simp add: ArrayStore_def Object_def)


[STATEMENT]
lemma NegativeArraySize_not_Object[simp]: "NegativeArraySize \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NegativeArraySize \<noteq> Object
[PROOF STEP]
by(simp add: NegativeArraySize_def Object_def)


[STATEMENT]
lemma ArithmeticException_not_Object[simp]: "ArithmeticException \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ArithmeticException \<noteq> Object
[PROOF STEP]
by(simp add: ArithmeticException_def Object_def)


[STATEMENT]
lemma IllegalMonitorState_not_Object[simp]: "IllegalMonitorState \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IllegalMonitorState \<noteq> Object
[PROOF STEP]
by(simp add: IllegalMonitorState_def Object_def)


[STATEMENT]
lemma IllegalThreadState_not_Object[simp]: "IllegalThreadState \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IllegalThreadState \<noteq> Object
[PROOF STEP]
by(simp add: IllegalThreadState_def Object_def)


[STATEMENT]
lemma InterruptedException_not_Object[simp]: "InterruptedException \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InterruptedException \<noteq> Object
[PROOF STEP]
by(simp add: InterruptedException_def Object_def)


[STATEMENT]
lemma sys_xcpts_neqs_aux:
  "NullPointer \<noteq> ClassCast" "NullPointer \<noteq> OutOfMemory" "NullPointer \<noteq> ArrayIndexOutOfBounds"
  "NullPointer \<noteq> ArrayStore" "NullPointer \<noteq> NegativeArraySize" "NullPointer \<noteq> IllegalMonitorState"
  "NullPointer \<noteq> IllegalThreadState" "NullPointer \<noteq> InterruptedException" "NullPointer \<noteq> ArithmeticException"
  "ClassCast \<noteq> OutOfMemory" "ClassCast \<noteq> ArrayIndexOutOfBounds"
  "ClassCast \<noteq> ArrayStore" "ClassCast \<noteq> NegativeArraySize" "ClassCast \<noteq> IllegalMonitorState"
  "ClassCast \<noteq> IllegalThreadState" "ClassCast \<noteq> InterruptedException" "ClassCast \<noteq> ArithmeticException"
  "OutOfMemory \<noteq> ArrayIndexOutOfBounds"
  "OutOfMemory \<noteq> ArrayStore" "OutOfMemory \<noteq> NegativeArraySize" "OutOfMemory \<noteq> IllegalMonitorState"
  "OutOfMemory \<noteq> IllegalThreadState" "OutOfMemory \<noteq> InterruptedException"
  "OutOfMemory \<noteq> ArithmeticException"
  "ArrayIndexOutOfBounds \<noteq> ArrayStore" "ArrayIndexOutOfBounds \<noteq> NegativeArraySize" "ArrayIndexOutOfBounds \<noteq> IllegalMonitorState"
  "ArrayIndexOutOfBounds \<noteq> IllegalThreadState" "ArrayIndexOutOfBounds \<noteq> InterruptedException" "ArrayIndexOutOfBounds \<noteq> ArithmeticException"
  "ArrayStore \<noteq> NegativeArraySize" "ArrayStore \<noteq> IllegalMonitorState"
  "ArrayStore \<noteq> IllegalThreadState" "ArrayStore \<noteq> InterruptedException"
  "ArrayStore \<noteq> ArithmeticException"
  "NegativeArraySize \<noteq> IllegalMonitorState"
  "NegativeArraySize \<noteq> IllegalThreadState" "NegativeArraySize \<noteq> InterruptedException"
  "NegativeArraySize \<noteq> ArithmeticException"
  "IllegalMonitorState \<noteq> IllegalThreadState" "IllegalMonitorState \<noteq> InterruptedException"
  "IllegalMonitorState \<noteq> ArithmeticException"
  "IllegalThreadState \<noteq> InterruptedException"
  "IllegalThreadState \<noteq> ArithmeticException"
  "InterruptedException \<noteq> ArithmeticException"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((NullPointer \<noteq> ClassCast &&& NullPointer \<noteq> OutOfMemory) &&& NullPointer \<noteq> ArrayIndexOutOfBounds &&& NullPointer \<noteq> ArrayStore &&& NullPointer \<noteq> NegativeArraySize) &&& (NullPointer \<noteq> IllegalMonitorState &&& NullPointer \<noteq> IllegalThreadState &&& NullPointer \<noteq> InterruptedException) &&& NullPointer \<noteq> ArithmeticException &&& ClassCast \<noteq> OutOfMemory &&& ClassCast \<noteq> ArrayIndexOutOfBounds) &&& ((ClassCast \<noteq> ArrayStore &&& ClassCast \<noteq> NegativeArraySize) &&& ClassCast \<noteq> IllegalMonitorState &&& ClassCast \<noteq> IllegalThreadState &&& ClassCast \<noteq> InterruptedException) &&& (ClassCast \<noteq> ArithmeticException &&& OutOfMemory \<noteq> ArrayIndexOutOfBounds &&& OutOfMemory \<noteq> ArrayStore) &&& OutOfMemory \<noteq> NegativeArraySize &&& OutOfMemory \<noteq> IllegalMonitorState &&& OutOfMemory \<noteq> IllegalThreadState) &&& (((OutOfMemory \<noteq> InterruptedException &&& OutOfMemory \<noteq> ArithmeticException) &&& ArrayIndexOutOfBounds \<noteq> ArrayStore &&& ArrayIndexOutOfBounds \<noteq> NegativeArraySize &&& ArrayIndexOutOfBounds \<noteq> IllegalMonitorState) &&& (ArrayIndexOutOfBounds \<noteq> IllegalThreadState &&& ArrayIndexOutOfBounds \<noteq> InterruptedException &&& ArrayIndexOutOfBounds \<noteq> ArithmeticException) &&& ArrayStore \<noteq> NegativeArraySize &&& ArrayStore \<noteq> IllegalMonitorState &&& ArrayStore \<noteq> IllegalThreadState) &&& ((ArrayStore \<noteq> InterruptedException &&& ArrayStore \<noteq> ArithmeticException &&& NegativeArraySize \<noteq> IllegalMonitorState) &&& NegativeArraySize \<noteq> IllegalThreadState &&& NegativeArraySize \<noteq> InterruptedException &&& NegativeArraySize \<noteq> ArithmeticException) &&& (IllegalMonitorState \<noteq> IllegalThreadState &&& IllegalMonitorState \<noteq> InterruptedException &&& IllegalMonitorState \<noteq> ArithmeticException) &&& IllegalThreadState \<noteq> InterruptedException &&& IllegalThreadState \<noteq> ArithmeticException &&& InterruptedException \<noteq> ArithmeticException
[PROOF STEP]
by(simp_all add: NullPointer_def ClassCast_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def IllegalThreadState_def InterruptedException_def ArithmeticException_def)


[STATEMENT]
lemma Thread_neq_sys_xcpts_aux:
  "Thread \<noteq> NullPointer"
  "Thread \<noteq> ClassCast"
  "Thread \<noteq> OutOfMemory"
  "Thread \<noteq> ArrayIndexOutOfBounds"
  "Thread \<noteq> ArrayStore"
  "Thread \<noteq> NegativeArraySize"
  "Thread \<noteq> ArithmeticException"
  "Thread \<noteq> IllegalMonitorState"
  "Thread \<noteq> IllegalThreadState"
  "Thread \<noteq> InterruptedException"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((Thread \<noteq> NullPointer &&& Thread \<noteq> ClassCast) &&& Thread \<noteq> OutOfMemory &&& Thread \<noteq> ArrayIndexOutOfBounds &&& Thread \<noteq> ArrayStore) &&& (Thread \<noteq> NegativeArraySize &&& Thread \<noteq> ArithmeticException) &&& Thread \<noteq> IllegalMonitorState &&& Thread \<noteq> IllegalThreadState &&& Thread \<noteq> InterruptedException
[PROOF STEP]
by(simp_all add: Thread_def NullPointer_def ClassCast_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def IllegalThreadState_def InterruptedException_def ArithmeticException_def)


[STATEMENT]
lemma [simp]:
  assumes "wf_syscls P"
  shows wf_syscls_is_class_Object: "is_class P Object"
  and wf_syscls_is_class_Thread: "is_class P Thread"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P Object &&& is_class P Thread
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_syscls P

goal (1 subgoal):
 1. is_class P Object &&& is_class P Thread
[PROOF STEP]
by(simp_all add: is_class_def wf_syscls_class_Object wf_syscls_class_Thread)


[STATEMENT]
lemma wf_syscls_xcpt_subcls_Throwable:
  "\<lbrakk> C \<in> sys_xcpts; wf_syscls P \<rbrakk> \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* Throwable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> sys_xcpts; wf_syscls P\<rbrakk> \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* Throwable
[PROOF STEP]
by(simp add: wf_syscls_def is_class_def class_def)


[STATEMENT]
lemma wf_syscls_is_class_Throwable:
  "wf_syscls P \<Longrightarrow> is_class P Throwable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls P \<Longrightarrow> is_class P Throwable
[PROOF STEP]
by(auto simp add: wf_syscls_def is_class_def class_def map_of_SomeI)


[STATEMENT]
lemma wf_syscls_is_class_sub_Throwable:
  "\<lbrakk> wf_syscls P; P \<turnstile> C \<preceq>\<^sup>* Throwable \<rbrakk> \<Longrightarrow> is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_syscls P; P \<turnstile> C \<preceq>\<^sup>* Throwable\<rbrakk> \<Longrightarrow> is_class P C
[PROOF STEP]
by(erule subcls_is_class1)(erule wf_syscls_is_class_Throwable)


[STATEMENT]
lemma wf_syscls_is_class_xcpt:
  "\<lbrakk> C \<in> sys_xcpts; wf_syscls P \<rbrakk> \<Longrightarrow> is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<in> sys_xcpts; wf_syscls P\<rbrakk> \<Longrightarrow> is_class P C
[PROOF STEP]
by(blast intro: wf_syscls_is_class_sub_Throwable wf_syscls_xcpt_subcls_Throwable)


[STATEMENT]
lemma wf_syscls_code [code]:
  "wf_syscls P \<longleftrightarrow>
   (\<forall>C \<in> set [Object, Throwable, Thread]. is_class P C) \<and> (\<forall>C \<in> sys_xcpts. P \<turnstile> C \<preceq>\<^sup>* Throwable)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls P = ((\<forall>C\<in>set [Object, Throwable, Thread]. is_class P C) \<and> (\<forall>C\<in>sys_xcpts. P \<turnstile> C \<preceq>\<^sup>* Throwable))
[PROOF STEP]
by(simp only: wf_syscls_def) simp


[STATEMENT]
lemma sphere_bounds':
  assumes "x*x + y*y + z*z = (1::real)"
  shows "-1 \<le> x \<and> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x * x + y * y + z * z = 1
[PROOF STEP]
have "x*x \<le> 1"
[PROOF STATE]
proof (prove)
using this:
x * x + y * y + z * z = 1

goal (1 subgoal):
 1. x * x \<le> 1
[PROOF STEP]
by (smt real_minus_mult_self_le)
[PROOF STATE]
proof (state)
this:
x * x \<le> 1

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
hence "x\<^sup>2 \<le> 1\<^sup>2" "(- x)\<^sup>2 \<le> 1\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
x * x \<le> 1

goal (1 subgoal):
 1. x\<^sup>2 \<le> 1\<^sup>2 &&& (- x)\<^sup>2 \<le> 1\<^sup>2
[PROOF STEP]
by (auto simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 \<le> 1\<^sup>2
(- x)\<^sup>2 \<le> 1\<^sup>2

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
show "-1 \<le> x \<and> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
proof (cases "x \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
 2. \<not> 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> x

goal (2 subgoals):
 1. 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
 2. \<not> 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> x

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
using \<open>x\<^sup>2 \<le> 1\<^sup>2\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
x\<^sup>2 \<le> 1\<^sup>2

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
by (smt power2_le_imp_le)
[PROOF STATE]
proof (state)
this:
- 1 \<le> x \<and> x \<le> 1

goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> x

goal (1 subgoal):
 1. \<not> 0 \<le> x \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> x

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
using \<open>(-x)\<^sup>2 \<le> 1\<^sup>2\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> x
(- x)\<^sup>2 \<le> 1\<^sup>2

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1
[PROOF STEP]
by (smt power2_le_imp_le)
[PROOF STATE]
proof (state)
this:
- 1 \<le> x \<and> x \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
- 1 \<le> x \<and> x \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sphere_bounds:
  assumes "x*x + y*y + z*z = (1::real)"
  shows "-1 \<le> x \<and> x \<le> 1"  "-1 \<le> y \<and> y \<le> 1"  "-1 \<le> z \<and> z \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1 &&& - 1 \<le> y \<and> y \<le> 1 &&& - 1 \<le> z \<and> z \<le> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x * x + y * y + z * z = 1

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1 &&& - 1 \<le> y \<and> y \<le> 1 &&& - 1 \<le> z \<and> z \<le> 1
[PROOF STEP]
using sphere_bounds'[of x y z] sphere_bounds'[of y x z] sphere_bounds'[of z x y]
[PROOF STATE]
proof (prove)
using this:
x * x + y * y + z * z = 1
x * x + y * y + z * z = 1 \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
y * y + x * x + z * z = 1 \<Longrightarrow> - 1 \<le> y \<and> y \<le> 1
z * z + x * x + y * y = 1 \<Longrightarrow> - 1 \<le> z \<and> z \<le> 1

goal (1 subgoal):
 1. - 1 \<le> x \<and> x \<le> 1 &&& - 1 \<le> y \<and> y \<le> 1 &&& - 1 \<le> z \<and> z \<le> 1
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma sphere_params_on_sphere:
  fixes \<alpha> \<beta> :: real
  assumes "x = cos \<alpha> * cos \<beta>" and "y = cos \<alpha> * sin \<beta>" "z = sin \<alpha>"
  shows "x*x + y*y + z*z = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
have "x*x + y*y = (cos \<alpha> * cos \<alpha>) * (cos \<beta> * cos \<beta>) + (cos \<alpha> * cos \<alpha>) * (sin \<beta> * sin \<beta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x + y * y = cos \<alpha> * cos \<alpha> * (cos \<beta> * cos \<beta>) + cos \<alpha> * cos \<alpha> * (sin \<beta> * sin \<beta>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = cos \<alpha> * cos \<beta>
y = cos \<alpha> * sin \<beta>
z = sin \<alpha>

goal (1 subgoal):
 1. x * x + y * y = cos \<alpha> * cos \<alpha> * (cos \<beta> * cos \<beta>) + cos \<alpha> * cos \<alpha> * (sin \<beta> * sin \<beta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * x + y * y = cos \<alpha> * cos \<alpha> * (cos \<beta> * cos \<beta>) + cos \<alpha> * cos \<alpha> * (sin \<beta> * sin \<beta>)

goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
hence "x*x + y*y = cos \<alpha> * cos \<alpha>"
[PROOF STATE]
proof (prove)
using this:
x * x + y * y = cos \<alpha> * cos \<alpha> * (cos \<beta> * cos \<beta>) + cos \<alpha> * cos \<alpha> * (sin \<beta> * sin \<beta>)

goal (1 subgoal):
 1. x * x + y * y = cos \<alpha> * cos \<alpha>
[PROOF STEP]
using sin_cos_squared_add3[of \<beta>]
[PROOF STATE]
proof (prove)
using this:
x * x + y * y = cos \<alpha> * cos \<alpha> * (cos \<beta> * cos \<beta>) + cos \<alpha> * cos \<alpha> * (sin \<beta> * sin \<beta>)
cos \<beta> * cos \<beta> + sin \<beta> * sin \<beta> = 1

goal (1 subgoal):
 1. x * x + y * y = cos \<alpha> * cos \<alpha>
[PROOF STEP]
by (subst (asm) distrib_left[symmetric]) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x * x + y * y = cos \<alpha> * cos \<alpha>

goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x * x + y * y = cos \<alpha> * cos \<alpha>

goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x * x + y * y = cos \<alpha> * cos \<alpha>
x = cos \<alpha> * cos \<beta>
y = cos \<alpha> * sin \<beta>
z = sin \<alpha>

goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
using sin_cos_squared_add3[of \<alpha>]
[PROOF STATE]
proof (prove)
using this:
x * x + y * y = cos \<alpha> * cos \<alpha>
x = cos \<alpha> * cos \<beta>
y = cos \<alpha> * sin \<beta>
z = sin \<alpha>
cos \<alpha> * cos \<alpha> + sin \<alpha> * sin \<alpha> = 1

goal (1 subgoal):
 1. x * x + y * y + z * z = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * x + y * y + z * z = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sphere_params:
  fixes x y z :: real
  assumes "x*x + y*y + z*z = 1"
  shows "x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
proof (cases "z=1 \<or> z = -1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 1 \<or> z = - 1 \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
 2. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = 1 \<or> z = - 1

goal (2 subgoals):
 1. z = 1 \<or> z = - 1 \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
 2. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
hence "x = 0 \<and> y = 0"
[PROOF STATE]
proof (prove)
using this:
z = 1 \<or> z = - 1

goal (1 subgoal):
 1. x = 0 \<and> y = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z = 1 \<or> z = - 1
x * x + y * y + z * z = 1

goal (1 subgoal):
 1. x = 0 \<and> y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = 0 \<and> y = 0

goal (2 subgoals):
 1. z = 1 \<or> z = - 1 \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
 2. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0 \<and> y = 0

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
using \<open>z = 1 \<or> z = -1\<close>
[PROOF STATE]
proof (prove)
using this:
x = 0 \<and> y = 0
z = 1 \<or> z = - 1

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
by (auto simp add: cos_arcsin)
[PROOF STATE]
proof (state)
this:
x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)

goal (1 subgoal):
 1. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (z = 1 \<or> z = - 1)

goal (1 subgoal):
 1. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
hence "x \<noteq> 0 \<or> y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (z = 1 \<or> z = - 1)

goal (1 subgoal):
 1. x \<noteq> 0 \<or> y \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> (z = 1 \<or> z = - 1)
x * x + y * y + z * z = 1

goal (1 subgoal):
 1. x \<noteq> 0 \<or> y \<noteq> 0
[PROOF STEP]
by (auto simp add: square_eq_1_iff)
[PROOF STATE]
proof (state)
this:
x \<noteq> 0 \<or> y \<noteq> 0

goal (1 subgoal):
 1. \<not> (z = 1 \<or> z = - 1) \<Longrightarrow> x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0 \<or> y \<noteq> 0

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
using real_sqrt_unique[of y "1 - z*z"]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0 \<or> y \<noteq> 0
\<lbrakk>y\<^sup>2 = 1 - z * z; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (1 - z * z) = y

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
using real_sqrt_unique[of "-y" "1 - z*z"]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0 \<or> y \<noteq> 0
\<lbrakk>y\<^sup>2 = 1 - z * z; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (1 - z * z) = y
\<lbrakk>(- y)\<^sup>2 = 1 - z * z; 0 \<le> - y\<rbrakk> \<Longrightarrow> sqrt (1 - z * z) = - y

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
using sphere_bounds[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0 \<or> y \<noteq> 0
\<lbrakk>y\<^sup>2 = 1 - z * z; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (1 - z * z) = y
\<lbrakk>(- y)\<^sup>2 = 1 - z * z; 0 \<le> - y\<rbrakk> \<Longrightarrow> sqrt (1 - z * z) = - y
- 1 \<le> x \<and> x \<le> 1
- 1 \<le> y \<and> y \<le> 1
- 1 \<le> z \<and> z \<le> 1
x * x + y * y + z * z = 1

goal (1 subgoal):
 1. x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)
[PROOF STEP]
by (auto simp add: cos_arcsin cos_arctan sin_arctan power2_eq_square field_simps real_sqrt_divide atan2_def)
[PROOF STATE]
proof (state)
this:
x = cos (arcsin z) * cos (atan2 y x) \<and> y = cos (arcsin z) * sin (atan2 y x) \<and> z = sin (arcsin z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_sphere_params:
  assumes "x*x + y*y + z*z = 1"
  shows "\<exists> \<alpha> \<beta>. x = cos \<alpha> * cos \<beta> \<and> y = cos \<alpha> * sin \<beta> \<and> z = sin \<alpha> \<and> -pi / 2 \<le> \<alpha> \<and> \<alpha> \<le> pi / 2 \<and> -pi \<le> \<beta> \<and> \<beta> < pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. x = cos \<alpha> * cos \<beta> \<and> y = cos \<alpha> * sin \<beta> \<and> z = sin \<alpha> \<and> - pi / 2 \<le> \<alpha> \<and> \<alpha> \<le> pi / 2 \<and> - pi \<le> \<beta> \<and> \<beta> < pi
[PROOF STEP]
using assms arcsin_bounded[of z] sphere_bounds[of x y z]
[PROOF STATE]
proof (prove)
using this:
x * x + y * y + z * z = 1
\<lbrakk>- 1 \<le> z; z \<le> 1\<rbrakk> \<Longrightarrow> - (pi / 2) \<le> arcsin z \<and> arcsin z \<le> pi / 2
x * x + y * y + z * z = 1 \<Longrightarrow> - 1 \<le> x \<and> x \<le> 1
x * x + y * y + z * z = 1 \<Longrightarrow> - 1 \<le> y \<and> y \<le> 1
x * x + y * y + z * z = 1 \<Longrightarrow> - 1 \<le> z \<and> z \<le> 1

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. x = cos \<alpha> * cos \<beta> \<and> y = cos \<alpha> * sin \<beta> \<and> z = sin \<alpha> \<and> - pi / 2 \<le> \<alpha> \<and> \<alpha> \<le> pi / 2 \<and> - pi \<le> \<beta> \<and> \<beta> < pi
[PROOF STEP]
by (rule_tac x="arcsin z" in exI, rule_tac x="atan2 y x" in exI) (simp add: sphere_params arcsin_bounded atan2_bounded)


[STATEMENT]
lemma Re_stereographic:
  shows "Re (2 * z / (1 + z * cnj z)) = 2 * Re z / (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (2 * z / (1 + z * cnj z)) = 2 * Re z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using one_plus_square_neq_zero
[PROOF STATE]
proof (prove)
using this:
1 + (cor ?x)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. Re (2 * z / (1 + z * cnj z)) = 2 * Re z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (subst complex_mult_cnj_cmod, subst Re_divide_real) (auto simp add: power2_eq_square)


[STATEMENT]
lemma Im_stereographic:
  shows "Im (2 * z / (1 + z * cnj z)) = 2 * Im z / (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (2 * z / (1 + z * cnj z)) = 2 * Im z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using one_plus_square_neq_zero
[PROOF STATE]
proof (prove)
using this:
1 + (cor ?x)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. Im (2 * z / (1 + z * cnj z)) = 2 * Im z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (subst complex_mult_cnj_cmod, subst Im_divide_real) (auto simp add: power2_eq_square)


[STATEMENT]
lemma inv_stereographic_on_sphere:
  assumes "X = Re (2*z / (1 + z*cnj z))" and "Y = Im (2*z / (1 + z*cnj z))" and "Z = ((cmod z)\<^sup>2 - 1) / (1 + (cmod z)\<^sup>2)"
  shows "X*X + Y*Y + Z*Z = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X * X + Y * Y + Z * Z = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X * X + Y * Y + Z * Z = 1
[PROOF STEP]
have "1 + (cmod z)\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (cmod z)\<^sup>2 \<noteq> 0
[PROOF STEP]
by (smt power2_less_0)
[PROOF STATE]
proof (state)
this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. X * X + Y * Y + Z * Z = 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. X * X + Y * Y + Z * Z = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0
X = Re (2 * z / (1 + z * cnj z))
Y = Im (2 * z / (1 + z * cnj z))
Z = ((cmod z)\<^sup>2 - 1) / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. X * X + Y * Y + Z * Z = 1
[PROOF STEP]
by (simp add: Re_stereographic Im_stereographic)
       (cases z, simp add: power2_eq_square real_sqrt_mult[symmetric] add_divide_distrib[symmetric], simp add: complex_norm power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
X * X + Y * Y + Z * Z = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stereographic_North:
  shows "stereographic x = \<infinity>\<^sub>h \<longleftrightarrow> x = North"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stereographic x = \<infinity>\<^sub>h) = (x = North)
[PROOF STEP]
by (transfer, transfer, auto split: if_split_asm)


[STATEMENT]
lemma stereographic_inv_stereographic':
  assumes
  z: "z = z1/z2" and "z2 \<noteq> 0" and
  X: "X = Re (2*z / (1 + z*cnj z))" and Y: "Y = Im (2*z / (1 + z*cnj z))" and Z: "Z = ((cmod z)\<^sup>2 - 1) / (1 + (cmod z)\<^sup>2)"
  shows "\<exists> k. k \<noteq> 0 \<and> (X + \<i>*Y, complex_of_real (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
have "1 + (cmod z)\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (cmod z)\<^sup>2 \<noteq> 0
[PROOF STEP]
by (metis one_power2 sum_power2_eq_zero_iff zero_neq_one)
[PROOF STATE]
proof (state)
this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
hence "(1 - Z) = 2 / (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. 1 - Z = 2 / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using Z
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0
Z = ((cmod z)\<^sup>2 - 1) / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. 1 - Z = 2 / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 - Z = 2 / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
hence "cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
1 - Z = 2 / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
have "X = 2 * Re(z) / (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = 2 * Re z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X = Re (2 * z / (1 + z * cnj z))

goal (1 subgoal):
 1. X = 2 * Re z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (simp add: Re_stereographic)
[PROOF STATE]
proof (state)
this:
X = 2 * Re z / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
have "Y = 2 * Im(z) / (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y = 2 * Im z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using Y
[PROOF STATE]
proof (prove)
using this:
Y = Im (2 * z / (1 + z * cnj z))

goal (1 subgoal):
 1. Y = 2 * Im z / (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (simp add: Im_stereographic)
[PROOF STATE]
proof (state)
this:
Y = 2 * Im z / (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
have "X + \<i>*Y = 2 * z / cor (1 + (cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
[PROOF STEP]
using \<open>1 + (cmod z)\<^sup>2 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
[PROOF STEP]
unfolding Complex_eq[of X Y, symmetric]
[PROOF STATE]
proof (prove)
using this:
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. Complex X Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
[PROOF STEP]
by (subst \<open>X = 2*Re(z) / (1 + (cmod z)\<^sup>2)\<close>, subst \<open>Y = 2*Im(z) / (1 + (cmod z)\<^sup>2)\<close>, simp add: Complex_scale4 Complex_scale1)
[PROOF STATE]
proof (state)
this:
cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
have "1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0
[PROOF STEP]
by (rule one_plus_square_neq_zero)
[PROOF STATE]
proof (state)
this:
1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)
cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)
cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
using \<open>z2 \<noteq> 0\<close> \<open>1 + (cmod z)\<^sup>2 \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
cor (1 - Z) = 2 / cor (1 + (cmod z)\<^sup>2)
cor X + \<i> * cor Y = 2 * z / cor (1 + (cmod z)\<^sup>2)
1 + (cor (cmod (z1 / z2)))\<^sup>2 \<noteq> 0
z2 \<noteq> 0
1 + (cmod z)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)
[PROOF STEP]
by (simp, subst z)+
       (rule_tac x="(2 / (1 + (cor (cmod (z1 / z2)))\<^sup>2)) / z2" in exI, auto)
[PROOF STATE]
proof (state)
this:
\<exists>k. k \<noteq> 0 \<and> (cor X + \<i> * cor Y, cor (1 - Z)) = k *\<^sub>s\<^sub>v (z1, z2)

goal:
No subgoals!
[PROOF STEP]
qed