proposition: Theorem rIwF : wellFormedArray (rArrayInit vM (fun _ : rNat => class nil)).
proof: Proof. apply wellFormedArrayDef; auto with stalmarck. apply pointerDecreaseDef; simpl in |- *; auto with stalmarck. intros r; case r; simpl in |- *; intros; discriminate. apply pointToClassRefDef; simpl in |- *; auto with stalmarck. intros r; case r; simpl in |- *; intros; discriminate. apply pointToClassClassRef; simpl in |- *; auto with stalmarck. intros r; case r; simpl in |- *. intros p s Lr H'; inversion H'. intros H'0; inversion H'0. intros p s Lr H'; inversion H'. intros H'0; inversion H'0. intros s Lr H'; inversion H'. intros H'0; inversion H'0. intros r; case r; simpl in |- *; intros; discriminate. apply OlistArrayDef; simpl in |- *; auto with stalmarck. intros r; case r; simpl in |- *. intros H' Lr H'0; inversion H'0; red in |- *; apply OlistNil; auto with stalmarck. intros H' Lr H'0; inversion H'0; red in |- *; apply OlistNil; auto with stalmarck. intros Lr H'; inversion H'; red in |- *; apply OlistNil; auto with stalmarck. Qed.
imports: Stalmarck(makeTriplet)