A finite basis theorem for residually finite, congruence meet-semidistributive varieties

We derive a Mal'cev condition for congruence meet-semidistributivity and th en use it to prove two theorems. Theorem A: if a variety in a finite langua ge is congruence meet-semidistributive and residually less than some finite cardinal, then it is finitely based. Theorem a: there is an algorithm whic h. given m < omega and a finite algebra in a finite language, determines wh ether the variety generated by the algebra is congruence meet-semidistribut ive and residually less than m.