[STATEMENT]
theorem ate_validity:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and initv: "\<forall>q. x (rho 0 q) = v"
  and dp: "decide (rho r p) = Some w"
  shows "w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
have "\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v
[PROOF STEP]
proof (induct r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>qq. sendMsg Ate_M 0 qq p (rho 0 qq) = v
 2. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
from run initv
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>q. x (rho 0 q) = v
[PROOF STEP]
show "\<forall>qq. sendMsg Ate_M 0 qq p (rho 0 qq) = v"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>q. x (rho 0 q) = v

goal (1 subgoal):
 1. \<forall>qq. sendMsg Ate_M 0 qq p (rho 0 qq) = v
[PROOF STEP]
by (auto simp: SHORun_eq SHOnextConfig_eq Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M 0 qq p (rho 0 qq) = v

goal (1 subgoal):
 1. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
assume ih:"\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v"
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v

goal (1 subgoal):
 1. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
have "\<forall>qq. x (rho (Suc r) qq) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qq. x (rho (Suc r) qq) = v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qq. x (rho (Suc r) qq) = v
[PROOF STEP]
fix qq
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qq. x (rho (Suc r) qq) = v
[PROOF STEP]
from run
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
[PROOF STEP]
obtain \<mu>qq
          where nxt: "nextState Ate_M r qq (rho r qq) \<mu>qq (rho (Suc r) qq)"
            and mu: "\<mu>qq \<in> SHOmsgVectors Ate_M r qq (rho r) (HOs r qq) (SHOs r qq)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

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

goal (1 subgoal):
 1. \<And>qq. x (rho (Suc r) qq) = v
[PROOF STEP]
from nxt
[PROOF STATE]
proof (chain)
picking this:
nextState Ate_M r qq (rho r qq) \<mu>qq (rho (Suc r) qq)
[PROOF STEP]
have "(card {pp. \<mu>qq pp \<noteq> None} > T \<and> x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq))
            \<or> (card {pp. \<mu>qq pp \<noteq> None} \<le> T \<and> x (rho (Suc r) qq) = x (rho r qq))"
[PROOF STATE]
proof (prove)
using this:
nextState Ate_M r qq (rho r qq) \<mu>qq (rho (Suc r) qq)

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

goal (1 subgoal):
 1. \<And>qq. x (rho (Suc r) qq) = v
[PROOF STEP]
thus "x (rho (Suc r) qq) = v"
[PROOF STATE]
proof (prove)
using this:
T < card {pp. \<mu>qq pp \<noteq> None} \<and> x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq) \<or> card {pp. \<mu>qq pp \<noteq> None} \<le> T \<and> x (rho (Suc r) qq) = x (rho r qq)

goal (1 subgoal):
 1. x (rho (Suc r) qq) = v
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
 2. \<lbrakk>card {pp. \<mu>qq pp \<noteq> None} \<le> T; x (rho (Suc r) qq) = x (rho r qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
assume "x (rho (Suc r) qq) = x (rho r qq)"
[PROOF STATE]
proof (state)
this:
x (rho (Suc r) qq) = x (rho r qq)

goal (2 subgoals):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
 2. \<lbrakk>card {pp. \<mu>qq pp \<noteq> None} \<le> T; x (rho (Suc r) qq) = x (rho r qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
with ih
[PROOF STATE]
proof (chain)
picking this:
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v
x (rho (Suc r) qq) = x (rho r qq)
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v
x (rho (Suc r) qq) = x (rho r qq)

goal (1 subgoal):
 1. x (rho (Suc r) qq) = v
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
x (rho (Suc r) qq) = v

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
assume threshold_T:"T < card {pp. \<mu>qq pp \<noteq> None}"
             and xsmall:"x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)"
[PROOF STATE]
proof (state)
this:
T < card {pp. \<mu>qq pp \<noteq> None}
x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
have "card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
from comm
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have 1:"card (HOs r qq - SHOs r qq) \<le> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. card (HOs r qq - SHOs r qq) \<le> \<alpha>
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
[PROOF STATE]
proof (state)
this:
card (HOs r qq - SHOs r qq) \<le> \<alpha>

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (HOs r qq - SHOs r qq) \<le> \<alpha>

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
from mu ih
[PROOF STATE]
proof (chain)
picking this:
\<mu>qq \<in> SHOmsgVectors Ate_M r qq (rho r) (HOs r qq) (SHOs r qq)
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v
[PROOF STEP]
have "SHOs r qq \<inter> HOs r qq \<subseteq> {pp. \<mu>qq pp = Some v}"
              and "HOs r qq = {pp. \<mu>qq pp \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
\<mu>qq \<in> SHOmsgVectors Ate_M r qq (rho r) (HOs r qq) (SHOs r qq)
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v

goal (1 subgoal):
 1. SHOs r qq \<inter> HOs r qq \<subseteq> {pp. \<mu>qq pp = Some v} &&& HOs r qq = {pp. \<mu>qq pp \<noteq> None}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
SHOs r qq \<inter> HOs r qq \<subseteq> {pp. \<mu>qq pp = Some v}
HOs r qq = {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
hence "{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}
                   \<subseteq> HOs r qq - SHOs r qq"
[PROOF STATE]
proof (prove)
using this:
SHOs r qq \<inter> HOs r qq \<subseteq> {pp. \<mu>qq pp = Some v}
HOs r qq = {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. {pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} \<subseteq> HOs r qq - SHOs r qq
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} \<subseteq> HOs r qq - SHOs r qq

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
hence "card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v})
                      \<le> card (HOs r qq - SHOs r qq)"
[PROOF STATE]
proof (prove)
using this:
{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} \<subseteq> HOs r qq - SHOs r qq

goal (1 subgoal):
 1. card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> card (HOs r qq - SHOs r qq)
[PROOF STEP]
by (auto simp:card_mono)
[PROOF STATE]
proof (state)
this:
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> card (HOs r qq - SHOs r qq)

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (HOs r qq - SHOs r qq) \<le> \<alpha>
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> card (HOs r qq - SHOs r qq)
[PROOF STEP]
have "card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2"
[PROOF STATE]
proof (prove)
using this:
card (HOs r qq - SHOs r qq) \<le> \<alpha>
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> card (HOs r qq - SHOs r qq)

goal (1 subgoal):
 1. card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2
[PROOF STEP]
using Tge2a
[PROOF STATE]
proof (prove)
using this:
card (HOs r qq - SHOs r qq) \<le> \<alpha>
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> card (HOs r qq - SHOs r qq)
2 * \<alpha> \<le> T

goal (1 subgoal):
 1. card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
have "{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}
                  = {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} = {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} = {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2
{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} = {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v}) \<le> T div 2
{pp. \<mu>qq pp \<noteq> None} - {pp. \<mu>qq pp = Some v} = {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
have "{pp. \<mu>qq pp \<noteq> None}
                = {pp. \<mu>qq pp = Some v} \<union> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
            and "{pp. \<mu>qq pp = Some v} \<inter> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {pp. \<mu>qq pp \<noteq> None} = {pp. \<mu>qq pp = Some v} \<union> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} &&& {pp. \<mu>qq pp = Some v} \<inter> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>qq pp \<noteq> None} = {pp. \<mu>qq pp = Some v} \<union> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
{pp. \<mu>qq pp = Some v} \<inter> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} = {}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
hence "card {pp. \<mu>qq pp \<noteq> None}
                 = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
[PROOF STATE]
proof (prove)
using this:
{pp. \<mu>qq pp \<noteq> None} = {pp. \<mu>qq pp = Some v} \<union> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
{pp. \<mu>qq pp = Some v} \<inter> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} = {}

goal (1 subgoal):
 1. card {pp. \<mu>qq pp \<noteq> None} = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
by (auto simp: card_Un_Int)
[PROOF STATE]
proof (state)
this:
card {pp. \<mu>qq pp \<noteq> None} = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {pp. \<mu>qq pp \<noteq> None} = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
note threshold_T
[PROOF STATE]
proof (state)
this:
T < card {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
card {pp. \<mu>qq pp \<noteq> None} = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
T < card {pp. \<mu>qq pp \<noteq> None}
[PROOF STEP]
have "card {pp. \<mu>qq pp = Some v} > card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
[PROOF STATE]
proof (prove)
using this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} \<le> T div 2
card {pp. \<mu>qq pp \<noteq> None} = card {pp. \<mu>qq pp = Some v} + card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
T < card {pp. \<mu>qq pp \<noteq> None}

goal (1 subgoal):
 1. card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
assume "w \<noteq> v"
[PROOF STATE]
proof (state)
this:
w \<noteq> v

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
hence "{pp. \<mu>qq pp = Some w} \<subseteq> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> v

goal (1 subgoal):
 1. {pp. \<mu>qq pp = Some w} \<subseteq> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>qq pp = Some w} \<subseteq> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
hence "card {pp. \<mu>qq pp = Some w} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}"
[PROOF STATE]
proof (prove)
using this:
{pp. \<mu>qq pp = Some w} \<subseteq> {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. card {pp. \<mu>qq pp = Some w} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card {pp. \<mu>qq pp = Some w} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?wa7 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?wa7} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}
?wa7 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?wa7} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}
[PROOF STEP]
have zz:"\<And>w. w \<noteq> v \<Longrightarrow>
                       card {pp. \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}"
