data specification
using event ,
view
xview = mkxview( . .view : event → viewstate; . .er : event × event → bool);
variables
xview, xview0, xview1 : xview;
view : event → viewstate;
eqrel : event × event → bool;
end data specification