1		package(load_event_b_project([event_b_model(none,'CBC_M',[sees(none,['CBC_C']),variables(none,[identifier(none,locVar),identifier(none,tested)]),invariant(none,[member(rodinpos('CBC_M',inv1,'_G9VGwG8mEeSGauWZB5HqCA'),identifier(none,locVar),total_function(none,interval(none,integer(none,0),integer(none,4)),interval(none,integer(none,0),integer(none,10)))),member(rodinpos('CBC_M',inv2,'_8lS4sW_lEeSoLMHHCqh0Jg'),identifier(none,tested),bool_set(none))]),theorems(none,[]),events(none,[event(rodinpos('CBC_M','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('CBC_M',act1,'_Ns7LQG8mEeSGauWZB5HqCA'),[identifier(none,locVar)],[set_extension(none,[couple(none,[integer(none,0),integer(none,0)]),couple(none,[integer(none,1),integer(none,1)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,3)]),couple(none,[integer(none,4),integer(none,4)])])]),assign(rodinpos('CBC_M',act2,'_8lQccG_lEeSoLMHHCqh0Jg'),[identifier(none,tested)],[boolean_false(none)])],[]),event(rodinpos('CBC_M',inc,'_bZLHgW_kEeSoLMHHCqh0Jg'),inc,ordinary(none),[],[identifier(rodinpos('CBC_M',[],'_bZLukG_kEeSoLMHHCqh0Jg'),prm)],[member(rodinpos('CBC_M',grd1,'_bZLukW_kEeSoLMHHCqh0Jg'),identifier(none,prm),interval(none,integer(none,0),integer(none,4))),less(rodinpos('CBC_M',grd2,'_bZMVoG_kEeSoLMHHCqh0Jg'),function(none,identifier(none,locVar),[identifier(none,prm)]),integer(none,10))],[],[assign(rodinpos('CBC_M',act1,'_bZMVoW_kEeSoLMHHCqh0Jg'),[identifier(none,locVar)],[overwrite(none,identifier(none,locVar),set_extension(none,[couple(none,[identifier(none,prm),add(none,function(none,identifier(none,locVar),[identifier(none,prm)]),integer(none,1))])]))])],[]),event(rodinpos('CBC_M',test,'_VYpg0G8mEeSGauWZB5HqCA'),test,ordinary(none),[],[identifier(rodinpos('CBC_M',[],'_VYpg0W8mEeSGauWZB5HqCA'),prm),identifier(rodinpos('CBC_M',[],'_2pU3UG8mEeSGauWZB5HqCA'),val)],[greater(rodinpos('CBC_M',grd1,'_VYqH4G8mEeSGauWZB5HqCA'),identifier(none,prm),integer(none,2)),member(rodinpos('CBC_M',grd2,'_VYqH4W8mEeSGauWZB5HqCA'),identifier(none,val),natural_set(none)),equal(rodinpos('CBC_M',grd3,'_2pVeYG8mEeSGauWZB5HqCA'),identifier(none,val),function(none,identifier(none,locVar),[identifier(none,prm)])),member(rodinpos('CBC_M',grd4,'_-lA7gG8mEeSGauWZB5HqCA'),couple(none,[identifier(none,val),integer(none,2)]),identifier(none,relations))],[],[assign(rodinpos('CBC_M',act1,'_BjwWwG_mEeSoLMHHCqh0Jg'),[identifier(none,tested)],[boolean_true(none)])],[]),event(rodinpos('CBC_M',dec,'_prDRsG_kEeSoLMHHCqh0Jg'),dec,ordinary(none),[],[identifier(rodinpos('CBC_M',[],'_prDRsW_kEeSoLMHHCqh0Jg'),prm)],[member(rodinpos('CBC_M',grd1,'_prDRsm_kEeSoLMHHCqh0Jg'),identifier(none,prm),interval(none,integer(none,0),integer(none,2))),greater(rodinpos('CBC_M',grd2,'_prD4wG_kEeSoLMHHCqh0Jg'),function(none,identifier(none,locVar),[identifier(none,prm)]),integer(none,0))],[],[assign(rodinpos('CBC_M',act1,'_prD4wW_kEeSoLMHHCqh0Jg'),[identifier(none,locVar)],[overwrite(none,identifier(none,locVar),set_extension(none,[couple(none,[identifier(none,prm),minus(none,function(none,identifier(none,locVar),[identifier(none,prm)]),integer(none,1))])]))])],[])])])],[event_b_context(none,'CBC_C',[extends(none,[]),constants(none,[identifier(none,relations)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('CBC_C',axm1,'_407MMW8mEeSGauWZB5HqCA'),identifier(none,relations),set_extension(none,[couple(none,[integer(none,0),integer(none,0)]),couple(none,[integer(none,1),integer(none,1)]),couple(none,[integer(none,2),integer(none,2)]),couple(none,[integer(none,3),integer(none,3)]),couple(none,[integer(none,4),integer(none,4)])]))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('CBC_M','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],false),po('CBC_M','Well-definedness of Guard',[guard(grd2),event(inc)],true),po('CBC_M','Invariant preservation',[event(inc),invariant(inv1)],false),po('CBC_M','Well-definedness of action',[action(act1)],true),po('CBC_M','Well-definedness of Guard',[guard(grd3),event(test)],false),po('CBC_M','Well-definedness of Guard',[guard(grd2),event(dec)],false),po('CBC_M','Invariant preservation',[event(dec),invariant(inv1)],false),po('CBC_M','Well-definedness of action',[action(act1)],true)],_Error)).
2