[PROOF STATE]
proof (prove)
using this:
card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}
?wa7 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?wa7} \<le> card {pp. \<exists>w. w \<noteq> v \<and> \<mu>qq pp = Some w}

goal (1 subgoal):
 1. \<And>w. w \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some w} < card {pp. \<mu>qq pp = Some v}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?w5 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?w5} < card {pp. \<mu>qq pp = Some v}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
hence "\<And>w. card {pp. \<mu>qq pp = Some v} \<le> card {pp. \<mu>qq pp = Some w}
                      \<Longrightarrow> w = v"
[PROOF STATE]
proof (prove)
using this:
?w5 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?w5} < card {pp. \<mu>qq pp = Some v}

goal (1 subgoal):
 1. \<And>w. card {pp. \<mu>qq pp = Some v} \<le> card {pp. \<mu>qq pp = Some w} \<Longrightarrow> w = v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card {pp. \<mu>qq pp = Some v} \<le> card {pp. \<mu>qq pp = Some ?w5} \<Longrightarrow> ?w5 = v

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
with zz
[PROOF STATE]
proof (chain)
picking this:
?w5 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?w5} < card {pp. \<mu>qq pp = Some v}
card {pp. \<mu>qq pp = Some v} \<le> card {pp. \<mu>qq pp = Some ?w5} \<Longrightarrow> ?w5 = v
[PROOF STEP]
have "mostOftenRcvd \<mu>qq = {v}"
[PROOF STATE]
proof (prove)
using this:
?w5 \<noteq> v \<Longrightarrow> card {pp. \<mu>qq pp = Some ?w5} < card {pp. \<mu>qq pp = Some v}
card {pp. \<mu>qq pp = Some v} \<le> card {pp. \<mu>qq pp = Some ?w5} \<Longrightarrow> ?w5 = v

