proposition: Theorem evalZMin : forall (Ar : rArray vM) (War : wellFormedArray Ar) (S : State), rArrayState Ar S -> forall a c : rZ, rZlt c (evalZ Ar a) -> ~ eqStateRz S a c.
proof: Proof. intros Ar War S H'0 a c H'1; red in |- *; intros H'2. absurd (evalZ Ar c = evalZ Ar a); auto with stalmarck. generalize H'1 H'2; clear H'1 H'2. case c; case a; simpl in |- *; intros a' c'; unfold evalN in |- *; CaseEq (rArrayGet vM Ar a'); CaseEq (rArrayGet vM Ar c'); auto with stalmarck; intros r H' r0 H'1 H'2 H'3; red in |- *; intros H'4; (absurd (rVlt r c'); [ idtac | apply wfPd with (Ar := Ar) ]); auto with stalmarck; try (rewrite H'4; unfold rVlt in |- *; apply rltAntiSym; auto with stalmarck); rewrite (rZCompInvol r); rewrite H'4; unfold rVlt in |- *; apply rltAntiSym; generalize H'2; case r0; simpl in |- *; auto with stalmarck. apply rArrayStateDef1 with (S := S); auto with stalmarck. Qed.