proposition: Theorem getTCorrect : forall (L : list triplet) (a : rZ), incl (getT (buildL L) a) L.
proof: Proof. unfold getT in |- *; intros L; elim L; simpl in |- *. intros a; elim a; simpl in |- *. intros r; case r; simpl in |- *; auto with datatypes stalmarck. intros r; case r; simpl in |- *; auto with datatypes stalmarck. intros t; case t; auto with stalmarck. intros r r0 r1 r2 l H' a; unfold letP, getT in |- *; simpl in |- *. case (rNatDec (valRz r2) (valRz a)); intros Eq1. repeat rewrite Eq1. repeat rewrite rArrayDef1 with (m := valRz a). case (rNatDec (valRz r1) (valRz a)); intros Eq2. repeat rewrite Eq2. repeat rewrite rArrayDef1 with (m := valRz a). case (rNatDec (valRz r0) (valRz a)); intros Eq3. repeat rewrite Eq3. repeat rewrite rArrayDef1 with (m := valRz a); auto with datatypes stalmarck. repeat rewrite rArrayDef2 with (m2 := valRz a); auto with datatypes stalmarck. rewrite rArrayDef2 with (m2 := valRz a); auto with stalmarck. case (rNatDec (valRz r0) (valRz a)); intros Eq3. repeat rewrite Eq3. repeat rewrite rArrayDef1 with (m := valRz a); auto with datatypes stalmarck. rewrite rArrayDef2 with (m2 := valRz a); auto with datatypes stalmarck. rewrite rArrayDef2 with (m2 := valRz a); auto with datatypes stalmarck. case (rNatDec (valRz r1) (valRz a)); intros Eq2. repeat rewrite Eq2. repeat rewrite rArrayDef1 with (m := valRz a). case (rNatDec (valRz r0) (valRz a)); intros Eq3. repeat rewrite Eq3. repeat rewrite rArrayDef1 with (m := valRz a); auto with datatypes stalmarck. repeat rewrite rArrayDef2 with (m2 := valRz a); auto with datatypes stalmarck. rewrite rArrayDef2 with (m2 := valRz a); auto with stalmarck. case (rNatDec (valRz r0) (valRz a)); intros Eq3. repeat rewrite Eq3. repeat rewrite rArrayDef1 with (m := valRz a); auto with datatypes stalmarck. rewrite rArrayDef2 with (m2 := valRz a); auto with datatypes stalmarck. Qed.
imports: Stalmarck(makeTriplet)