goal (1 subgoal):
 1. mostOftenRcvd \<mu>qq = {v}
[PROOF STEP]
by (force simp: mostOftenRcvd_def)
[PROOF STATE]
proof (state)
this:
mostOftenRcvd \<mu>qq = {v}

goal (1 subgoal):
 1. \<lbrakk>T < card {pp. \<mu>qq pp \<noteq> None}; x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)\<rbrakk> \<Longrightarrow> x (rho (Suc r) qq) = v
[PROOF STEP]
with xsmall
[PROOF STATE]
proof (chain)
picking this:
x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)
mostOftenRcvd \<mu>qq = {v}
[PROOF STEP]
show "x (rho (Suc r) qq) = v"
[PROOF STATE]
proof (prove)
using this:
x (rho (Suc r) qq) = Min (mostOftenRcvd \<mu>qq)
mostOftenRcvd \<mu>qq = {v}

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

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

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

goal (1 subgoal):
 1. \<And>r. \<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v \<Longrightarrow> \<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v
[PROOF STEP]
thus "\<forall>qq. sendMsg Ate_M (Suc r) qq p (rho (Suc r) qq) = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>qq. x (rho (Suc r) qq) = v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M ?ra7 qq p (rho ?ra7 qq) = v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
note P = this
[PROOF STATE]
proof (state)
this:
\<forall>qq. sendMsg Ate_M ?ra7 qq p (rho ?ra7 qq) = v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from run dp
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
decide (rho r p) = Some w
[PROOF STEP]
obtain rp
    where rp: "rp < r" "decide (rho rp p) \<noteq> Some w"
              "decide (rho (Suc rp) p) = Some w"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
decide (rho r p) = Some w

goal (1 subgoal):
 1. (\<And>rp. \<lbrakk>rp < r; decide (rho rp p) \<noteq> Some w; decide (rho (Suc rp) p) = Some w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule decisionNonNullThenDecided)
[PROOF STATE]
proof (state)
this:
rp < r
decide (rho rp p) \<noteq> Some w
decide (rho (Suc rp) p) = Some w

goal (1 subgoal):
 1. w = 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 rp p (rho rp p) \<mu>p (rho (Suc rp) p)"
      and mu: "\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs

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

goal (1 subgoal):
 1. w = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
nextState Ate_M rp p (rho rp p) \<mu>p (rho (Suc rp) p)
\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)

goal (1 subgoal):
 1. w = v
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
assume w: "w \<noteq> v"
[PROOF STATE]
proof (state)
this:
w \<noteq> v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from comm
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
[PROOF STEP]
have "card (HOs rp p - SHOs rp p) \<le> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)

