1		package(load_event_b_project([event_b_model(none,'NoDisabling',[sees(none,['DataNoDisabling']),variables(none,[identifier(none,v1),identifier(none,v2),identifier(none,v3),identifier(none,v4),identifier(none,v5)]),invariant(none,[member(rodinpos('NoDisabling',inv1,'_bf-GNP72EeSb-sa7n0l8mQ'),identifier(none,v1),natural_set(none)),member(rodinpos('NoDisabling',inv2,'_bf-GNf72EeSb-sa7n0l8mQ'),identifier(none,v2),natural_set(none)),member(rodinpos('NoDisabling',inv3,'_bf-GNv72EeSb-sa7n0l8mQ'),identifier(none,v3),natural_set(none)),member(rodinpos('NoDisabling',inv4,'_bf-GN_72EeSb-sa7n0l8mQ'),identifier(none,v4),natural_set(none)),member(rodinpos('NoDisabling',inv5,'_bf-GOP72EeSb-sa7n0l8mQ'),identifier(none,v5),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('NoDisabling','INITIALISATION','_bf9fIf72EeSb-sa7n0l8mQ'),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('NoDisabling',act1,'_bf9fIv72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[integer(none,1)]),assign(rodinpos('NoDisabling',act2,'_bf9fI_72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[integer(none,1)]),assign(rodinpos('NoDisabling',act3,'_bf9fJP72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[integer(none,1)]),assign(rodinpos('NoDisabling',act4,'_bf9fJf72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[integer(none,1)]),assign(rodinpos('NoDisabling',act5,'_bf9fJv72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[integer(none,1)])],[]),event(rodinpos('NoDisabling',e1,'_bf-GOf72EeSb-sa7n0l8mQ'),e1,ordinary(none),[],[],[greater(rodinpos('NoDisabling',grd1,'_bf-GOv72EeSb-sa7n0l8mQ'),identifier(none,v1),integer(none,0)),less(rodinpos('NoDisabling',grd2,'_bf-GO_72EeSb-sa7n0l8mQ'),identifier(none,v1),identifier(none,mx1))],[],[assign(rodinpos('NoDisabling',act1,'_bf-GPP72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[add(none,identifier(none,v1),integer(none,1))]),assign(rodinpos('NoDisabling',act2,'_bf-GPf72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[modulo(none,identifier(none,v2),add(none,identifier(none,v2),integer(none,1)))]),assign(rodinpos('NoDisabling',act3,'_bf-GPv72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[modulo(none,identifier(none,v3),add(none,identifier(none,v3),integer(none,1)))]),assign(rodinpos('NoDisabling',act4,'_bf-tQP72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[modulo(none,identifier(none,v4),add(none,identifier(none,v4),integer(none,1)))]),assign(rodinpos('NoDisabling',act5,'_bf-tQf72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[modulo(none,identifier(none,v5),add(none,identifier(none,v5),integer(none,1)))])],[]),event(rodinpos('NoDisabling',e2,'_bf-tQv72EeSb-sa7n0l8mQ'),e2,ordinary(none),[],[],[greater(rodinpos('NoDisabling',grd1,'_bf-tQ_72EeSb-sa7n0l8mQ'),identifier(none,v2),integer(none,0)),less(rodinpos('NoDisabling',grd2,'_bf-tRP72EeSb-sa7n0l8mQ'),identifier(none,v2),identifier(none,mx1))],[],[assign(rodinpos('NoDisabling',act1,'_bf-tRf72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[modulo(none,identifier(none,v1),add(none,identifier(none,v1),integer(none,1)))]),assign(rodinpos('NoDisabling',act2,'_bf-tRv72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[add(none,identifier(none,v2),integer(none,1))]),assign(rodinpos('NoDisabling',act3,'_bf-tR_72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[modulo(none,identifier(none,v3),add(none,identifier(none,v3),integer(none,1)))]),assign(rodinpos('NoDisabling',act4,'_bf-tSP72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[modulo(none,identifier(none,v4),add(none,identifier(none,v4),integer(none,1)))]),assign(rodinpos('NoDisabling',act5,'_bf-tSf72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[modulo(none,identifier(none,v5),add(none,identifier(none,v5),integer(none,1)))])],[]),event(rodinpos('NoDisabling',e3,'_bf-tSv72EeSb-sa7n0l8mQ'),e3,ordinary(none),[],[],[greater(rodinpos('NoDisabling',grd1,'_bf-tS_72EeSb-sa7n0l8mQ'),identifier(none,v3),integer(none,0)),less(rodinpos('NoDisabling',grd2,'_bf-tTP72EeSb-sa7n0l8mQ'),identifier(none,v3),identifier(none,mx1))],[],[assign(rodinpos('NoDisabling',act1,'_bf-tTf72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[modulo(none,identifier(none,v1),add(none,identifier(none,v1),integer(none,1)))]),assign(rodinpos('NoDisabling',act2,'_bf-tTv72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[modulo(none,identifier(none,v2),add(none,identifier(none,v2),integer(none,1)))]),assign(rodinpos('NoDisabling',act3,'_bf-tT_72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[add(none,identifier(none,v3),integer(none,1))]),assign(rodinpos('NoDisabling',act4,'_bf_UUP72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[modulo(none,identifier(none,v4),add(none,identifier(none,v4),integer(none,1)))]),assign(rodinpos('NoDisabling',act5,'_bf_UUf72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[modulo(none,identifier(none,v5),add(none,identifier(none,v5),integer(none,1)))])],[]),event(rodinpos('NoDisabling',e4,'_bf_UUv72EeSb-sa7n0l8mQ'),e4,ordinary(none),[],[],[greater(rodinpos('NoDisabling',grd1,'_bf_UU_72EeSb-sa7n0l8mQ'),identifier(none,v4),integer(none,0)),less(rodinpos('NoDisabling',grd2,'_bf_UVP72EeSb-sa7n0l8mQ'),identifier(none,v4),identifier(none,mx1))],[],[assign(rodinpos('NoDisabling',act1,'_bf_UVf72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[modulo(none,identifier(none,v1),add(none,identifier(none,v1),integer(none,1)))]),assign(rodinpos('NoDisabling',act2,'_bf_UVv72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[modulo(none,identifier(none,v2),add(none,identifier(none,v2),integer(none,1)))]),assign(rodinpos('NoDisabling',act3,'_bf_UV_72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[modulo(none,identifier(none,v3),add(none,identifier(none,v3),integer(none,1)))]),assign(rodinpos('NoDisabling',act4,'_bf_UWP72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[add(none,identifier(none,v4),integer(none,1))]),assign(rodinpos('NoDisabling',act5,'_bf_UWf72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[modulo(none,identifier(none,v5),add(none,identifier(none,v5),integer(none,1)))])],[]),event(rodinpos('NoDisabling',e5,'_bf_UWv72EeSb-sa7n0l8mQ'),e5,ordinary(none),[],[],[greater(rodinpos('NoDisabling',grd1,'_bf_UW_72EeSb-sa7n0l8mQ'),identifier(none,v5),integer(none,0)),less(rodinpos('NoDisabling',grd2,'_bf_UXP72EeSb-sa7n0l8mQ'),identifier(none,v5),identifier(none,mx1))],[],[assign(rodinpos('NoDisabling',act1,'_bf_UXf72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[modulo(none,identifier(none,v1),add(none,identifier(none,v1),integer(none,1)))]),assign(rodinpos('NoDisabling',act2,'_bf_UXv72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[modulo(none,identifier(none,v2),add(none,identifier(none,v2),integer(none,1)))]),assign(rodinpos('NoDisabling',act3,'_bf_7YP72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[modulo(none,identifier(none,v3),add(none,identifier(none,v3),integer(none,1)))]),assign(rodinpos('NoDisabling',act4,'_bf_7Yf72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[modulo(none,identifier(none,v4),add(none,identifier(none,v4),integer(none,1)))]),assign(rodinpos('NoDisabling',act5,'_bf_7Yv72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[add(none,identifier(none,v5),integer(none,1))])],[]),event(rodinpos('NoDisabling',loop,'_bf_7Y_72EeSb-sa7n0l8mQ'),loop,ordinary(none),[],[],[greater_equal(rodinpos('NoDisabling',grd1,'_bf_7ZP72EeSb-sa7n0l8mQ'),identifier(none,v1),integer(none,0)),greater_equal(rodinpos('NoDisabling',grd2,'_bf_7av72EeSb-sa7n0l8mQ'),identifier(none,v2),integer(none,0)),greater_equal(rodinpos('NoDisabling',grd3,'_bf_7a_72EeSb-sa7n0l8mQ'),identifier(none,v3),integer(none,0)),greater_equal(rodinpos('NoDisabling',grd4,'_bf_7bP72EeSb-sa7n0l8mQ'),identifier(none,v4),integer(none,0)),greater_equal(rodinpos('NoDisabling',grd5,'_bf_7bf72EeSb-sa7n0l8mQ'),identifier(none,v5),integer(none,0))],[],[assign(rodinpos('NoDisabling',act1,'_bf_7Zf72EeSb-sa7n0l8mQ'),[identifier(none,v1)],[modulo(none,identifier(none,v1),add(none,identifier(none,v1),integer(none,1)))]),assign(rodinpos('NoDisabling',act2,'_bf_7Zv72EeSb-sa7n0l8mQ'),[identifier(none,v2)],[modulo(none,identifier(none,v2),add(none,identifier(none,v2),integer(none,1)))]),assign(rodinpos('NoDisabling',act3,'_bf_7Z_72EeSb-sa7n0l8mQ'),[identifier(none,v3)],[modulo(none,identifier(none,v3),add(none,identifier(none,v3),integer(none,1)))]),assign(rodinpos('NoDisabling',act4,'_bf_7aP72EeSb-sa7n0l8mQ'),[identifier(none,v4)],[modulo(none,identifier(none,v4),add(none,identifier(none,v4),integer(none,1)))]),assign(rodinpos('NoDisabling',act5,'_bf_7af72EeSb-sa7n0l8mQ'),[identifier(none,v5)],[modulo(none,identifier(none,v5),add(none,identifier(none,v5),integer(none,1)))])],[])])])],[event_b_context(none,'DataNoDisabling',[extends(none,[]),constants(none,[identifier(none,mx1)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('DataNoDisabling',axm1,'_BKiFsP8FEeSfsrr51oWxaw'),identifier(none,mx1),integer(none,5))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('NoDisabling','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po('NoDisabling','Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po('NoDisabling','Invariant establishment',[event('INITIALISATION'),invariant(inv3)],true),po('NoDisabling','Invariant establishment',[event('INITIALISATION'),invariant(inv4)],true),po('NoDisabling','Invariant establishment',[event('INITIALISATION'),invariant(inv5)],true),po('NoDisabling','Invariant preservation',[event(e1),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(e1),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(e1),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(e1),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(e1),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act2)],false),po('NoDisabling','Well-definedness of action',[action(act3)],false),po('NoDisabling','Well-definedness of action',[action(act4)],false),po('NoDisabling','Well-definedness of action',[action(act5)],false),po('NoDisabling','Invariant preservation',[event(e2),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(e2),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(e2),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(e2),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(e2),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act1)],false),po('NoDisabling','Well-definedness of action',[action(act3)],false),po('NoDisabling','Well-definedness of action',[action(act4)],false),po('NoDisabling','Well-definedness of action',[action(act5)],false),po('NoDisabling','Invariant preservation',[event(e3),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(e3),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(e3),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(e3),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(e3),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act1)],false),po('NoDisabling','Well-definedness of action',[action(act2)],false),po('NoDisabling','Well-definedness of action',[action(act4)],false),po('NoDisabling','Well-definedness of action',[action(act5)],false),po('NoDisabling','Invariant preservation',[event(e4),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(e4),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(e4),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(e4),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(e4),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act1)],false),po('NoDisabling','Well-definedness of action',[action(act2)],false),po('NoDisabling','Well-definedness of action',[action(act3)],false),po('NoDisabling','Well-definedness of action',[action(act5)],false),po('NoDisabling','Invariant preservation',[event(e5),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(e5),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(e5),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(e5),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(e5),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act1)],false),po('NoDisabling','Well-definedness of action',[action(act2)],false),po('NoDisabling','Well-definedness of action',[action(act3)],false),po('NoDisabling','Well-definedness of action',[action(act4)],false),po('NoDisabling','Invariant preservation',[event(loop),invariant(inv1)],false),po('NoDisabling','Invariant preservation',[event(loop),invariant(inv2)],false),po('NoDisabling','Invariant preservation',[event(loop),invariant(inv3)],false),po('NoDisabling','Invariant preservation',[event(loop),invariant(inv4)],false),po('NoDisabling','Invariant preservation',[event(loop),invariant(inv5)],false),po('NoDisabling','Well-definedness of action',[action(act1)],false),po('NoDisabling','Well-definedness of action',[action(act2)],false),po('NoDisabling','Well-definedness of action',[action(act3)],false),po('NoDisabling','Well-definedness of action',[action(act4)],false),po('NoDisabling','Well-definedness of action',[action(act5)],false)],_Error)).
2