proposition: Theorem addEqMem2Correct : forall (Ar : rArray vM) (a b c d : rZ) (S : State), wellFormedArray Ar -> rArrayState Ar S -> match addEqMem2 Ar a b c d with | triple Ar' false L => wellFormedArray Ar' /\ rArrayState Ar' (addEq (c, d) (addEq (a, b) S)) /\ OlistRz L /\ (forall e : rNat, ~ InRz (rZPlus e) L -> rArrayGet _ Ar' e = rArrayGet _ Ar e) | triple Ar' true L => contradictory (addEq (c, d) (addEq (a, b) S)) end.
proof: Proof. intros Ar a b c d S War H'; unfold addEqMem2 in |- *. generalize (addEqMemCorrect Ar a b S War H'). case (addEqMem Ar a b); simpl in |- *. intros Ar' b' L'; case b'; simpl in |- *. intros H'0; red in |- *; inversion H'0. exists x; auto with stalmarck. intros H'0; Elimc H'0; intros H'0 H'1; Elimc H'1; intros H'1 H'2; Elimc H'2; intros H'2 H'3. generalize (addEqMemCorrect Ar' c d (addEq (pair a b) S) H'0 H'1); case (addEqMem Ar' c d); simpl in |- *. intros Ar'' b'' L''; case b''; simpl in |- *; auto with stalmarck. intros H'4; Elimc H'4; intros H'4 H'5; Elimc H'5; intros H'5 H'6; Elimc H'6; intros H'6 H'7; repeat (split; auto with stalmarck). red in |- *; unfold appendRz in |- *; apply appendfOlist; auto with stalmarck. exact rZltEqComp. intros e H'8. rewrite H'7; auto with stalmarck. apply H'3; auto with stalmarck. Contradict H'8; auto with stalmarck. cut (InclEq _ eqRz L' (appendf _ rZlt eqRz rZltEDec L' L'')). intros H'9; inversion H'9; red in |- *; auto with stalmarck. apply appendfInclEq1; auto with stalmarck. Contradict H'8; auto with stalmarck. cut (InclEq _ eqRz L'' (appendf _ rZlt eqRz rZltEDec L' L'')). intros H'9; inversion H'9; red in |- *; auto with stalmarck. apply appendfInclEq2; auto with stalmarck. Qed.
imports: Stalmarck(stateDec)