goal (1 subgoal):
 1. card (HOs rp p - SHOs rp p) \<le> \<alpha>
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_commPerRd_def)
[PROOF STATE]
proof (state)
this:
card (HOs rp p - SHOs rp p) \<le> \<alpha>

goal (1 subgoal):
 1. w = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (HOs rp p - SHOs rp p) \<le> \<alpha>

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from mu P
[PROOF STATE]
proof (chain)
picking this:
\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)
\<forall>qq. sendMsg Ate_M ?ra7 qq p (rho ?ra7 qq) = v
[PROOF STEP]
have "SHOs rp p \<inter> HOs rp p \<subseteq> {pp. \<mu>p pp = Some v}"
      and "HOs rp p = {pp. \<mu>p pp \<noteq> None}"
[PROOF STATE]
proof (prove)
using this:
\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)
\<forall>qq. sendMsg Ate_M ?ra7 qq p (rho ?ra7 qq) = v

goal (1 subgoal):
 1. SHOs rp p \<inter> HOs rp p \<subseteq> {pp. \<mu>p pp = Some v} &&& HOs rp p = {pp. \<mu>p pp \<noteq> None}
[PROOF STEP]
by (auto simp: SHOmsgVectors_def)
[PROOF STATE]
proof (state)
this:
SHOs rp p \<inter> HOs rp p \<subseteq> {pp. \<mu>p pp = Some v}
HOs rp p = {pp. \<mu>p pp \<noteq> None}

goal (1 subgoal):
 1. w = v
[PROOF STEP]
hence "{pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}
           \<subseteq> HOs rp p - SHOs rp p"
[PROOF STATE]
proof (prove)
using this:
SHOs rp p \<inter> HOs rp p \<subseteq> {pp. \<mu>p pp = Some v}
HOs rp p = {pp. \<mu>p pp \<noteq> None}

goal (1 subgoal):
 1. {pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v} \<subseteq> HOs rp p - SHOs rp p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v} \<subseteq> HOs rp p - SHOs rp p

goal (1 subgoal):
 1. w = v
[PROOF STEP]
hence "card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})
            \<le> card (HOs rp p - SHOs rp p)"
[PROOF STATE]
proof (prove)
using this:
{pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v} \<subseteq> HOs rp p - SHOs rp p

goal (1 subgoal):
 1. card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) \<le> card (HOs rp p - SHOs rp p)
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) \<le> card (HOs rp p - SHOs rp p)

goal (1 subgoal):
 1. w = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (HOs rp p - SHOs rp p) \<le> \<alpha>
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) \<le> card (HOs rp p - SHOs rp p)
[PROOF STEP]
have "card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) < E"
[PROOF STATE]
proof (prove)
using this:
card (HOs rp p - SHOs rp p) \<le> \<alpha>
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) \<le> card (HOs rp p - SHOs rp p)

goal (1 subgoal):
 1. card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) < E
[PROOF STEP]
using Egta
[PROOF STATE]
proof (prove)
using this:
card (HOs rp p - SHOs rp p) \<le> \<alpha>
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) \<le> card (HOs rp p - SHOs rp p)
\<alpha> < E

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

goal (1 subgoal):
 1. w = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) < E

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from w
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> v
[PROOF STEP]
have "{pp. \<mu>p pp = Some w}
                 \<subseteq> {pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> v

goal (1 subgoal):
 1. {pp. \<mu>p pp = Some w} \<subseteq> {pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{pp. \<mu>p pp = Some w} \<subseteq> {pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}

goal (1 subgoal):
 1. w = v
[PROOF STEP]
hence "card {pp. \<mu>p pp = Some w}
             \<le> card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})"
[PROOF STATE]
proof (prove)
using this:
{pp. \<mu>p pp = Some w} \<subseteq> {pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}

goal (1 subgoal):
 1. card {pp. \<mu>p pp = Some w} \<le> card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card {pp. \<mu>p pp = Some w} \<le> card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})

goal (1 subgoal):
 1. w = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) < E
card {pp. \<mu>p pp = Some w} \<le> card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})
[PROOF STEP]
have "card {pp. \<mu>p pp = Some w} < E"
[PROOF STATE]
proof (prove)
using this:
card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v}) < E
card {pp. \<mu>p pp = Some w} \<le> card ({pp. \<mu>p pp \<noteq> None} - {pp. \<mu>p pp = Some v})

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

goal (1 subgoal):
 1. w = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?wa7 \<noteq> v \<Longrightarrow> card {pp. \<mu>p pp = Some ?wa7} < E

goal (1 subgoal):
 1. w = v
