proposition: Theorem getClassOlist : forall (Ar : rArray vM) (a : rZ), wellFormedArray Ar -> OlistRz (evalZ Ar a :: getClassN Ar (valRz (evalZ Ar a))).
proof: Proof. intros Ar a War; case a; simpl in |- *. intros r; unfold evalN, getClassN in |- *. CaseEq (rArrayGet vM Ar r); simpl in |- *. intros r0; CaseEq (rArrayGet vM Ar (valRz r0)); simpl in |- *. intros r1 H' H'0; red in |- *; apply OlistOne; auto with stalmarck. intros l; case l. intros H' H'0; red in |- *; apply OlistOne; auto with stalmarck. intros r1 l0 H' H'0; red in |- *; apply OlistCons; auto with stalmarck. apply wfOl with (Ar := Ar) (r := valRz r0); auto with stalmarck. cut (rVlt (samePol r1 (valRz r0)) (valRz r1)). case r1; simpl in |- *; auto with stalmarck. apply wfPd with (Ar := Ar); auto with stalmarck. apply wfPcc1 with (Lr := r1 :: l0); simpl in |- *; auto with stalmarck. intros l; case l. intros H'; rewrite H'; red in |- *; apply OlistOne; auto with stalmarck. intros r0 l0 H'; rewrite H'; red in |- *; apply OlistCons; auto with stalmarck. apply wfOl with (Ar := Ar) (r := r); auto with stalmarck. cut (rVlt (samePol r0 r) (valRz r0)). case r0; simpl in |- *; auto with stalmarck. apply wfPd with (Ar := Ar); auto with stalmarck. apply wfPcc1 with (Lr := r0 :: l0); simpl in |- *; auto with stalmarck. intros r; unfold evalN, getClassN in |- *. CaseEq (rArrayGet vM Ar r); simpl in |- *. intros r0; rewrite (valRzComp r0); CaseEq (rArrayGet vM Ar (valRz r0)); simpl in |- *. intros r1 H' H'0; red in |- *; apply OlistOne; auto with stalmarck. intros l; case l. intros H' H'0; red in |- *; apply OlistOne; auto with stalmarck. intros r1 l0 H' H'0; red in |- *; apply OlistCons; auto with stalmarck. apply wfOl with (Ar := Ar) (r := valRz r0); auto with stalmarck. cut (rVlt (samePol r1 (valRz r0)) (valRz r1)). case r0; case r1; simpl in |- *; auto with stalmarck. apply wfPd with (Ar := Ar); auto with stalmarck. apply wfPcc1 with (Lr := r1 :: l0); simpl in |- *; auto with stalmarck. intros l; case l. intros H'; rewrite H'; red in |- *; apply OlistOne; auto with stalmarck. intros r0 l0 H'; rewrite H'; red in |- *; apply OlistCons; auto with stalmarck. apply wfOl with (Ar := Ar) (r := r); auto with stalmarck. cut (rVlt (samePol r0 r) (valRz r0)). case r0; simpl in |- *; auto with stalmarck. apply wfPd with (Ar := Ar); auto with stalmarck. apply wfPcc1 with (Lr := r0 :: l0); simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(stateDec)