Ob Algoritme dokazatelʹstva svojstv abstraktnych tipov dannych