[PROOF STEP]
hence PP: "\<And>w. card {pp. \<mu>p pp = Some w} \<ge> E \<Longrightarrow> w = v"
[PROOF STATE]
proof (prove)
using this:
?wa7 \<noteq> v \<Longrightarrow> card {pp. \<mu>p pp = Some ?wa7} < E

goal (1 subgoal):
 1. \<And>w. E \<le> card {pp. \<mu>p pp = Some w} \<Longrightarrow> w = v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
E \<le> card {pp. \<mu>p pp = Some ?w5} \<Longrightarrow> ?w5 = v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from rp nxt mu
[PROOF STATE]
proof (chain)
picking this:
rp < r
decide (rho rp p) \<noteq> Some w
decide (rho (Suc rp) p) = Some w
nextState Ate_M rp p (rho rp p) \<mu>p (rho (Suc rp) p)
\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)
[PROOF STEP]
have "card {q. \<mu>p q = Some w} > E"
[PROOF STATE]
proof (prove)
using this:
rp < r
decide (rho rp p) \<noteq> Some w
decide (rho (Suc rp) p) = Some w
nextState Ate_M rp p (rho rp p) \<mu>p (rho (Suc rp) p)
\<mu>p \<in> SHOmsgVectors Ate_M rp p (rho rp) (HOs rp p) (SHOs rp p)

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

goal (1 subgoal):
 1. w = v
[PROOF STEP]
with PP
[PROOF STATE]
proof (chain)
picking this:
E \<le> card {pp. \<mu>p pp = Some ?w5} \<Longrightarrow> ?w5 = v
E < card {q. \<mu>p q = Some w}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E \<le> card {pp. \<mu>p pp = Some ?w5} \<Longrightarrow> ?w5 = v
E < card {q. \<mu>p q = Some w}

goal (1 subgoal):
 1. w = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_decision:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nvp: "decide (rho r p) \<noteq> Some v"
  and vp: "decide (rho (Suc r) p) = Some v"
  and nwq: "decide (rho r q) \<noteq> Some w"
  and wq: "decide (rho (Suc r) q) = Some w"
  shows "w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
have gtn: "card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
             + card {qq. sendMsg Ate_M r qq q (rho r qq) = w} > N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
from run comm nvp vp
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
[PROOF STEP]
have "card {qq. sendMsg Ate_M r qq p (rho r qq) = v} > E - \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v

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

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
from run comm nwq wq
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r q) \<noteq> Some w
decide (rho (Suc r) q) = Some w
[PROOF STEP]
have "card {qq. sendMsg Ate_M r qq q (rho r qq) = w} > E - \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r q) \<noteq> Some w
decide (rho (Suc r) q) = Some w

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
by (rule decide_sent_msgs_threshold)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = w}

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = w}

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
using majE
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
E - \<alpha> < card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
N \<le> 2 * (E - \<alpha>)

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}

goal (1 subgoal):
 1. w = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
assume vw:"w \<noteq> v"
[PROOF STATE]
proof (state)
this:
w \<noteq> v

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[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. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with vw
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> v
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = sendMsg Ate_M r qq q (rho r qq)
[PROOF STEP]
have "{qq. sendMsg Ate_M r qq p (rho r qq) = v}
          \<inter> {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> v
\<forall>qq. sendMsg Ate_M r qq p (rho r qq) = sendMsg Ate_M r qq q (rho r qq)

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with gtn
[PROOF STATE]
proof (chain)
picking this:
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}
[PROOF STEP]
have "card ({qq. sendMsg Ate_M r qq p (rho r qq) = v}
                 \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) > N"
[PROOF STATE]
proof (prove)
using this:
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M r qq q (rho r qq) = w}
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M r qq q (rho r qq) = w} = {}

goal (1 subgoal):
 1. N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w})
[PROOF STEP]
by (auto simp: card_Un_Int)
[PROOF STATE]
proof (state)
this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w})

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w})

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
have "card ({qq. sendMsg Ate_M r qq p (rho r qq) = v}
                 \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) \<le> N
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) \<le> N

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w})
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) \<le> N
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w})
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M r qq q (rho r qq) = w}) \<le> N

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma laterProcessDecidesSameValue :
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and nd1: "decide (rho r p) \<noteq> Some v"
  and d1: "decide (rho (Suc r) p) = Some v"
  and nd2: "decide (rho (r+k) q) \<noteq> Some w"
  and d2: "decide (rho (Suc (r+k)) q) = Some w"
  shows "w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
