[STATEMENT]
lemma HEndPhase1_HInv4a_p:
  assumes act: "HEndPhase1 s s' p"
  and inv: "HInv4a s p"
  and inv2a: "Inv2a s"
  shows "HInv4a s' p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
from act
[PROOF STATE]
proof (chain)
picking this:
HEndPhase1 s s' p
[PROOF STEP]
have phase: "0 < phase s p"
[PROOF STATE]
proof (prove)
using this:
HEndPhase1 s s' p

goal (1 subgoal):
 1. 0 < phase s p
[PROOF STEP]
by(auto simp add: EndPhase1_def)
[PROOF STATE]
proof (state)
this:
0 < phase s p

goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
with act inv inv2a
[PROOF STATE]
proof (chain)
picking this:
HEndPhase1 s s' p
HInv4a s p
Inv2a s
0 < phase s p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HEndPhase1 s s' p
HInv4a s p
Inv2a s
0 < phase s p

goal (1 subgoal):
 1. HInv4a s' p
[PROOF STEP]
by(auto simp del: HEndPhase1_def simp  add: HInv4a_def 
               elim: HEndPhase1_HInv4a1 HEndPhase1_HInv4a2)
[PROOF STATE]
proof (state)
this:
HInv4a s' p

goal:
No subgoals!
[PROOF STEP]
qed