proposition: Theorem getEquivIdR : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> forall a : rNat, eqStateRz S2 (rZPlus a) (evalZ Ar1 (rZPlus a)) -> getEquivMin Ar1 Ar2 a = evalZ Ar1 (rZPlus a).
proof: Proof. intros Ar1 Ar2 War1 War2 S1 S2 Sar1 Sar2 a H'0; case (rZltEDec (getEquivMin Ar1 Ar2 a) (evalZ Ar1 (rZPlus a))); intros s; [ Casec s; intros s | idtac ]. case evalZMin with (3 := s) (S := S1); auto with stalmarck. apply getEquivMinEq1; auto with stalmarck. case getEquivMinMinEq with (5 := s) (S1 := S1) (S2 := S2); auto with stalmarck; split; auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar1); auto with stalmarck. rewrite evalZInv; auto with stalmarck. case (eqRzElim _ _ s); auto with stalmarck. intros H'1; absurd (contradictory S1); auto with stalmarck. red in |- *; intros H'; elim H'. intros x H'2; absurd (evalZ Ar1 x = evalZ Ar1 (rZComp x)). rewrite evalZComp; auto with stalmarck. apply rArrayStateDef1 with (S := S1); auto with stalmarck. red in |- *; auto with stalmarck. exists (rZPlus a); auto with stalmarck. apply eqStateRzTrans with (b := evalZ Ar1 (rZPlus a)); auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar1); auto with stalmarck. rewrite evalZInv; auto with stalmarck. apply eqStateInvInv; auto with stalmarck. rewrite <- H'1; auto with stalmarck. rewrite <- rZCompInvol; auto with stalmarck. apply eqStateRzSym. apply getEquivMinEq1; auto with stalmarck. Qed.