assume vdifw:"w \<noteq> v"
[PROOF STATE]
proof (state)
this:
w \<noteq> v

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
have kgt0: "k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < k \<Longrightarrow> False
[PROOF STEP]
assume "\<not> k > 0"
[PROOF STATE]
proof (state)
this:
\<not> 0 < k

goal (1 subgoal):
 1. \<not> 0 < k \<Longrightarrow> False
[PROOF STEP]
hence "k = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < k

goal (1 subgoal):
 1. k = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = 0

goal (1 subgoal):
 1. \<not> 0 < k \<Longrightarrow> False
[PROOF STEP]
with run comm nd1 d1 nd2 d2
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
decide (rho (r + k) q) \<noteq> Some w
decide (rho (Suc (r + k)) q) = Some w
k = 0
[PROOF STEP]
have "w = v"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
decide (rho (r + k) q) \<noteq> Some w
decide (rho (Suc (r + k)) q) = Some w
k = 0

goal (1 subgoal):
 1. w = v
[PROOF STEP]
by (auto dest: common_decision)
[PROOF STATE]
proof (state)
this:
w = v

goal (1 subgoal):
 1. \<not> 0 < k \<Longrightarrow> False
[PROOF STEP]
with vdifw
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> v
w = v
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
w \<noteq> v
w = v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < k

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
have 1: "{qq. sendMsg Ate_M r qq p (rho r qq) = v}
           \<inter> {qq. sendMsg Ate_M (r+k) qq q (rho (r+k) qq) = w} = {}"
    (is "?sentv \<inter> ?sentw = {}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {}

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {}
[PROOF STEP]
obtain qq
      where xrv: "x (rho r qq) = v" and rkw: "x (rho (r+k) qq) = w"
[PROOF STATE]
proof (prove)
using this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {}

goal (1 subgoal):
 1. (\<And>qq. \<lbrakk>x (rho r qq) = v; x (rho (r + k) qq) = w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Ate_SHOMachine_def Ate_sendMsg_def)
[PROOF STATE]
proof (state)
this:
x (rho r qq) = v
x (rho (r + k) qq) = w

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "\<exists>k' < k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
assume f: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
fix k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
assume kk':"k' < k"
[PROOF STATE]
proof (state)
this:
k' < k

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

goal (1 subgoal):
 1. x (rho (r + k') qq) \<noteq> w
[PROOF STEP]
proof (induct k')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < k \<Longrightarrow> x (rho (r + 0) qq) \<noteq> w
 2. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
from xrv vdifw
[PROOF STATE]
proof (chain)
picking this:
x (rho r qq) = v
w \<noteq> v
[PROOF STEP]
show "x (rho (r + 0) qq) \<noteq> w"
[PROOF STATE]
proof (prove)
using this:
x (rho r qq) = v
w \<noteq> v

goal (1 subgoal):
 1. x (rho (r + 0) qq) \<noteq> w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x (rho (r + 0) qq) \<noteq> w

goal (1 subgoal):
 1. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
fix k'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
assume ih:"k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w"
             and ksk':"Suc k' < k"
[PROOF STATE]
proof (state)
this:
k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w
Suc k' < k

goal (1 subgoal):
 1. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
from ksk'
[PROOF STATE]
proof (chain)
picking this:
Suc k' < k
[PROOF STEP]
have "k' < k"
[PROOF STATE]
proof (prove)
using this:
Suc k' < k

goal (1 subgoal):
 1. k' < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' < k

goal (1 subgoal):
 1. \<And>k'. \<lbrakk>k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w; Suc k' < k\<rbrakk> \<Longrightarrow> x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
with ih f
[PROOF STATE]
proof (chain)
picking this:
k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)
k' < k
[PROOF STEP]
show "x (rho (r + Suc k') qq) \<noteq> w"
[PROOF STATE]
proof (prove)
using this:
k' < k \<Longrightarrow> x (rho (r + k') qq) \<noteq> w
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)
k' < k

goal (1 subgoal):
 1. x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc k') qq) \<noteq> w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x (rho (r + k') qq) \<noteq> w

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k'7 < k \<Longrightarrow> x (rho (r + ?k'7) qq) \<noteq> w

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)
?k'7 < k \<Longrightarrow> x (rho (r + ?k'7) qq) \<noteq> w
[PROOF STEP]
have "\<forall>k' < k. x (rho (r + Suc k') qq) \<noteq> w"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w)
?k'7 < k \<Longrightarrow> x (rho (r + ?k'7) qq) \<noteq> w

