1		package(load_event_b_project([event_b_model(none,'InfiniteChanges',[sees(none,[]),variables(none,[identifier(none,f)]),invariant(none,[member(rodinpos('InfiniteChanges',inv,'_N0WewO5jEeSfYuujsKbFjQ'),identifier(none,f),relations(none,integer_set(none),integer_set(none)))]),theorems(none,[]),events(none,[event(rodinpos('InfiniteChanges','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',ini,'_N0XF0O5jEeSfYuujsKbFjQ'),[identifier(none,f)],[cartesian_product(none,integer_set(none),set_extension(none,[integer(none,0)]))])],[]),event(rodinpos('InfiniteChanges',compute1,'_zBDUAO5lEeSfYuujsKbFjQ'),compute1,ordinary(none),[],[identifier(rodinpos('InfiniteChanges',[],'_zBDUAe5lEeSfYuujsKbFjQ'),x)],[equal(rodinpos('InfiniteChanges',g,'_zBDUAu5lEeSfYuujsKbFjQ'),identifier(none,x),function(none,identifier(none,f),[integer(none,1)]))],[],[],[]),event(rodinpos('InfiniteChanges',compute100,'_N0XF0e5jEeSfYuujsKbFjQ'),compute100,ordinary(none),[],[identifier(rodinpos('InfiniteChanges',[],'_N0Xs4O5jEeSfYuujsKbFjQ'),x)],[equal(rodinpos('InfiniteChanges',g,'_N0Xs4e5jEeSfYuujsKbFjQ'),identifier(none,x),function(none,identifier(none,f),[integer(none,100)]))],[],[],[]),event(rodinpos('InfiniteChanges',compute200,'_S5MRoO5jEeSfYuujsKbFjQ'),compute200,ordinary(none),[],[identifier(rodinpos('InfiniteChanges',[],'_S5M4sO5jEeSfYuujsKbFjQ'),x)],[equal(rodinpos('InfiniteChanges',g,'_S5M4se5jEeSfYuujsKbFjQ'),identifier(none,x),function(none,identifier(none,f),[integer(none,200)]))],[],[],[]),event(rodinpos('InfiniteChanges',compute10000,'_n0YSIO5jEeSfYuujsKbFjQ'),compute10000,ordinary(none),[],[identifier(rodinpos('InfiniteChanges',[],'_n0YSIe5jEeSfYuujsKbFjQ'),x)],[equal(rodinpos('InfiniteChanges',g,'_n0YSIu5jEeSfYuujsKbFjQ'),identifier(none,x),function(none,identifier(none,f),[integer(none,10000)]))],[],[],[]),event(rodinpos('InfiniteChanges',change3,'_S5M4su5jEeSfYuujsKbFjQ'),change3,ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'_S5NfwO5jEeSfYuujsKbFjQ'),[identifier(none,f)],[cartesian_product(none,integer_set(none),set_extension(none,[integer(none,3)]))])],[]),event(rodinpos('InfiniteChanges',change3NAT,'_V53F8O5mEeSfYuujsKbFjQ'),change3NAT,ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'_V53F8e5mEeSfYuujsKbFjQ'),[identifier(none,f)],[cartesian_product(none,natural_set(none),set_extension(none,[integer(none,3)]))])],[]),event(rodinpos('InfiniteChanges',changeInc,'_ka84MO5jEeSfYuujsKbFjQ'),changeInc,ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'_ka9fQO5jEeSfYuujsKbFjQ'),[identifier(none,f)],[event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),add(none,identifier(none,x),integer(none,1))]),conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),integer_set(none))))])],[]),event(rodinpos('InfiniteChanges',changeAt1,'_t8BT4O5lEeSfYuujsKbFjQ'),changeAt1,ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'_t8BT4e5lEeSfYuujsKbFjQ'),[identifier(none,f)],[overwrite(none,identifier(none,f),set_extension(none,[couple(none,[integer(none,1),integer(none,17)])]))])],[]),event(rodinpos('InfiniteChanges','IncAllByOne','_zgA2AO5nEeSfYuujsKbFjQ'),'IncAllByOne',ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'_zgBdEO5nEeSfYuujsKbFjQ'),[identifier(none,f)],[composition(none,identifier(none,f),event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),add(none,identifier(none,x),integer(none,1))]),conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),integer_set(none)))))])],[]),event(rodinpos('InfiniteChanges','IncAllByOneV2','__ir9sO5nEeSfYuujsKbFjQ'),'IncAllByOneV2',ordinary(none),[],[],[],[],[assign(rodinpos('InfiniteChanges',i,'__iskwO5nEeSfYuujsKbFjQ'),[identifier(none,f)],[event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),add(none,function(none,identifier(none,f),[identifier(none,x)]),integer(none,1))]),conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),integer_set(none))))])],[])])])],[],[exporter_version(3),po('InfiniteChanges','Well-definedness of Guard',[guard(g),event(compute1)],false),po('InfiniteChanges','Well-definedness of Guard',[guard(g),event(compute100)],false),po('InfiniteChanges','Well-definedness of Guard',[guard(g),event(compute200)],false),po('InfiniteChanges','Well-definedness of Guard',[guard(g),event(compute10000)],false),po('InfiniteChanges','Well-definedness of action',[action(i)],false)],_Error)).
2