proposition: Theorem updatePointToClassClassRef2 : forall (r : rNat) (s : rZ) (Ls : list rZ), rArrayGet _ updateArray r = ref s -> rArrayGet _ updateArray (valRz s) = class Ls -> In (samePol s r) Ls.
proof: Proof. intros r s Ls. case (rNatDec r a); intros eqra. rewrite eqra; auto with stalmarck; rewrite updateArraya; auto with stalmarck; intros H'; inversion H'. case (rNatDec r b); intros eqrb. rewrite eqrb; auto with stalmarck; rewrite updateArrayb; auto with stalmarck; intros H'; inversion H'. rewrite samePolRzValRz; auto with stalmarck. rewrite updateArraya; auto with stalmarck; intros H'2. replace Ls with (fappendRz La (appendRz (rZPlus b :: nil) Lb)). unfold fappendRz in |- *; unfold appendRz in |- *; generalize fappendfIncl2; unfold incl in |- *; intros incl2; apply incl2; auto with stalmarck; clear incl2. intros; apply samePolRzEqRz; auto with stalmarck. try exact rZltEqComp. apply DisjLaLc with (3 := geta) (4 := getb); auto with stalmarck. rewrite <- eqrb; auto with stalmarck. rewrite samePolSamePolRz; auto with stalmarck. apply in_map with (A := rZ) (B := rZ); auto with stalmarck. generalize appendfIncl1; unfold incl in |- *; intros incl1; apply incl1; auto with datatypes stalmarck; clear incl1. apply DisjbLb with (2 := getb); auto with stalmarck. injection H'2; trivial. case (InRzDec (rZPlus r) Lb); intros InRLb; auto with stalmarck. case (InEqInv (rZPlus r) Lb); auto with stalmarck; intros InRLb'. replace r with (valRz (rZPlus r)); auto with stalmarck. rewrite updateArrayInb; auto with stalmarck; intros H'2; inversion H'2. simpl in |- *; rewrite samePolRzValRz. rewrite updateArraya; auto with stalmarck. intros H'. replace Ls with (fappendRz La (appendRz (rZPlus b :: nil) Lb)). unfold fappendRz in |- *; unfold appendRz in |- *; generalize fappendfIncl2; unfold incl in |- *; intros incl2; apply incl2; auto with stalmarck; clear incl2. intros a0; apply samePolRzEqRz; auto with stalmarck. try exact rZltEqComp. apply DisjLaLc with (3 := geta) (4 := getb); auto with stalmarck. apply rltDef2; auto with stalmarck. rewrite samePolSamePolRz; auto with stalmarck. apply in_map with (A := rZ) (B := rZ); auto with stalmarck. generalize appendfIncl2; unfold incl in |- *; intros incl1; apply incl1; auto with datatypes stalmarck; clear incl1. apply DisjbLb with (2 := getb); auto with stalmarck. injection H'; trivial. replace r with (valRz (rZMinus r)); auto with stalmarck. rewrite updateArrayInb; auto with stalmarck; intros H'2; inversion H'2. simpl in |- *; rewrite valRzComp; rewrite samePolRzValRz. rewrite updateArraya; auto with stalmarck. intros H'. replace Ls with (fappendRz La (appendRz (rZPlus b :: nil) Lb)). unfold fappendRz in |- *; unfold appendRz in |- *; generalize fappendfIncl2; unfold incl in |- *; intros incl2; apply incl2; auto with stalmarck; clear incl2. intros a0; apply samePolRzEqRz; auto with stalmarck. try exact rZltEqComp. apply DisjLaLc with (3 := geta) (4 := getb); auto with stalmarck. apply rltDef2; auto with stalmarck. replace (samePol (rZComp (samePolRz pol (rZPlus a))) r) with (samePolRz pol (rZMinus r)). apply in_map with (A := rZ) (B := rZ); auto with stalmarck. generalize appendfIncl2; unfold incl in |- *; intros incl1; apply incl1; auto with datatypes stalmarck; clear incl1. apply DisjbLb with (2 := getb); auto with stalmarck. case pol; auto with stalmarck. injection H'; trivial. rewrite updateArrayOtherwise; auto with stalmarck; intros Eqr. case (rNatDec (valRz s) a); intros Eqt. rewrite Eqt; auto with stalmarck; rewrite updateArraya; auto with stalmarck; intros H'. replace Ls with (fappendRz La (appendRz (rZPlus b :: nil) Lb)). unfold fappendRz in |- *; unfold appendRz in |- *; generalize fappendfIncl1; unfold incl in |- *; intros incl2; apply incl2; auto with stalmarck; clear incl2. intros a0; apply samePolRzEqRz; auto with stalmarck. try exact rZltEqComp. apply DisjLaLc with (3 := geta) (4 := getb); auto with stalmarck. apply rltDef2; auto with stalmarck. apply wfPcc2 with (Ar := Ar); auto with stalmarck. rewrite Eqt; auto with stalmarck. injection H'; trivial. intros Eqs. apply wfPcc2 with (Ar := Ar); auto with stalmarck. apply updateGetIsClass with (1 := Eqs); auto with stalmarck. Qed.