1		package(load_event_b_project([event_b_model(none,'VariantWDError2',[sees(none,[]),variables(none,[identifier(none,x)]),invariant(none,[member(rodinpos('VariantWDError2',inv,'_6iLo4dl7EeaQvaSSR625bA'),identifier(none,x),natural_set(none))]),theorems(none,[]),variant(none,minus(none,integer(none,1000),div(none,integer(none,100),minus(none,integer(none,5),identifier(none,x))))),events(none,[event(rodinpos('VariantWDError2','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('VariantWDError2',ini,'_6iLB0Nl7EeaQvaSSR625bA'),[identifier(none,x)],[integer(none,1)])],[]),event(rodinpos('VariantWDError2',inc,'_6iLo49l7EeaQvaSSR625bA'),inc,convergent(none),[],[],[less(rodinpos('VariantWDError2',g,'_6iLo5Nl7EeaQvaSSR625bA'),identifier(none,x),integer(none,5))],[],[assign(rodinpos('VariantWDError2',inc,'_6iLo5dl7EeaQvaSSR625bA'),[identifier(none,x)],[add(none,identifier(none,x),integer(none,1))])],[])])])],[],[exporter_version(3),po('VariantWDError2','Well-definedness of variant',[variant('VariantWDError2')],false),po('VariantWDError2','Invariant establishment',[event('INITIALISATION'),invariant(inv)],false),po('VariantWDError2','Invariant preservation',[event(inc),invariant(inv)],false),po('VariantWDError2','Variant of event',[variant('VariantWDError2'),event(inc)],false),po('VariantWDError2','Natural number variant of event',[variant('VariantWDError2'),event(inc)],false)],_Error)).
2