This paper demonstrates by help of an example how algebraic Petri nets can be used for modelling and verification of distributed algorithms. For lack of space we could only sketch the used proof techniques; still the proof should provide a flavour of our method. In essence the basic technique for deriving simple temporal properties is to verify the validity of some state formulas which are derived from the structure of the net and the verified formula: equations for place invariants, simple implications for siphons and traps, and some more complex implications for assertions. Though not completely explained here, even the pick up rule for leadsto properties can be reduced to checking the validity of some state formulas. For combining temporal formulas in order to verify more complex properties we mainly use standard rules: weakening of invariants, PSP-rule and proof graphs for liveness properties.