[STATEMENT]
lemma HStartBallot_HInv4d_q:
  assumes act: "HStartBallot s  s' p"
  and inv: "HInv4d s q"
  and pnq: "p\<noteq>q"
  shows "HInv4d s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HStartBallot s s' p
p \<noteq> q
[PROOF STEP]
have disk': "disk s'=disk s" 
   and dblock': "dblock s' q=dblock s q"
[PROOF STATE]
proof (prove)
using this:
HStartBallot s s' p
p \<noteq> q

goal (1 subgoal):
 1. disk s' = disk s &&& dblock s' q = dblock s q
[PROOF STEP]
by(auto simp add: StartBallot_def)
[PROOF STATE]
proof (state)
this:
disk s' = disk s
dblock s' q = dblock s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HStartBallot s s' p
p \<noteq> q
[PROOF STEP]
have blocksRead': "\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q"
[PROOF STATE]
proof (prove)
using this:
HStartBallot s s' p
p \<noteq> q

goal (1 subgoal):
 1. \<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
by(auto simp add: StartBallot_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk' dblock'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
have "blocksOf s' q \<subseteq> blocksOf s q"
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. blocksOf s' q \<subseteq> blocksOf s q
[PROOF STEP]
by(auto simp add: allRdBlks_def blocksOf_def rdBy_def, blast)
[PROOF STATE]
proof (state)
this:
blocksOf s' q \<subseteq> blocksOf s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from subsetD[OF this] inv
[PROOF STATE]
proof (chain)
picking this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q
[PROOF STEP]
have "\<forall>bk\<in>blocksOf s' q. 
           \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal(disk s d q)"
[PROOF STATE]
proof (prove)
using this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q

goal (1 subgoal):
 1. \<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
HInv4d s' q

goal:
No subgoals!
[PROOF STEP]
qed