goal (1 subgoal):
 1. \<forall>k'<k. x (rho (r + Suc k') qq) \<noteq> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k'<k. x (rho (r + Suc k') qq) \<noteq> w

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k'<k. x (rho (r + Suc k') qq) \<noteq> w

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
from kgt0
[PROOF STATE]
proof (chain)
picking this:
0 < k
[PROOF STEP]
have "k - 1 < k" and kk:"Suc (k - 1) = k"
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. k - 1 < k &&& Suc (k - 1) = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k - 1 < k
Suc (k - 1) = k

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k'<k. x (rho (r + Suc k') qq) \<noteq> w
k - 1 < k
Suc (k - 1) = k
[PROOF STEP]
have "x (rho (r + Suc (k - 1)) qq) \<noteq> w"
[PROOF STATE]
proof (prove)
using this:
\<forall>k'<k. x (rho (r + Suc k') qq) \<noteq> w
k - 1 < k
Suc (k - 1) = k

goal (1 subgoal):
 1. x (rho (r + Suc (k - 1)) qq) \<noteq> w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x (rho (r + Suc (k - 1)) qq) \<noteq> w

goal (1 subgoal):
 1. \<not> (\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w) \<Longrightarrow> False
[PROOF STEP]
with rkw kk
[PROOF STATE]
proof (chain)
picking this:
x (rho (r + k) qq) = w
Suc (k - 1) = k
x (rho (r + Suc (k - 1)) qq) \<noteq> w
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x (rho (r + k) qq) = w
Suc (k - 1) = k
x (rho (r + Suc (k - 1)) qq) \<noteq> w

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

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

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w
[PROOF STEP]
obtain k'
      where "k' < k"
        and w: "x (rho (r + Suc k') qq) = w"
        and qqupdatex: "x (rho (r + Suc k') qq) \<noteq> x (rho (r + k') qq)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<k. x (rho (r + k') qq) \<noteq> w \<and> x (rho (r + Suc k') qq) = w

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' < k; x (rho (r + Suc k') qq) = w; x (rho (r + Suc k') qq) \<noteq> x (rho (r + k') qq)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' < k
x (rho (r + Suc k') qq) = w
x (rho (r + Suc k') qq) \<noteq> x (rho (r + k') qq)

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from run comm nd1 d1 qqupdatex
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
x (rho (r + Suc k') qq) \<noteq> x (rho (r + k') qq)
[PROOF STEP]
have "x (rho (r + Suc k') qq) = v"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
x (rho (r + Suc k') qq) \<noteq> x (rho (r + k') qq)

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

goal (1 subgoal):
 1. {qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with w vdifw
[PROOF STATE]
proof (chain)
picking this:
x (rho (r + Suc k') qq) = w
w \<noteq> v
x (rho (r + Suc k') qq) = v
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x (rho (r + Suc k') qq) = w
w \<noteq> v
x (rho (r + Suc k') qq) = v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} = {}

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
from run comm nd1 d1
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v
[PROOF STEP]
have sentv: "card ?sentv > E - \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho r p) \<noteq> Some v
decide (rho (Suc r) p) = Some v

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

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
from run comm nd2 d2
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho (r + k) q) \<noteq> Some w
decide (rho (Suc (r + k)) q) = Some w
[PROOF STEP]
have "card ?sentw > E - \<alpha>"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
decide (rho (r + k) q) \<noteq> Some w
decide (rho (Suc (r + k)) q) = Some w

goal (1 subgoal):
 1. E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}
[PROOF STEP]
by (auto dest: decide_sent_msgs_threshold)
[PROOF STATE]
proof (state)
this:
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with sentv majE
[PROOF STATE]
proof (chain)
picking this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
N \<le> 2 * (E - \<alpha>)
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}
[PROOF STEP]
have "(card ?sentv) + (card ?sentw) > N"
[PROOF STATE]
proof (prove)
using this:
E - \<alpha> < card {qq. sendMsg Ate_M r qq p (rho r qq) = v}
N \<le> 2 * (E - \<alpha>)
E - \<alpha> < card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}

goal (1 subgoal):
 1. N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with 1 vdifw
[PROOF STATE]
proof (chain)
picking this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} = {}
w \<noteq> v
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}
[PROOF STEP]
have 2: "card (?sentv \<union> ?sentw) > N"
[PROOF STATE]
proof (prove)
using this:
{qq. sendMsg Ate_M r qq p (rho r qq) = v} \<inter> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w} = {}
w \<noteq> v
N < card {qq. sendMsg Ate_M r qq p (rho r qq) = v} + card {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}

goal (1 subgoal):
 1. N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w})
[PROOF STEP]
by (auto simp: card_Un_Int)
[PROOF STATE]
proof (state)
this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w})

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
have "card (?sentv \<union> ?sentw) \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}) \<le> N
[PROOF STEP]
by (auto simp: card_mono)
[PROOF STATE]
proof (state)
this:
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}) \<le> N

