proposition: Theorem rArrayContradictory : forall (Ar : rArray vM) (War : wellFormedArray Ar) (S : State), rArrayState Ar S -> ~ contradictory S.
proof: Proof. intros Ar H' S H'0; red in |- *; intros H'1; case H'1. intros x H'2; absurd (evalZ Ar x = evalZ Ar (rZComp x)). rewrite evalZComp; auto with stalmarck. apply rArrayStateDef1 with (S := S); auto with stalmarck. Qed.
imports: Stalmarck(rZ) Stalmarck(OrderedListEq) Stalmarck(LetP) Coq(Relation_Definitions) Stalmarck(state) Stalmarck(restrictState) Stalmarck(ltState)