proposition: Theorem stalCorrect : forall (m : nat) (Ar : rArray vM) (a b : rZ) (S : State), wellFormedArray Ar -> rArrayState Ar S -> match stal m Ar a b with | quatuor Ar' false L T => True | quatuor Ar' true L T => exists S' : State, stalmarckP (addEq (a, b) S) LL S' /\ contradictory S' /\ evalTrace (addEq (a, b) S) T S' end.
proof: Proof. intros m Ar a b S H' H'0; unfold stal in |- *. generalize (addEqMemCorrect Ar a b S). case (addEqMem Ar a b). intros Ar1 b1 L1; case b1. intros H'1; exists (addEq (pair a b) S); repeat (split; auto with stalmarck). intros H'1; elim H'1; [ intros H'4 H'5; elim H'5; intros H'6 H'7; elim H'7; intros H'8 H'9; clear H'7 H'5 H'1 | clear H'1 | clear H'1 ]; auto with stalmarck. generalize (stalNCorrect L1 0 m Ar1). case (stalN L1 0 m Ar1). intros Ar2 b2 L2 T2; case b2; auto with stalmarck. unfold FStalCorrect in |- *; simpl in |- *; auto with stalmarck. Qed.