goal (1 subgoal):
 1. w \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w})
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}) \<le> N
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
N < card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w})
card ({qq. sendMsg Ate_M r qq p (rho r qq) = v} \<union> {qq. sendMsg Ate_M (r + k) qq q (rho (r + k) qq) = w}) \<le> N

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ate_agreement:
  assumes run: "SHORun Ate_M rho HOs SHOs"
  and comm: "\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)"
  and p: "decide (rho m p) = Some v"
  and q: "decide (rho n q) = Some w"
  shows "w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
from run p
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
decide (rho m p) = Some v
[PROOF STEP]
obtain k where
    k: "k < m" "decide (rho k p) \<noteq> Some v" "decide (rho (Suc k) p) = Some v"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
decide (rho m p) = Some v

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < m; decide (rho k p) \<noteq> Some v; decide (rho (Suc k) p) = Some v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule decisionNonNullThenDecided)
[PROOF STATE]
proof (state)
this:
k < m
decide (rho k p) \<noteq> Some v
decide (rho (Suc k) p) = Some v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
from run q
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
decide (rho n q) = Some w
[PROOF STEP]
obtain l where
    l: "l < n" "decide (rho l q) \<noteq> Some w" "decide (rho (Suc l) q) = Some w"
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
decide (rho n q) = Some w

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l < n; decide (rho l q) \<noteq> Some w; decide (rho (Suc l) q) = Some w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule decisionNonNullThenDecided)
[PROOF STATE]
proof (state)
this:
l < n
decide (rho l q) \<noteq> Some w
decide (rho (Suc l) q) = Some w

goal (1 subgoal):
 1. w = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v
[PROOF STEP]
proof (cases "k \<le> l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<le> l \<Longrightarrow> w = v
 2. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<le> l

goal (2 subgoals):
 1. k \<le> l \<Longrightarrow> w = v
 2. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<le> l
[PROOF STEP]
obtain i where "l = k+i"
[PROOF STATE]
proof (prove)
using this:
k \<le> l

goal (1 subgoal):
 1. (\<And>i. l = k + i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: le_iff_add)
[PROOF STATE]
proof (state)
this:
l = k + i

goal (2 subgoals):
 1. k \<le> l \<Longrightarrow> w = v
 2. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
with run comm k l
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
k < m
decide (rho k p) \<noteq> Some v
decide (rho (Suc k) p) = Some v
l < n
decide (rho l q) \<noteq> Some w
decide (rho (Suc l) q) = Some w
l = k + i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
k < m
decide (rho k p) \<noteq> Some v
decide (rho (Suc k) p) = Some v
l < n
decide (rho l q) \<noteq> Some w
decide (rho (Suc l) q) = Some w
l = k + i

goal (1 subgoal):
 1. w = v
[PROOF STEP]
by (auto dest: laterProcessDecidesSameValue)
[PROOF STATE]
proof (state)
this:
w = v

goal (1 subgoal):
 1. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> k \<le> l

goal (1 subgoal):
 1. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
hence "l \<le> k"
[PROOF STATE]
proof (prove)
using this:
\<not> k \<le> l

goal (1 subgoal):
 1. l \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> k

goal (1 subgoal):
 1. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<le> k
[PROOF STEP]
obtain i where m: "k = l+i"
[PROOF STATE]
proof (prove)
using this:
l \<le> k

goal (1 subgoal):
 1. (\<And>i. k = l + i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: le_iff_add)
[PROOF STATE]
proof (state)
this:
k = l + i

goal (1 subgoal):
 1. \<not> k \<le> l \<Longrightarrow> w = v
[PROOF STEP]
with run comm k l
[PROOF STATE]
proof (chain)
picking this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
k < m
decide (rho k p) \<noteq> Some v
decide (rho (Suc k) p) = Some v
l < n
decide (rho l q) \<noteq> Some w
decide (rho (Suc l) q) = Some w
k = l + i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SHORun Ate_M rho HOs SHOs
\<forall>r. SHOcommPerRd Ate_M (HOs r) (SHOs r)
k < m
decide (rho k p) \<noteq> Some v
decide (rho (Suc k) p) = Some v
l < n
decide (rho l q) \<noteq> Some w
decide (rho (Suc l) q) = Some w
k = l + i

goal (1 subgoal):
 1. w = v
[PROOF STEP]
by (auto dest: laterProcessDecidesSameValue)
[PROOF STATE]
proof (state)
this:
w = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w = v

goal:
No subgoals!
[PROOF STEP]
qed