proposition: Theorem nax_sound : forall m r i r' g, exec r i r' -> forall P Q, nax m P i Q -> i_a m (r@g) P -> i_a m (r'@g) Q.
proof: Proof. intros m r i r' g H; induction H; intros P Q Ha; inversion Ha; unfold valid in *; simpl in *; intros; subst; clear Ha; eauto. match goal with H: aeval _ _ _, G: s_update _ _ _ _ |- _ => destruct (a_subst_correct P' _ _ _ m g _ _ H G) as [Hs1 _] end; auto. match goal with H:nax m (a_conj _ ?P') ?i1 ?Q',G:exec _ (while ?b _) ?r'', K: _ |- _ => assert (Ha := H); apply K; change (i_a m (r''@g) (a_conj (a_not (a_b b)) P')); apply IHexec2 with (P:=P') end. apply nax4 with (3:= Ha); unfold valid; simpl; auto. apply IHexec1 with (1:= Ha); simpl; auto. Qed.
imports: syntax little denot Bool List String ZArith