proposition: Theorem HoareWhileRule : forall (P:state->Prop)(b:bExp)(i:inst)(s s':state), (forall s1 s2:state, P s1 -> evalB s1 b = Some true -> exec s1 i s2 -> P s2)-> P s -> exec s (WhileDo b i) s' -> P s' /\ evalB s' b = Some false.
proof: Proof. intros P b i s s' H_invariant HP Hexec. apply (HoareWhileRule_aux P b i s s');simpl; auto. Qed.
imports: ZArith