data specification using nat partelem := pe(. .first : nat, . .last : nat, . .count : nat) ; variables p : partelem; end data specification